Skip to main content
SpringerLink
Log in

The Synthesis Problem for Repeatedly Communicating Petri Games

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13288))

Abstract

Petri games are a multi-player game model for the automatic synthesis of distributed systems, where the players are represented as tokens on a Petri net and grouped into environment players and system players. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the entire causal history of the other players.

We present a subclass of Petri games, for which the synthesis problem is decidable, with finitely many sources of nondeterminism, which are caused by the finitely many environment players, and with finitely many system players. All players satisfy a synchronisation condition guaranteeing that they know within a bounded number of own moves what each other player’s next (non)deterministic move has been. This differs from existing approaches that limit the number of the system players or environment players. We show that for Petri games in this subclass deciding the existence of a winning strategy for the system players with a global safety condition is in EXPTIME.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Full proofs will appear in an extended version of this paper on arXiv.

References

  1. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  2. Alur, R., Madhusudan, P., Nam, W.: Symbolic computational techniques for solving games. Int. J. Softw. Tools Technol. Transf. 7(2), 118–128 (2005)

    Article  Google Scholar 

  3. Beutner, R., Finkbeiner, B., Hecking-Harbusch, J.: Translating asynchronous games for distributed synthesis. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, 27–30 August 2019. LIPIcs, vol. 140, pp. 26:1–26:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.26

  4. Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LTL synthesis. In: Fisman, D., Jacobs, S. (eds.) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017. EPTCS, vol. 260, pp. 4–22 (2017). https://doi.org/10.4204/EPTCS.260.4

  5. Buy, U.A., Darabi, H., Lehene, M., Venepally, V.: Supervisory control of time Petri nets using net unfolding. In: 29th Annual International Computer Software and Applications Conference, COMPSAC 2005, Edinburgh, Scotland, UK, 25–28 July 2005, vol. 2. pp. 97–100. IEEE Computer Society (2005). https://doi.org/10.1109/COMPSAC.2005.148

  6. Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. Summ. Summer Inst. Symb. Logic 1, 3–50 (1957)

    Google Scholar 

  7. Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)

    Article  MathSciNet  Google Scholar 

  8. Esparza, J.: Model checking using net unfoldings. Sci. Comput. Program. 23(2), 151–195 (1994)

    Article  MathSciNet  Google Scholar 

  9. Finkbeiner, B.: Bounded synthesis for petri games. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 223–237. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23506-6_15

    Chapter  Google Scholar 

  10. Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: Global winning conditions in synthesis of distributed systems with causal memory. CoRR abs/2107.09280 (2021). https://arxiv.org/abs/2107.09280

  11. Finkbeiner, B., Gieseking, M., Olderog, E.-R.: Adam: causality-based synthesis of distributed systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 433–439. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_25

    Chapter  Google Scholar 

  12. Finkbeiner, B., Gölz, P.: Synthesis in distributed environments. In: Lokam, S., Ramanujam, R. (eds.) 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 93, pp. 28:1–28:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28. http://drops.dagstuhl.de/opus/volltexte/2018/8406

  13. Finkbeiner, B., Olderog, E.R.: Petri games: synthesis of distributed systems with causal memory. Inf. Comput. 253, 181–203 (2017)

    Article  MathSciNet  Google Scholar 

  14. Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26–29 June 2005, pp. 321–330 (2005). https://doi.org/10.1109/LICS.2005.53

  15. Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 275–286. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_26

    Chapter  Google Scholar 

  16. Kupferman, O., Vardi, M.: Synthesizing distributed systems. In: Proceedings - Symposium on Logic in Computer Science, pp. 389–398 (2001). https://doi.org/10.1109/LICS.2001.932514. https://www.scopus.com/inward/record.uri?eid=2-s2.0-0034873871&doi=10.1109

  17. Madhusudan, P., Thiagarajan, P.S., Yang, S.: The MSO theory of connectedly communicating processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 201–212. Springer, Heidelberg (2005). https://doi.org/10.1007/11590156_16

    Chapter  Google Scholar 

  18. Meseguer, J., Montanari, U., Sassone, V.: Process versus unfolding semantics for place/transition petri nets. Theoret. Comput. Sci. 153(1), 171–210 (1996)

    Article  MathSciNet  Google Scholar 

  19. Mohalik, S., Walukiewicz, I.: Distributed games. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 338–351. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24597-1_29

    Chapter  Google Scholar 

  20. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theoret. Comput. Sci. 13(1), 85–108 (1981)

    Article  MathSciNet  Google Scholar 

  21. Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0035790

    Chapter  Google Scholar 

  22. Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, 22–24 October 1990, vol. II, pp. 746–757 (1990). https://doi.org/10.1109/FSCS.1990.89597

  23. Raskin, J., Samuelides, M., Begin, L.V.: Petri games are monotone but difficult to decide. Technical report, Université Libre De Bruxelles (2003)

    Google Scholar 

  24. Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel (1992)

    Google Scholar 

  25. Zielonka, W.: Notes in finite asynchronous automata. RAIRO - Theoret. Inform. Appl. - Informatique Théorique et Applications 21(2), 99–135 (1987)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carl von Ossietzky University Oldenburg, 26129, Oldenburg, Germany

    Paul Hannibal & Ernst-Rüdiger Olderog

Authors
  1. Paul Hannibal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paul Hannibal .

Editor information

Editors and Affiliations

  1. University of Milano-Bicocca, Milano, Italy

    Luca Bernardinello

  2. Paris 13 University, Villetaneuse, France

    Laure Petrucci

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hannibal, P., Olderog, ER. (2022). The Synthesis Problem for Repeatedly Communicating Petri Games. In: Bernardinello, L., Petrucci, L. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2022. Lecture Notes in Computer Science, vol 13288. Springer, Cham. https://doi.org/10.1007/978-3-031-06653-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-06653-5_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-06652-8

  • Online ISBN: 978-3-031-06653-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation