Game Development Reference

In-Depth Information

it serves as a witness. The explicit bound obtained plays a key role in the

design and analysis of the (game parity) progress measure lifting algorithm.

For a set
D

V
and for every odd
q
, let
n
q
be the number of vertices

of priority
q
in
D
, and let
M
D
be the set of tuples (
x
d−
1
,...,x
3
,x
1
)
∈
N

⊆

d/
2
,

. For simplicity, we write
n
q
for the number
n
q

of vertices of priority
q
in the whole game graph. Note that the set
M
D
∪{}

is totally ordered by the lexicographic order.

0
,
1
,...,n
q
}

such that
x
q
∈{

Exercise 3.19

Assume that
D

⊆

V
is a 0-dominion. Prove that there is a

game parity progress measure
ξ
:
V

dom
(
ξ
).

One way to approach this task is to first invoke positional determinacy of

parity games, and then to formalise the insight that the bounds, considered in

Exercise 3.16, for the numbers of occurrences of vertices of an odd priority
q

before a vertex of priority higher than
q
occurs, can be 'optimised' not to

exceed
n
q
. Another approach is to construct a progress measure
ξ
:
D

→

M
D
∪{}

, such that
D

⊆

M
D

by induction on the size of
D
, similar to that employed in the design and

the proof of correctness of algorithm
parity-win
(
G
).

→

We now use the insight from Exercise 3.19, that game parity progress

measures with 'small' ranges exist, to devise an e
cient algorithm for

finding such progress measures, and hence for finding 0-dominions if any

exist. In fact, we argue that the
pointwise-lexicographic least game

parity progress measure
ξ
∗
exists, and that its domain
dom
(
ξ
∗
)isthe

greatest possible, i.e.,
dom
(
ξ
∗
)=
win
0
(
G
). Moreover, the algorithm com-

putes this pointwise-lexicographic least progress measure, and it returns the

pair (
win
0
(
G
)
, win
1
(
G
)) of the winning sets of both players. The algorithm

progress-measure-lifting
(
G
), shown in Figure 3.4 can be viewed as a
value

iteration
procedure that computes the least solution
ξ
∗

of the system of

constraints expressed by conditions (3.4) and (3.5).

algorithm
progress-measure-lifting
(
G
)

for all
v

∈

V
do
ξ
(
v
)

←

(0
,
0
,...,
0)

∈
N

d/
2

while
ξ<lift
(
ξ, v
) for some
v

∈

V

do
ξ

←

lift
(
ξ, v
)

endwhile

return
(
dom
(
ξ
)
,V \ dom
(
ξ
))

Figure 3.4 The progress measure lifting algorithm for parity games

The algorithm
progress-measure-lifting
(
G
) uses operators
lift
(

·

,v
), for all

Search Nedrilad ::

Custom Search