Model Checking the Full Modal Mu-Calculus for Infinite Sequential Processes

Olaf Burkart and Bernhard Steffen


In this paper we develop a new elementary algorithm for model-checking infinite sequential processes, including context-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus. Whereas the actual model checking algorithm results from considering conditional semantics together with backtracking caused by alternation, the corresponding correctness proof requires a stronger framework, which uses dynamic environments modelled by finite-state automata.


This report is available in the following formats:

Previous | Index | Next