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}
}