*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.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file