On the decidability of model checking for several mu-calculi and Petri nets

Javier Esparza

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

This file is a slightly modified version of the LFCS Technical Report of July 1993. This version will appear in the Proceedings of the Colloquium on Trees in Algebra and Programming (CAAP) to be held in Edinburgh in April, 1994. The proceedings of CAAP '94 will be published in the Springer-Verlag LNCS series.

LFCS report ECS-LFCS-93-274 (updated), July 1993.

Previous | Index | Next