Document Open Access Logo

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

Authors Caroline Lemke , Benjamin Bisping

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.29.pdf
  • Filesize: 1.49 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Energy games
  • Galois connection
  • Reachability
  • Game theory
  • Decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2025.29

Author Details

Caroline Lemke
  • Department of Computing Science, Carl von Ossietzky Universität Oldenburg, Germany
Benjamin Bisping
  • Institute of Software Engineering and Theoretical Computer Science, Technische Universität Berlin, Germany

Acknowledgements

We want to thank Gabriel Vogel for the WebGPU prototype implementation and Uli Fahrenberg, Lukas Panneke and the anonymous reviewers for their valuable feedback.

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Ahmed Bouajjani, and Julien d’Orso. Deciding monotonic games. In Computer Science Logic (CSL), volume 2803 of Lecture Notes in Computer Science, pages 1-14. Springer Berlin Heidelberg, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_1.
  2. Parosh Aziz Abdulla, Richard Mayr, Arnaud Sangnier, and Jeremy Sproston. Solving parity games on integer vectors. In Concurrency Theory (CONCUR), volume 8052 of Lecture Notes in Computer Science, pages 106-120. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_9.
  3. Benjamin Bisping. Process equivalence problems as energy games. In Computer Aided Verification (CAV), volume 13964 of Lecture Notes in Computer Science, pages 85-106. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-37706-8_5.
  4. Benjamin Bisping. Generalized Equivalence Checking of Concurrent Programs. PhD thesis, Technische Universität Berlin, 2025. URL: https://generalized-equivalence-checking.equiv.io/.
  5. Benjamin Bisping and David N. Jansen. One energy game for the spectrum between branching bisimilarity and weak trace semantics. In Georgiana Caltais and Cinzia Di Giusto, editors, Proceedings Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics, Calgary, Canada, 9th September 2024, volume 412, pages 71-88. Open Publishing Association, 2024. URL: https://doi.org/10.4204/EPTCS.412.6.
  6. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. Journal of the ACM, 68(5):32-43, 2021. URL: https://doi.org/10.1145/3464794.
  7. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G Larsen, and Simon Laursen. Average-energy games. Acta Informatica, 55:91-127, 2018. URL: https://doi.org/10.1007/s00236-016-0274-1.
  8. Thomas Brihaye and Aline Goeminne. Multi-weighted reachability games. In Reachability Problems, volume 14235 of Lecture Notes in Computer Science, pages 85-97. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-45286-4_7.
  9. Thomas Brihaye, Aline Goeminne, James C. A. Main, and Mickael Randour. Reachability games and friends: A journey through the lens of memory and complexity. In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 284 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1-1:26, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2023.1.
  10. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 505-516, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505.
  11. Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. In Concurrency Theory (CONCUR), volume 7454 of Lecture Notes in Computer Science, pages 115-131. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_10.
  12. Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, and Łukasz Orlikowski. Reachability in 3-vass is elementary. arXiv preprint arXiv:2502.13916, 2025. URL: https://doi.org/10.48550/arXiv.2502.13916.
  13. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pages 1229-1240, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  14. Marcel Erné, Jürgen Koslowski, Austin Melton, and George E. Strecker. A primer on galois connections. Annals of the New York Academy of Sciences, 704(1):103-125, 1993. URL: https://doi.org/10.1111/j.1749-6632.1993.tb52513.x.
  15. Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jiří Srba. Energy games in multiweighted automata. In Antonio Cerone and Pekka Pihlajasaari, editors, Theoretical Aspects of Computing (ICTAC), pages 95-115. Springer Berlin Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-23283-1_9.
  16. Line Juhl, Kim Guldstrand Larsen, and Jean-François Raskin. Optimal Bounds for Multiweighted and Parametrised Energy Games, pages 244-255. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-39698-4_15.
  17. Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in vass revisited: Improving rackoff’s bound to obtain conditional optimality. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 131:1-131:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.131.
  18. Orna Kupferman and Naama Shamash Halevy. Energy games with resource-bounded environments. In Concurrency Theory (CONCUR), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1-19:23, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.19.
  19. Caroline Lemke. crmrtz/galois-energy-games - A formal proof of decidability of multi-weighted declining energy games. Master’s thesis, Technische Universität Berlin, 2024. Collection (visited on 2025-08-05). URL: https://github.com/crmrtz/galois-energy-games
    full metadata available at: https://doi.org/10.4230/artifacts.24329
  20. Caroline Lemke. Galois energy games. Archive of Formal Proofs, 2025. Formal proof development. URL: https://isa-afp.org/entries/Galois_Energy_Games.html.
  21. Caroline Lemke and Benjamin Bisping. Galois energy games: To solve all kinds of quantitative reachability problems, 2025. URL: https://doi.org/10.48550/arXiv.2505.14691.
  22. Mehryar Mohri. Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics, 7(3):321-350, 2002. URL: https://doi.org/10.25596/jalc-2002-321.
  23. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  24. Sven Schewe, Alexander Weinert, and Martin Zimmermann. Parity games with weights. Logical Methods in Computer Science, 15, 2019. URL: https://doi.org/10.23638/LMCS-15(3:20)2019.
  25. Joseph E Stoy. Denotational semantics : the Scott-Strachey approach to programming language theory. The MIT Press series in computer science. The MIT Press, 3. print edition, 1981. Google Scholar
  26. Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In Jos C. M. Baeten and Jan Willem Klop, editors, Theories of Concurrency: Unification and Extension (CONCUR), volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer Berlin Heidelberg, 1990. URL: https://doi.org/10.1007/BFb0039066.
  27. Gabriel Vogel. Accelerating process equivalence energy games using WebGPU. Bachelor’s thesis, Technische Universität Berlin, 2024. URL: https://github.com/Gobbel2000/gpuequiv.
  28. Akihisa Yamada and Jérémy Dubut. Complete non-orders and fixed points. Archive of Formal Proofs, 2019. URL: https://www.isa-afp.org/entries/Complete_Non_Orders.html.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact