Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems
Caroline Lemke, Benjamin Bisping
TL;DR
This work introduces Galois energy games, a generic framework where energies reside in a well-founded bounded join-semilattice and updates admit a Galois inversion, enabling a fixed-point decision procedure for attacker winning budgets. It unifies and extends existing energy-game models (including vector-addition, declining updates, and multi-weighted reachability) and provides a formal Isabelle/HOL proof of decidability along with two concrete implementations. The core result is a polynomial-time algorithm in the game graph size and exponential in the dimension, making it practical for higher-dimensional quantitative problems like VASS coverability and shortest-path variants. The approach is demonstrated through multiple instantiations, formal verification, and GPU-accelerated implementations, highlighting its applicability to automatic reasoning, synthesis, and verification in systems with interacting resources.
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.