c773b13f6d21246a.tex
1: \begin{abstract}
2: 
3: Two-player graph games have found numerous applications,  most notably in the synthesis of reactive systems from temporal specifications, but also in verification.
4: The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games.
5: 
6: We propose novel  symbolic semi-algorithms for solving infinite-state games with temporal winning conditions.
7: 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.
8: 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. 
9: Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations.
10: 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.
11: Ours is the  first method for solving infinite-state games to employ acceleration.
12: 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.
13: 
14: \end{abstract}
15: