Automated Approach for Solving Infinite-state Polynomial Reachability Games
Researchers have developed an automated algorithm for solving infinite-state polynomial reachability games, a class of two-player strategic games with applications in AI and reactive synthesis. The approach introduces ranking certificates as a formal proof mechanism and demonstrates the ability to solve previously intractable problems, including computing optimal strategies for the classical Cinderella-Stepmother game.