Game Development Reference
InDepth Information
hypothesis, we know that, for every interpretation
T
0
of
T
,(
A
,T
0
)

=
ϕ
(
a
) if,
and only if, Player 0 has a winning strategy for the game
G
((
A
,T
0
)
,ϕ
(
a
)
)
.
It su
ces therefor to show that Player 0 win
s
the game
G
:=
G
(
A
,ψ
(
a
))
,T
α
)
,ϕ
(
a
). But this follows from a
general fact on parity game, the socalled
Unfolding Lemma
.
if, and only if, she wins all games
G
((
A
The unfolding of a parity game.
Let
=(
V,V
0
,V
1
,E,
Ω) be a parity
game that has at least one node with priority 0 and in which every node
v
with priority 0 has a unique s
u
ccessor
s
(
v
) (i.e.,
vE
=
G
{
s
(
v
)
}
). This condition
holds for the game
Gg
(
,ψ
(
a
)), since the positions of mi
n
imal priority are
the fixedpoint atoms
T b
which have unique successors
ϕ
(
b
).
Let
Z
be the set of nodes with priority 0 and let
A
G
−
be the game obtained
by deleting from
V
) so that the nodes
in
Z
become terminal positions. The
unfolding
of
G
all edges (
v, s
(
v
))
∈
E
∩
(
Z
×
α
G
is a sequence
G
G
−
up to the
(where
α
ranges over the ordinals) which all coincide with
winning conditions for the terminal positions
v
Z
. For every
α
, we define
a decomposition
Z
=
Z
0
∪ Z
1
, where
Z
σ
is the set of terminal positions
v ∈ Z
at which we declare, for the game
G
∈
α
, that Player
σ
has won. Further,
for every
α
, we define
W
σ
to be winning region of Player
σ
in the game
G
α
.
Note that
W
σ
depends of course on the decomposition
Z
=
Z
0
∪ Z
1
(also
for positions outside
Z
). In turn, the decomposition of
Z
for
α
+ 1 depends
on the winning sets
W
σ
in
α
.Weset
G
Z
0
:=
Z
Z
α
+
0
:=
{v ∈ Z
:
s
(
v
)
∈ W
0
}
Z
0
:=
α<λ
Z
0
for limit ordinals
λ.
W
1
for all
α
, and with increasing
α
, the
winning sets of Player 0 are decreasing and the winning sets of Player 1 are
increasing:
By determinacy,
V
=
W
0
∪
W
0
⊇
W
0
⊇···
W
0
⊇
W
α
+1
⊇···
0
W
1
⊆
W
1
⊆···
W
1
⊆
W
α
+1
⊆···
.
1
Hence there exists an ordinal
α
(whose cardinality is bounded by the
cardinality of
V
) for which
W
0
=
W
α
+1
0
=:
W
0
and
W
1
=
W
α
+
1
=:
W
1
.
The crucial result on unfoldings of parity games states that these fixedpoints
coincide with the winning regions
W
0
and
W
1
of the original game
G
.
W
0
=
W
0
and W
1
=
W
1
.
Lemma 4.11
(Unfolding Lemma)
For a proof, see Gradel [2007].
Search Nedrilad ::
Custom Search