🤖 AI

Automated Approach for Solving Infinite-state Polynomial Reachability Games

This paper introduces a sound, semi-complete, and sub-exponential automated algorithm that utilizes ranking certificates to solve infinite-state polynomial reachability games, successfully computing winning strategies for the REACH player in challenging scenarios like the Cinderella-Stepmother game where previous methods failed.

Original authors: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, {\DJ}or{\dj}e Žikelić

Published 2026-05-12

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, {\DJ}or{\dj}e Žikelić

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a game played on a giant, infinite chessboard where the pieces aren't just black and white squares, but complex mathematical values like temperature, speed, or water levels. This paper introduces a new way to solve these "infinite-state" games, specifically focusing on a battle between two players: REACH (the attacker) and SAFE (the defender).

Here is a simple breakdown of what the authors did, using everyday analogies.

The Game: A Never-Ending Tug-of-War

In these games, the board is defined by real numbers (like a thermometer reading or a bank account balance).

The Goal of REACH: To push the game into a specific "Target Zone" (e.g., a bucket overflowing, a robot reaching a destination).
The Goal of SAFE: To keep the game away from that Target Zone forever.

Usually, if the board is infinite, figuring out who wins is impossible to solve with a computer. It's like trying to count every single grain of sand on a beach to see if you have enough to build a castle; the task is too big.

The Big Idea: The "Progress Meter" (Ranking Certificates)

The authors invented a new tool called a Ranking Certificate. Think of this as a magic progress meter or a battery level attached to every possible state of the game.

Here is how it works:

The Battery Rule: The meter must always show a positive number (or zero).
The Drain Rule: Every time a move is made, the battery level must go down by at least a little bit.
The Winner: If the battery hits zero (or goes negative), the game ends, and REACH wins because they reached the target.

The Catch:

If it's SAFE's turn, the meter must go down no matter which move SAFE chooses. SAFE cannot find a way to keep the battery high.
If it's REACH's turn, REACH just needs to find one move that drains the battery.

If you can draw a map where every single move drains the battery, you have proven that REACH will eventually win, no matter how hard SAFE tries to stop them. This is the "Ranking Certificate."

The Problem: The "Infinite Choice" Trap

The authors discovered a flaw in this idea. Imagine SAFE has a superpower: they can choose from an infinite number of moves.

Analogy: Imagine SAFE can choose to lower the battery by 0.1, or 0.01, or 0.0000001. If SAFE keeps choosing smaller and smaller drops, the battery might never actually hit zero, even though it's going down. In this specific "infinite choice" scenario, the battery meter trick fails to prove a win.

However, the authors proved that if SAFE is limited to a finite number of choices at each step (like a normal board game), the battery meter trick works perfectly and is a complete proof.

The Solution: An Automated Robot Solver

The paper presents a fully automated computer program that does the following:

Guesses the Shape: It assumes the "battery meter" is a polynomial equation (a fancy math formula involving variables like $x$ , $y$ , $x^2$ , etc.).
Fills in the Blanks: It uses a computer solver to find the exact numbers that make the formula work as a valid battery meter.
Outputs a Strategy: If it finds the numbers, it gives you the exact winning moves for REACH and the mathematical proof (the certificate) that they work.

Why is this special?
Previous methods were like trying to solve a puzzle by checking every single piece one by one, which took forever or failed on complex puzzles. This new method is faster (sub-exponential time) and can handle much more complex math (polynomials) than previous tools, which were limited to simple linear math.

The Real-World Test: The Cinderella-Stepmother Game

To prove their method works, they tested it on a famous puzzle called the Cinderella-Stepmother Game.

The Setup: A Stepmother (REACH) pours water into 5 buckets. A Cinderella (SAFE) empties two buckets. The Stepmother wins if any bucket overflows.
The Challenge: For years, computers could only solve this if the buckets were very small. If the buckets were almost full (but not quite), computers got stuck.
The Result: The authors' new tool solved the game for any bucket size, even ones that were arbitrarily close to overflowing. It found a winning strategy for the Stepmother where no other computer tool could.

Summary

The paper introduces a new "battery meter" proof rule to show that an attacker can win a complex, infinite game. They built a robot that automatically designs this battery meter using advanced math. This robot is the first to successfully solve difficult, infinite-state games that were previously impossible for computers to crack, specifically the classic "Cinderella-Stepmother" water bucket puzzle.

Technical Summary: Automated Approach for Solving Infinite-state Polynomial Reachability Games

Problem Statement

The paper addresses the problem of solving infinite-state reachability games. These are two-player, turn-based games played on graphs where nodes are partitioned between a REACH player (whose objective is to force the game into a specific target set of states) and a SAFE player (whose objective is to avoid the target set indefinitely).

