UppDMC: A Distributed Model Checker for Fragments of the mu-Calculus

We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and mu-calculus specifications with at most one alternation of minimal and maximal fixedpoint operators. This fragment is also known as L-mu(2). Recently, efficient game-based algorithms for this logic have been outlined. We describe the implementation of these algorithms within UppDMC and study their performance on practical examples. Running UppDMC on a simple workstation cluster, we were able to check liveness properties of the largest examples given in the VLTS Benchmark Suite, for which no answers were previously known.