Abstract

Parity games are infinite two-player games, which are used in verification, automata theory, and reactive synthesis. 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. Last year, a major breakthrough occurred: parity games are solvable in quasi-polynomial time.

From an automata-perspective, solving parity games can be done by transforming alternating parity word automata into alternating weak automata. From a logician’s perspective, solving parity games can be done by finding a mu-calculus formula that recognises the winning region of a player in the parity game. Then, the size blow-up of the automaton in the first case, and the complexity of the formula in the second case, determine the complexity of the consequent algorithm for solving parity games.

In this talk, I present a quasi-polynomial solution for all three problems, based on playing parameterised games on parity-game arenas.

This talk is based on “A modal mu perspective on solving parity games in quasi-polynomial time”, presented at LICS ’18 and subsequent work with Udi Boker on weak automata.