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...

• Type: Conference
• Year: 1994
• Where: LICS
• Authors: Shipei Zhang, Oleg Sokolsky, Scott A. Smolka
• Keywords: Automated Reasoning, Circuit Value Problem, LICS 1994, Modal Mu-calculus, Model Checking