Document Open Access Logo

Universal Properties of Petri Net Unfoldings

Authors Serge Lechenne , Hugo Paquet

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.23.pdf
  • Filesize: 1.24 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Concurrency
Keywords
  • Petri nets
  • Event structures
  • Symmetry
  • Unfolding
  • 2-Categories

Metrics

Abstract

It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in practical analysis and verification. 
This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it generally fails to satisfy the expected universal property. This is because the unfolding construction overlooks the net’s internal symmetries. 
There are two solutions: make these symmetries explicit to obtain a weak universal property (one that holds only "up to symmetry"); or break the symmetries by assigning individual identities to components of the net. We review these two solutions and establish, in each case, a universal unfolding of Petri nets to event structures.
This paper demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two constructions can be related formally via an appropriate morphism of adjunctions. We exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.

Cite As Get BibTex

Serge Lechenne and Hugo Paquet. Universal Properties of Petri Net Unfoldings. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.23

Author Details

Serge Lechenne
  • Inria & École Normale Supérieure - PSL, France
Hugo Paquet
  • Inria & École Normale Supérieure - PSL, France

References

  1. Nathanael Arkor and Dylan McDermott. The formal theory of relative monads. Journal of Pure and Applied Algebra, 228(9):107676, September 2024. URL: https://doi.org/10.1016/j.jpaa.2024.107676.
  2. John C Baez, Fabrizio Genovese, Jade Master, and Michael Shulman. Categories of nets. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470566.
  3. John C Baez and Jade Master. Open petri nets. Mathematical Structures in Computer Science, 30(3):314-341, 2020. URL: https://doi.org/10.1017/S0960129520000043.
  4. Kris Brown, Kevin Carlson, Owen Lynch, and Evan Patterson. Catcolab software. URL: https://catcolab.org/help/.
  5. Roberto Bruni, José Meseguer, Ugo Giovanni Erasmo Montanari, and Vladimiro Sassone. Functorial models for petri nets. Information and Computation, 170(2):207-236, 2001. URL: https://doi.org/10.1006/inco.2001.3050.
  6. Benjamin Merlin Bumpus, Sophie Libkind, Jordy Lopez Garcia, Layla Sorkatti, and Samuel Tenka. Additive invariants of open petri nets. Compositionality, 7, 2025. Google Scholar
  7. Aurelio Carboni, Stefano Kasangian, and Ross Street. Bicategories of spans and relations. Journal of pure and applied algebra, 33(3):259-267, 1984. Google Scholar
  8. Simon Castellan and Pierre Clairambault. The geometry of causality: Multi-token geometry of interaction and its causal unfolding. Proc. ACM Program. Lang., 7(POPL):689-717, 2023. URL: https://doi.org/10.1145/3571217.
  9. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Logical Methods in Computer Science, Volume 13, Issue 3, September 2017. URL: https://doi.org/10.23638/lmcs-13(3:35)2017.
  10. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of pcf. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 232-243. IEEE, 2015. URL: https://doi.org/10.1109/LICS.2015.31.
  11. David Dalrymple. Safeguarded ai: Constructing safety by design. Advanced Research and Invention Agency, 2024. URL: https://aria.org.uk/media/3nhijno4/aria-safeguarded-ai-programme-thesis-v1.pdf.
  12. Elena Di Lavore, Wilmer Leal, and Valeria de Paiva. Dialectica petri nets. Fundamenta Informaticae, 194, 2025. URL: https://doi.org/10.46298/fi.13125.
  13. Uli Fahrenberg, Christian Johansen, Christopher Trotter, and Krzysztof Ziemianski. Sculptures in concurrency. Log. Methods Comput. Sci., 17(2), April 2021. URL: https://doi.org/10.23638/lmcs-17(2:5)2021.
  14. Eric Goubault and Samuel Mimram. Formal relationships between geometrical and classical models for concurrency. In Lisbeth Fajstrup, Eric Goubault, and Martin Raussen, editors, Proceedings of the workshop on Geometric and Topological Methods in Computer Science, GETCO 2010, Aalborg, Denmark, January 11-15, 2010, volume 283 of Electronic Notes in Theoretical Computer Science, pages 77-109. Elsevier, June 2010. URL: https://doi.org/10.1016/j.entcs.2012.05.007.
  15. Jonathan Hayman and Glynn Winskel. Symmetry in petri nets. Unpublished manuscript, January 2008. Google Scholar
  16. Jonathan Hayman and Glynn Winskel. The unfolding of general Petri nets. In Ramesh Hariharan, Madhavan Mukund, and V Vinay, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 2 of Leibniz International Proceedings in Informatics (LIPIcs), pages 223-234, Dagstuhl, Germany, 2008. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1755.
  17. G. M. Kelly. Basic Concepts of Enriched Category Theory, volume 64 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1982. Reprinted in: Reprints in Theory and Applications of Categories, No. 10 (2005), pp. 1-136. Google Scholar
  18. Joachim Kock. Whole-grain petri nets and processes. J. ACM, 70(1), December 2022. URL: https://doi.org/10.1145/3559103.
  19. Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo. A compositional framework for petri nets. In Barbara König and Henning Urbat, editors, Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Proceedings, volume 14617 of Lecture Notes in Computer Science, pages 174-193, Berlin, Heidelberg, 2024. Springer. URL: https://doi.org/10.1007/978-3-031-66438-0_9.
  20. Jade Master and Joe Moeller. Colored petri nets are monoidal double functors. arXiv preprint, 2025. URL: https://arxiv.org/abs/2510.01946.
  21. Kenneth L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In Gregor von Bochmann and David K. Probst, editors, Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings, volume 663 of Lecture Notes in Computer Science, pages 164-177, Berlin, Heidelberg, 1992. Springer. URL: https://doi.org/10.1007/3-540-56496-9_14.
  22. José Meseguer and Ugo Montanari. Petri nets are monoids. Information and computation, 88(2):105-155, 1990. URL: https://doi.org/10.1016/0890-5401(90)90013-8.
  23. José Meseguer, Ugo Montanari, and Vladimiro Sassone. On the semantics of place/transition petri nets. Mathematical Structures in Computer Science, 7(4):359-397, 1997. URL: https://doi.org/10.1017/S0960129597002314.
  24. T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989. URL: https://doi.org/10.1109/5.24143.
  25. 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.
  26. 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.
  27. Sam Staton and Glynn Winskel. On the expressivity of symmetry in event structures. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 392-401, 2010. URL: https://doi.org/10.1109/LICS.2010.37.
  28. Rob J van Glabbeek and Gordon D Plotkin. Configuration structures, event structures and petri nets. Theoretical Computer Science, 410(41):4111-4159, 2009. URL: https://doi.org/10.1016/j.tcs.2009.06.014.
  29. Glynn Winskel. A new definition of morphism on petri nets. In Annual Symposium on Theoretical Aspects of Computer Science, pages 140-150. Springer, 1984. URL: https://doi.org/10.1007/3-540-12920-0_13.
  30. Glynn Winskel. Event structures. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, volume 255 of Lecture Notes in Computer Science, pages 325-392, Berlin, Heidelberg, 1986. Springer. URL: https://doi.org/10.1007/3-540-17906-2_31.
  31. Glynn Winskel. Petri nets, algebras, morphisms, and compositionality. Information and Computation, 72(3):197-238, 1987. URL: https://doi.org/10.1016/0890-5401(87)90032-0.
  32. Glynn Winskel. Event structures with symmetry. In Luca Cardelli, Marcelo Fiore, and Glynn Winskel, editors, Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, volume 172 of Electronic Notes in Theoretical Computer Science, pages 611-652. Elsevier, 2007. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin. URL: https://doi.org/10.1016/j.entcs.2007.02.022.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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