Subject: RE: How Sugar supports the assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 30 2001 - 09:49:38 PDT
Hi Cindy,
Please see my comments below.
Regards, Roy
> -----Original Message-----
> From: Cindy Eisner [mailto:EISNER@il.ibm.com]
> Sent: Monday, July 30, 2001 4:14 PM
> To: Armoni, Roy
> Cc: vfv@eda.org
> Subject: Re: How Sugar supports the assume/guarantee paradigm
>
>
> roy,
>
> you are not playing fair. according to your definition of soundness
> (definition 2 from your manifesto), sugar is not sound with
> respect to the
> assume/guarantee paradigm. however, the reason stems from a
> bias towards
> linear logics in your definition. let me explain:
>
> your definition: for a logic $L$, we say that $L$ is sound
> with respect to
> the assume-guarantee paradigm if for every models $M$ and $E$
> and for every
> formulae $f, g \in L$ we have that $E \models f$ and $M \models f \
> longrightarrow g$ implies that $E || M \models g$.
>
> a more general definition: for a logic $L$, we say that $L$
> is sound with
> respect to the assume-guarantee paradigm if for all models
> $M$ and $E$ and
> for every formulae $f, g \in L$ we have that $E \models f$
> and $M \assume f
> \models g$ implies that $E || M \models g$.
>
> where $M \assume f$ is model $M$ under assumption $f$.
I am sorry, but I fail to have a good understanding of what is
your definition for soundness. The reason is that "\assume"
is not really defined. I am willing to guess though, on the intuitive
level.
>
> in other words, your definition makes an assumption (excuse
> the pun) about
> the way assumptions are implemented - requiring them to be implemented
> using an implication (f -> g). if we take away that
> assumption and use the
> more general definition, then sugar is sound with respect to
> the paradigm.
I would appreciate it if you could support the above claim with some
sketch of proof - that is of course after giving a reasonable definition
for assume.
>
> regarding completeness, we have already said that only a
> subset of sugar
> formulas can be assumed. also, that fairness can be used to
> augment this
> set of formulas. from a practical point of view - every challenge you
> raised in the property document regarding assumptions was met
> by sugar.
How would you guarantee the fairness?
Here you actually explain why Sugar is NOT complete. The fact that
you need one description for the property when you want to assume
it and another when you want to discharge the assumption requires
double encoding of the same spec and leads to errors (how do you
verify that the two formalisms are equivalent?).
>
> regarding complexity - let me point out that the forspec
> reference manual
> lists three advantages of using assignments over assumptions,
> one of which
> is efficiency. this makes sense to me, since we never want to assume
> simply $f$. rather, we have a whole list of assumptions,
> $f_1$ through
> $f_n$, where for a typical block, $n$ can be in the tens or
> even hundreds.
> are you really claiming that verifying $(f_1 \wedge f_2
> \wedge \cdots \
> wedge f_n) \rightarrow g$ is practical and that formulas with tens or
> hundreds of assumptions are routinely verified by forspec
> users? since ltl
> model checking is exponential in the size of the formula, i
> would find this
> hard to believe.
Assignments are more efficient in our implementation of "cone of
influence" calculation. It has nothing to do with complexity.
I never claimed for hundreds of assumptions, but specs with 30-50
assumptions are typical to the Pentium 4. Without assume/guarantee,
using FV to a large scale in the Pentium 4 would have not been
feasible.
As for the complexity issue, two comments:
1. It would be very interesting to see an exponential lower bound
for LTL model checking. The only known lower bound is PSPACE
hardness.
2. Model checking is also PSPACE hard with respect to the size of the
RTL and we all know how to handle that. Moreover, given a language,
the RTL that implements the language will be not smaller than the FTL
formula for the same language.
To summarize, it still looks like my perceptions on Sugar from the note
attached below are all correct, right?
>
> cindy.
>
> 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
>
>
> "Armoni, Roy" <roy.armoni@intel.com> on 16/07/2001 22:38:14
>
> Please respond to "Armoni, Roy" <roy.armoni@intel.com>
>
> To: Cindy Eisner/Haifa/IBM@IBMIL
> cc: vfv <vfv@eda.org>
> Subject: How Sugar supports the assume/guarantee paradigm
>
>
>
>
> 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 30 2001 - 09:50:40 PDT