Subject: Re: Temporal e
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Tue Jul 10 2001 - 00:02:16 PDT
>
> vardi> It seems to me that without negation the expressive power of
> vardi> the language is quite limited (and in particular, you cannot do
> vardi> compositional reasoning).
>
> for the purposes of defining the semantics of temporal e we introduced
> negation as an operator to the abstract syntax, but you will see that
> we use it only to define user-expressible constructs "firstmatch" and
> "fail" -- without which the language would indeed be rather weak. the
> operational semantics of both these operators introduce deterministic
> state machines.
Does "Temporal e" includes negation? Your document indicates that it
does.
>
> vardi> On the other hand, with negation, it is known that the
> vardi> complexity of the language is nonelementary,
>
> i'm not sure quite i understand where you plucked this nonelementary
> assertion from (my dear Watson)... perhaps you refer to the work of
> Hiraishi that Ed Clark mentioned? i only know that work en passant,
> but believe the expressiveness of Regular Temporal Logic to be similar
> to that of temporal e.
It is well known that emptiness of regular expressions with negation )even
star-free) is nonelementary. See
L. Stockmeyer. The complexity of decision problems in automata and
logic, Ph.D. Thesis, MIT, 1974.
>
> vardi> Has Verisity implemented a model checker of Temporal E? AT
> vardi> least with CBV, ForSpec, and Sugar we have a record of
> vardi> industrial usage in FV.
>
> Verisity is 100% committed to FV (functional verification!) but as you
> probably know we do not build model checkers nor, for that matter, HDL
> simulators. we build interfaces to such tools when practical, and when
> there is sufficient interest amongst our users.
Still, to build a checker for Temoral e would be of nonelementary
complexity.
>
> as some of you may recall i demonstrated such an interface to Cadence
> SMV at CAV in Trento (model checking e properties of e models). since
> then we worked with Cadence on model checking temporal e properties of
> HDL models with FormalCheck, something which was demonstrated on the
> floor at DAC 2000 in LA. i am, however, currently unsure how Cadence
> are positioning FormalCheck in the verification market.
>
> still, to the above ends we have developed tableau constructions
>
> o for the sigma star fragment of the language
> o for the omega extension of the sigma star language
> - to L automata/L processes
> - to Buechi automata
>
What is the "sigma star fragment"? What is "the omega extension of the
sigma star language"?
> and can confirm that the complexity is EXPSPACE. we are also convinced
> that it is elementary although, frankly, we have made little effort to
> date to derive formal complexity bounds. however we have encouraging
> empirical evidence from compiling properties of industrial designs
> from hundreds of companies that use temporal e in simulation 24/7.
> most such properties involve fail.
Yes, EXPSPACE is indeed elementary, since it is included in dobly
exponential time. I infer, however, that youhave not developed a tableau
construction for full Temporal e. Right?
>
> as i am sure you know both Cadence SMV and Cospan support their own
> approaches to rely/guarantee, approaches that may well differ from
> that mandated by you at Intel. we have experimented with both, as i
> said, and have not found temporal e to be limited in expressiveness.
> in particular our support of the fail operator enables full
> rely/guarantee reasoning with SMV.
>
Can you explain what you mean by "full rely/guarantee reasoning with SMV"?
Thanks,
Moshe
This archive was generated by hypermail 2b28 : Tue Jul 10 2001 - 00:02:52 PDT