Solving Parity Games via Priority Promotion Techniques

We consider parity games, a special form of two-player infinite-duration games on numerically labelled graphs, whose winning condition requires that the maximal value of a label, called priority, occurring infinitely often during a play be of some specific parity. The problem has a rather intriguing status from a complexity theoretic viewpoint, since it belongs to the class UPTime ∩ Co-UPTime and still open is the question whether it can be solved in polynomial time. Parity games also have great practical interest, as they arise in many fields of theoretical computer science, most notably logic, automata theory, and formal verification and synthesis.

In this paper, we propose a new family of algorithms, based on the idea of promoting vertices to higher priorities during the search for winning regions. The proposed techniques differ on the promotion strategy employed. The resulting family has nice computational properties, exhibiting the best space complexity among the currently known solutions to the problem. Experimental results on both random games and benchmark families show that the approach is also very effective in practice.