Stratified Guarded First-Order Transition Systems
summary
Defines a class of first-order transition systems that is stratified and strictly guarded, shows weakest-precondition fixpoint iteration eliminates existentials via second-order quantifier elimination and therefore stays within universal first-order formulas, and proves the iteration terminates with a bounded number of universals. Decision procedure: with an initial hypothesis in Bernays-Schönfinkel form, universal safety invariants are decidable. Demonstrates the conference-management example fits the restrictions, so the method succeeds there.
AI-written summary · about
chapters (11)
- 0:00First-order transition systems
- 1:35Parametric systems
- 3:17Invariant verification
- 6:27Fixpoint iteration challenges
- 7:23IVY verification approach
- 8:57Abstract interpretation
- 11:10Second-order quantifier elimination
- 13:11Guarded stratified systems
- 15:23Fixpoint iteration termination
- 17:29Conference management case
- 18:12Conclusion
related talks
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
16mParameterized Verification of Disjunctive Timed Networks
25mStep-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
46mPropagators