Local Parallel Model Checking for the Alternation Free mu-Calculus

Benedikt Bollig, Martin Leucker, Michael Weber

In this paper, we describe the design and implementation 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 model checking problem for this fragment in terms of two-player
games.  Our algorithm determines the corresponding winner in parallel.
Furthermore, a winning strategy is computed which may be employed for
interactively debugging the underlying system. The algorithm is designed
to run on a network of workstations. Depending on the chosen variant,
its complexity is linear or quadratic. A prototype implementation within
the verification tool Truth shows promising run--time and memory behaviour
in practice.