Pushdown Processes: Games and Model Checking

Igor Walukiewicz

December 1996


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 tex2html_wrap_inline19 -calculus. It is show that this model checking problem is DEXPTIME-complete

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.