Petri net unfoldings mapped with universal symmetry properties
Universal Properties of Petri Net Unfoldings
Logic in Computer Science
Summary
Petri nets are a way to represent processes that can happen at the same time. Unfoldings show all possible ways these processes can play out. The authors explain why the usual way of unfolding doesn't perfectly capture all the symmetries inside a Petri net. They review two ways to fix this: either allowing some wiggle room due to symmetry differences or giving unique identities to parts of the net. Their work uses higher-level mathematics to show how these fixes relate and why the unfolding approach is essentially unique.
What this means in practice
- •For concurrent system designers: Clarify and improve models of concurrent system behaviors by capturing hidden symmetries in their process unfoldings.
- •For formal verification engineers: Enhance analysis techniques for verifying concurrent systems by applying refined unfolding semantics that consider net symmetries.
A theory result. No direct application yet.
Authors
Serge Lechenne, Hugo Paquet
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.