Solving Infinite-State Games via Acceleration

Explore a groundbreaking approach to solving infinite-state games with temporal winning conditions in this 19-minute video presentation from POPL 2024. Delve into the novel symbolic semi-algorithms proposed by Philippe Heim and Rayna Dimitrova from CISPA Helmholtz Center for Information Security. Learn how their acceleration technique enhances fixpoint-based game-solving methods, potentially leading to convergence in cases where existing algorithms require infinite iterations. Discover how this method, the first to employ acceleration for infinite-state games, outperforms state-of-the-art techniques on various benchmarks. Gain insights into the applications of two-player graph games in reactive system synthesis and verification, and understand the significance of this research for infinite-state systems.

[POPL'24] Solving Infinite-State Games via Acceleration