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-hard even for a very restrictive version of the problem involving the alternation-free fragment. In particular, MCMMC is P-hard even if the formula is fixed and alternationfree, 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 known as Synchronous Alternating Monotone Fanout 2 Circuit Value Problem. Our P-hardness 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. Specifically, we exhibit NC-algorithms for two potentially useful versio..