Parity games are infinite two-player path-forming games, played on finite graphs. Fun as that sounds, they are more than just a way to idle away long winter evenings: they turn out to be a way of modeling all sorts of verification problems.
The exact complexity of solving parity games has been an open question for over 25 years. A breakthrough occurred in 2017, when two independent quasi-polynomial algorithms were published. I proposed a third independent approach, based on the tight connection between the modal $\mu$ calculus and parity games, providing descriptive-complexity perspective on the issue. This work was published at LICS 2018 and a journal verion is in the works.
Recently, I’ve also looked at the other quasi-polynomial algorithms (see the automata page), including Paweł Parys' recursive algorithm. Parys’s idea is to turn Zielonka’s classic exponential-time algorithm into a quasi-polynomial one by using precision parameters that guarantee that most recursive calls are cheap. Parys shows that a single call with full precision is enough to guarantee the correctness of the algorithm. We propose a version of the algorithm with a simpler recursive structure that bring the complexity down by a quasi-polynomial factor. To tie this algorithm in with the conversation around universal trees, we observe that our algorithm’s call structure follows the shape of the universal tree implicit in Marcin Jurdziński and Ranko Lazić’s Succinct Progress Measure algorithm.
-
Register games. with U. Boker
-
A modal mu perspective on solving parity games in quasi-polynomial time. LICS'18
-
Improving the complexity of Parys' recursive algorithm with Sven Schewe and Dominik Wojtczak