Game Development Reference
InDepth Information
x
1
,y
1
,y
2
x
2
,y
1
,y
2
x
2
σ
(
m
0
,x
1
)=
y
1
σ
(
m
1
,x
1
)=
y
2
σ
(
m
0
m
1
x
1
·
,x
2
)=
y
1
Figure 2.2 Finite memory strategy
example play together with the sequence of memory states could look as
follows, where the moves that are determined by
σ
are marked:
σ
σ
σ
σ
σ
y
1
x
1
y
1
x
1
y
1
x
2
y
1
x
1
y
2
x
1
y
1
···
m
0
m
0
m
0
m
0
m
0
m
0
m
1
m
1
m
0
m
0
m
0
We have defined winning conditions to be given by some set
Win ⊆ C
ω
.
Usually, this set
Win
is defined in terms of the colours that appear infinitely
often during a play. Some of the most common winning conditions are listed
below:
•
A
Buchi condition
is given by a set
F
C
of colours. The set
Win
contains all sequences
γ ∈ C
ω
such that Inf(
γ
)
∩ F
=
∅
, i.e., Eva wins a
play
α
if at least one colour from
F
occurs infinitely often in
α
.
⊆
2
C
of sets of colours. The
set
Win
contains all sequences
γ ∈ C
ω
such that Inf(
γ
)
∈F
, i.e., Eva wins
if the set of colours that occur infinitely often in
α
is a set that is listed
in
F
.
•
A
parity condition
is specified over a finite set of natural numbers as
colours:
C ⊆
N. The set
Win
contains all sequences
γ ∈ C
ω
•
A
Muller condition
is given by a family
F⊆
for which the
maximal number that occurs infinitely often is even.
Clearly, Buchi conditions and parity conditions are special cases of Muller
conditions. For a Buchi condition defined by
F
the equivalent Muller condition
is
F
=
{
D
⊆
C

D
∩
F
=
∅}
. For a parity condition defined over
C
⊆
N
the
equivalent Muller condition is
F
=
{D ⊆ C 
max(
D
)iseven
}
.
The central role of parity conditions in the theory of infinite games on
graphs is due to the following result.
Theorem 2.5
(Emerson and Jutla [1988], Mostowski [1991])
Parity games
are determined with positional strategies.
We make use of this result throughout this chapter. A proof is given in
chapter 3,
Algorithms for Solving Parity Games
by Marcin Jurdzinski in this
Search Nedrilad ::
Custom Search