Game Development Reference

In-Depth Information

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 [1996])
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 [1996] uses a reduction to games

on finite graphs. A construction based on tree automata can be found in

Vardi [1998].

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 [2003]) which

use nested stacks, and to the even more expressive model of collapsible

higher-order pushdown automata (Hague et al. [2008]), 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. [2002], 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. [2003], Serre [2004], Loding et al. [2004].

Search Nedrilad ::

Custom Search