Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Michaël Cadilhac, Antonio Casares, Pierre Ohlmann

TL;DR

The paper addresses solving energy and mean-payoff games (and related parity games) by introducing a unified Fast value iteration framework based on potential reductions. It formalizes a meta-algorithm that, via sound and complete potential assigners, guarantees termination and exact recovery of energy values, while providing a platform that subsumes and simplifies existing approaches such as OSI, GKK, and QDPM. It also explores symmetric, alternating variants and a dynamic extension to improve practical performance, and backs these theoretical insights with comprehensive empirical evaluations showing competitive robustness across benchmarks. The work advances both the theoretical understanding and practical toolbox for solving large-scale energy/mean-payoff games, with implications for synthesis and verification tasks where such games arise.

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.

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

TL;DR

The paper addresses solving energy and mean-payoff games (and related parity games) by introducing a unified Fast value iteration framework based on potential reductions. It formalizes a meta-algorithm that, via sound and complete potential assigners, guarantees termination and exact recovery of energy values, while providing a platform that subsumes and simplifies existing approaches such as OSI, GKK, and QDPM. It also explores symmetric, alternating variants and a dynamic extension to improve practical performance, and backs these theoretical insights with comprehensive empirical evaluations showing competitive robustness across benchmarks. The work advances both the theoretical understanding and practical toolbox for solving large-scale energy/mean-payoff games, with implications for synthesis and verification tasks where such games arise.

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.

Paper Structure

This paper contains 12 sections, 4 theorems, 4 equations, 2 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Mean-payoff and energy games.
  3. Algorithmic paradigms.
  4. (1) Fast value iteration framework.
  5. (2) Unifying and simplifying existing algorithms.
  6. (3) Empirical evaluation.
  7. Preliminaries
  8. Attractors.
  9. Simple games.
  10. Fast value iteration: A meta-algorithm based on potential reductions
  11. Potential reductions
  12. The fast value iteration meta-algorithm

Key Result

theorem thmcountertheorem

For each $\mathrm{val} \in \{\MP,\En,\Enp\}$, there exist strategies $\sigma_0$ for Min and $\tau_0$ for Max such that for all $v \in V$ we have where $\sigma, \tau$ and $\pi$ respectively range over strategies for Min, strategies for Max, and infinite paths from $v$.

Figures (2)

  • Figure 1: Example of a game; circles belong to Min and squares belong to Max. From left to right, the mean-payoff values are $-2,-2,-\frac{1}{2}, - \frac{1}{2},1$ and $1$, and positional strategies for mean-payoff values are identified in bold. Energy values are $0,2,9,0,\infty$ and $\infty$, and with optimal strategies given by the double-headed arrows.
  • Figure 2: The three valuations over a given sequence of weights. The mean-payoff value is given by the slope of the line, which corresponds to the long-term average. In this case, the mean-payoff is $\leq 0$, and both $\En$ and $\Enp$ are finite.

Theorems & Definitions (5)

  • theorem thmcountertheorem: EM79BFLMS08
  • corollary thmcountercorollary: BCDGR11
  • lemma thmcounterlemma
  • theorem thmcountertheorem
  • remark thmcounterremark