Subject: Re: Temporal e
From: David Van Campenhout (dvc@verisity.com)
Date: Tue Jul 10 2001 - 08:13:56 PDT
Moshe Vardi writes:
>
> >
> > 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.
Temporal e does not have a negation operator, but it has 'fail'.
For top level temporal expressions under an 'expect' or 'assume'
statement, only the omega semantics matter. The omega semantics of
'fail t', is the complement of the omega semantics of 't'. So a 'fail'
operator that appears at the top-level of a temporal expression really
acts like negation. However for a nested 'fail' operator the story is
more complicated. In general, to derive the semantics of a temporal
expression, both the omega AND the star semantics of its
subexpressions are required. The star semantics of 'fail t' are very
different from that of negation. (See 'e' Semantics Manual).
The bottom line is that our fail operator acts like negation if it is
the top-level operator. So for the purpose of assume/guarantee
reasoning, we can use 'fail'. However, nested fail is a very different
beast from nested negation; in particular, it does not suffers from
negation's complexity woes.
>
>
> >
> > 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.
thanks; but I think this is not relevant (see my explanation above).
>
> >
> > 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.
Again, this statement assumes that fail is negation...
>
> >
> > 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"?
The sigma star fragment is the semantics when interpreted over
finite-length sequences. The sigma omega fragment is the semantics
when interpreted over infinite-length sequences.
>
> > 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?
Not right. We have a tableau construction for both the star and omega
fragments of full temporal e.
>
> >
> > 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"?
>
We can translate any property + set of constraints formulated in
temporal e so that it can be model checked with SMV.
Hope this helps.
David
This archive was generated by hypermail 2b28 : Tue Jul 10 2001 - 08:17:14 PDT