Distributed synthesis for synchronous systems
Paul Gastin
LSV, ENS de Cachan, France.
06-12-06

---

Abstract

Given a distributed architecture and a specification, the distributed synthesis consists in finding a local program for each process of the system so that the joint behavior of the distributed system meets the specification. This problem depends on several parameters: the class of architectures under consideration, the semantics used for the behaviors, the specification language, and the type of memory allowed for the controllers. Pnueli and Rosner proved that the distributed synthesis problem is undecidable for very simple architectures and a synchronous semantics. Most undecidability results are based on the fact that the specification constrains variables that are not connected in the architecture.

Here, we introduce the notion of uniformly well-connected (UWC) architectures. We give a decidability criterium for the distributed synthesis on UWC architectures. We also show that this condition is not sufficient if we loosen slightly the connectedness assumption. Finally, we define robust specifications and show that they are decidable for all UWC architectures.

Joint work with Nathalie Sznajder and Marc Zeitoun.