Back to the Future: A Fresh Look at Linear Temporal Logic
summary
Claims a single-exponential normalization for LTL (instead of the old non‑elementary blowup), gives rewrite rules that push GF/GF and U/W patterns into a Δ2 normal form, and uses that form to produce much smaller limit-deterministic Büchi automata. Implements the idea in tools (normalizer + the Strix synthesis tool) and reports orders-of-magnitude state reductions (examples where prior constructions produced ~100k states collapse to tiny automata), winning recent synthesis competitions and enabling faster probabilistic verification.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:43What is temporal logic
- 3:38Linear temporal logic
- 7:27Safety progress hierarchy
- 11:14Where to find the proof
- 15:28Automata theoretic approach
- 19:31Technical challenge
- 21:51Algorithmic challenge
- 25:58Back to the Future
- 27:49Alternation Hierarchy
- 31:39Temporal Formulas
- 33:53Normal Form Theorem
- 35:32Maxwell Equations
- 41:11What has changed
- 42:18What is a limit deterministic automaton
- 45:47Comparison
- 47:40Alternating Bush Automata
- 55:58Conclusion
related talks
01h 02mTheory and Control
18mLanguages with Decidable Learning: A Meta-theorem
25mLearning Formulas in Finite Variable Logics
33mA Historical Perspective on Program Transformation and Recent Developments (Invi...
14mHigher-order Automation In TLAPS
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
15mFormulog: Datalog for SMT-Based Static Analysis
35mFlattening Meets Effects: A Surprising Connection