Nets within nets from the Grothendieck construction
by Jade Master
This blog post is regarding (elementary) object systems. Object systems were first introduced in
- Rüdiger Valk, Object Petri nets, In Advanced Course on Petri Nets, pp. 819-848, 2003.
An object system is a very meta thing, it is a Petri net, whose tokens are marked Petri nets. Here is an example from Valk's paper
meant to represent three people simultaneously putting out a fire. The lower Petri net in this picture represents the global Petri net. In the top half of the image, squares with local Petri nets in them are depicted pointing to the tokens which they are represented by. When, for example, the first <approachFire> transition in the global Petri net fires, two things occur:
- The token in place A is moved to place B and,
- This Petri net represented by this token fires its own <approachFire> transition, putting a token in the place q.1.
So in general, a firing of an elementary object system is either a firing of a global net or a local net. If the global net fires, then the corresponding transitions in the local net must be fired as well. As you may imagine, this type of net is great for modelling hierarchical concurrent systems where there are multiple agents who interact in a concurrent way.
In this blog post I'll show you how to construct a category of object systems and their generalizations using the Grothendieck construction! It starts with an idea that has been central to my research so far, that the space of all firing sequences of Petri can be represented as a symmetric monoidal category. Indeed for a Petri net P, there is a symmetric monoidal category F(P) where
- objects are sums of species, i.e. markings of P,
- morphisms are arbitrary sums and composites of transitions i.e. firing sequences and,
- monoidal product is sum, which represents parallel composition on a pair of firing sequences.
Furthermore this process of forming firing sequences forms a left adjoint functor
$ F: \mathsf{Petri} \to \mathsf{CMC}$
where $ \mathsf{CMC}$ is the category of strictly commutative symmetric monoidal categories (the type of symmetric monoidal category that Petri nets happen to generate). Commutative monoidal categories are in particular categories so there is a forgetful functor
$ R: \mathsf{CMC} \to \mathsf{Cat}$
which does nothing to the objects and morphisms. We can compose R with our left adjoint from before to get a functor
$ R \circ F : \mathsf{Petri} \to \mathsf{Cat}$.
At this point you should pause and guess what I do next, it's something I do over and over on this blog
...
...
...
...
...
The answer is the Grothendieck construction. For a review of the Grothendieck construction check out my blog:
If we take the Grothendieck construction of the functor $ R \circ L$, then we obtain a category $ \int R \circ F$ where
- objects are pairs $ (P, m)$ where P is a Petri net and m is a marking of P and,
- morphisms are pairs $ (f,t): (P,m) \to (Q,n)$ where f is a morphism of Petri nets and t is a firing sequence from $ f(m) \to n$.
I actually talked about this category in a previous blog post:
Which contains a more in-depth discussion of the construction we have just performed. $ \int R \circ F$ is a category whose objects are marked Petri nets and whose morphisms represent changing the structure of your Petri net and firing your initial marking. Because $ \int G \circ F$ has marked Petri nets as objects, let's call it $ \mathsf{MkPetri}$. $ \mathsf{MkPetri}$ is symmetric monoidal with monoidal product given by
$ (P,m) \oplus (Q,n) = (P+Q,m+n)$
Here $ P+Q$ is the coproduct of Petri nets and $ m+n$ is the marking of P+Q which agrees with m on the P-component and agrees with n on the Q component. In other words, m+n is the formal sum of m and n. The main claim of this blog post is that the following is a reasonable definition:
Definition: An object system is a symmetric monoidal functor
$ E : (FP,+) \to (\mathsf{MkPetri},\oplus)$
where $ FP$ is the free commutative monoidal category on a Petri net P.
The idea is that P is the global Petri net and the functor E assigns the local Petri nets and their transformation rules. Explicitly, for a place p, the marked Petri net E(p) is the local Petri net which is assigned to p. This determines the action of E on objects up to isomorphism because FP is free. For a transition $ \tau$ with source $a +b$ and target $c+d$,
$ E(\tau) : E(a) \oplus E(b) \to E(c) \oplus E(d)$
is a pair (f,s) where
- f is a morphism from disjoint union local Petri nets in the source to the disjoint union of the local Petri nets in the target (this determines how the transition $\tau$ mutates the structure of each local Petri net in the source and target) and,
- s is firing sequence, (this determines how $ \tau$ alters the markings of the local Petri nets).
- Because FP is free, this case determines the action of E on all firing sequences.
This definition describes object systems using Lawvere's idea of functorial semantics. The global Petri net P provides a syntax and the functor equips that syntax with a semantics based in marked Petri nets.
Beware that this definition does not match exactly the definition introduced by Valk. In those object systems, transitions in the global net are not allowed to mutate the local Petri nets. I see this as a feature not a bug, object systems by our definition are more general than the object systems defined by Valk. The ability to mutate the local nets means that these object systems are more expressive.
The second thing about this definition which doesn't match Valk's is that our global nets don't come equipped with an initial marking. However, you can equip them with an initial marking using the same construction that we used to obtain marked Petri nets. I won't go into too many details here, but the idea is that object systems also have a "category of firing sequences functor"
$ \mathsf{ObSys} \to \mathsf{CMC}$
which we can take the Grothendieck construction to obtain a category of marked object systems. At this point we would be two Grothendieck constructions in, which I find to be very confusing as well as fun; it's kind of like a double integral.
Thank you for reading and please let me know if you would like me to clarify something.