Please note: This PhD defence will take place in DC 2310.
Ruoxi Zhang, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Richard Trefler
Reactive systems, such as controllers, web services, communication protocols, and hardware circuits, are computational entities that continuously interact with their environment. Reactive synthesis studies the automatic construction of 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 the global correctness specifications under fair scheduling. Such systems induce local symmetries, as they are constructed from a finite number of process types instantiated across potentially large underlying networks. Instead of synthesizing global product machines, we synthesize a representative process for each process type from its local specification, which describes the process behavior in its neighborhood.
We start by considering fixed neighborhood topologies, such as rings, meshes, and tori, and then extend the work 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 model concretization. The rewriting step supports both local safety and liveness properties parameterized by the number of neighbors.
A key challenge is that the neighbors are unknown before the representatives are constructed. To address this, we propose an iterative synthesis framework that incrementally infers neighboring interferences from partially constructed process transitions. Our framework adapts a tableau-based decision procedure for Fair CTL specifications and a game-theoretic approach for LTL specifications. We show that the construction converges to a fixpoint structure from which representative processes can be extracted and instantiated across networks. The cost of synthesis is independent of the network size and neighborhood configuration.