Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems

TL;DR

This paper introduces a unified decision procedure for a broad class of energy games, extending previous models to include well-founded bounded join-semilattices and Galois connections, with practical instantiations and efficient algorithms.

Contribution

It generalizes energy game frameworks using Galois connections and well-founded semilattices, enabling polynomial algorithms for complex reachability problems.

Findings

Algorithm is polynomial in game graph size.

Applicable to multiple energy game variants.

Formalized in Isabelle and implemented practically.

Abstract

We provide a generic decision procedure for energy games with energy-bounded attacker and reachability objective, moving beyond vector-valued energies and vector-addition updates. All we demand is that energies form well-founded bounded join-semilattices, and that energy updates have an upward-closed domain and can be "undone" through a Galois-connected function. We instantiate these Galois energy games to common energy games, declining energy games, multi-weighted reachability games, coverability on vector addition systems with states and shortest path problems, supported by an Isabelle-formalization and two implementations. For these instantiations, our simple algorithm is polynomial w.r.t. game graph size and exponential w.r.t. dimension.