Tim Willemse: On Recursive Algorithms for Solving Parity Games


Event Details


Parity Games are infinite duration, two-player graph games. Such games play an important role in verification, satisfiability and synthesis. In recent years, several quasi-polynomial time algorithms for solving parity games have appeared. One of the more recent ones, by Pawel Parys, is based on the classical divide-and-conquer algorithm by McNaughton/Zielonka. In this talk, I will reiterate this classical algorithm and shed some light on the modifications that allow for achieving the quasi-polynomial runtime. While the big leap in runtime complexity is impressive, experiments indicate that the performance of this new algorithm sucks. This seems to be characteristic for all ‘improved’ algorithms.