Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications

Learn about a methodology for synthesizing parametric distributed systems in this 24-minute conference talk from VMCAI 2025. Explore how researchers Ruoxi Zhang, Richard Trefler, and Kedar Namjoshi tackle the challenge of constructing scalable protocol instances where both the number of isomorphic components (K) and the number of neighbors per component (k) can vary arbitrarily. Discover their innovative approach that leverages locality, symmetry, and abstraction to eliminate parameter dependencies, first by refining system-wide specifications to local temporal specifications, then abstracting away the neighborhood parameter. The presentation demonstrates how their automated synthesis procedure constructs abstract processes that can be concretized for any parameter values while maintaining correctness, with applications shown for atomic snapshot protocols on fully connected networks and dining philosophers protocols on hypercubes. This ACM SIGPLAN-sponsored talk was presented at the VMCAI conference in January 2025.