Subject: Re: A Complexity Question (was RE: Temporal e)
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Wed Jul 11 2001 - 00:03:28 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
In the case of concurrent structures, there is a single exponential
blow-up in the complexity (wrt the model). This has been studied lately
by several people, including Alur, Rabinovich, Schnoebelen, and
Kupferman&V. For example, the complexity of ForSpec model checing wrt
concurrent models is PSPACE in both the model and the propetry.
Moshe
This archive was generated by hypermail 2b28 : Wed Jul 11 2001 - 00:04:37 PDT