Reduction theorems for effective parameterized verification of round- based distributed algorithms
summary
Presents reduction theorems that collapse the unbounded round dimension into a bounded sliding window (if round jumps are bounded by B) and encode anonymous processes as counters, reduces rounds to finite sliding window. The parameterized verification problem becomes LTL model checking on a counter system; the pipeline outputs an SMV model and uses NuXmv (IC3) as the backend. Demonstrated on consensus variants and a Raft leader election encoding: properties over all n satisfying resilience (e.g., n>2t) verify fast; limitations: manual translation, requires threshold guards, common/cyclic templates and bounded jump.
AI-written summary · about
chapters (11)
- 0:00Parameterized verification intro
- 13:24Existing verification approaches
- 17:01Challenges in verification
- 19:31New reduction approach
- 21:40Modeling with automata
- 27:07Parameterized semantics
- 29:59History state count logic
- 35:20Reduction steps for model checking
- 45:02Encoding to LTL model checking
- 45:48Experimental validation
- 48:35Conclusion and challenges
related talks
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...
25mProperty-agnostic base case extension for scalable verification of distributed systems
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
29mTowards Scalable Constant-Round MPC from Minimal Assumptions via Round Collapsing
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
16mParameterized Verification of Disjunctive Timed Networks