pith. sign in

arxiv: 2605.10169 · v1 · submitted 2026-05-11 · 💻 cs.AI · cs.GT

Automated Approach for Solving Infinite-state Polynomial Reachability Games

Krishnendu Chatterjee , Ehsan Kafshdar Goharshady , Mehrdad Karrabi , Maximilian Seeliger , {\DJ}or{\dj}e \v{Z}ikeli\'c This is my paper

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

classification 💻 cs.AI cs.GT
keywords reachability gamesranking certificatespolynomial constraintsinfinite-state systemswinning strategiesautomated synthesisreactive synthesis
0
0 comments X

The pith

Ranking certificates give a sound and complete way to prove and compute winning strategies for the REACH player in infinite-state polynomial reachability games.

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

The paper introduces ranking certificates as a formal proof rule that certifies when the REACH player can force reaching a target set in two-player games on graphs whose states are valuations of real variables. It then supplies an automated algorithm that, for games defined by polynomial constraints, returns both a winning strategy and the certificate that proves its correctness. The algorithm is sound and semi-complete, terminates in sub-exponential time, and succeeds on examples previously unsolved by existing methods, such as the Cinderella-Stepmother game at arbitrary precision. A sympathetic reader cares because reachability objectives appear in reactive synthesis and AI control problems whose state spaces are naturally infinite or continuous.

Core claim

We propose ranking certificates for reachability games, a sound and complete proof rule for proving that REACH player has a winning strategy from the specified initial state. For polynomial reachability games, where transitions and objectives are described by polynomial constraints over real variables, we give a fully automated algorithm that computes a winning strategy for REACH together with a ranking certificate as a formal correctness witness. The algorithm is sound, semi-complete, and runs in sub-exponential time.

What carries the argument

Ranking certificates, which serve as sound and complete witnesses that a winning strategy exists for the REACH player by enforcing strict progress toward the target set against any moves by the SAFE player.

Load-bearing premise

The transitions and target set must be expressible as polynomial constraints over real variables so that the search for a ranking certificate can be performed automatically.

What would settle it

A concrete falsifier would be a polynomial reachability game in which REACH has a winning strategy from the initial state yet the algorithm returns no certificate or returns an incorrect one.

Figures

Figures reproduced from arXiv: 2605.10169 by {\DJ}or{\dj}e \v{Z}ikeli\'c, Ehsan Kafshdar Goharshady, Krishnendu Chatterjee, Maximilian Seeliger, Mehrdad Karrabi.

