# {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
- Phillip Bende
- Martin Blankenburg
- Gerhard Buntrock
- David Caraveo
- Lukas Convent
- Sebastian Hungerecker
- Elisabeth Husmann
- Hannes Kallwies
- Karam Kharraz
- Uwe Kienitz
- Nikolas Knickrehm
- Grigory Markin
- Maria Ostanina
- André Pedro
- Torben Scheffel
- Malte Schmitz
- Nina Strugalla
- Annette Stümpel
- Daniel Thoma
- Gunnar Bergmann
- Open Positions

- Contact