Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
summary
Framework that reduces parameterized systems to a finite 01 counter abstraction and proves reachability, coverability and target properties are decidable iff their 0/1 image is reachable. Uses a refined 01 well-quasi order with forward/backward compatibility as the technical criterion; if a counter system satisfies compatibility and is polynomially abstractable then the cardinality-reachability problem is decidable in PSPACE. Captures lossy broadcast, disjunctive guards, synchronizations, fixed shared variables, adds guarded synchronization and a single-controller extension.
AI-written summary · about
chapters (19)
- 0:00Parameterized verification intro
- 1:03Motivation for parameterized systems
- 2:47Parameterized model checking
- 4:54Known results in verification
- 7:46Lossy broadcast and guards
- 9:35Simple synchronization
- 10:41Proof techniques overview
- 11:0301 counter abstraction intro
- 13:29Precision of 01 abstraction
- 14:12Well-quasi orders in verification
- 17:06Compatibility with well-quasi orders
- 19:15Decidability via 01 abstraction
- 20:54Cardinality reachability
- 22:56Main result and complexity
- 23:40Beyond guarded synchronization
- 25:28Unified framework summary
- 26:10Subclass with better complexity
- 26:33Conclusion and future work
- 27:14Q&A
related talks
15mStructural Abstraction and Refinement for Probabilistic Programs
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
20mStratified Guarded First-Order Transition Systems
16mParameterized Verification of Disjunctive Timed Networks
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
21mMechanizing the CMP Abstraction for Parameterized Verification
15mProducts of Recursive Programs for Hypersafety Verification