Solving Parity Games in Practice

EPFL IC Tresor talks

by Martin Lange The unsettled question of the exact complexity of solving parity games has led to the invention of several (quite different) algorithms for this problem. They are often compared w.r.t. the analytical terms describing their worst-case runtime behaviour. This is of course hardly meaningful for practical purposes: solving parity games is for example a crucial ingredient of decision procedures for branching time temporal logics. In this talk I will give a brief introduction to the theory of parity games, present existing algorithms and try to answer the question “which one is the best in practice?” I will present the PGSolver library - a collection of algorithms and heuristics for solving parity games - present the “meta”-algorithm of this library that incorporates several optimisations useful for all other algorithms, report on experiments, etc. This is joint work with Oliver Friedmann.