Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - On the Decidability of Model Checking for Several mu-calculi and Petri Nets

Reference:

J. Esparza. On the decidability of model checking for several mu-calculi and petri nets. In S. Tison, editor, Proceedings of Trees in Algebra and Programming - CAAP '94, 19th International Colloquium 1994, number 787 in Lecture Notes in Computer Science, pages 115–129, 1994.

Abstract:

The decidability of the model checking problem for several mu-calculi and Petri nets is analysed. The linear time mu-calculus without atomic sentences is decidable; if simple atomic sentences are added, it becomes undecidable. A very simple subset of the modal mu-calculus is undecidable.

Suggested BibTeX entry:

@inproceedings{Esp94,
    author = {J. Esparza},
    booktitle = {Proceedings of Trees in Algebra and Programming - CAAP '94, 19th International Colloquium 1994},
    editor = {S. Tison},
    number = {787},
    pages = {115-129},
    series = {{Lecture Notes in Computer Science}},
    title = {On the Decidability of Model Checking for Several mu-calculi and Petri Nets},
    year = {1994}
}

PDF (1 MB)