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

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.