Sciweavers

Share
LICS
1994
IEEE

On the Parallel Complexity of Model Checking in the Modal Mu-Calculus

9 years 5 months ago
On the Parallel Complexity of Model Checking in the Modal Mu-Calculus
The modal mu-calculus is an expressive logic that can be used to specify safety and liveness properties of concurrent systems represented as labeled transition systems (LTSs). We show that Model Checking in the Modal Mu-Calculus (MCMMC) -- the problem of checking whether an LTS is a model of a formula of the propositional modal mu-calculus -is P-complete even for a very restrictive version of the problem involving the alternationfree fragment. In particular, MCMMC is P-complete even if the formula is fixed and alternation-free, and the LTS is deterministic, acyclic, and has fan-in and fan-out bounded by 2. The reduction used is from a restricted version of the circuit value problem (Does a circuit output a 1 on inputs x1, . . ., xn?) known as Synchronous Alternating Monotone Fanout 2 Circuit Value Problem. Our P-completeness result is tight in the sense that placing any further non-trivial restrictions on either the formula or the LTS results in membership in NC for MCMMC. Specifical...
Shipei Zhang, Oleg Sokolsky, Scott A. Smolka
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where LICS
Authors Shipei Zhang, Oleg Sokolsky, Scott A. Smolka
Comments (0)
books