Infinite-state Games with Energy Objectives Beyond Counters
Irmak Sa\u{g}lam, Georg Zetzsche

TL;DR
This paper explores viability games on infinite-state systems, revealing decidability results for complex combinations of pushdowns and counters under energy-like semantics.
Contribution
It introduces viability games with energy semantics on valence systems over graph monoids and characterizes their decidability and complexity landscape.
Findings
Decidability of viability games varies across different system combinations.
Viability games are decidable even when control-state reachability is undecidable.
Certain pushdown and counter combinations admit decidable viability games.
Abstract
In the theory of games on infinite-state arenas, there is a stark contrast between (i) recursion-based models such as pushdown systems and extensions on one hand, and (ii) counter-based models like vector addition systems with states (VASS) on the other. For pushdown systems and extensions, there is a rich variety of decidable and well-understood games, whereas on VASS arenas, even extremely simple games are undecidable. Here, a VASS is an automaton with counters that can be incremented and decremented, but not tested for zero. Crucially, the counters can only assume non-negative values. However, certain VASS games become decidable when using energy semantics: An energy game is played on a system with counters, but the arena includes configurations with negative counters. The requirement that the counters stay non-negative is, instead, part of the winning condition of the existential…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