While reachability games on finite graphs are well-understood and solvable in linear time, the infinite-state variant is generally undecidable (per Rice's theorem), even for restricted cases where one player has only a single action. Existing methods often rely on reducing the problem to logical satisfiability (e.g., Constrained Horn Clauses) or fixed-point computations, but these approaches face limitations in handling polynomial constraints, providing completeness guarantees, or achieving efficient runtime. The specific challenge addressed here is determining the existence of, and computing, a winning strategy for the REACH player in games defined over real-valued variables with polynomial constraints.

Methodology

1. Ranking Certificates

The core theoretical contribution is the introduction of ranking certificates for reachability games. Drawing inspiration from ranking functions used to prove program termination, a ranking certificate is a function $f: S \to \mathbb{R}$ that maps game states to real values. To serve as a witness for a winning strategy for REACH, $f$ must satisfy three conditions:

Non-negativity at Start: $f(s_{init}) \ge 0$ .
Safety Progress (SAFE's turn): If the current state $s$ belongs to SAFE and $f(s) \ge 0$ , then for all possible successor states $s'$ , $f(s) - 1 \ge f(s') \ge 0$ . This ensures SAFE cannot prevent the value from decreasing.
Reachability Progress (REACH's turn): If the current state $s$ belongs to REACH and $f(s) \ge 0$ , there exists a successor state $s'$ such that $f(s) - 1 \ge f(s') \ge 0$ . This ensures REACH can choose a move that strictly decreases the value.

The value of the function acts as a measure of progress toward the target set. The paper proves that the existence of such a certificate implies the existence of a memoryless winning strategy for REACH (Soundness). While the proof rule is not complete for general infinite-state games (due to the possibility of SAFE choosing from infinitely many values to force an unbounded lower bound), it is proven to be sound and complete if SAFE has only finitely many choices at each step.

2. Automated Synthesis Algorithm

The authors propose a fully automated algorithm for polynomial reachability games, where guards, updates, and objectives are defined by polynomial inequalities over real variables. The algorithm operates in four steps:

Template Setup: The algorithm fixes symbolic polynomial templates of a maximal degree $D$ for the ranking certificate $f$ and the memoryless strategy $\sigma$ .
Constraint Collection: It generates a system of constraints over the symbolic template variables. These constraints encode the conditions (C1–C3) of the ranking certificate definition, substituting the symbolic templates for the functions.
Quantifier Elimination: The constraints contain universal quantifiers (e.g., "for all $x$ "). The algorithm applies a translation based on Putinar's theorem (for general polynomials) or Farkas' lemma (for linear polynomials) to convert these into a system of purely existentially quantified polynomial constraints.
Solving: An off-the-shelf SMT solver (e.g., Z3, MathSAT5) solves the resulting system. A solution yields concrete coefficients for the polynomial templates, producing a valid ranking certificate and the corresponding winning strategy.

The algorithm is sound (any computed strategy is correct) and semi-complete (it is guaranteed to find a solution if one exists within the class of polynomial certificates and the state space is compact). The runtime is sub-exponential with respect to the input size for a fixed polynomial degree.

Key Contributions

Theoretical Framework: The introduction of ranking certificates as a sound and complete proof rule for a specific subclass of infinite-state games (where SAFE has finite choices). This generalizes the concept of ranking functions from program termination to game theory.
Automation: The development of a fully automated algorithm that synthesizes winning strategies and formal correctness witnesses (the certificates) for polynomial reachability games.
Complexity and Scope: The approach handles polynomial arithmetic (unlike previous methods limited to linear arithmetic) and achieves sub-exponential complexity (improving upon the double-exponential complexity of prior linear arithmetic approaches).
Experimental Validation: The implementation of a prototype that successfully solves challenging benchmarks previously out of reach for existing tools.

Experimental Results

The authors evaluated their method on two primary benchmarks:

The Cinderella-Stepmother Game:
- Classical Variant: The stepmother (REACH) distributes water to buckets, and Cinderella (SAFE) empties two adjacent buckets. The goal is to overflow a bucket.
- Results: The proposed method solved the game for bucket capacities up to $2 - 10^{-10}$ and, crucially, for the symbolic case $2 - \epsilon$ (where $\epsilon > 0$ ) in under 1 second.
- Comparison: State-of-the-art tools (GenSys and rpgsolve) failed (timeout or not supported) on the $2 - 10^{-10}$ case and could not handle the symbolic $2 - \epsilon$ case. This represents the first automated solution for arbitrary precision parameters in this game.
- Non-linear Variant: A version where the stepmother's distribution is constrained by a Euclidean norm ( $\ell_2$ ) rather than Manhattan norm ( $\ell_1$ ), introducing non-linearity. The proposed method solved fixed capacity cases in under 1 second, while baselines failed completely.
Faulty Robot Benchmark:
- A game modeling a robot mixing chemicals where an adversary introduces faults. The robot aims to reach a specific density and volume.
- Results: The proposed method solved the game in 44 seconds. The baseline GenSys failed to terminate within a 5-minute timeout.

Significance and Claims

The paper claims that its approach significantly advances the state of the art in solving infinite-state reachability games by offering a unique combination of features not previously available in a single method:

Applicability to Polynomial Games: Unlike prior sound/semi-complete methods restricted to linear arithmetic.
Semi-completeness Guarantees: Unlike fixed-point methods that may not terminate or lack completeness guarantees.
Efficiency: Sub-exponential runtime compared to double-exponential alternatives.

The authors emphasize that their method is the first to compute an optimal winning strategy for the classical Cinderella-Stepmother game for an arbitrary precision parameter ( $2 - \epsilon$ ), a problem that remained open for automated solvers. They acknowledge limitations, noting the method currently applies only to polynomial games and focuses on reachability objectives, leaving extensions to non-polynomial games and other objectives (e.g., $\omega$ -regular or quantitative) as directions for future work.