Geodesy

Algorithm

Benchmark (surveying)

Philosophy

Theoretical computer science

Archaeology

Operating system

Liveness

Computer science

Simple (philosophy)

Dentistry

Suite

Calculus (dental)

Geography

Epistemology

Workstation

Fragment (logic)

Medicine

Programming language

Model checking

History

Electronic Notes in Theoretical Computer Science

We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and μ-calculus specifications with at most one alternation of minimal and maximal fixed-point operators. This fragment is also known as Lμ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.

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