Infinite-State Energy Games

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 a generalization of energy games by replacing the finite game graph with an infinite game graph derived from a pushdown automaton (modelling recursion) or its subclass of a one-counter machine.

Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter machine and the energy is one-dimensional. On the other hand, every generalized energy game is undecidable: Energy games on one-counter machines 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.