An Optimal Value Iteration Algorithm for Parity Games

TL;DR

This paper analyzes and generalizes algorithms for solving parity games using universal trees, showing the quasipolynomial size of these trees and suggesting the current algorithms are optimal within this framework.

Contribution

It introduces a generic value iteration algorithm based on universal trees and proves the minimal size of such trees, indicating the optimality of existing quasipolynomial algorithms.

Findings

Universal trees lead to a generic value iteration algorithm.

Both small and succinct progress measure algorithms are special cases.

Universal trees have at least quasipolynomial size, indicating optimality of current algorithms.

Abstract

The quest for a polynomial time algorithm for solving parity games gained momentum in 2017 when two different quasipolynomial time algorithms were constructed. In this paper, we further analyse the second algorithm due to Jurdzi\'nski and Lazi\'c and called the succinct progress measure algorithm. It was presented as an improvement over a previous algorithm called the small progress measure algorithm, using a better data structure. The starting point of this paper is the observation that the underlying data structure for both progress measure algorithms are (subgraph-)universal trees. We show that in fact any universal tree gives rise to a value iteration algorithm \`a la succinct progress measure, and the complexity of the algorithm is proportional to the size of the chosen universal tree. We then show that both algorithms are instances of this generic algorithm for two constructions of universal trees, the first of exponential size (for small progress measure) and the second of quasipolynomial size (for succinct progress measure). The technical result of this paper is to show that the latter construction is asymptotically tight: universal trees have at least quasipolynomial size. This suggests that the succinct progress measure algorithm of Jurdzi\'nski and Lazi\'c is in this framework optimal, and that the polynomial time algorithm for parity games is hiding someplace else.