Abstract:
Games given by transition graphs of pushdown processes are
considered. It is shown that if there is a winning strategy in such a game
then there is a winning strategy that is realized by a pushdown process. This
fact turns out to be connected with the model checking problem for the
pushdown automata and the propositional 
-calculus. It is show that this
model checking problem is DEXPTIME-complete
Available as PostScript, PDF, DVI.