# Solving Infinite-State Games via Acceleration (Full Version)

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 May 2023.

## Built on by (most cited first, 3 of 3)

- [Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis](https://mlsanity.com/paper/2407.09348/) (2024)
- [Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis](https://mlsanity.com/paper/2503.11475/) (2025)
- [Automated Approach for Solving Infinite-state Polynomial Reachability Games](https://mlsanity.com/paper/2605.10169/) (2026)

## Abstract (arXiv)

Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games. We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation.