Solving Parity Games in Practice

8 years 11 months ago
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.
Oliver Friedmann, Martin Lange
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ATVA
Authors Oliver Friedmann, Martin Lange
Comments (0)