Subject: RE: Sugar - Complexity Question
From: Armoni, Roy (roy.armoni@intel.com)
Date: Sat Jul 07 2001 - 11:40:59 PDT
Hi Hillel,
Since the issue of assume/guarantee is so important, I plan to
write a short manuscript that will explain all the details of how
assume/guarantee is supported in ForSpec. It will also contain
a description of some artifact of the assume/guarantee paradigm
that I discussed in private with the IBM people and Cindy asked me
to explain to the committee. It will take me a few days though
because I am leaving on a business trip tomorrow morning - hope
to be able to complete it during the long flights :)
At this point, I can answer some of the assumptions that you make
below:
1) No, we do not agree that converting an assertion to an
assumption requires determinism. Actually, if you follow the
so called "tableau construction" of LTL, you realize that the
assertions are those that require negation, but the assumptions
are compiled as they are. There are more than one approach to
tableau construction, some of them require to bring the formula
first to negation-normal-form(NNF) and some do not. Note that at
any rate, FTL is closed under negation, and it is possible to
bring every FTL formula to NNF, thus allowing both approaches to
tableau construction.
2) Having said that, we also do not agree that assuming FTL
formulas is sometimes not practical - there is no difference
between assuming and asserting an FTL formula. I will answer
this issue while discussing complexity in my manuscript, but
the short answer is that model-checking of an FTL formula (either
assumed or asserted) is in PSPACE if time windows are not used,
and since time windows are logarithmic notation, then with time
windows the problem is in EXPSPACE (actually, maybe even in ESPACE,
but I have to check this point).
3) I believe that since your assumptions about assume/guarantee
in ForSpec are not correct, the answer to the rest of your
questions is obvious. There is nothing special in the tools that
identifies practical properties to be used as assumptions. I
will repeat the mantra: every FTL property can be used as an
assumption (and as an assertion). The answer is in the careful
design of the language, and that makes our users happy rather than
frustrated.
Stay tuned for the full answer :)
Regards, Roy
-----Original Message-----
From: Hillel Miller [mailto:hillelm@msil.sps.mot.com]
Sent: Thursday, July 05, 2001 7:11 PM
To: Moshe Vardi
Cc: eisner@il.ibm.com; Edmund.Clarke@cs.cmu.edu; Sudhir_Kadkade@sifr.com;
Vassilios.Gerousis@infineon.com; arif@synopsys.com; avner.landver@intel.com;
axels@cadence.com; badru@athdl.com; bdeadman@sdvinc.com;
cbrowy@avery-design.com; coelho@verplex.com; dana@wisdom.weizmann.ac.il;
danaf@il.ibm.com; davidg@synopsys.com; dudani@synopsys.com; emc@cs.cmu.edu;
erichm@cadence.com; fitz@co-design.com; flake@co-design.com;
foster@rsn.hp.com; geist@il.ibm.com; gkhoory@synopsys.com;
jbhasker@cadence.com; johne@verplex.com; kchen@verplex.com;
limor.fix@intel.com; mac@verisity.com; matthew@verisity.com;
michael.siegel@mchp.siemens.de; pixley@adttx.sps.mot.com;
prakash@realintent.com; roy.armoni@intel.com; shoham@il.ibm.com;
skshukla@ics.uci.edu; smeier@synopsys.com; swamiv@synopsys.com;
tla@0-in.com; wolfstal@il.ibm.com; yaron@verisity.com; ychsu@novas.com;
zhong@innologic-systems.com
Subject: Re: Sugar - Complexity Question
Moshe, Roy
Could you please explain in detail the user model with Forspec as to the
assume/gurantee
paradigm ?
I think we agree that converting an assertion to an assumption requires
determinism.
I think we also agree that this is sometimes not practical.
What is unique about ForSpec that makes this practical ?
Is it the fact that your tools know how to identify such assertions that
can
be converted ? If this is the case, then a user may spend hours writing an
assertion to discover on invocation that this is not feasable for an
environment ?
Will this not frustrate the user ?
Hillel
Moshe Vardi wrote:
> But you could have "(r1 && r2, r3)[*],r4", so you cannot determinize in
> advance.
>
> It is known that universality of SERE is EXPSPACE-complete, so I doubt
> that you'll be able to beat that lower bound.
>
> Moshe
This archive was generated by hypermail 2b28 : Sat Jul 07 2001 - 11:42:03 PDT