Solving Infinite-State Games via Acceleration
summary
Presents a new symbolic semi-algorithm that uses acceleration lemmas to force convergence of attractor fixpoint computations that otherwise diverge on infinite-state games. It instantiates uninterpreted-template lemmas by SMT-based synthesis over linear integer/real arithmetic, encodes loop games to prove unbounded iterability, and extracts controllers via simple bookkeeping and function synthesis. A prototype implementation solves benchmark cases that existing abstraction- or lifting-based tools time out on and reports reproducible artifact results.
AI-written summary · about
chapters (13)
- 0:00Infinite-state games intro
- 2:27Why infinite-state games matter
- 3:53Game formalism explained
- 7:00Limitations of existing game-solving techniques
- 8:25Acceleration lemmas role
- 10:10Loop games step checks
- 11:37Extracting executable systems
- 12:41Evaluation and benchmarks
- 14:08Summary and future work
- 14:30Q&A: Learning-based attractors
- 16:17Q&A: Beyond acceleration scope
- 17:21Q&A: Step relation in loops
- 18:05Q&A: Parity and Rabin games
related talks
27mParameterized Infinite-State Reactive Synthesis
20mThe Complexity of Infinite-Horizon General-Sum Stochastic Games
27mRecurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
35mSymmetry-Preserving Finite Synthesis and Amalgamation
15mStructural Abstraction and Refinement for Probabilistic Programs
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...