Characterizing Implementability of Global Protocols with Infinite States and Data
summary
Provides a semantic characterization that reduces implementability of symbolic global protocols to (co)reachability checks per participant and a set of concrete coherence conditions that capture when locally indistinguishable states force impossible choices. Builds a symbolic decision procedure via a muCLP reduction (least and greatest fixpoints over a background theory), proves decidability and complexity bounds: finite explicit cases are co-NP-complete, boolean symbolic cases are PSPACE-complete. Implements the reduction and mechanizes the preciseness theorem in the rock prover.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:09Global protocols implementability
- 4:36Implementability with CLTS
- 5:39Information asymmetry
- 7:23Concrete runs indistinguishability
- 8:50Coherence conditions
- 10:35Synthesis and complexity
- 10:55Conclusion
- 11:22Q&A
related talks
20mImplementability of Global Distributed Protocols Modulo Network Architectures
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
45mCorrectness proofs of distributed systems with Isabelle
25mProperty-agnostic base case extension for scalable verification of distributed systems
21mTowards composable proofs of cache coherence protocols
21mMechanizing the CMP Abstraction for Parameterized Verification
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...