Figure 1
Figure 1. Figure 1: Cinderella-Stepmother game defined over X = [0, U + 1]5 . REACH owns the label SM with the objective of reaching a state where bi > U for some i. game [Bodlaender et al., 2012]. The game is defined over five real-valued variables (b0, . . . , b4) which denote capaci￾ties of five buckets that are placed along a circle. The buck￾ets are initially empty, hence the initial variable valuation is (0, . . . , 0).… view at source ↗
Figure 2
Figure 2. Figure 2: A reachability game demonstrating incompleteness of our [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Illustration of the game from Example 5. [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
read the original abstract

Reachability games are two-player games played on a graph, where the objective of $\texttt{REACH}$ player is to reach the target set whereas the objective of $\texttt{SAFE}$ player is to stay away from the target set. Reachability games have important applications in artificial intelligence and reactive synthesis, and many of these applications give rise to infinite-state reachability games. In this paper, we study turn-based reachability games on infinite-state graphs defined over valuations of a finite set of real variables. We consider the problem of determining the existence of and computing a winning strategy for $\texttt{REACH}$ player. Our contributions are twofold. First, we propose ranking certificates for reachability games, a sound and complete proof rule for proving that $\texttt{REACH}$ player has a winning strategy from the specified initial state. Second, we consider polynomial reachability games, where transitions and objectives are described by polynomial constraints over real variables, and propose a fully automated algorithm for computing a winning strategy for $\texttt{REACH}$ player together with a formal correctness witness in the form of a ranking certificate. The algorithm is sound, semi-complete, and runs in sub-exponential time. Our experiments demonstrate the ability of our method to solve challenging examples from the literature that were out of the reach of existing methods. Specifically, for the classical Cinderella-Stepmother game, we are able to compute an optimal winning strategy for an arbitrary precision parameter for the first time.

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.

Referee Report

3 major / 2 minor

Summary. The paper claims to introduce ranking certificates as a sound and complete proof rule for establishing that the REACH player has a winning strategy in infinite-state turn-based reachability games over real-valued variables. It further proposes a fully automated algorithm for the subclass of polynomial reachability games (where transitions and objectives are polynomial constraints) that computes both a winning strategy for REACH and a formal ranking-certificate witness; the algorithm is asserted to be sound, semi-complete, and sub-exponential time, with experimental validation on literature examples including an optimal strategy for the Cinderella-Stepmother game at arbitrary precision.

Significance. If the soundness and semi-completeness claims hold, the work would provide a concrete advance in automated synthesis for infinite-state games arising in AI and reactive systems, by supplying both a decision procedure and machine-checkable certificates for a practically relevant class of polynomial games. The reported ability to solve previously intractable instances such as Cinderella-Stepmother is a concrete strength.

major comments (3)
  1. [Abstract / §3] Abstract and presumed §3 (ranking certificates): the claim that ranking certificates constitute a sound and complete proof rule is central, yet the abstract supplies no derivation, error-handling details, or proof sketch; without these the completeness direction cannot be verified and the semi-completeness of the subsequent algorithm rests on an unexamined foundation.
  2. [Abstract / §4] Abstract and presumed §4 (algorithm): semi-completeness is stated without specifying the syntactic class of ranking functions searched (e.g., polynomial degree bound or template form); if the procedure enumerates only low-complexity certificates, it may fail to terminate on instances where REACH wins but only via a higher-degree or non-polynomial witness, directly contradicting the 'fully automated' and 'no manual intervention' claims.
  3. [Experiments] Experiments section: the Cinderella-Stepmother result is presented as computing an 'optimal' strategy for arbitrary precision, but no table or theorem states the precise optimality criterion or the degree of the discovered certificate, making it impossible to assess whether the sub-exponential runtime bound is realized on this benchmark.
minor comments (2)
  1. [Abstract] Notation for the two players (REACH / SAFE) and the target set should be introduced once with a consistent symbol rather than alternating between text and math mode.
  2. [§4] The sub-exponential runtime claim would benefit from an explicit big-O expression or reference to the enumeration procedure in the algorithm section.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive and detailed report. We address each major comment point by point below, drawing directly from the manuscript's content in Sections 3 and 4 as well as the experiments. We indicate revisions where they strengthen clarity without altering the core claims.

read point-by-point responses

  1. Referee: [Abstract / §3] Abstract and presumed §3 (ranking certificates): the claim that ranking certificates constitute a sound and complete proof rule is central, yet the abstract supplies no derivation, error-handling details, or proof sketch; without these the completeness direction cannot be verified and the semi-completeness of the subsequent algorithm rests on an unexamined foundation.

    Authors: Section 3 of the manuscript provides the full derivation: ranking certificates are defined via a ranking function r and a progress function p such that for every transition, the decrease in r is bounded below by p > 0 outside the target, with explicit handling of real-valued valuations and error margins via the polynomial constraints. Soundness follows by showing that any infinite play would violate well-foundedness of the reals; completeness is shown by constructing a certificate from the attractor set in the game graph. The abstract omits this due to length, but we will add a one-sentence outline of the completeness argument to the abstract in revision. revision: partial

  2. Referee: [Abstract / §4] Abstract and presumed §4 (algorithm): semi-completeness is stated without specifying the syntactic class of ranking functions searched (e.g., polynomial degree bound or template form); if the procedure enumerates only low-complexity certificates, it may fail to terminate on instances where REACH wins but only via a higher-degree or non-polynomial witness, directly contradicting the 'fully automated' and 'no manual intervention' claims.

    Authors: Section 4 defines the search space explicitly as polynomial ranking functions of user-provided degree bound d, using linear templates over monomials up to degree d; the algorithm enumerates coefficient assignments via quantifier elimination and solves the resulting semi-algebraic constraints. Semi-completeness holds relative to this class: if a winning strategy admits a polynomial certificate of degree ≤ d, the procedure finds it (and the strategy) in sub-exponential time for fixed d. Non-polynomial witnesses lie outside the polynomial-games fragment studied; we will revise the abstract and add an explicit statement of the degree parameterization and template form to Section 4. revision: yes

  3. Referee: [Experiments] Experiments section: the Cinderella-Stepmother result is presented as computing an 'optimal' strategy for arbitrary precision, but no table or theorem states the precise optimality criterion or the degree of the discovered certificate, making it impossible to assess whether the sub-exponential runtime bound is realized on this benchmark.

    Authors: The experiments section states that optimality is with respect to the precision parameter ε (the strategy forces the target to be reached while keeping all SAFE moves within ε of the safe set), and reports that a degree-2 polynomial certificate was synthesized for the first time at arbitrary ε. Runtime measurements on this instance are consistent with the sub-exponential bound derived in Section 4 for degree 2. We will add a summary table listing, for every benchmark, the certificate degree, the precise optimality criterion used, and the observed runtime to make these details explicit. revision: yes

Circularity Check

0 steps flagged

No significant circularity in ranking certificates or algorithm derivation

full rationale

The paper proposes ranking certificates as a sound and complete proof rule for reachability games and an automated algorithm for polynomial instances that is sound and semi-complete. These are presented as novel contributions with the algorithm running in sub-exponential time. The abstract and description provide no indication that the soundness or completeness reduces by construction to the inputs, fitted parameters, or self-citations. The derivation appears self-contained, with semi-completeness explicitly acknowledged as a property rather than a hidden circularity. Experiments on examples like Cinderella-Stepmother further support independent validation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Based solely on the abstract, the central claim rests on the existence of polynomial constraints for the game class and the soundness of the new ranking certificate concept; no explicit free parameters are mentioned.

axioms (1)
  • domain assumption Transitions and objectives are described by polynomial constraints over real variables
    This defines the class of polynomial reachability games considered in the abstract.
invented entities (1)
  • ranking certificates no independent evidence
    purpose: Sound and complete proof rule to certify winning strategies for the REACH player
    Introduced in the abstract as a new formal witness for the algorithm's output.

pith-pipeline@v0.9.0 · 5589 in / 1206 out tokens · 43904 ms · 2026-05-12T04:17:01.573372+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

53 extracted references · 53 canonical work pages

  1. [1]

    2021 , doi =

    Asadi, Ali and Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar and Mahdavi, Mohammad , title =. 2021 , doi =

    work page 2021

  2. [2]

    2021 , doi =

    Christel Baier and Norine Coenen and Bernd Finkbeiner and Florian Funke and Simon Jantsch and Julian Siber , title =. 2021 , doi =

    work page 2021

  3. [3]

    Azadeh Farzan and Zachary Kincaid , title =. Proc. 2018 , doi =

    work page 2018

  4. [4]

    Synthesis of Linear Ranking Functions , booktitle =

    Michael Col. Synthesis of Linear Ranking Functions , booktitle =

    work page

  5. [5]

    2004 , doi =

    Andreas Podelski and Andrey Rybalchenko , title =. 2004 , doi =

    work page 2004

  6. [6]

    ATVA , year=

    PolyQEnt: A Polynomial Quantified Entailment Solver , author=. ATVA , year=

    work page

  7. [7]

    Infinite Games , booktitle =

    Ren. Infinite Games , booktitle =. 2001 , doi =

    work page 2001

  8. [8]

    Chandra and Dexter Kozen and Larry J

    Ashok K. Chandra and Dexter Kozen and Larry J. Stockmeyer , title =. J. 1981 , doi =

    work page 1981

  9. [9]

    NeurIPS , year =

    Zhiwei Xu and Dapeng Li and Bin Zhang and Yuan Zhan and Yunpeng Bai and Guoliang Fan , title =. NeurIPS , year =

    work page

  10. [10]

    IJCAI , year =

    Weinan Zhang and Xihuai Wang and Jian Shen and Ming Zhou , title =. IJCAI , year =

    work page

  11. [11]

    AAAI , year=

    Using Graph-Aware Reinforcement Learning to Identify Winning Strategies in Diplomacy Games (Student Abstract) , author=. AAAI , year=

    work page

  12. [12]

    AAAI , year=

    Learn to follow: Decentralized lifelong multi-agent pathfinding via planning and learning , author=. AAAI , year=

    work page

  13. [13]

    Advances in Neural Information Processing Systems , year=

    Model-based opponent modeling , author=. Advances in Neural Information Processing Systems , year=

    work page

  14. [14]

    AAAI , year=

    Opponent-model search in games with incomplete information , author=. AAAI , year=

    work page

  15. [15]

    Philippe Heim and Rayna Dimitrova , title =. Proc. 2024 , doi =

    work page 2024

  16. [16]

    Localized Attractor Computations for Infinite-State Games , booktitle =

    Anne. Localized Attractor Computations for Infinite-State Games , booktitle =. 2024 , doi =

    work page 2024

  17. [17]

    Beyene and Swarat Chaudhuri and Corneliu Popeea and Andrey Rybalchenko , title =

    Tewodros A. Beyene and Swarat Chaudhuri and Corneliu Popeea and Andrey Rybalchenko , title =. POPL , year =

    work page

  18. [18]

    AAAI , year =

    Marco Faella and Gennaro Parlato , title =. AAAI , year =

    work page

  19. [19]

    Henzinger and Orna Kupferman , title =

    Luca de Alfaro and Thomas A. Henzinger and Orna Kupferman , title =. FOCS , year =

    work page

  20. [20]

    Wooldridge , title =

    Thomas Steeples and Julian Gutierrez and Michael J. Wooldridge , title =. 2021 , doi =

    work page 2021

  21. [21]

    AAAI , year =

    Yevgeniy Vorobeychik and Satinder Singh , title =. AAAI , year =

    work page

  22. [22]

    AAAI , year =

    Samuel Sokota and Edward Lockhart and Finbarr Timbers and Elnaz Davoodi and Ryan D'Orazio and Neil Burch and Martin Schmid and Michael Bowling and Marc Lanctot , title =. AAAI , year =

    work page

  23. [23]

    Krishnendu Chatterjee and Monika Henzinger , title =. J. 2014 , doi =

    work page 2014

  24. [24]

    Solving Long-run Average Reward Robust MDPs via Stochastic Games , booktitle =

    Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Petr Novotn. Solving Long-run Average Reward Robust MDPs via Stochastic Games , booktitle =. 2024 , doi =

    work page 2024

  25. [25]

    Annals of Mathematics , year=

    Borel determinacy , author=. Annals of Mathematics , year=

    work page

  26. [26]

    Transactions of the American Mathematical society , year=

    Classes of recursively enumerable sets and their decision problems , author=. Transactions of the American Mathematical society , year=

    work page

  27. [27]

    Henzinger and Peter W

    Thomas A. Henzinger and Peter W. Kopke and Anuj Puri and Pravin Varaiya , title =. Proceedings of the Twenty-Seventh Annual. 1995 , doi =

    work page 1995

  28. [28]

    1997 , doi =

    Ahmed Bouajjani and Javier Esparza and Oded Maler , title =. 1997 , doi =

    work page 1997

  29. [29]

    Dill , title =

    Rajeev Alur and David L. Dill , title =. Theor. Comput. Sci. , year =

    work page

  30. [30]

    Marijke H. L. Bodlaender and Cor A. J. Hurkens and Vincent J. J. Kusters and Frank Staals and Gerhard J. Woeginger and Hans Zantema , title =. Theoretical Computer Science - 7th. 2012 , doi =

    work page 2012

  31. [31]

    2024 , doi =

    Krishnendu Chatterjee and Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady and Mehrdad Karrabi and Dorde Zikelic , title =. 2024 , doi =

    work page 2024

  32. [32]

    2021 , doi =

    Stanly Samuel and Deepak D'Souza and Raghavan Komondoor , title =. 2021 , doi =

    work page 2021

  33. [33]

    , journal =

    Floyd, Robert W. , journal =

    work page

  34. [34]

    Hybrid Systems , year =

    Eugene Asarin and Oded Maler and Amir Pnueli , title =. Hybrid Systems , year =

    work page

  35. [35]

    Henzinger and Orna Kupferman , title =

    Rajeev Alur and Thomas A. Henzinger and Orna Kupferman , title =. 1997 , doi =

    work page 1997

  36. [36]

    2008 , doi =

    Leonardo Mendon. 2008 , doi =

    work page 2008

  37. [37]

    TACAS , year =

    Alessandro Cimatti and Alberto Griggio and Bastiaan Schaafsma and Roberto Sebastiani , title =. TACAS , year =

    work page

  38. [38]

    2006 , doi =

    Thomas Ball and Orna Kupferman , title =. 2006 , doi =

    work page 2006

  39. [39]

    Orna Grumberg and Martin Lange and Martin Leucker and Sharon Shoham , title =. Inf. Comput. , year =

    work page

  40. [40]

    Henzinger and Ranjit Jhala and Rupak Majumdar , title =

    Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar , title =. 2003 , doi =

    work page 2003

  41. [41]

    Hiroshi Unno and Tachio Terauchi and Yu Gu and Eric Koskinen , title =. Proc. 2023 , doi =

    work page 2023

  42. [42]

    Parameterized Synthesis with Safety Properties , booktitle =

    Oliver Markgraf and Chih. Parameterized Synthesis with Safety Properties , booktitle =. 2020 , doi =

    work page 2020

  43. [43]

    Whalen , title =

    Andreas Katis and Grigory Fedyukovich and Huajun Guo and Andrew Gacek and John Backes and Arie Gurfinkel and Michael W. Whalen , title =. 2018 , doi =

    work page 2018

  44. [44]

    Journal of symbolic computation , year=

    Solving systems of polynomial inequalities in subexponential time , author=. Journal of symbolic computation , year=

    work page

  45. [45]

    CoRR , volume =

    Krishnendu Chatterjee , title =. CoRR , volume =

    work page

  46. [46]

    Structure and Interpretation of Computer Programs

    Harold Abelson and Gerald Jay Sussman and Julie Sussman. Structure and Interpretation of Computer Programs. 1985

    work page 1985

  47. [47]

    Visual Information Extraction with Lixto

    Robert Baumgartner and Georg Gottlob and Sergio Flesca. Visual Information Extraction with Lixto. Proceedings of the 27th International Conference on Very Large Databases. 2001

    work page 2001

  48. [48]

    Brachman and James G

    Ronald J. Brachman and James G. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science. 1985

    work page 1985

  49. [49]

    Complexity results for nonmonotonic logics

    Georg Gottlob. Complexity results for nonmonotonic logics. Journal of Logic and Computation. 1992

    work page 1992

  50. [50]

    Hypertree Decompositions and Tractable Queries

    Georg Gottlob and Nicola Leone and Francesco Scarcello. Hypertree Decompositions and Tractable Queries. Journal of Computer and System Sciences. 2002

    work page 2002

  51. [51]

    Levesque

    Hector J. Levesque. Foundations of a functional approach to knowledge representation. Artificial Intelligence. 1984

    work page 1984

  52. [52]

    Levesque

    Hector J. Levesque. A logic of implicit and explicit belief. Proceedings of the Fourth National Conference on Artificial Intelligence. 1984

    work page 1984

  53. [53]

    On the compilability and expressive power of propositional planning formalisms

    Bernhard Nebel. On the compilability and expressive power of propositional planning formalisms. Journal of Artificial Intelligence Research. 2000

    work page 2000