Algorithms for solving parity games
Marcin Jurdzinski
(University of Warwick).
Course Summary 
About the lecturer 
Location and schedule 
Materials

Assignment
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 polynomialtime equivalent to checking emptiness of tree automata and to the modal mucalculus model checking. It is a longstanding open question whether there is a polynomialtime algorithm for solving parity games. The quest for a polynomialtime 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 longstanding 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 divideandconquer algorithms, progress measures, strategy improvement, and dynamic algorithms. In the second part, I will present new algorithmic techniques that have sprung after the first quasipolynomialtime 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 meanpayoff games, discounted games, and simple stochastic games; mention algorithmic problems that share similar complexitytheoretic status inside TFNP (Total Function NP), such as computing Banach fixpoints and the Pmatrix 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 infinitestate 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.



Materials
Assignment: problem set. Please submit the solutions at the address parys@mimuw.edu.pl by June 25.