Séminaire Logique et Interactions

24 octobre 2019, 11:00 : Séminaire

Karoliina Lehtinen (University of Liverpool), Quasi-polynomial techniques for parity games and and other problems

Parity games are central to the verification and synthesis of reactive systems: various model-checking, realisability and synthesis problems reduce to solving these games. Solving parity games -- that is, deciding which player has a winning strategy -- is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years.

In 2017 a major breakthrough occurred: parity games are solvable in quasi-polynomial time. Since then, several seemingly very distinct quasi-polynomial algorithms have been published, and some of these ideas have been used to solve other automata-theoretic problems.

In this talk, I will give an overview of these developments and the state-of-the art, with a slight automata-theoretic bias.

Bibliography: Roughly, this talk is based on developments presented in the following papers, by myself and others:

• Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. W. Czerwiński, L. Daviaud, N. Fijalkow, M. Jurdziński, R. Lazić, P. Parys. SODA 2019
• Improving the complexity of Parys’ recursive algorithm. K. Lehtinen, S. Schewe and D. Wojtczak. Unpublished.
• Parity Games: Zielonka's Algorithm in Quasi-polynomial Time. P. Parys. MFCS 2019.
• Alternating weak automata from universal trees. L. Daviaud, M. Jurdziński and K. Lehtinen CONCUR 2019
• On the way to alternating weak automata. U. Boker and K. Lehtinen. FSTTCS 2018.
• A modal μ perspective on solving parity games in quasi-polynomial time. K. Lehtinen. LICS 2018
• Succinct progress measures for solving parity games. M. Jurdziński and R. Lazić. LICS 2017.
• Deciding Parity Games in Quasipolynomial Time. C. Calude, S. Jain, B. Khoussainov, W. Li and F. Stephan. STOC 2017.