## Paper: Uniform Distributed Synthesis (at LICS 2005)

Authors:**Bernd Finkbeiner Sven Schewe**

### Abstract

We provide a uniform solution to the problem of synthesizing a finite-state distributed system. An instance of the synthesis problem consists of a system architecture and a temporal specification. The architecture is given as a directed graph, where the nodes represent processes (including the environment as a special process) that communicate synchronously through shared variables attached to the edges. The same variable may occur on multiple outgoing edges of a single node, allowing for the broadcast of data. A solution to the synthesis problem is a collection of finite-state programs for the processes in the architecture, such that the joint behavior of the programs satisfies the specifi- cation in an unrestricted environment. We define information forks, a comprehensive criterion that characterizes all architectures with an undecidable synthesis problem. The criterion is effective: for a given architecture with n processes and v variables, it can be determined in O(n2 · v) time whether the synthesis problem is decidable. We give a uniform synthesis algorithm for all decidable cases. Our algorithm works for all ù-regular tree specification languages, including the µ- calculus. The undecidability proof, on the other hand, uses only LTL or, alternatively, CTL as the specification language. Our results therefore hold for the entire range of specification languages from LTL/CTL to the µ-calculus.

### BibTeX

@InProceedings{FinkbeinerSchewe-UniformDistributedS, author = {Bernd Finkbeiner and Sven Schewe}, title = {Uniform Distributed Synthesis}, booktitle = {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005}, year = 2005, editor = {Prakash Panangaden}, month = {June}, pages = {321--330}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }