Game Development Reference
InDepth Information
v
V
. In order to define this family of operators we recall the definition of the
set
M
D
, and observe that
M
D
⊆
∈
V
. In particular, the latter
holds for
D
=
win
0
(
G
) and hence, by Exercise 3.19, there is a game parity
progress measure
ξ
:
V
M
V
for every
D
⊆
→
M
V
∪{}
, such that
dom
(
ξ
)=
win
0
(
G
). For a
function
ξ
:
V
→
M
V
∪{}
and a vertex
w
∈
V
, we define
lift
(
ξ, w
)=
ξ
(
w
)
if
w
=
v
, and we set
lift
(
ξ, v
) to be the least element of
M
V
∪{}
that makes
the thusdefined function
lift
(
ξ,
·
):
V
→
M
V
∪{}
satisfy the condition (3.4)
or (3.5), respectively, at
v
.
The condition
ξ<lift
(
ξ, v
)ofthe
while
loop in the algorithm
progress
measurelifting
(
G
) uses the strict inequality symbol
<
to compare functions.
It should be interpreted as the
pointwiselexicographic order
, in which
for every vertex the lexicographic order on
M
V
is used, and for the strict
pointwiselexicographic inequality to hold it su
ces that the strict lexico
graphic inequality holds for at least one vertex.
,v
) is monotone
with respect to the pointwiselexicographic order. Use the KnasterTarski
theorem for complete lattices to conclude that the least game parity progress
measure
ξ
∗
exists in every parity game, and that the
while
loop in algorithm
progressmeasurelifting
(
G
) computes it.
Conclude that
win
0
(
G
)=
dom
(
ξ
∗
), and hence that the algorithm
progress
measurelifting
(
G
) is correct.
Exercise 3.20
Argue that for all
v
∈
V
, the operator
lift
(
·
Finally, we analyse the worstcase running time of algorithm
progress
measurelifting
(
G
). The key element of the analysis of the algorithm is an
upper bound on the size of the set
M
V
.
=
q∈{
1
,
3
,...,d−
1
}
(
n
q
+1)
(
n/
(
d/
2))
d/
2
.
Provide implementation details of the algorithm
progressmeasurelifting
(
G
)
that make its worstcase running time
O
(
dm ·
(
n/
(
d/
2))
d/
2
). In order to
establish this worstcase running time bound, use the property that the sum
of all vertex outdegrees in a directed graph is
O
(
m
), and that lexicographic
comparison of (
d/
2)tuples of numbers can be carried out in time
O
(
d
).
Exercise 3.21
Prove that

M
V

≤
Theorem 3.9
(Browne et al. [1997], Seidl [1996], Jurdzinski [2000])
The
winning sets and positional winning strategies of both players in parity games
can be computed in time O
(
dm ·
(
n/
(
d/
2))
d/
2
)=
O
(
n
d/
2+
O
(1)
)
.
Search Nedrilad ::
Custom Search