A Hierarchy of Supermartingales for ω-Regular Verification
summary
Defines four new certificate classes and proves a strict hierarchy: GSSMs complete for positive recurrence, DVSSMs complete for null recurrence and the most powerful, and LexPMSMs equal in power to LexGSSMs but often smaller. Uses least-fixed-point characterisations and lexicographic/stochastic orders, provides a template-based synthesiser with polynomial templates and an algorithm that picks lexicographic depth automatically, and reports a prototype that synthesises certificates for examples that Streett supermartingales cannot, matching the theoretical ordering.
AI-written summary · about
chapters (12)
- 0:00ω-regular verification intro
- 1:01Problem definition examples
- 2:49State supermartingales technique
- 4:59Limitations of strict supermartingales
- 6:02Supermartingale hierarchy
- 8:16Generalized state supermartingales
- 9:41Positive recurrence competence
- 11:05Lexicographic and distribution-valued SMs
- 12:54Soundness completeness of DVSSM
- 14:17Supermartingales for parity
- 15:44Implementation experimental results
- 17:08Conclusion open questions
related talks
23mHigher-Order MSL Horn Constraints
18mVerifying Solutions to Semantics-Guided Synthesis Problems
27mBig Steps in Higher-Order Mathematical Operational Semantics
30mRelatively Complete Verification of Probabilistic Programs
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
24mBounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
47mIsomorph-Free Generation Of Combinatorial Objects With Sat Modulo Symmetries
18mEquivalence and Similarity Refutation for Probabilistic Programs