Two-player graph games have found numerous applications, most notably the synthesis of reactive systems from temporal specifications, where they are successfully used to generate finite-state systems. Due to their relevance for practical applications, reactive synthesis of infinite-state systems, and hence the need for techniques for solving infinite-state games, have attracted attention in recent years. We propose novel semi-algorithms for solving infinite-state games with $\omega$-regular winning conditions. The novelty lies in the utilization of an acceleration technique that is helpful in avoiding divergence. The key idea is to enhance the game-solving algorithm with the ability to use combinations of simple inductive arguments in order to summarize unbounded iterations of strategic decisions in the game. This enables our method to solve games on which state-of-the-art techniques diverge, as we demonstrate in the evaluation of a prototype implementation.

翻译：双人图博弈已广泛应用于诸多领域，最显著的是根据时序规范综合反应式系统，并成功用于生成有限状态系统。由于其在实际应用中的重要性，近年来无穷状态系统的反应式综合（进而对无穷状态博弈求解技术的需求）引起了广泛关注。我们提出了求解具有ω-正则获胜条件的无穷状态博弈的新型半算法。其创新之处在于利用加速技术来有效避免发散。核心思想是对博弈求解算法进行增强，使其能够组合使用简单归纳论证来概括博弈中策略决策的无界迭代过程。原型实现的评估表明，该方法能够求解现有前沿技术无法收敛的博弈问题。