Distributed Synthesis for Acyclic Architectures

Authors Anca Muscholl, Igor Walukiewicz

Thumbnail PDF


  • Filesize: 2.46 MB
  • 13 pages

Document Identifiers

Author Details

Anca Muscholl
Igor Walukiewicz

Cite AsGet BibTex

Anca Muscholl and Igor Walukiewicz. Distributed Synthesis for Acyclic Architectures. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 639-651, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


The distributed synthesis problem is about constructing correct distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendez-vous (Zielonka automata). We show decidability of the synthesis problem for all omega-regular local specifications, under the restriction that the communication graph of the system is acyclic. This result extends a previous decidability result for a restricted form of local reachability specifications.
  • Distributed synthesis
  • distributed control
  • causal memory


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. A. Arnold, A. Vincent, and I. Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science, 303(1):7-34, 2003. Google Scholar
  2. Julian Bradfield and Colin Stirling. Modal mu-calculi. In P. Blackburn, J. van Benthem, and F. Wolter, editors, The Handbook of Modal Logic, pages 721-756. Elsevier, 2006. Google Scholar
  3. Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri games: Synthesis of distributed systems with causal memory. In Proc. of GandALF, EPTCS, pages 217-230, 2014. Google Scholar
  4. Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In LICS, pages 321-330, 2005. Google Scholar
  5. Paul Gastin, Benjamin Lerman, and Marc Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In FSTTCS, volume 3328 of LNCS, pages 275-286, 2004. Google Scholar
  6. Paul Gastin and Nathalie Sznajder. Fair synthesis for asynchronous distributed systems. ACM Transactions on Computational Logic, 2013. Google Scholar
  7. Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Asynchronous games over tree architectures. In Proceedings of ICALP'13, 2013. Google Scholar
  8. Susanne Graf, Doron Peled, and Sophie Quinton. Achieving distributed control through model checking. Formal Methods in System Design, 40(2):263-281, 2012. Google Scholar
  9. Julian Gutierrez and Glynn Winskel. Borel determinacy of concurrent games. In Proceedings of CONCUR'13, 2013. Google Scholar
  10. O. Kupferman and M. Y. Vardi. Synthesizing distributed systems. In LICS, 2001. Google Scholar
  11. P. Madhusudan and P. S. Thiagarajan. Distributed control and synthesis for local specifications. In ICALP'01, volume 2076 of LNCS, pages 396-407. Springer, 2001. Google Scholar
  12. P. Madhusudan, P. S. Thiagarajan, and S. Yang. The MSO theory of connectedly communicating processes. In FSTTCS, volume 3821 of LNCS, pages 201-212, 2005. Google Scholar
  13. Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. TCS, 358(2-3):200-228, 2006. Google Scholar
  14. Madhavan Mukund and Milind A. Sohoni. Keeping Track of the Latest Gossip in a Distributed System. Distributed Computing, 10(3):137-148, 1997. Google Scholar
  15. Anca Muscholl and Sven Schewe. Unlimited decidability of distributed synthesis with limited missing knowledge. In Proceedings of MFCS'13, 2013. Google Scholar
  16. A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In 31th IEEE Symposium Foundations of Computer Science (FOCS 1990), pages 746-757, 1990. Google Scholar
  17. P. J. G. Ramadge and W. M. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77(2):81-98, 1989. Google Scholar
  18. Igor Walukiewicz. Pushdown processes: Games and model checking. Information and Computation, 164(2):234-263, 2001. Google Scholar
  19. W. Zielonka. Notes on finite asynchronous automata. RAIRO-Theoretical Informatics and Applications, 21:99-135, 1987. Google Scholar