Distributed Synthesis for Well-Connected Architectures

Abstract. We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.

• Type: Conference
• Year: 2006
• Where: FSTTCS
• Authors: Paul Gastin, Nathalie Sznajder, Marc Zeitoun
• Keywords: Architectures, FSTTCS 2006, Output Variables, Software Engineering, Synthesis Problem