Reachability Games and Parity Games

TL;DR

This paper provides detailed proofs of classical and recent results on parity games, including their positional determinacy and quasi-polynomial time algorithms for solving finite parity games, with some new insights and simplifications.

Contribution

It offers a self-contained presentation of key results on parity games, including proofs of positional determinacy and quasi-polynomial algorithms, with some novel proofs and simplifications.

Findings

Parity games are positionally determined.

Finite parity games can be solved in quasi-polynomial time.

The paper includes simplified proofs and definitions related to reachability and attractor computations.

Abstract

Parity games are positionally determined. This is a fundamental and classical result. In 2010, Calude et al. showed a breakthrough result for finite parity games: the winning regions and their positional winning strategies can be computed in quasi-polynomial time. In the present paper we give a self-contained and detailed proofs for both results. The results in this paper are not meant to be original. The positional determinacy result is shown for possibly infinite parity games using the ideas of Zielonka which he published in 1998. In order to show quasi-polynomial time, we follow Lehtinen's register games, which she introduced in 2018. Although the time complexity of Lehtinen's algorithm is not optimal, register games are conceptually simple and interesting in their own right. Various of our proofs are either new or simplifications of the original proofs. The topics in this paper include the definition and the computation of optimal attractors for reachability games, too.