Subject: RE: A Complexity Question (was RE: Temporal e)
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Sun Jul 15 2001 - 00:11:55 PDT
>
> 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
>
Does these results include arbitrary nesting of parallel (concurrent)
structures?
I know that bisimulation with top level concurrency and hiding abstraction
was EXPTIME-hard, and
doesn't that show that CTL model checking is as hard for such models?
I also remember Rabinovich
showed that trace equivalence with top level concurrency was PSPACE complete
without hiding. Do these results or more recent results of Alur, Kupferman
and
Vardi show the similar results for unlimited nesting of concurrent
structures
and hiding abstractions?
regards
Sandeep
This archive was generated by hypermail 2b28 : Wed Jul 11 2001 - 00:16:00 PDT