# Automated Approach for Solving Infinite-state Polynomial Reachability Games

arXiv: https://arxiv.org/abs/2605.10169 · HTML: https://mlsanity.com/paper/2605.10169/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 47 references that are in the map.
- First posted on arXiv 11 May 2026.

## Builds on (most cited first, 13 of 13)

- [Learn to Follow: Decentralized Lifelong Multi-agent Pathfinding via Planning and Learning](https://mlsanity.com/paper/2310.01207/) (2023)
- [Model-based Multi-agent Policy Optimization with Adaptive Opponent-wise Rollouts](https://mlsanity.com/paper/2105.03363/) (2021)
- [Model-Based Opponent Modeling](https://mlsanity.com/paper/2108.01843/) (2021)
- [Solving Common-Payoff Games with Approximate Policy Iteration](https://mlsanity.com/paper/2101.04237/) (2021)
- [Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts](https://mlsanity.com/paper/1709.04986/) (2017)
- [GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces](https://mlsanity.com/paper/2107.08794/) (2021)
- [Causality-Based Game Solving](https://mlsanity.com/paper/2105.14247/) (2021)
- [Using Graph-Aware Reinforcement Learning to Identify Winning Strategies in Diplomacy Games (Student Abstract)](https://mlsanity.com/paper/2112.15331/) (2021)
- [Solving Infinite-State Games via Acceleration (Full Version)](https://mlsanity.com/paper/2305.16118/) (2023)
- [Localized Attractor Computations for Infinite-State Games (Full Version)](https://mlsanity.com/paper/2405.09281/) (2024)
- [PolyQEnt: A Polynomial Quantified Entailment Solver](https://mlsanity.com/paper/2408.03796/) (2024)
- [Parameterized Synthesis with Safety Properties](https://mlsanity.com/paper/2009.13459/) (2020)
- [Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs](https://mlsanity.com/paper/2403.05386/) (2024)

## Abstract (arXiv)

Reachability games are two-player games played on a graph, where the objective of textttREACH player is to reach the target set whereas the objective of textttSAFE 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 textttREACH player. Our contributions are twofold. First, we propose ranking certificates for reachability games, a sound and complete proof rule for proving that textttREACH 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 textttREACH 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.