Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
summary
Presents a concrete criterion that turns uniqueness of least fixed points into a usable lower-bound proof: existence of a U-ranking supermartingale plus a postfixed candidate L implies L is a lower bound. Implements a template-based checker MuVal QFL that encodes polynomial templates, hands constraints to Polytool, and verifies all exact-barrier benchmarks from the literature; harder approximate cases succeed with configuration tweaks. Method handles termination probability, expected runtime, higher moments, and conditional preexpectations.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:23Quantitative verification
- 3:31Fixed point characterization
- 5:18Lower bound challenges
- 6:03Fixed point uniqueness
- 8:33Ranking supermartingales
- 11:00Lower bound theorem
- 12:29Random walk example
- 13:32Approach generality
- 14:36Extending with under-approximation
- 15:59MuVal QFL tool
- 18:51Limitations and future work
- 19:11Summary
- 19:33Q&A: Fixed point uniqueness
- 20:16Q&A: Theorem assumptions
related talks
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
48mBeyond SAT - Proofs for QBF, and more
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
59mExact Performance Verification of First‑Order Methods in Parametric Convex Optimization
01h 16mIn Search of the Hard Instances
14mA Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and(…)
34mWeak Versions of Extended Resolution
58mA New Perspective on Commutativity in Verification