The Theory of Universal Graphs for Infinite Duration Games

TL;DR

This paper develops the theory of universal graphs to design efficient algorithms for solving various infinite duration games, including parity and mean payoff games, with improved complexity results.

Contribution

It introduces the theory of universal graphs, establishes equivalence and normalization results, and provides generic algorithms for multiple game objectives.

Findings

Algorithms matching or surpassing best known complexity for parity games.

Algorithms matching or surpassing best known complexity for mean payoff games.

Effective solutions for combined objectives involving disjunctions.

Abstract

We introduce the notion of universal graphs as a tool for constructing algorithms solving games of infinite duration such as parity games and mean payoff games. In the first part we develop the theory of universal graphs, with two goals: showing an equivalence and normalisation result between different recently introduced related models, and constructing generic value iteration algorithms for any positionally determined objective. In the second part we give four applications: to parity games, to mean payoff games, to a disjunction between a parity and a mean payoff objective, and to disjunctions of several mean payoff objectives. For each of these four cases we construct algorithms achieving or improving over the best known time and space complexity.