Subject: Re: Temporal e
From: Matthew Morley (matthew@verisity.com)
Date: Mon Jul 09 2001 - 20:22:56 PDT
Hi Moshe,
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.
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.
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.
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
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.
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.
i look forward to continuing this dialogue at CAV. bon chance!
M
--
This archive was generated by hypermail 2b28 : Mon Jul 09 2001 - 20:26:19 PDT