Automated Approach for Solving Infinite-state Polynomial Reachability Games

A new paper on arXiv presents an automated method for solving infinite-state polynomial reachability games. Reachability games involve two players, REACH and SAFE, where REACH aims to reach a target set while SAFE tries to avoid it. These games have applications in AI and reactive synthesis, often involving infinite-state graphs. The study focuses on turn-based games over real variable valuations. The authors propose ranking certificates as a sound and complete proof rule for determining if REACH has a winning strategy. They also consider polynomial reachability games with transitions and objectives defined by polynomials. The paper introduces an automated approach for solving such games, contributing to the theory of infinite-state games.