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