I’ve been talking about my new paper with Jade Master:
In Part 1 we saw the double category of open Petri nets; in Part 2 we saw the reachability semantics for open Petri nets as a double functor. Now I’d like to wrap up by showing you the engine beneath the hood of our results.
I fell in love with Petri nets when I realized that they were really just presentations of free symmetric monoidal categories. If you like category theory, this turns Petri nets from something mysterious into something attractive.
In any category you can compose morphisms and and get a morphism In a monoidal category you can also tensor morphisms and and get a morphism This of course relies on your ability to tensor objects. In a symmetric monoidal category you also have And of course, there is more to it than this. But this is enough to get started.
A Petri net has ‘places’ and also ‘transitions’ going between multisets of places:
From this data we can try to generate a symmetric monoidal category whose objects are built from the places and whose morphisms are built from the transitions. So, for example, the above Petri net would give a symmetric monoidal category with an object
2 susceptible + infected
and a morphism from this to the object
susceptible + 2 infected
(built using the transition infection), and a morphism
from this to the object
susceptible + infected + resistant
(built using the transition recovery) and so on. Here we are using to denote the tensor product in our symmetric monoidal category, as usual in chemistry.
When we do this sort of construction, the resulting symmetric monoidal category is ‘free’. That is, we are not imposing any really interesting equations: the objects are freely generated by the places in our Petri net by tensoring, and the morphisms are freely generated by the transitions by tensoring and composition.
That’s the basic idea. The problem is making this idea precise!
Many people have tried in many different ways. I like this approach the best:
• José Meseguer and Ugo Montanari, Petri nets are monoids, Information and Computation 88 (1990), 105–155.
but I think it can be simplified a bit, so let me describe what Jade and I did in our paper.
The problem is that there are different notions of symmetric monoidal category, and also different notions of morphism between Petri nets. We take the maximally strict approach, and work with ‘commutative’ monoidal categories. These are just commutative monoid objects in so their associator:
their left and right unitor:
and even—disturbingly—their braiding:
are all identity morphisms.
The last would ordinarily be seen as ‘going too far’, since while every symmetric monoidal category is equivalent to one with trivial associator and unitors, this ceases to be true if we also require the braiding to be trivial. However, it seems that Petri nets most naturally serve to present symmetric monoidal categories of this very strict sort. There just isn’t enough information in a Petri net to make it worthwhile giving them a nontrivial braiding
It took me a while to accept this, but now it seem obvious. If you want a nontrivial braiding, you should be using something a bit fancier than a Petri net.
Thus, we construct adjoint functors between a category of Petri nets, which we call and a category of ‘commutative monoidal categories’, which we call
An object of is a Petri net: that is, a set of places, a set of transitions, and source and target functions
where is the underlying set of the free commutative monoid on
More concretely, is the set of formal finite linear combinations of elements of with natural number coefficients. The set naturally includes in , and for any function
there is a unique monoid homomorphism
A Petri net morphism from a Petri net
to a Petri net
is a pair of functions
making the two obvious diagrams commute:
There is a category with Petri nets as objects and Petri net morphisms as morphisms.
On the other hand, a commutative monoidal category is a commutative monoid object in Explicitly, it’s a strict monoidal category such that for all objects and we have
and for all morphisms and
Note that a commutative monoidal category is the same as a strict symmetric monoidal category where the symmetry isomorphisms
are all identity morphisms. Every strict monoidal functor between commutative monoidal categories is automatically a strict symmetric monoidal functor. So, we let be the category whose objects are commutative monoidal categories and whose morphisms are strict monoidal functors.
There’s a functor
sending any commutative monoidal category to its underlying Petri net. This Petri net has the set of objects as its set of places and the set of morphisms as its set of transitions, and
as its source and target maps.
Proposition. The functor has a left adjoint
This is Proposition 10 in our paper, and we give an explicit construction of this left adjoint.
So that’s our conception of the free commutative monoidal category on a Petri net. It’s pretty simple. How could anyone have done anything else?
Montanari and Meseguer do almost the same thing, but our category of Petri nets is a subcategory of theirs: our morphisms of Petri nets send places to places, while they allow more general maps that send a place to a formal linear combination of places. On the other hand, they consider a full subcategory of our containing only commutative monoidal categories whose objects form a free commutative monoid.
Other papers do a variety of more complicated things. I don’t have the energy to explain them all, but you can see some here:
• Pierpaolo Degano, José Meseguer and Ugo Montanari, Axiomatizing net computations and processes, in Logic in Computer Science 1989, IEEE, New Jersey, 1989, pp. 175–185.
• Vladimiro Sassone, Strong concatenable processes: an approach to the category of Petri net computations, BRICS Report Series, Dept. of Computer Science, U. Aarhus, 1994.
• Vladimiro Sassone, On the category of Petri net computations, in Colloquium on Trees in Algebra and Programming, Springer, Berlin, 1995.
• Vladimiro Sassone, An axiomatization of the algebra of Petri net concatenable processes, in Theoretical Computer Science 170 (1996), 277–296.
• Vladimiro Sassone and Pavel Sobociński, A congruence for Petri nets, Electronic Notes in Theoretical Computer Science 127 (2005), 107–120.
Getting the free commutative monoidal category on a Petri net right is key to developing the reachability semantics for open Petri nets in a nice way. But to see that, you’ll have to read our paper!
• Part 1: the double category of open Petri nets.
• Part 2: the reachability semantics for open Petri nets.
• Part 3: the free symmetric monoidal category on a Petri net.