Fast value iteration: A uniform approach to efficient algorithms for energy games

TL;DR

This paper introduces a unified framework called Fast value iteration for analyzing and improving algorithms solving energy, parity, and mean-payoff games, leading to more efficient practical algorithms and new symmetric variants.

Contribution

The paper presents a systematic framework unifying and simplifying existing algorithms for energy and related games, and introduces novel symmetric algorithms with practical efficiency.

Findings

New symmetric algorithms are highly efficient in practice.

Fast value iteration algorithms are competitive with top parity game solvers.

The framework simplifies correctness proofs and comparisons of algorithms.

Abstract

We study algorithms for solving parity, mean-payoff and energy games. We propose a systematic framework, which we call Fast value iteration, for describing, comparing, and proving correctness of such algorithms. The approach is based on potential reductions, as introduced by Gurvich, Karzanov and Khachiyan (1988). This framework allows us to provide simple presentations and correctness proofs of known algorithms, unifying the Optimal strategy improvement algorithm by Schewe (2008) and the quasi dominions approach by Benerecetti et al. (2020), amongst others. The new approach also leads to novel symmetric versions of these algorithms, highly efficient in practice, but for which we are unable to prove termination. We report on empirical evaluation, comparing the different fast value iteration algorithms, and showing that they are competitive even to top parity game solvers.