CISPA
Browse
3632899.pdf (424.61 kB)

Solving Infinite-State Games via Acceleration

Download (424.61 kB)
journal contribution
posted on 2024-02-28, 08:35 authored by Philippe HeimPhilippe Heim, Rayna DimitrovaRayna Dimitrova
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.

History

Primary Research Area

  • Reliable Security Guarantees

Journal

Proceedings of the ACM on Programming Languages

Volume

8

Page Range

1696-1726

Publisher

Association for Computing Machinery (ACM)

Open Access Type

  • Not Open Access

Sub Type

  • Article

BibTeX

@article{Heim:Dimitrova:2024, title = "Solving Infinite-State Games via Acceleration", author = "Heim, Philippe" AND "Dimitrova, Rayna", year = 2024, month = 1, journal = "Proceedings of the ACM on Programming Languages", number = "POPL", pages = "1696--1726", publisher = "Association for Computing Machinery (ACM)", issn = "2475-1421", doi = "10.1145/3632899" }