{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
- Mahmoud Abdelrehim
- Aliyu Ali
- Christopher Walther
- Phillip Bende
- Moritz Bayerkuhnlein
- Marc Bätje
- Tobias Braun
- Gerhard Buntrock
- Raik Dankworth
- Anja Grotrian
- Raik Hipler
- Elaheh Hosseinkhani
- Frauke Kerlin
- Karam Kharraz
- Mohammad Khodaygani
- Ludwig Pechmann
- Waqas Rehan
- Martin Sachenbacher
- Andreas Schuldei
- Mahdi Pourghasem
- Manuel Herbst
- Inger Struve
- Annette Stümpel
- Gesina Schwalbe
- Tobias Schwartz
- Daniel Thoma
- Sparsh Tiwari
- Lars Vosteen
- Open Positions
- Contact