Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
summary
Automated procedure synthesizes an abstract representative process from a fair-CTL local specification using a modified tableau that adds interference transitions; synthesis cost is exponential in spec length while concretizing and instantiating costs are linear in K. Method uses counting abstraction to remove dependence on k, concretization guarantees any resulting instance (any k and arbitrarily large K) satisfies the original global property. Rewriting and abstraction steps remain manual and some neighbor-parameterized eventualities and non-Boolean data are unsupported.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:59Problem overview
- 3:47Running example
- 8:34Specification rewriting
- 17:40Tableau construction
- 21:17Applications
- 23:04Future work & Q&A
related talks
27mParameterized Infinite-State Reactive Synthesis
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
23mA Synthetic Reconstruction of Multiparty Session Types
16mParameterized Verification of Disjunctive Timed Networks
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
35mSymmetry-Preserving Finite Synthesis and Amalgamation
42mTime-sensitive protocol: Links From Design to Implementation
13mCharacterizing Implementability of Global Protocols with Infinite States and Data