Partial Solvers for Parity Games: Effective Polynomial-Time Composition

Patrick Ah-Fat
(Imperial College London)
Michael Huth
(Imperial College London)

Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve *all* standard benchmarks of structured games. For one of these polynomial-time partial solvers not even a sole random game from a few billion random games of varying configuration was found that it won't solve completely.

In Domenico Cantone and Giorgio Delzanno: Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Catania, Italy, 14-16 September 2016, Electronic Proceedings in Theoretical Computer Science 226, pp. 1–15.
Published: 13th September 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.226.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org