Game Development Reference
In-Depth Information
monadic second-order logic (S1S), or by automata-theoretic conditions such
as Muller conditions, Streett-Rabin conditions, or parity conditions (see the
contributions by Christof Loding and Marcin Jurdzinski to this topic). In
this chapter, only parity conditions will be used.
A parity game is given by a game graph
G
=( V,V 0 ,V 1 ,E ) together
with a priority function Ω: V
ω assigning to each position a natural
number. An infinite play π = v 0 v 1 ... is won by Player 0 if the least priority
appearing infinitely often in π is even, or no priority appears infinitely often
(which may only happen if the range of Ω is infinite).
Winning strategies, winning regions, and determinacy. A (deter-
ministic) strategy for Player σ is a partial function f : V V σ → V that
assigns to finite paths through G ending in a position v ∈ V σ a successor
w ∈ vE . A play v 0 v 1 ···∈V ω is consistent with f if, for each initial seg-
ment v 0 ...v i with v i ∈ V σ , we have that v i +1 = f ( v 0 ...v i ). We say that
such a strategy f is winning from position v 0 if every play that starts at
v 0 and that is consistent with f is won by Player σ . The winning region
of Player σ , denoted W σ , is the set of positions from which Player σ has a
winning strategy.
A game
W 1 = V , i.e., if
from each position one of the two players has a winning strategy. For games
with draws, it is appropriate to define determinacy in a slightly different way:
we call a game with draws determined if from each position, either one of the
two players has a winning strategy, or both players have a strategy to achieve
at least a draw. To put it differently, this means that from every position
v
G
, without draws, is called determined if W 0
σ has a strategy to guarantee that Player σ does
not win. It has been known for almost 100 years that chess is determined
in this sense, see Zermelo [1913]. However, we still do not know which of
the three possibilities holds for the initial position of chess: whether White
has a winning strategy, whether Black has one, or whether both players can
guarantee a draw.
There is a large class of games that are known to be determined, including
all games for which the winning condition is a Borel set (Martin [1975]). One
can show (based on the Boolean Prime Ideal Theorem, which is a weak form
of the the Axiom of Choice) that non-determined games exist. However, all
games considered in this chapter are determined in a strong sense.
V
\
W σ , Player 1
Computing winning regions of reachability games. To solve a game
algorithmically means to compute the winning regions for the two players.
When considering algorithmic problems of this kind, we always assume that
game graphs are finite. For reachability games, the winning regions can easily