2016/09/13 by Patrick Ah-Fat, Michael Huth
Computer Science · Mathematics · #Advanced Database Systems and Queries #Algorithm #Composition (language) #Computability #Computer science #Formal Methods in Verification #Logic, programming, and type systems #Mathematics #Merge (version control) #Parallel computing #Parity (physics) #Polynomial #Theoretical computer science #Time complexity #cs.LO
paper · pdf · doi:10.4204/eptcs.226.1
published as EPTCS 226, 2016, pp. 1-15 · In Proceedings GandALF 2016, arXiv:1609.03648
openalex publication_date 2016/09/13 · arxiv created 2016/09/14 · arxiv updated 2016/09/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.