Algorithms for solving parity games

Marcin Jurdzinski (University of Warwick).

Course Summary | About the lecturer | Location and schedule | Materials | Assignment

Course summary:

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.

About the lecturer:

Marcin Jurdzinski is an Associate Professor of Computer Science at the University of Warwick, UK. He has obtained his MSc and PhD in Computer Science from the Univeristy of Warsaw, Poland, and from the University of Aarhus, Denmark, respectively. Before settling down at Warwick, he has worked as a postdoctoral researcher at the University of California, Berkeley, USA and at Université Paris 7, France. His research interests span a range of topics in theoretical computer science from logic and automata to algorithmic game theory. His work includes undecidability results for models of concurrency, computational complexity results for infinite-state systems, and efficient algorithms for computing approximate Nash equilibria, but his most persistent line of research, spanning his whole career, is the work on computational complexity and algorithms for solving parity games and other related games on graphs.

Location and schedule:

MIMUW building, room 3180.

Thursday, March 15
14:15 - 15:45 lecture
15:45 - 16:00coffee and cake
16:00 - 17:00 class
Friday, March 16
14:15 - 15:45 lecture
15:45 - 16:00 coffee and cake
16:00 - 17:00 class
Saturday, March 17
10:15 - 11:30 lecture
11:30 - 11:45 coffee and cake
11:45 - 13:00 class


Assignment: problem set. Please submit the solutions at the address by June 25.