Below the Branches of Universal Trees

Solving parity games is an intriguing problem that combines practical relevance with a long standing academic challenge. Its practical relevance is drawn from its prime position as the most difficult and most expensive step in automatically constructing (synthesis) and proving the correctness (model checking) of safety critical systems. It has further applications in the evaluation of nested fixed points and tropical algebra.

It is academically intriguing, because the complexity of solving parity games is a long standing challenge. The theoretical understanding of the computational complexity of solving parity games is a coveted prize since the algorithmic challenge of solving parity games efficiently first arose as a fundamental and impactful open problem posed in the early 1990s. For example, the existence of a polynomial-time algorithm has been recently listed as one of the six most important open problems in the Automata Column of the ACM SIGLOG News.

This high-risk project will attempt to show that solving parity games is computationally cheap.

Attempting this challenge is bold (as it should be for a New Horizons project), but it is also timely: while five years ago all algorithms were exponential, a number of different approaches that are merely quasi-polynomial have recently been established. This makes the attempt to tear down the last barrier to polynomial time, and thus to efficient algorithms, is within reach for the first time.

While the project is driven by scientific curiosity, it also feeds the conveyor belt of achieving higher technology readiness levels in follow-up research: once tractable algorithms are established in principle, highly efficient algorithms follow in due course, and they will help creating faster model checking and synthesis tools, and ultimately contributing to safer and better software.