DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.29

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

Authors: Caroline Lemke and Benjamin Bisping

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

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 the instantiations, our simple algorithm is polynomial w.r.t. game graph size and exponential w.r.t. dimension.

Cite as

Caroline Lemke and Benjamin Bisping. Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lemke_et_al:LIPIcs.CONCUR.2025.29,
  author =	{Lemke, Caroline and Bisping, Benjamin},
  title =	{{Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.29},
  URN =		{urn:nbn:de:0030-drops-239795},
  doi =		{10.4230/LIPIcs.CONCUR.2025.29},
  annote =	{Keywords: Energy games, Galois connection, Reachability, Game theory, Decidability}
}

Search Results

Documents authored by Bisping, Benjamin

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

Abstract

Cite as

Thanks for your feedback!

Could not send message