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