Decidability of well-connectedness for distributed synthesis

Although the synthesis problem is often undecidable for distributed, synchronous systems, it becomes decidable for the subclass of uniformly well-connected (UWC) architectures, provided that only robust specifications are considered. It is then an important issue to be able to decide whether a given architecture falls in this class. This is the problem addressed in this paper: we establish the decidability and precise complexity of checking this property. This problem is in EXPSPACE and NP-hard in the general case, but falls into PSPACE when restricted to a natural subclass of architectures.

► The problem we study is motivated by the synthesis problem for distributed systems.
► We study the class of UWC architectures (giving decidability results for the previous problem).
► This leads to look carefully at the information flow in such architectures.
► We show that deciding if an architecture is UWC is decidable, and give its complexity.