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