Skip to main content

Universal trees grow inside separating automata: Quasi-polynomial bounds for parity games

Marcin Jurdzinski

Several distinct techniques have been proposed to solve parity games in quasi-polynomial time since the breakthrough result of Calude, Jain, Khoussainov, Li, and Stephan (2017): play summaries, progress measures, and register games. We argue that all those techniques can be viewed as instances of the separation approach to solving parity games---a key component of which is constructing an automaton that separates languages of words encoding plays that are decisively won by either of the two players---thus establishing a single model that unifies the recent approaches to solving parity games efficiently.

Our main technical results are the nearly matching quasi-polynomial upper and lower bounds on the sizes of all separating automata.  In particular, the lower bound forms a barrier that the existing approaches must overcome in the ongoing quest for a polynomial-time algorithm for solving parity games.

We obtain our main results by introducing and studying universal ordered trees, a concept that may be of independent interest.  Firstly, we establish the nearly matching quasi-polynomial upper and lower bounds on the sizes of smallest universal trees.  Then we prove that the sizes of the smallest separating automata and of the smallest universal trees coincide---and hence both are quasi-polynomial---by showing how to turn universal trees into separating automata, and that there is a universal tree hiding in the states of every separating automaton.

The talk is based on joint work with Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Ranko Lazić, and Paweł Parys. 

Share this: