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

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.

• Type: Conference
• Year: 1997
• Where: ICALP
• Authors: Olaf Burkart, Bernhard Steffen
• Keywords: Context-free Processes, ICALP 1997, Infinite Sequential Processes, Model Checking Algorithm, Programming Languages