Document Open Access Logo

Translating Asynchronous Games for Distributed Synthesis

Authors Raven Beutner, Bernd Finkbeiner, Jesko Hecking-Harbusch

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.26.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Raven Beutner
  • Saarland University, Saarbrücken, Germany
Bernd Finkbeiner
  • Saarland University, Saarbrücken, Germany
Jesko Hecking-Harbusch
  • Saarland University, Saarbrücken, Germany

Funding

Supported by the German Research Foundation (DFG) Grant Petri Games (392735815) and the 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

Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.26

Abstract

In distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka’s asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question.
In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of the two game types based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations allow to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
Keywords
  • synthesis
  • distributed systems
  • causal memory
  • Petri games
  • control games

Metrics

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

Related Versions

References

  1. Cyril Autant and Philippe Schnoebelen. Place Bisimulations in Petri Nets. In Proceedings of Application and Theory of Petri Nets, pages 45-61, 1992. URL: https://doi.org/10.1007/3-540-55676-1_3.
  2. Eike Best, Raymond R. Devillers, Astrid Kiehn, and Lucia Pomello. Concurrent Bisimulations in Petri Nets. Acta Inf., 28(3):231-264, 1991. URL: https://doi.org/10.1007/BF01178506.
  3. Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis (Full Version). arXiv preprint, 2019. URL: http://arxiv.org/abs/1907.00829.
  4. J. Richard Buchi and Lawrence H. Landweber. Solving sequential conditions by finite state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  5. Joost Engelfriet. Branching Processes of Petri Nets. Acta Inf., 28(6):575-591, 1991. URL: https://doi.org/10.1007/BF01463946.
  6. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77426-6.
  7. Bernd Finkbeiner. Bounded Synthesis for Petri Games. In Proceedings of Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pages 223-237, 2015. URL: https://doi.org/10.1007/978-3-319-23506-6_15.
  8. Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Symbolic vs. Bounded Synthesis for Petri Games. In Proceedings of SYNT@CAV, pages 23-43, 2017. URL: https://doi.org/10.4204/EPTCS.260.5.
  9. Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog. Adam: Causality-Based Synthesis of Distributed Systems. In Proceedings of CAV, pages 433-439, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_25.
  10. Bernd Finkbeiner and Paul Gölz. Synthesis in Distributed Environments. In Proceedings of FSTTCS, pages 28:1-28:14, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28.
  11. Bernd Finkbeiner and Ernst-Rüdiger Olderog. Petri games: Synthesis of distributed systems with causal memory. Inf. Comput., 253:181-203, 2017. URL: https://doi.org/10.1016/j.ic.2016.07.006.
  12. Paul Gastin, Benjamin Lerman, and Marc Zeitoun. Distributed Games with Causal Memory Are Decidable for Series-Parallel Systems. In Proceedings of FSTTCS, pages 275-286, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_23.
  13. Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Asynchronous Games over Tree Architectures. In Proceedings of ICALP, pages 275-286, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_26.
  14. Hugo Gimbert. On the Control of Asynchronous Automata. In Proceedings of FSTTCS, pages 30:1-30:15, 2017. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.30.
  15. Jesko Hecking-Harbusch and Niklas O. Metzger. Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. In Proceedings of ATVA, 2019. Google Scholar
  16. P. Madhusudan and P. S. Thiagarajan. A Decidable Class of Asynchronous Distributed Controllers. In Proceedings of CONCUR, pages 145-160, 2002. URL: https://doi.org/10.1007/3-540-45694-5_11.
  17. P. Madhusudan, P. S. Thiagarajan, and Shaofa Yang. The MSO Theory of Connectedly Communicating Processes. In Proceedings of FSTTCS, pages 201-212, 2005. URL: https://doi.org/10.1007/11590156_16.
  18. José Meseguer, Ugo Montanari, and Vladimiro Sassone. Process versus Unfolding Semantics for Place/Transition Petri Nets. Theor. Comput. Sci., 153(1&2):171-210, 1996. URL: https://doi.org/10.1016/0304-3975(95)00121-2.
  19. Anca Muscholl. Automated Synthesis of Distributed Controllers. In Proceedings of ICALP, pages 11-27, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_2.
  20. Anca Muscholl and Igor Walukiewicz. Distributed Synthesis for Acyclic Architectures. In Proceedings of FSTTCS, pages 639-651, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.639.
  21. Anca Muscholl, Igor Walukiewicz, and Marc Zeitoun. A look at the control of asynchronous automata. Perspectives in Concurrency Theory, pages 356-371, 2009. Google Scholar
  22. Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci., 13:85-108, 1981. URL: https://doi.org/10.1016/0304-3975(81)90112-2.
  23. Ernst-Rüdiger Olderog. Nets, terms and formulas: three views of concurrent processes and their relationship, volume 23. Cambridge University Press, 2005. Google Scholar
  24. Amir Pnueli and Roni Rosner. Distributed Reactive Systems Are Hard to Synthesize. In 31st Annual Symposium on Foundations of Computer Science, 1990, Volume II, pages 746-757, 1990. URL: https://doi.org/10.1109/FSCS.1990.89597.
  25. Wolfgang Reisig. Petri Nets: An Introduction. Springer, 1985. URL: https://doi.org/10.1007/978-3-642-69968-9.
  26. Wieslaw Zielonka. Notes on Finite Asynchronous Automata. ITA, 21(2):99-135, 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