arxiv: 2605.05935 · v2 · submitted 2026-05-07 · 💻 cs.FL

Recognition: no theorem link

Infinite-state Games with Energy Objectives Beyond Counters

Irmak Sa\u{g}lam , Georg Zetzsche

Authors on Pith no claims yet

Pith reviewed 2026-05-12 04:54 UTC · model grok-4.3

classification 💻 cs.FL

keywords viability gamesvalence systemsgraph monoidsinfinite-state gamesenergy objectivesdecidabilitypushdown systemsvector addition systems

0 comments

The pith

Viability games on valence systems over graph monoids have their decidability and complexity fully classified, including decidable cases where reachability is undecidable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies viability games, which move the legality requirement for instructions into the winning condition rather than the arena rules, generalizing energy games beyond pure counters. It employs valence systems over graph monoids as a uniform framework that captures pushdown systems, vector addition systems with states, integer counters, and their combinations. The central result is a complete map of decidability and complexity for these games across all such systems. A sympathetic reader would care because the results identify islands of decidability in mixed recursion-counter systems where standard game problems and even single-player reachability remain undecidable.

Core claim

Valence systems over graph monoids provide a uniform model in which viability games admit a complete decidability and complexity classification; this includes pushdown-counter hybrids where viability is decidable despite undecidability of non-termination games, and further systems where viability remains decidable even though control-state reachability is undecidable.

What carries the argument

Valence systems over graph monoids, which encode the operational semantics of diverse infinite-state systems via undirected graphs that define the allowed actions on the underlying monoid.

If this is right

Viability games are decidable for certain pushdown-counter combinations even though non-termination games are undecidable on the same arenas.
Viability games remain decidable for some systems in which single-player control-state reachability is already undecidable.
The complexity of viability games is completely pinned down for every graph monoid in the framework.
Energy-style objectives can be lifted from pure counter systems to broader classes that include recursion without losing all decidability.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The approach suggests that relocating legality into the objective can restore decidability for verification tasks on hybrid stack-counter systems.
Similar objective-based relaxations might be tested on other undecidable problems such as parity games or mean-payoff games within the same monoid framework.
The classification supplies a practical guide for choosing which subsystems of a mixed infinite-state model can be verified algorithmically.

Load-bearing premise

The valence systems over graph monoids framework faithfully captures the semantics of pushdown systems, VASS, integer counters, and their combinations once legality constraints are moved into the winning condition.

What would settle it

An explicit graph monoid together with a concrete viability game for which either the claimed decidability status or the exact complexity class differs from the paper's classification.

read the original 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 player. We study an analogue of energy semantics -- legality of instructions as part of the winning condition rather than arena -- on a broad class of infinite-state systems, where we call them viability games. Specifically, we study viability games in the framework of valence systems over graph monoids, where (undirected, loops allowed) graphs specify various infinite-state systems, such as pushdowns, VASS counters, integer counters, and combinations thereof. In our main results, we provide a complete description of the decidability and complexity landscape of viability games across valence systems over graph monoids. Our results reveal encouraging decidability properties. For example, in certain combinations of pushdowns and counters, viability games are decidable, despite non-termination games being undecidable there. Moreover, viability games are even decidable for certain systems where (single-player) control-state reachability is undecidable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper maps decidability for viability games across valence systems over graph monoids, showing decidable cases in pushdown-counter hybrids where non-termination and reachability games are not.

read the letter

This paper maps out the decidability and complexity landscape for viability games on valence systems over graph monoids. It treats the non-negativity constraints as part of the winning condition rather than the arena, extending the energy-game idea from counters to a single framework that includes pushdowns, VASS, integer counters, and combinations of them. The main new results are that viability games remain decidable in certain pushdown-plus-counter systems even though non-termination games are undecidable there, and that they are decidable even in some systems where single-player control-state reachability is undecidable. That contrast is the useful part. The work does well by giving one coherent classification instead of separate treatments for each model, and the graph-monoid setup appears to capture the operational semantics without obvious post-hoc restrictions. The distinction between arena-level legality and winning-condition legality is handled in the standard way. The soft spots are limited. The abstract states a complete landscape, so the proofs will need checking for whether every monoid construction and reduction covers the edge cases without gaps; that is the usual place where these kinds of classifications can slip. The assumption that the framework faithfully models the hybrids is reasonable and not circular, but it is the part that would benefit most from explicit verification in the full text. This is for people working on infinite-state games, automata theory, and decidability borders between recursion and counters. A reader who already knows pushdown games or VASS results will get the most out of the comparisons. I would send it to peer review; the claims are specific enough and the extension is coherent enough to justify referee time.

Referee Report

0 major / 3 minor

Summary. The paper introduces viability games as an analogue of energy games on valence systems over graph monoids, a framework that unifies pushdown systems, VASS counters, integer counters, and their combinations by moving legality constraints into the winning condition. The central claim is a complete decidability and complexity landscape for these games, with positive results showing decidability for certain pushdown-counter combinations where non-termination and control-state reachability games are undecidable.

