Game Development Reference
In-Depth 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