Uniform Distributed Synthesis

12 years 7 months ago
Uniform Distributed Synthesis
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 specification 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) t...
Bernd Finkbeiner, Sven Schewe
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where LICS
Authors Bernd Finkbeiner, Sven Schewe
Comments (0)