Significance. If the classification holds, the work provides a valuable unification of recursion-based and counter-based infinite-state game models, identifying new decidable fragments that could aid verification and synthesis. The framework's ability to recover decidability by relocating constraints is a conceptually clean contribution, and the complete landscape offers a reference point for the field.

minor comments (3)

[Abstract] The abstract and introduction introduce 'valence systems over graph monoids' and 'viability games' without a concise one-sentence definition or diagram; adding this early would improve accessibility for readers unfamiliar with the model.
[Main results] The paper should include an explicit table or diagram summarizing the decidability results across representative graph monoids (e.g., pushdown-only, VASS-only, mixed cases) to make the 'complete landscape' claim immediately verifiable.
[Preliminaries] Notation for graph monoids and valence systems could be standardized with a dedicated preliminary section listing all used symbols and their meanings to avoid scattered definitions.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript and for recommending minor revision. The referee's summary correctly captures the core contribution: a complete decidability and complexity classification for viability games on valence systems over graph monoids, including decidable cases for certain pushdown-counter combinations where non-termination games remain undecidable.

Circularity Check

0 steps flagged

No significant circularity; results derived independently from model definitions

full rationale

The paper classifies decidability and complexity of viability games on valence systems over graph monoids by analyzing structural properties of the underlying monoids and applying standard techniques from infinite-state game theory. No load-bearing step reduces by construction to a fitted parameter, self-definition, or unverified self-citation chain; the decidability landscape (e.g., decidability in certain pushdown+counter combinations where reachability is undecidable) follows from the framework's separation of arena constraints and winning conditions. The derivation is self-contained against external benchmarks in automata theory and does not rely on renaming known results or smuggling ansatzes via prior author work.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claims rest on the newly introduced definitions of valence systems over graph monoids and viability games. No numeric free parameters appear. Axioms are standard mathematical properties of graphs and monoids. Invented entities are the unifying framework and the viability-game concept itself.

axioms (2)

standard math Standard algebraic properties of monoids generated by graph-labeled transitions
Invoked to define the operational semantics of valence systems.
domain assumption Undirected graphs with loops correctly encode the allowed operations for pushdowns, VASS, and integer counters
Used to unify the various infinite-state models under one framework.

invented entities (2)

valence systems over graph monoids no independent evidence
purpose: Unified model capturing pushdowns, counters, and combinations
New framework introduced to study viability games across systems.
viability games no independent evidence
purpose: Energy-semantics analogue where instruction legality is part of the winning condition
Core new concept enabling the decidability results.

pith-pipeline@v0.9.0 · 5626 in / 1536 out tokens · 61514 ms · 2026-05-12T04:54:38.131939+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

[1]

10 Hans-Juergen Boehm

