Automated Approach for Solving Infinite-state Polynomial Reachability Games
2026-05-11 • Artificial Intelligence
Artificial IntelligenceComputer Science and Game Theory
AI summaryⓘ
The authors study a type of game where two players take turns moving on a graph with an infinite number of states, trying to either reach a goal or avoid it. They introduce a new proof method called ranking certificates that can reliably show whether the player trying to reach the goal can win from a starting point. Additionally, they develop an automated algorithm that works with games involving polynomial rules over real numbers, which not only finds winning strategies but also provides a correctness proof. Their method runs efficiently and can solve tough problems that older methods couldn't, including finding optimal strategies for a well-known example called the Cinderella-Stepmother game.
reachability gamesinfinite-state graphsranking certificateswinning strategypolynomial constraintsreactive synthesisturn-based gamesCinderella-Stepmother gamesemi-complete algorithmautomated verification
Authors
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, Đorđe Žikelić
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.