Energy Games with Resource-Bounded Environments
An energy game is played between two players, modeling a resource-bounded system and its environment. The players take turns moving a token along a finite graph. Each edge of the graph is labeled by an integer, describing an update to the energy level of the system that occurs whenever the edge is traversed. The system wins the game if it never runs out of energy. Different applications have led to extensions of the above basic setting. For example, addressing a combination of the energy requirement with behavioral specifications, researchers have studied richer winning conditions, and addressing systems with several bounded resources, researchers have studied games with multi-dimensional energy updates. All extensions, however, assume that the environment has no bounded resources.
We introduce and study both-bounded energy games (BBEGs), in which both the system and the environment have multi-dimensional energy bounds. In BBEGs, each edge in the game graph is labeled by two integer vectors, describing updates to the multi-dimensional energy levels of the system and the environment. A system wins a BBEG if it never runs out of energy or if its environment runs out of energy. We show that BBEGs are determined, and that the problem of determining the winner in a given BBEG is decidable iff both the system and the environment have energy vectors of dimension 1. We also study how restrictions on the memory of the system and/or the environment as well as upper bounds on their energy levels influence the winner and the complexity of the problem.
Energy Games
Infinite-State Systems
Decidability
Theory of computation
19:1-19:23
Regular Paper
Supported by the Israel Science Foundation, grant No. 2357/19.
https://www.cs.huji.ac.il/~ornak/publications/concur22.pdf
Orna
Kupferman
Orna Kupferman
School of Computer Science and Engineering, Hebrew University of Jerusalem, Israel
Naama
Shamash Halevy
Naama Shamash Halevy
School of Computer Science and Engineering, Hebrew University of Jerusalem, Israel
10.4230/LIPIcs.CONCUR.2022.19
P.A. Abdulla, M.F. Atig, P. Hofman, R. Mayr, K.N. Kumar, and P. Totzke. Infinite-state energy games. In Proc. 29th IEEE Symp. on Logic in Computer Science, pages 7:1-7:10. ACM, 2014.
G. Amram, S. Maoz, O. Pistiner, and J. O. Ringert. Efficient algorithms for omega-regular energy games. In 24th International Symposium on Formal Methods, volume 13047 of Lecture Notes in Computer Science, pages 163-181. Springer, 2021.
R. Bloem, K. Chatterjee, and B. Jobstmann. Graph games and reactive synthesis. In Handbook of Model Checking., pages 921-962. Springer, 2018.
M. Blondin, A. Finkel, S. Göller, C. Haase, and P. McKenzie. Reachability in two-dimensional vector addition systems with states is pspace-complete. In Proc. 30th IEEE Symp. on Logic in Computer Science, pages 32-43. IEEE, 2015.
A. Borodin and R. El-Yaniv. Online Computation and Competitive Analysis. Cambridge University Press, 1998.
P. Bouyer, U. Fahrenberg, K.G. Larsen, N. Markey, and J. Srba. Infinite runs in weighted timed automata with energy constraints. In 6th International Conference on Formal Modeling and Analysis of Timed Systems, volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer, 2008.
T. Brázdil, P. Jančar, and A. Kučera. Reachability games on extended vector addition systems with states. In Proc. 37th Int. Colloq. on Automata, Languages, and Programming, pages 478-489. Springer, 2010.
A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and M. Stoelinga. Resource interfaces. In International Workshop on Embedded Software, pages 117-133. Springer, 2003.
K. Chatterjee and L. Doyen. Energy parity games. Theoretical Computer Science, 458:49-60, 2012.
K. Chatterjee, L. Doyen, T.A. Henzinger, and J-F. Raskin. Generalized mean-payoff and energy games. In Proc. 30th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 8 of LIPIcs, pages 505-516. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010.
K. Chatterjee, A.K. Goharshady, and Y. Velner. Quantitative analysis of smart contracts. In 27th European Symposium on Programming Languages and Systems, volume 10801 of Lecture Notes in Computer Science, pages 739-767. Springer, 2018.
J-B. Courtois and S. Schmitz. Alternating vector addition systems with states. In 39th Int. Symp. on Mathematical Foundations of Computer Science, pages 220-231. Springer, 2014.
R. Ehlers. Symbolic bounded synthesis. In Proc. 22nd Int. Conf. on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 365-379. Springer, 2010.
E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. Workshop on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79-87. Springer, 1985.
U. Fahrenberg, L. Juhl, K. G. Larsen, and J. Srba. Energy games in multiweighted automata. In 8th International Colloquium on Theoretical Aspects of Computing, volume 6916 of Lecture Notes in Computer Science, pages 95-115. Springer, 2011.
L. Hélouët, N. Markey, and R. Raha. Reachability games with relaxed energy constraints. Information and Computation, page 104806, 2021.
T.A. Henzinger. From Boolean to quantitative notions of correctness. In Proc. 37th ACM Symp. on Principles of Programming Languages, pages 157-158, 2010.
J.E. Hopcroft and J-J. Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8:135-159, 1979.
M. Jurdzinski, R. Lazic, and S. Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In Proc. 42nd Int. Colloq. on Automata, Languages, and Programming, volume 9135 of Lecture Notes in Computer Science, pages 260-272. Springer, 2015.
M. Jurdziński, R. Lazić, and S. Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In Proc. 42nd Int. Colloq. on Automata, Languages, and Programming, pages 260-272. Springer, 2015.
O. Kupferman, Y. Lustig, M.Y. Vardi, and M. Yannakakis. Temporal synthesis for bounded systems and environments. In Proc. 28th Symp. on Theoretical Aspects of Computer Science, pages 615-626, 2011.
J. Leroux and S. Schmitz. Reachability in vector addition systems demystified. In Proc. 35th IEEE Symp. on Logic in Computer Science, 2015.
D.A. Martin. Borel determinacy. Annals of Mathematics, 65:363-371, 1975.
A. Menezes, P.C. van Oorschot, and S.A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996.
M.L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1 edition, 1967.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179-190, 1989.
S. Schewe and B. Finkbeiner. Bounded synthesis. In 5th Int. Symp. on Automated Technology for Verification and Analysis, volume 4762 of Lecture Notes in Computer Science, pages 474-488. Springer, 2007.
C. Wrathall. Complete sets and the polynomial-time hierarchy. Theoretical Computer Science, 3(1):23-33, 1976.
Orna Kupferman and Naama Shamash Halevy
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode