Document Open Access Logo

Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory

Authors Bernd Finkbeiner , Manuel Gieseking , Jesko Hecking-Harbusch , Ernst-Rüdiger Olderog

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.20.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Bernd Finkbeiner
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Manuel Gieseking
  • University of Oldenburg, Germany
Jesko Hecking-Harbusch
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Ernst-Rüdiger Olderog
  • University of Oldenburg, Germany

Funding

Supported by the German Research Foundation (DFG) Grant Petri Games (392735815) and Collaborative Research Center "Foundations of Perspicuous Software Systems" (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (683300).

Cite As Get BibTex

Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.20

Abstract

In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components. 
In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Synthesis
  • distributed systems
  • reactive systems
  • Petri games
  • decidability

Metrics

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

Related Versions

References

  1. Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating asynchronous games for distributed synthesis. In 30th International Conference on Concurrency Theory, CONCUR, volume 140 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.26.
  2. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Acacia+, a tool for LTL synthesis. In Computer Aided Verification - 24th International Conference, CAV, volume 7358 of Lecture Notes in Computer Science. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_45.
  3. Krishnendu Chatterjee and Monika Henzinger. An O(n²) time algorithm for alternating Büchi games. In Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA. SIAM, 2012. URL: https://doi.org/10.1137/1.9781611973099.109.
  4. Rüdiger Ehlers. Unbeast: Symbolic bounded synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS, volume 6605 of Lecture Notes in Computer Science. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19835-9_25.
  5. Joost Engelfriet. Branching processes of Petri nets. Acta Informatica, 28(6), 1991. URL: https://doi.org/10.1007/BF01463946.
  6. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77426-6.
  7. Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of bounded synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS, volume 10205 of Lecture Notes in Computer Science, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_20.
  8. Bernd Finkbeiner. Bounded synthesis for Petri games. In Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, volume 9360 of Lecture Notes in Computer Science. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23506-6_15.
  9. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Symbolic vs. bounded synthesis for Petri games. In Sixth Workshop on Synthesis, SYNT@CAV, volume 260 of EPTCS, 2017. URL: https://doi.org/10.4204/EPTCS.260.5.
  10. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Model checking data flows in concurrent network updates. In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA, volume 11781 of Lecture Notes in Computer Science. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_30.
  11. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. AdamMC: A model checker for Petri nets with transits against Flow-LTL. In Computer Aided Verification - 32nd International Conference, CAV, volume 12225 of Lecture Notes in Computer Science. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_5.
  12. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Global winning conditions in synthesis of distributed systems with causal memory (Full Version). CoRR, abs/2107.09280, 2021. URL: http://arxiv.org/abs/2107.09280.
  13. Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog. Adam: Causality-based synthesis of distributed systems. In Computer Aided Verification - 27th International Conference, CAV, volume 9206 of Lecture Notes in Computer Science. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_25.
  14. Bernd Finkbeiner and Paul Gölz. Synthesis in distributed environments. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 93 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28.
  15. Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri games: Synthesis of distributed systems with causal memory. Inf. Comput., 253, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.006.
  16. Paul Gastin, Benjamin Lerman, and Marc Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In FSTTCS: Foundations of Software Technology and Theoretical Computer Science, volume 3328 of Lecture Notes in Computer Science. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_23.
  17. Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Asynchronous games over tree architectures. In Automata, Languages, and Programming - 40th International Colloquium, ICALP, volume 7966 of Lecture Notes in Computer Science. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_26.
  18. Manuel Gieseking, Jesko Hecking-Harbusch, and Ann Yanich. A web interface for Petri nets with transits and Petri games. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS, volume 12652 of Lecture Notes in Computer Science. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_22.
  19. Hugo Gimbert. On the control of asynchronous automata. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 93 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.30.
  20. Ursula Goltz and Wolfgang Reisig. The non-sequential behavior of Petri nets. Inf. Control., 57(2/3), 1983. URL: https://doi.org/10.1016/S0019-9958(83)80040-0.
  21. Jesko Hecking-Harbusch and Niklas O. Metzger. Efficient trace encodings of bounded synthesis for asynchronous distributed systems. In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA, volume 11781 of Lecture Notes in Computer Science. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_22.
  22. Jesko Hecking-Harbusch and Leander Tentrup. Solving QBF by abstraction. In Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF, volume 277 of EPTCS, 2018. URL: https://doi.org/10.4204/EPTCS.277.7.
  23. Swen Jacobs, Roderick Bloem, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Philipp J. Meyer, Thibaud Michaud, Mouhammad Sakr, Salomon Sickert, Leander Tentrup, and Adam Walker. The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR, abs/1904.07736, 2019. URL: http://arxiv.org/abs/1904.07736.
  24. Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, and Roderick Bloem. Anzu: A tool for property synthesis. In Computer Aided Verification, 19th International Conference, CAV, volume 4590 of Lecture Notes in Computer Science. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_29.
  25. Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57(1-2), 2020. URL: https://doi.org/10.1007/s00236-019-00349-3.
  26. P. Madhusudan and P. S. Thiagarajan. A decidable class of asynchronous distributed controllers. In CONCUR - Concurrency Theory, volume 2421 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45694-5_11.
  27. P. Madhusudan, P. S. Thiagarajan, and Shaofa Yang. The MSO theory of connectedly communicating processes. In FSTTCS: Foundations of Software Technology and Theoretical Computer Science, volume 3821 of Lecture Notes in Computer Science. Springer, 2005. URL: https://doi.org/10.1007/11590156_16.
  28. José Meseguer, Ugo Montanari, and Vladimiro Sassone. Process versus unfolding semantics for place/transition Petri nets. Theor. Comput. Sci., 153(1&2), 1996. URL: https://doi.org/10.1016/0304-3975(95)00121-2.
  29. Thibaud Michaud and Maximilien Colange. Reactive synthesis from LTL specification with Spot. In 7th Workshop on Synthesis, SYNT@CAV, 2018. Google Scholar
  30. Anca Muscholl. Automated synthesis of distributed controllers. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP, volume 9135 of Lecture Notes in Computer Science. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_2.
  31. Anca Muscholl and Igor Walukiewicz. Distributed synthesis for acyclic architectures. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS, volume 29 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.639.
  32. Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, Part I. Theor. Comput. Sci., 13, 1981. URL: https://doi.org/10.1016/0304-3975(81)90112-2.
  33. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science FOCS. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  34. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science FOCS. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/FSCS.1990.89597.
  35. Emil L. Post. A variant of a recursively unsolvable problem. Bull. Am. Math. Soc., 52(4), 1946. Google Scholar
  36. John H. Reif. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci., 29(2), 1984. URL: https://doi.org/10.1016/0022-0000(84)90034-5.
  37. Wolfgang Reisig. Petri Nets: An Introduction, volume 4 of EATCS Monographs on Theoretical Computer Science. Springer, 1985. URL: https://doi.org/10.1007/978-3-642-69968-9.
  38. Sven Schewe. Distributed synthesis is simply undecidable. Inf. Process. Lett., 114(4), 2014. URL: https://doi.org/10.1016/j.ipl.2013.11.012.
  39. Wieslaw Zielonka. Notes on finite asynchronous automata. ITA, 21(2), 1987. URL: https://doi.org/10.1051/ita/1987210200991.
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