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 $\omega$-regular 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.

翻译：双人图博弈在众多领域有着广泛应用，最突出的是基于时序规约的反应式系统合成，在验证领域同样如此。无限状态系统在这些领域中的重要性，促使研究人员高度重视开发求解无限状态博弈的技术。我们提出了新颖的符号化半算法，用于求解带有$\omega$-正则获胜条件的无限状态博弈。我们方法的创新之处在于引入了一种加速技术，该技术能增强基于不动点的博弈求解方法，并有助于避免发散问题。经典的基于不动点的算法在应用于无限状态博弈时，在很多情况下必然会发散，因为这些算法会迭代计算某一玩家拥有获胜策略的状态集合。我们所提出的方法能够在现有算法需要无限次迭代才能收敛的情况下实现收敛。这是通过加速技术实现的：计算一个无限的状态集合，从中可以无限次迭代一个更简单的子策略，从而赢得博弈。我们提出的方法是首个采用加速技术求解无限状态博弈的方法。正因如此，在众多基准测试中，它能超越现有最先进的技术，我们对原型实现的评估也证明了这一点。