Local parallel model checking for the alternation-free μ-calculus

We describe the design of (several variants of) a local parallel model-checking algorithm for the alternation-free fragment of the mu-calculus. It exploits a characterisation of the problem for this fragment in terms of two-player games. For the corresponding winner, our algorithm determines in parallel a winning strategy, which may be employed for debugging the underlying system interactively, and is designed to run on a network of workstations. Depending on the variant, its complexity is linear or quadratic. A prototype implementation within the verification tool TRUTH shows promising results in practice.