In this paper we develop a new exponential 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 work was supported during my stay at IRISA by the European Community under HCM grant ERBCHBGCT 920017, and during my stay at the LFCS by the DAAD under grant D/95/14834 of the NATO science committee.