Marked Petri Nets via the Grothendieck Construction
by Jade Master
I started this blog with the goal of applying the Grothendieck construction to everything in sight. The idea was that more often than not, if you can take a functor and interpret it as a functor into $ \mathsf{Cat}$, then the Grothendieck construction of that functor is an interesting category worthy of time and consideration.
With this in mind it seems obscene that I haven't yet turned this blog onto my PhD research. This post intends to fix that omission. In this post I will take the Grothendieck construction of the operational semantics functor
$ F : \mathsf{Petri} \to \mathsf{CMC}$
where $ \mathsf{CMC}$ is the category of commutative monoidal categories. The Grothendieck construction $ \int F$ is a category whose objects are marked Petri nets, a popular and practical variant of Petri nets.
Categorical Operational Semantics of Petri Nets
The operation of a Petri net is shown in the following gif:
The circles are called places and the rectangles are called transitions. Specific instances of each place are called tokens and denoted by the black dots. The transitions can fire, and output a token for every arrow going out of it and consume a token for every arrow going into it. The operational semantics of a Petri net aims to formalize and reason about the sequences of firings which can occur within a Petri net.
The idea introduced by Messeguer and Montanari in Petri Nets are Monoids was that these firings can be modeled by categories. For a Petri net $ P$, its categorical operational semantics is a category $ FP$ whose objects represent configurations of tokens (markings) and whose morphisms represent sequences of firings. Nailing down the details of this category is a matter of debate, and there are different constructions suited for different purposes. However, in this post we will use an operational semantics which is very mathematically natural, with the understanding that marked Petri nets can also be obtained with the Grothendieck construction if another form of categorical operational semantics is chosen. This operational semantics can be defined inductively.
Definition: For a Petri net $ P= s,t :T \to \mathbb{N}[S]$, its categorical operational semantics is a category $ FP$ where
- objects are multisets of places i.e. elements of the free commutative monoid $ \mathbb{N}[S]$ and,
- morphisms are generated inductively by the following rules:
- Every transition $ \tau \in T$ becomes a morphism $ \tau : s(\tau) \to t(\tau)$.
- Every marking $ m \in \mathbb{N}[S]$ is equipped with an identity morphism $ 1_m: m \to m$.
- For every pair of morphisms $ f : x \to y$ and $ g : y \to z$ there is a formal composite $ g \circ f : x \to z$.
- For every pair of morphisms $ f : x \to y$ and $ f' : x' \to y'$ there is a formal sum $ f +f' : x +x' \to y+y'$.
- These morphisms are quotiented to:
- satisfy the axioms of a category on $ \circ$ (unitality, associativity),
- the axioms of a commutative monoid on $ +$ (associativity, commutativity, unitality) and,
- axioms expressing compatability between these two operations. $ +$ must be a functor and the functions of composition, source, target, and identity assignment must be monoid homomorphisms.
This construction is extended to a functor
$ F : \mathsf{Petri} \to \mathsf{CMC} $
where $ \mathsf{CMC}$ is the category of commutative monoidal categories i.e. commutative monoid objects in the category of categories. For a morphism of Petri nets $ (f,g) : P \to Q$, the functor $ F(f,g) : FP \to FQ$ is given by $ \mathbb{N}[g]$ on objects and by the unique functorial and strict monoidal extension of $ f$ to formal composites and sums of transitions.
This functor is a left adjoint, justifying the statement that Petri nets are the generating data for commutative monoidal categories. To see a more in depth discussion of this left adjoint see Section 2 of Open Petri Nets To learn more about this left adjoint and get a deeper sense about how it works, check out my paper Generalized Petri Nets.
Let's Grothendieck It
$ F : \mathsf{Petri} \to \mathsf{CMC}$ can be regarded as a functor into $ \mathsf{Cat}$ by forgetting that each commutative monoidal category has the structure of a commutative monoid. In other words, there is a forgetful functor $ G: \mathsf{CMC} \to \mathsf{Cat}$ which does nothing except regard commutative monoidal categories as ordinary categories and commutative monoidal functors as ordinary functors. Composition gives a functor $ \mathbf{F}: = G \circ F$ that we can Grothendieck.
The Grothendieck construction $ \int \mathbf{F}$ has
- objects given by pairs $ (P, m)$ where $ P$ is a Petri net and $ m \in \mathrm{Ob }FP$ is a marking of $ P$.
- A morphism from $ (P,m)$ to $ (Q,n)$ is a pair $ ((f,g),\tau)$ where
- $ (f,g) : P \to Q$ is a morphism of Petri nets and,
- $ \tau : \mathbb{N}[g](m) \to n$ is a firing sequence in $ Q$ i.e. a morphism in $ FQ$.
- For morphism $ ((f,g),\tau): (P,m) \to (Q,n)$ and $ ((h,k),\rho): (Q,n) \to (R,l)$ their composite is given by
$ ((h \circ f, k\circ g), \rho \circ F(h,k) (\tau)): (P,m) \to (R,l).$
In words, composition in $ \int \mathbf{F}$ composes the morphisms of Petri nets and maps $ \tau$ into the category $ FR$ so it can be composed with the firing sequence $ \rho$.
An object in this category is exactly a marked Petri net. Usually a morphism from a marked Petri net $ (P,m)$ to a marked Petri net $ (Q,n)$ is defined to be a morphism of Petri nets $ (f,g) : P \to Q$ which preserves the marking on the nose i.e. $ \mathbb{N}[g](m) = n$ (see for example Definition 10 of Petri Nets are Monoids). In this Grothendieck construction, morphisms are allowed a bit more flexibility. Now a morphism of marked Petri nets is a morphism of the underlying Petri nets $ (f,g)$ along with a transition which allows the image of $ m$ under $ \mathbb{N}[g]$ to evolve into $ n$.
In particular for a morphism $ ((f,g),\tau) : (P,m) \to (Q,n)$,
- restricting $ (f,g)$ to be the identity gives morphisms which are firing sequences of your Petri net.
- Restricting $ \tau$ to be the identity gives morphisms which only change the structure of your Petri net.
- Allowing both $ (f,g)$ and $ \tau$ to be non-trivial allows for morphisms which do both of these things at once.
Some remarks:
- The full Grothendieck construction gives an opfibration
$ \int \mathbf{F} \to \mathsf{Petri}$
which sends a marked Petri net to its underlying Petri net. This is comforting as it is a functor you would expect to exist.
- In Low- and High-Level Petri Nets with Individual Tokens, the authors discuss how transformation rules of marked Petri nets can allow for reasoning about systems in an adaptive way. A transformation rule for marked Petri nets gives a rule which changes the structure and behavior of a Petri net at the same time. In this way, the structure of Petri net can be altered in order to produce a desired firing sequence in the modified net. The existence of a sound rewriting system for marked Petri nets and relies on the category of marked Petri nets being nice enough (for a very technical definition of nice). The linked paper shows that marked Petri nets are in general not nice enough unless an operational semantics is chosen which keeps track of the identities of tokens. It seems plausible to me with a different choice of operational semantics than the one given here, we could recreate this category of nice marked Petri nets using the Grothendieck construction. If you know about this stuff and would like to talk about it let me know.
Thanks for reading! Next time we will use the the monoidal Grothendieck construction to construct various tensor products of marked Petri nets.
tags: