It is known that pushdown processes have a decidable monadic second-order t
heory (Muller and Schupp, Theoret. Comput. Sci. 37 (1985) 51-75) and that t
his result covers the model-checking problem for the modal mu-calculus. Unf
ortunately, the corresponding decidability procedure is not practical due t
o its nonelementary complexity. Recently, however, a very intricate element
ary algorithm for model checking the full modal mu-calculus for pushdown pr
ocesses based on games was presented by Walukiewicz (CAV'96, Lecture Notes
in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 62-74). Lifting
the classical finite-state model checking technique to second-order, we de
velop here a more structural and transparent elementary algorithm for model
-checking infinite sequential processes, including concert-free processes,
pushdown processes, and regular graphs, that captures the full modal mu-cal
culus as well. Whereas the actual model-checking algorithm simply resorts t
o backtracking in order to capture alternation, the corresponding correctne
ss proof requires to introduce the stronger framework of dynamic environmen
ts which are modelled by finite-state automata. (C) 1999 Elsevier Science B
.V. All rights reserved.