Infinite-state energy games

DOI10.1145/2603088.2603100zbMATH Open1401.68139arXiv1405.0628OpenAlexW2059317879MaRDI QIDQ4635588FDOQ4635588

Piotr Hofman, Richard M. Mayr, Mohamed Faouzi Atig, Patrick Totzke, Parosh A. Abdulla, K. Narayan Kumar

Publication date: 23 April 2018

Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Abstract: Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata. Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

Full work available at URL: https://arxiv.org/abs/1405.0628

Recommendations

• Energy parity games
• Energy parity games
• Generalized mean-payoff and energy games
• Energy games in multiweighted automata
• Efficient Algorithms for Omega-Regular Energy Games

zbMATH Keywords

automata theoryenergy games

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 2-person games (91A05) Games involving graphs (91A43)

Cited In (9)

• Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
• Title not available (Why is that?)
• Long-Run Average Behavior of Vector Addition Systems with States
• Church synthesis on register automata over linearly ordered data domains
• Energy parity games
• Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time
• Bounding Average-Energy Games
• Title not available (Why is that?)
• Optimally Resilient Strategies in Pushdown Safety Games

This page was built for publication: Infinite-state energy games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635588)