Please note: This PhD seminar will take place online.
Ruoxi Zhang, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Richard Trefler
In this talk, we present an algorithmic method to assist with the construction of correct-by-design distributed protocols. Such protocols are typically parameterized by the number of participating processes. They also exhibit local symmetry, as every protocol instance is constructed from one or more representative process templates. We assume that the protocol specification has been refined (possibly manually) to a local specification for each representative. The task is then to construct a set of representatives that satisfies those local specifications under interference from neighboring instances of the same set of representatives. The self-referential interference constraint poses a central difficulty for synthesis.
We show how to synthesize representatives that are parameterized by a possibly unbounded number of neighbors, from specifications in linear-time temporal logic (LTL) that may include parameterized liveness properties. That is a substantial improvement over prior methods, which work with a bounded neighborhood or for restricted branching-time specifications. Parameterized neighborhoods are handled through a counting-based specification abstraction. LTL is handled by a modification of the standard game-theoretic synthesis method that builds in the interference-closure requirement. Each synthesized representative has a finite-state skeleton, but with state transitions that can be concretized to any number of neighbors. By construction, every protocol instance formed from the synthesized representatives meets the protocol specification.