Subject: A Complexity Question (was RE: Temporal e)
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Sat Jul 14 2001 - 02:04:18 PDT
I have a complexity question:
We know that for LTL, the complexity of model checking is linear in the
state space, and PSPACE complete in the formula size.
Now, if we allow our models to have parallel operators
such as M1 || M2 || .... || Mk
then we know the state space is exponential in the size of the
description. Now if we allow arbitrary nesting (which is reasonable
for a hardware description language), then what is the complexity
of LTL model checking with respect to size of the input model? Is it
non-elementary?
I remember there was a result by Stockmeyer in a private communication
where he proved that with single level of nesting, bisimulation is
EXPTIME-Hard, by reducing the acceptance problem of alternating PSPACE
Turing machine. However, if some one has already characterized
the complexity of CTL and LTL model checking with respect to model
description
size with arbitrary level of concurrency, then I would like to
know the result. Also, probably that will settle some of the complexity
questions arising here, because usually model descriptions are much
larger than the property formulations, and hence if the complexity
of model checking is dominated by the COmplexity with respect to model
description size, one can ignore what it is with respect to formula size?
Isn't it? Or may be I am missing something here.
Regards
Sandeep
> -----Original Message-----
> From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of Moshe
> Vardi
> Sent: Tuesday, July 10, 2001 12:02 AM
> To: matthew@verisity.com; vfv@eda.org
> Subject: Re: Temporal e
>
>
>
> >
> > 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
> -----Original Message-----
> From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of Moshe
> Vardi
> Sent: Tuesday, July 10, 2001 12:02 AM
> To: matthew@verisity.com; vfv@eda.org
> Subject: Re: Temporal e
>
>
>
> >
> > 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 - 02:07:59 PDT