Game Development Reference
In-Depth Information
provide the detailed structure of an inductive correctness proof for the
algorithm, and we invite the reader to fill in the details.
Exercise 3.7 Assume that reach j ( p 1 ( d )) = V . Argue that if player j
follows a positional p 1 ( d )-reachability strategy from an arbitrary starting
vertex v
V , then a vertex in p 1 ( d ) occurs infinitely many times. Conclude
that in this case win j ( G )= V .
Assume that the games G and G are positionally determined, and that
there are positional i -dominion and j -dominion strategies μ and χ on the
winning sets W i = win i ( G ) and W j = win j ( G ), respectively, in game G , and
positional i -dominion and j -dominion strategies μ and χ on the winning
sets W i = win i ( G ) and W j = win j ( G ), respectively, in game G .
Exercise 3.8 Assume that W i = . Argue that the positional strategy
that is the union of χ and the p 1 ( d )-reachability strategy is a winning
strategy for j from every starting vertex in game G . Conclude that in this
case win j ( G )= V .
Assume that W i
Exercise 3.9
. Argue that the positional strategy μ
that is the union of μ and the W i -reachability strategy is a positional
i -dominion strategy on reach i ( W i ) in game G .
Observe that positional determinacy of game G implies that reach i ( W i )
=
W i = V
W j . Prove that the positional strategy that is the union of μ
and μ is a positional i -dominion strategy on V
\
W j in game G . Conclude
\
W
that V
win i ( G ).
Prove that χ is a j -dominion strategy on W j in game G . Conclude that
W
\
j
win j ( G ), that parity games are positionally determined, and that the
algorithm parity-win ( G ) is correct.
j
Theorem 3.5 (Emerson and Jutla [1991])
Parity games are positionally
determined.
Before we carry out a detailed analysis of the worst-case running time
of the algorithm parity-win ( G ), we observe that positional determinacy of
parity games implies that the problem of deciding the winner in parity games
is in NP and in co-NP.
A one-player parity game is a parity game in which either V 0 =
or
V 1 =
, i.e., one of the players owns all vertices in the game graph; in the
former case we have a player 1 one-player parity game, and in the latter
case we have a player 0 one-player parity game. An alternative, and for
all purposes equivalent, definition of a one-player game requires that every