Compositional Verification of Stigmergic Collective Systems
summary
Claim: compositional verification plus a lightweight static value analysis tames state-space explosion for stigmergic agent systems. Implementation encodes Labs→LNT processes, uses CADP compositional tools with root‑leaf reduction modulo simulation, and inserts a value‑analysis filter that limits variables (e.g., leader ∈ 0..n). Experiments (leader election, two‑phase commit, flocking) show sequential baseline wins for tiny instances but blows up at 6→7 agents, while compositional + value pruning scales far better in time and memory.
AI-written summary · about
chapters (8)
- 0:00Stigmergic collective systems
- 3:54Labs language and stigmergy
- 8:57Encoding Labs systems
- 14:37State space generation with root-leaf reduction
- 17:10Value analysis for state pruning
- 19:24Comparison with sequential verification
- 22:47Summary and future research
- 24:11Q&A
related talks
25mProperty-agnostic base case extension for scalable verification of distributed systems
22mCompositional Programming and Testing of Dynamic Distributed Systems
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
16mIgloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
39mCompositional protocol (..) communicating actors
28mReasoning about Distributed Reconfigurable Systems
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...