Subject: How Sugar supports the assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 16 2001 - 12:38:14 PDT
Hi Cindy,
My understanding from that is as follows:
1) In general, Sugar is not sound with respect to the assume/guarantee
paradigm.
2) There is some non-trivial subset ([1], weak suffix implications) of Sugar
that is sound with respect to the assume/guarantee paradigm, but it is
neither
tractable (ESPACE-hard) nor known to be complete with respect to the
assume-guarantee paradigm.
Am I correct?
Regards, Roy
-----Original Message-----
From: Cindy Eisner [mailto:EISNER@il.ibm.com]
Sent: Sunday, July 15, 2001 12:03 PM
To: vardi@cs.rice.edu
Cc: roy.armoni; vfv
Subject: Re: FTL fully supports that assume/guarantee paradigm
moshe,
regarding your question on assume/guarantee in sugar: as i explained
previously to the sub-committee, the subset of sugar formulas that can be
assumed is the same subset that can be model checked on the fly. these are
the sugar formulas defined in [1], and in addition, weak suffix
implication (i.e., {r_1} \rightarrow {r_2}). assumptions are implemented
by means of an invariant on the state machine used to check the property.
finally, i again note that mixing assumptions with a non-deterministic
environment, regardless of the language (sugar, ftl, ltl, etc.) will result
in the problem/phenomenon/artifact which was previously described. thus,
the assume/guarantee paradigm should be taken with a grain of salt.
off to the airport. see you tuesday.
regards,
cindy.
[1] @INPROCEEDINGS{rctl,
AUTHOR = "I. Beer and S. Ben-David and A. Landver",
TITLE = "On-the-fly Model Checking of {RCTL} Formulas",
BOOKTITLE = "Proc. $10^{th}$ International Conference on Computer
Aided Verification (CAV)",
SERIES = "LNCS 1427",
YEAR = {1998},
PUBLISHER = "Springer-Verlag",
PAGES = "184-194" }
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-855-0070
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Mon Jul 16 2001 - 12:39:03 PDT