{UppDMC} – A Distributed Model Checker for Fragments of the {$μ$}-calculus
Title | {UppDMC} – A Distributed Model Checker for Fragments of the {$μ$}-calculus |
Publication Type | Conference Paper |
Year of Publication | 2004 |
Authors | Holmén, F, Leucker, M, Lindström, M |
Editor | Brim, L, Leucker, M |
Conference Name | Proceedings of the $3rd$ Workshop on Parallel and Distributed Methods for Verification |
Series | Electronic Notes in Computer Science |
Volume | 128/3 |
Publisher | 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. |
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} }
PDF:
Postscript:
- News
- Research
- Teaching
- Staff
- Martin Leucker
- Diedrich Wolter
- Ulrike Schräger-Ahrens
- Aliyu Ali
- Mahmoud Abdelrehim
- Phillip Bende
- Juljan Bouchagiar
- Marc Bätje
- Tobias Braun
- Gerhard Buntrock
- Anja Grotrian
- Hannes Hesse
- Raik Hipler
- Elaheh Hosseinkhani
- Hannes Kallwies
- Frauke Kerlin
- Karam Kharraz
- Mohammad Khodaygani
- Ludwig Pechmann
- Waqas Rehan
- Martin Sachenbacher
- Andreas Schuldei
- Annette Stümpel
- Gesina Schwalbe
- Tobias Schwartz
- Daniel Thoma
- Lars Vosteen
- Open Positions
- Contact