1 Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In Thomas A. Henzinger and Dale Miller, editors,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 (LIC...

work page doi:10.1145/2603088.2603100 2014
[2]

Springer, 2013.doi:10.1007/978-3-642-40184-8_9

Proceedings, volume 8052 ofLecture Notes in Computer Science, pages 106–120. Springer, 2013.doi:10.1007/978-3-642-40184-8_9. 3 Ashwani Anand, Sylvain Schmitz, Lia Schütze, and Georg Zetzsche. Verifying unboundedness via amalgamation. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors,Proceedings of the 39th Annual ACM/IEEE Symposium on Logic i...

work page doi:10.1007/978-3-642-40184-8_9 2013
[3]

Springer, 2013.doi:10.1007/978-3-642-40313-2_22

Proceedings, Lecture Notes in Computer Science, pages 231–242. Springer, 2013.doi:10.1007/978-3-642-40313-2_22. 7 ThierryCachat. Symbolicstrategysynthesisforgamesonpushdowngraphs. InPeterWidmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan J. Eidenbenz, and Ricardo Conejo, editors,Automata, Languages and Programming, 29th Int...

work page doi:10.1007/978-3-642-40313-2_22 2013
[4]

Springer, 2012.doi:10.1007/978-3-642-32940-1_10

Proceedings, volume 7454 ofLecture Notes in Computer Science, pages 115–131. Springer, 2012.doi:10.1007/978-3-642-32940-1_10. 11 Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, and Sylvain Schmitz. Perfect half space games. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–11. IEEE Co...

work page doi:10.1007/978-3-642-32940-1_10 2012
[5]

12 Jean-Baptiste Courtois and Sylvain Schmitz

doi:10.1109/LICS.2017.8005105. 12 Jean-Baptiste Courtois and Sylvain Schmitz. Alternating vector addition systems with states. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors,Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29,

work page doi:10.1109/lics.2017.8005105 2017
[6]

Springer, 2014.doi:10.1007/978-3-662-44522-8_19

Proceedings, Part I, volume 8634 ofLecture Notes in Computer Science, pages 220–231. Springer, 2014.doi:10.1007/978-3-662-44522-8_19. 20 Infinite-state games with energy objectives beyond counters 13 Michael W. Davis and Tadeusz Januszkiewicz. Right-angled artin groups are commensurable with right-angled coxeter groups.Journal of Pure and Applied Algebra,...

work page doi:10.1007/978-3-662-44522-8_19 2014
[7]

and Januszkiewicz, Tadeusz , TITLE =

doi:10.1016/S0022-4049(99)00175-9. 14 Emanuele D’Osualdo, Roland Meyer, and Georg Zetzsche. First-order logic with reachability for infinite-state systems. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 457–46...

work page doi:10.1016/s0022-4049(99)00175-9 2016
[8]

17 Nathanaël Fijalkow, C

arXiv:2411.01592,doi:10.48550/arXiv.2411.01592. 17 Nathanaël Fijalkow, C. Aiswarya, Guy Avni, Nathalie Bertrand, Patricia Bouyer, Romain Bren- guier, ArnaudCarayol, AntonioCasares, JohnFearnley, PaulGastin, HugoGimbert, ThomasA. Henzinger, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Pierre Ohlmann, Mickael Randour, O...

work page doi:10.48550/arxiv.2411.01592 2025
[9]

Proceedings, volume 8762 ofLecture Notes in Computer Science, pages112–124.Springer, 2014.doi:10.1007/978-3-319-11439-2_

work page doi:10.1007/978-3-319-11439-2_ 2014
[10]

and Keel, S

21 Tim Hsu and Daniel T Wise. On linear and residual properties of graph products.Michigan Mathematical Journal, 46(2):251–259, 1999.doi:10.1307/mmj/1030132408. 22 Marcin Jurdzinski, Ranko Lazic, and Sylvain Schmitz. Fixed-dimensional energy games are in pseudo-polynomial time. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann,...

work page doi:10.1307/mmj/1030132408 1999
[11]

24 Richard J

doi:10.1007/978-3-662-47666-6_26. 24 Richard J. Lipton and Yechezkel Zalcstein. Word problems solvable in logspace.Journal of the ACM, 24(3):522–526, July 1977.doi:10.1145/322017.322031. 25 Markus Lohrey and Benjamin Steinberg. The submonoid and rational subset membership prob- lems for graph groups.Journal of Algebra, 320(2):728–755, 2008.doi:10.1016/j.j...

work page doi:10.1007/978-3-662-47666-6_26 1977
[12]

30 Sebastian Muskalla.Certificates for automata in a hostile environment

doi:10.4230/LIPICS.CONCUR.2018.12. 30 Sebastian Muskalla.Certificates for automata in a hostile environment. PhD thesis,

work page doi:10.4230/lipics.concur.2018.12 2018
[13]

31 Jean-François Raskin, Mathias Samuelides, and Laurent Van Begin

doi:10.24355/dbbs.084-202401201643-0. 31 Jean-François Raskin, Mathias Samuelides, and Laurent Van Begin. Games for counting abstractions. In Michael Huth, editor,Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems, AVoCS 2004, London, UK, September 4, 2004, volume 128 ofElectronic Notes in Theoretical Computer Sc...

work page doi:10.24355/dbbs.084-202401201643-0 2004
[14]

32 Aneesh K

doi:10.1016/J.ENTCS.2005.04.005. 32 Aneesh K. Shetty, S. Krishna, and Georg Zetzsche. Scope-bounded reachability in valence systems. In Serge Haddad and Daniele Varacca, editors,32nd International Conference on Concurrency Theory, CONCUR 2021, Virtual Conference, August 24-27, 2021, volume 203 ofLIPIcs, pages 29:1–29:19. Schloss Dagstuhl - Leibniz-Zentrum...

work page doi:10.1016/j.entcs.2005.04.005 2005
[15]

33 Igor Walukiewicz

doi:10.4230/LIPICS.CONCUR.2021.29. 33 Igor Walukiewicz. Pushdown processes: Games and model-checking.Inf. Comput., 164(2):234– 263, 2001.doi:10.1006/INCO.2000.2894. 34 Georg Zetzsche. Silent transitions in automata with storage. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors,Automata, Languages, and Programming - 40th ...

work page doi:10.4230/lipics.concur.2021.29 2021
[16]

positive

URL:https://kluedo.ub.rptu.de/frontdoor/index/index/docId/4400. 37 Georg Zetzsche. The emptiness problem for valence automata over graph monoids.Inf. Comput., 277:104583, 2021.doi:10.1016/J.IC.2020.104583. 38 Georg Zetzsche. Recent advances on reachability problems for valence systems (invited talk). In Paul C. Bell, Patrick Totzke, and Igor Potapov, edit...

work page doi:10.1016/j.ic.2020.104583 2021