Game Development Reference

In-Depth Information

3.3 Solving parity games

This is the main technical part of this chapter, where we establish positional

determinacy of parity games, we discuss the computational complexity of

deciding the winner in parity games, and we present several state-of-the-art

algorithms for solving them.

In Section 3.3.1 we present a natural generalisation of the divide-and-

conquer procedure, presented in Section 3.2 for repeated reachability and

eventual safety games, to parity games. While the idea of an inductive

argument for construction of winning strategies in omega-regular games

can be attributed to McNaughton [1993], here we follow the presentation

of McNaughton's algorithm for parity games due to Zielonka [1998]. A by-

product of the design and analysis of the algorithm is the fundamental result

that parity games are positionally determined (Emerson and Jutla [1991]).

We use positional determinacy to infer the result of Emerson et al. [1993] that

the problem of deciding the winner in parity games is in NP and in co-NP. We

also argue that the running time of the algorithm is
O
(
m

((
n
+
d
)
/d
)
d
)) =

O
(
n
d
+
O
(1)
), where
n
is the number of vertices in the game graph,
m
is the

number of edges, and
d
= max(
p
(
V
)) is the biggest priority of a vertex in

the parity game.

In Section 3.3.2 we present a refinement of the classical divide-and-conquer

procedure, due to Jurdzinski et al. [2008]. The innovation there is to dovetail

the recursive divide-and-conquer procedure with a brute-force search for

dominions
, i.e., sets of vertices inside which a player can trap the oppo-

nent forever and win. It turns out that if the size of dominions sought is

appropriately cho
se
n then the overall running time of the divide-and-conquer

algorithm is
n
O
(
√
n
)
, which is better than
O
(
n
d
+
O
(1)
)if
d
=Ω(
n
(1
/
2)+
ε
).

In Section 3.3.3 we present an altogether different algorithm for solving

parity games, the progress measure lifting algorithm due to Jurdzinski [2000].

The design of the algorithm is based on the concept of a game parity progress

measure that witnesses the existence of a winning strategy for one of the

players. We establish that relatively small such witnesses exist and that

they can be computed in time
O
(
dm

·

(
n/
(
d/
2))
d/
2
)=
O
(
n
d/
2+
O
(1)
), that is

better th
a
n the divide-and-conquer algorithms of Sections 3.3.1 and 3.3.2 if

·

d
=
O
(
√
n
). The procedure for computing progress measures can be viewed as

a value iteration procedure that is approximating the least progress measure

from below.

Finally, in Section 3.3.4 we present a refinement of the dovetailing divide-

and-conquer scheme of Section 3.3.2 due to Schewe [2007]. Schewe's insight

is that the dovetailing divide-and-conquer technique can be successfully

Search Nedrilad ::

Custom Search