Logic in Computer Science (LICS 2005)

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}
  }