The PGSolver collection of parity game solvers. 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.

References in zbMATH (referenced in 13 articles , 1 standard article )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Dittmann, Christoph; Kreutzer, Stephan; Tomescu, Alexandru I.: Graph operations on parity games and polynomial-time algorithms (2016)
  2. Huth, Michael; Kuo, Jim Huan-Pu; Piterman, Nir: The Rabin index of parity games: its complexity and approximation (2015)
  3. Schewe, Sven; Trivedi, Ashutosh; Varghese, Thomas: Symmetric strategy improvement (2015)
  4. Chebotarev, A.N.: Using the compatibility analysis of logical specifications of automata to solve game problems (2014)
  5. Friedmann, Oliver; Lange, Martin; Latte, Markus: Satisfiability games for branching-time logics (2013)
  6. Hoffmann, Philipp; Luttenberger, Michael: Solving parity games on the GPU (2013)
  7. Friedmann, Oliver; Lange, Martin: Two local strategy iteration schemes for parity game solving (2012)
  8. Doyen, Laurent; Raskin, Jean-François: Games with imperfect information: theory and algorithms (2011)
  9. Friedmann, Oliver: An exponential lower bound for the latest deterministic strategy iteration algorithms (2011)
  10. Friedmann, Oliver: Recursive algorithm for parity games requires exponential time (2011)
  11. Ploeger, B.; Wesselink, J.W.; Willemse, T.A.C.: Verification of reactive systems via instantiation of parameterised Boolean equation systems (2011)
  12. Friedmann, Oliver: The Stevens-Stirling-algorithm for solving parity games locally requires exponential time (2010)
  13. Friedmann, Oliver; Lange, Martin: Solving parity games in practice (2009)