Algorithms for solving parity games

Parity games have played a fundamental role in automata theory, logic, and their applications to verification and synthesis since early 1990's. Solving parity games is polynomial-time equivalent to checking emptiness of tree automata and to the modal mu-calculus model checking. It is a long-standing open question whether there is a polynomial-time algorithm for solving parity games. The quest for a polynomial-time algorithm has not only brought diverse algorithmic techniques to the theory and practice of verification and synthesis, but it has also significantly contributed to resolving long-standing open problems in other research areas, such as Markov Decision Processes and Linear Programming.

In the first part of this course, I will survey some of the algorithmic techniques that have been developed for solving parity games until 2016, such as recursive divide-and-conquer algorithms, progress measures, strategy improvement, and dynamic algorithms. In the second part, I will present new algorithmic techniques that have sprung after the first quasi-polynomial-time algorithm for solving parity games was developed by Calude et al. in 2017. In the final part, I will discuss how parity games are related to other games on graphs, such as mean-payoff games, discounted games, and simple stochastic games; mention algorithmic problems that share similar complexity-theoretic status inside TFNP (Total Function NP), such as computing Banach fixpoints and the P-matrix Linear Complementarity Problem; and speculate on other algorithmic techniques that could be explored in the context of solving games on graphs.

More info (including schedule) can be found here.