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

Search Nedrilad ::

Custom Search