Synthesizing Parameterized Protocols from Local Temporal Specifications

Abstract

Reactive systems, such as controllers, web services, communication protocols, and hardware circuits, are computational entities that continuously interact with the environment. Reactive synthesis aims to automatically generate such systems from their temporal specifications. This dissertation focuses on the synthesis of parametric, distributed reactive systems composed of copies of interacting processes that collectively satisfy global correctness specifications, under the assumption that the scheduler fairly selects processes for execution. The number of component processes thus serves as a natural parameter for such scalable systems that can handle increasing workloads by structurally adding more components without requiring the redesign of the entire system.

Parametric systems induce local symmetries, as they are constructed from a small, finite number of process types instantiated across potentially large underlying networks. To alleviate state explosion, we synthesize a representative process for each process type from its local specification instead of synthesizing the global product machine. We express the local specification as a temporal formula that describes the behavior of the process in its neighborhood. We begin by considering fixed neighborhood topologies, such as token rings, meshes, and tori, and then extend our approach to protocols with parametric neighborhood configurations, including hypercubes and fully connected networks. We manually formulate the local specifications and introduce a specification rewriting transformation based on counter abstraction that approximates parametric neighborhoods while preserving the context required for concretization of abstract models. The rewriting step supports both local safety and local liveness properties parameterized by the number of neighbors.

A key challenge in synthesis from local specifications is that the neighboring processes are unknown before the representatives are constructed. To address this challenge, we propose a local, iterative synthesis methodology that incrementally infers interference caused by the neighbors based on representative transitions constructed so far. Our approach adapts a tableau-based decision procedure for Fair CTL specifications and a game-theoretic approach for LTL specifications. We show that the iterative construction eventually converges to a fixpoint, at which no further interactions can be added. The approach then prunes the resulting structure to extract a representative model that can be instantiated at the corresponding network nodes to form system instances of arbitrary network sizes and neighborhood configurations, with synthesis cost independent of these parameters. We evaluate the local synthesis approach on various example protocols, including the dining philosophers, leader election, producer-consumer, and others.