We consider parity games, a special form of two-player in niteduration games on numerically labeled graphs, whose winning condition requires that the maximal value of a label occurring in nitely often during a play be of some speci c parity. We present a new family of algorithms for the solution of the problem, based on the idea of promoting vertices to higher priorities during the search for winning regions. The proposed approach has nice computational properties, exhibiting the best space complexity among the currently known solutions. Experimental results on both random games and benchmark families show that the technique is also very e ective in practice.
Parity games are perfect-information two-player turn-based games of in nite
duration, usually played on nite directed graphs. Their vertices, called positions,
are labeled by natural numbers, called priorities, and are assigned to one of two
players, named Even and Odd or, simply, 0 and 1, respectively. The game starts
at an arbitrary position and, during its evolution, players can take a move (an
outgoing edge) only at their own positions. The moves selected by the players
induce an in nite sequence of vertices, called play. If the maximal priority of the
vertices occurring in nitely often in the play is even, then the play is winning
for player 0, otherwise, player 1 takes it all. The importance of these games is
due to the numerous applications in automata theory and in the area of system
speci cation, veri cation, and synthesis, where it is used as algorithmic back-end
of satis ability and model-checking procedures for temporal logics automata
theory. In particular, it has been proved to be linear-time interreducible with
the model-checking problem for the modal Calculus [
This extended abstract presents the ideas underlying a new family of algorithms for solving parity games described in [2{4], based on the notions of quasi dominion and priority promotion. A quasi dominion Q for player 2 f0; 1g, called a quasi -dominion, is a set of vertices from each of which player can enforce a winning play that never leaves the region, unless one of the following two conditions holds: (i) the opponent can escape from Q or (ii) the only choice for player itself is to exit from Q. Quasi dominions of the same player can be merged together to form larger quasi -dominions until, eventually, a dominion for some player is found. The resulting technique, while still exhibiting exponential behaviors, only requires O(n log k) memory (with n and k the number of positions and priorities), which improves on the state-of-the-art. Experimental results show that the proposed approach performs very well in practice, most often signi cantly better than existing ones, as extensively shown in [1{4]. 2
For the sake of space, we refer to [
Priority promotion. The priority promotion approach attacks the problem of
solving a parity game a by computing one of its dominions D, for some player
, at a time. Indeed, once the -attractor D? of D is removed from a, the
smaller game a n D? is obtained, whose positions are winning for one player
i they are winning for the same player in the original game. This allows for
decomposing the problem of solving a parity game into iteratively nding its
dominions [
De nition 1 (Quasi Dominion [
If all induced plays remain in the set Q forever, then we have an -dominion, i.e., a subset of the -winning region. In this case, the escape set of Q is empty and we say that Q is -closed. Otherwise, we say that it is -open.
The priority promotion algorithm explores a partial order hS; i, whose elements, called states, record information about the open quasi dominions computed along the way. In the initial state > 2 S the quasi dominions are initialized to the sets of positions with the same priority. At each step, a new quasi dominion is extracted from the current state, by means of a query operator <, and used to compute a successor state, by means of a successor operator #, if the quasi dominion is open. If, on the other hand, it is closed, the search is over. The partial order hS; >; i together with the operators < and # form what is called a dominion space. The notion of dominion space is quite general and can be instantiated in di erent ways, by providing speci c query and successor operators (see [2{4]). The overall procedure is sound and complete on any dominion space and its time complexity is linear in the execution depth of the space, namely the length of the longest chain in the underlying partial order compatible with the successor operator. Its space complexity, instead, is only logarithmic in the size of the dominion-space, since only one state at the time needs to be maintained.
The priority promotion algorithm processes the input game in descending order of priority and, at each step, a subgame of the entire game, obtained by removing the quasi dominions previously computed at higher priorities, is considered. At each priority of parity : (i) a quasi -domain Q is extracted by the query operator from the current subgame; (ii) if Q is closed in the entire game, the search stops and returns Q as result; otherwise, (iii) a successor state in the underlying partial order is computed by the successor operator, depending on whether Q is open in the current subgame or not. In the rst case, the quasi -dominion is removed from the current subgame and the search restarts on the new subgame that can only contain positions with lower priorities. In the second case, Q is merged together with some previously computed quasi -dominion with higher priority. Being a dominion space well-ordered, the search is guaranteed to eventually terminate and return a closed quasi dominion. The procedure requires the solution of two crucial problems: (a) extracting a quasi dominion from a subgame and (b) merging together two quasi -dominions.
The solution of the rst problem relies on the de nition of a speci c class of
quasi dominions, called regions. An -region R of a game a is a quasi -dominion
of a all of whose escape positions have the maximal priority p , pr(a) 2 in a.
In this case, we say that the -region R has priority p. If player escapes from
-region R, it must visit a position with the highest priority in it and parity .
De nition 2 (Region [
It is important to observe that, in any parity game, an -region always exists, for some 2 f0; 1g. In particular, the set of positions of maximal priority in the game always forms an -region, with equal to the parity of that maximal priority. A closed -region in a game is clearly an -dominion in that game. In addition, the -attractor of an -region is always an -region. These observations give us an easy and e cient way to extract a quasi dominion from every subgame: collect the -attractor of the positions with maximal priority p in the subgame, where p 2 , and assign p as priority of the resulting region R. This priority, called measure of R, intuitively corresponds to an under-approximation of the best priority player can force the opponent to visit along any play exiting from R. During the search for a dominion, the computed regions, together with their current measure, are kept track of by means of an auxiliary priority function r : Ps ! Pr, called region function. Given a priority p, we denote by r( p) (resp., r(>p) and r(<p)) the function obtained by restricting the domain of r to the positions with measure greater than or equal to p (resp., greater than and lower than p). Moreover, the set of pairs (R; ), where R is an -region, is denoted by Rg, and is partitioned into the sets Rg and Rg+ of open and closed -region pairs, respectively.
Algorithm 1 provides the implementation for the query function com- signature <a : Sa ! 2Psa f0; 1g patible with the priority-promotion function <a(s) tmheecphaarniitsym. Lofintehe1psriimorpitlyy tcoo mprpoucteesss 21 let R(r; p)pa=tmrasosid(nr2 1(p)) in the state s , (r; p). Line 2, instead, computes the attractor w.r.t. player 3 return (R; )
in subgame as , a n dom r(>p) of
the region contained in r at the current priority p. The resulting set R is an
-region of as containing r 1(p) (see [
A solution to the second problem, the merging operation, is obtained as
follows. Given an -region R in some game a and an -dominion D in a subgame
of a that does not contain R itself, the two sets are merged together, if the only
moves exiting from -positions of D in the entire game lead to higher priority
-regions and R has the lowest priority among them. The priority of R is called
the best escape priority of D for . The correctness of this merging operation is
established in [
The merging operation is
implemented by promoting all the positions signature #a : a ! a Pra
of -dominion D to the measure of function s #a (R; )
R, thus improving the measure of D. let (r; p) = s in
iFtoyrptrhoims orteiaosno.nA,fitterisacaplrloemdoatiporniotro- 12 if (Rr?; ) r2[RR7 !gasp]then
some measure p, the regions with mea- 3 p? max(rng r?(<p) )
sure lower than p might need to be else
destroyed, by resetting all the con- 4 p? bepa(R; r)
tained positions to their original pri- 5 r? pra ] r( p?)[R 7! p?]
ority (see [
The result is a sound and complete solution procedure, as stated below. Theorem 1. The Priority Promotion algorithm is correct and solves a game with n 2 N positions and k 2 [1; n] priorities in O(n log k) space.