{UppDMC} – A Distributed Model Checker for Fragments of the {$μ$}-calculus

Title{UppDMC} – A Distributed Model Checker for Fragments of the {$μ$}-calculus
Publication TypeConference Paper
Year of Publication2004
AuthorsHolmén, F, Leucker, M, Lindström, M
EditorBrim, L, Leucker, M
Conference NameProceedings of the $3rd$ Workshop on Parallel and Distributed Methods for Verification
SeriesElectronic Notes in Computer Science
Volume128/3
PublisherElsevier Science Publishers
Abstract

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 fixed-point operators. This fragment is also known as LmuTwo. 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.

Bibtex: 
@inproceedings {LeuckerHL04,
	title = {{UppDMC} {\textendash} A Distributed Model Checker for Fragments of the {$μ$}-calculus},
	booktitle = {Proceedings of the $3rd$ Workshop on Parallel and Distributed Methods for Verification},
	series = {Electronic Notes in Computer Science},
	volume = {128/3},
	year = {2004},
	publisher = {Elsevier Science Publishers},
	organization = {Elsevier Science Publishers},
	abstract = {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 fixed-point operators. This fragment is also known as LmuTwo. 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.},
	author = {Fredrik Holm{\'e}n and Martin Leucker and Marcus Lindstr{\"o}m},
	editor = {Lubos Brim and Martin Leucker}
}
Postscript: