Solving Infinite-State Games via Acceleration

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.