Pushdown Processes: Games and Model-Checking

A pushdown game is a two player perfect information infinite game on a transition graph of a pushdown automaton. A winning condition in such a game is defined in terms of states appearing infinitely often in the play. It is shown that if there is a winning strategy in a pushdown game then there is a winning strategy realized by a pushdown automaton. An EXPTIME procedure for finding a winner in a pushdown game is presented. The procedure is then used to solve the model-checking problem for the pushdown processes and the propositional μ-calculus. The problem is shown to be DEXPTIME-complete.

Authors

• Igor Walukiewicz

Keywords

No keywords are indexed for this paper.