Document Open Access Logo

Symmetric Synthesis

Authors Rüdiger Ehlers, Bernd Finkbeiner

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.26.pdf
  • Filesize: 0.52 MB
  • 13 pages

Document Identifiers

Author Details

Rüdiger Ehlers
Bernd Finkbeiner

Cite As Get BibTex

Rüdiger Ehlers and Bernd Finkbeiner. Symmetric Synthesis. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 26:1-26:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.26

Abstract

We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is an important goal in the design of distributed systems, because systems that are composed from identical components are easier to build and maintain. We show that for the class of rotation-symmetric architectures, i.e., multi-process architectures where all processes have access to all system inputs, but see different rotations of the inputs, the symmetric synthesis problem is EXPTIME-complete in the number of processes. In architectures where the processes do not have access to all input variables, the symmetric synthesis problem becomes undecidable, even in cases where the standard distributed synthesis problem is decidable.

Subject Classification

Keywords
  • Reactive Synthesis
  • Symmetry

Metrics

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

References

  1. Dana Angluin. Local and global properties in networks of processors (extended abstract). In Twelfth Annual ACM Symposium on Theory of Computing (STOC), pages 82-93, 1980. Google Scholar
  2. Paul C. Attie and E. Allen Emerson. Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst., 20(1):51-115, 1998. URL: http://dx.doi.org/10.1145/271510.271519.
  3. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. Google Scholar
  4. E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999. Google Scholar
  5. Shimon Cohen, Daniel J. Lehmann, and Amir Pnueli. Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Theor. Comput. Sci., 34:215-225, 1984. Google Scholar
  6. Rüdiger Ehlers. Symmetric and efficient synthesis. PhD thesis, Saarland University, 2013. URL: http://scidok.sulb.uni-saarland.de/volltexte/2013/5607/.
  7. Rüdiger Ehlers and Bernd Finkbeiner. Symmetric synthesis. ArXiV/CoRR, 1710.05633, 2017. Full version of this paper. Google Scholar
  8. E. Allen Emerson and Jai Srinivasan. A decidable temporal logic to reason about many processes. In Proc. PODC, pages 233-246, 1990. Google Scholar
  9. Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In Proc. LICS, pages 321-330, 2005. Google Scholar
  10. Jörg Flum, Erich Grädel, and Thomas Wilke, editors. Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games. Amsterdam University Press, 2008. Google Scholar
  11. Swen Jacobs and Roderick Bloem. Parameterized synthesis. Logical Methods in Computer Science, 10(1), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(1:12)2014.
  12. Ralph E. Johnson and Fred B. Schneider. Symmetry and similarity in distributed systems. In Proc. PODC, pages 13-22. ACM, 1985. Google Scholar
  13. Evangelos Kranakis. Invited talk: Symmetry and computability in anonymous networks. In Nicola Santoro and Paul G. Spirakis, editors, Proc. SIROCCO, pages 1-16. Carleton Scientific, 1996. Google Scholar
  14. Orna Kupferman and Moshe Y. Vardi. Synthesis with incomplete information. In Proc. ICTL, 1997. Google Scholar
  15. Orna Kupferman and Moshe Y. Vardi. μ-calculus synthesis. In Proc. MFCS, pages 497-507, 2000. Google Scholar
  16. Orna Kupferman and Moshe Y. Vardi. Synthesizing distributed systems. In 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), July 2001. Google Scholar
  17. Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. In FOCS, pages 531-542. IEEE, 2005. Google Scholar
  18. Daniel J. Lehmann and Michael O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In Proc. POPL, 1981. Google Scholar
  19. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977. Google Scholar
  20. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors, ICALP, volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer, 1989. Google Scholar
  21. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In FOCS, volume II, pages 746-757. IEEE, 1990. Google Scholar
  22. Michael O. Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, 1972. Google Scholar
  23. Desh Ranjan, Richard Chang, and Juris Hartmanis. Space bounded computations: Review and new separation results. Theor. Comput. Sci., 80(2):289-302, 1991. URL: http://dx.doi.org/10.1016/0304-3975(91)90391-E.
  24. Sven Schewe and Bernd Finkbeiner. Bounded synthesis. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, ATVA, volume 4762 of Lecture Notes in Computer Science, pages 474-488. Springer, 2007. Google Scholar
  25. Pierre Wolper. Synthesis of Communicating Processes from Temporal-Logic Specifications. PhD thesis, Stanford University, 1982. Google Scholar
  26. Masafumi Yamashita and Tiko Kameda. Computing on an anonymous network. In Proc. PODC, pages 117-130, 1988. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact