POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 15:50 - 16:10 at Turing Lecture - Algorithmic Verification Chair(s): Andreas Pavlogiannis

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.

Thu 18 Jan

Displayed time zone: London change

15:30 - 16:50
Algorithmic VerificationPOPL at Turing Lecture
Chair(s): Andreas Pavlogiannis Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk Warsaw University, Bartek Klin University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
Pre-print