Game Development Reference
equipping a standard pushdown automaton with a parity condition on the
state set. Acceptance is defined as before.
Assume Win is specified by a deterministic pushdown ω -automaton with
parity condition. Taking the product of a game graph G with the pushdown
automaton (in the same way as in Section 2.3) results in a parity game on a
pushdown graph. These games can be solved and winning strategies can be
implemented by pushdown automata.
Theorem 2.22 (Walukiewicz ) Parity games on pushdown graphs
can be solved in exponential time and winning strategies can be implemented
by pushdown automata.
Note that as opposed to Proposition 2.21 the winning condition is spec-
ified directly as a parity condition on the pushdown graph. The proof of
Theorem 2.22 that is given in Walukiewicz  uses a reduction to games
on finite graphs. A construction based on tree automata can be found in
As a consequence we obtain that specifications given by deterministic
pushdown automata admit an algorithmic solution.
Corollary 2.23 The problem of deciding the winner in a game ( G, Win )
for a finite game graph, where Win is defined by a deterministic pushdown
ω-automaton (with parity condition), is decidable.
The result from Theorem 2.22 on pushdown parity games has been extended
to the model of higher-order pushdown automata (Cachat ) which
use nested stacks, and to the even more expressive model of collapsible
higher-order pushdown automata (Hague et al. ), which have a tight
relationship to higher-order recursion schemes.
Instead of considering more complex game graphs it is also possible to
study more complex winning conditions. This research has been initiated by
Cachat et al. , where it was shown that pushdown games with a winning
condition of the following form are decidable: 'there exists some configuration
(vertex of the game graph) that is visited infinitely often'. This condition
has the flavour of a Buchi condition because it asks for some configuration
to be visited infinitely often. But since the game graph is infinite and the
configuration to be visited infinitely often is quantified existentially, this adds
an extra level of complexity. Further results in this direction can be found in
Bouquet et al. , Serre , Loding et al. .