Email Gateway (Jun 17 2025 at 19:47): Email Gateway (Jun 17 2025 at 19:47):From: Tobias Nipkow <nipkow@in.tum.de>
Galois Energy Games
Caroline Lemke
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 upward-closed domains
and can be “undone” through Galois-connected functions. Offering a simple
framework to construct decidable energy games we introduce the class of Galois
energy games. We establish decidability of the (un)known initial credit problem
for Galois energy games assuming energy-positional determinacy. For this we show
correctness and termination of a simple algorihm relying on an inductive
characterization of winning budgets and properties of Galois connections.
Further, we prove that energy games over vectors of (extended) naturals with
vector-adition and min-updates form a subclass of Galois energy games and are
thus decidable.
https://www.isa-afp.org/entries/Galois_Energy_Games.html
Enjoy this astounding entry: it formalizes "Galois energy games", a new and
(afaiu) yet unpublished new theory that one could say is the one game to rule
them all. The formalization (of almost 10000 lines!) draws on a number of other
AFP entries, even making use of the obscure function "those". Amazing!
Last updated: Jun 20 2025 at 16:26 UTC