Solving Parity Games via Priority Promotion

The main contribution of the paper is a new family of algorithms for solving parity games, based on the notions of region and priority promotion. A region R for a given player is a set of vertices from each of which the player can enforce a winning play that never leaves the region, unless either the opponent can escape from R or the only choice for player itself is to exit from R (i. e. no edge from a vertex of remains in R). Therefore, a region is essentially a weaker form of winning region. Regions can be ordered by assigning to each of them a priority corresponding to the "best" priority the opponent can obtain along a play exiting from that region. An important property of regions is that, under suitable and easy to check assumptions, a higher priority region R1 and a lower priority region R2, with priorities p1 and p2, respectively, of the same parity, can be merged into a single region of the higher priority p1. We call this merging operation a priority promotion for R2. The underlying idea of the approach is then to iteratively enlarge regions by performing suitable sequences of promotions, until a closed -region, namely a region where player can force the game to remain, is obtained. When that happens, a winning region for has been found. Experimental results, comparing the new algorithms with the state of the art solvers, also show that all three algorithms perform very well in practice, most often significantly better than existing ones, on both random games and benchmark families proposed in the literature.

Authors

• Massimo Benerecetti

Keywords

No keywords are indexed for this paper.