Partial Solvers for Generalized Parity Games

Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, it has been shown that partial solvers for parity games that execute in polynomial time, while incomplete, can solve most games in publicly available benchmark suites. We combine those partial solvers with the classical Zielonka algorithm to obtain an algorithm that is efficient in practice and complete. We also show how to extend partial solvers to generalized parity games which are games with conjunction of parity objectives or disjunction of parity objectives. We also show how to combine those partial solvers with a generalization of the Zielonka algorithm for generalized parity games. We have implemented those algorithms and evaluated them on a large set of benchmarks. This is an ongoing joint work with Véronique Bruyère, Guillermo A. Perez and Jean-François Raskin.

Authors

• Clément Tamines.

Keywords

No keywords are indexed for this paper.