Solving Parity Games in Practice

Parity games are 2-player games of perfect information and infinite duration that have important applications in automata theory and decision procedures (validity as well as model checking) for temporal logics. In this paper we investigate practical aspects of solving parity games. The main contribution is a suggestion on how to solve parity games efficiently in practice: we present a generic solver that intertwines optimisations with any of the existing parity game algorithms which is only called on parts of a game that cannot be solved faster by simpler methods. This approach is evaluated empirically on a series of benchmarking games from the aforementioned application domains, showing that using this approach vastly speeds up the solving process. As a side-effect we obtain the surprising observation that Zielonka's recursive algorithm is the best parity game solver in practice.