Game Development Reference
In-Depth 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 so-called 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 fixed-point 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 fixed-points
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].