Home
 

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

Olaf Burkart and Bernhard Steffen

Abstract:

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.

ECS-LFCS-97-355.

This report is available in the following formats:

Previous | Index | Next