I’d like to continue talking about this paper:
Last time I explained, in a sketchy way, the double category of open Petri nets. This time I’d like to describe a ‘semantics’ for open Petri nets.
In his famous thesis Functorial Semantics of Algebraic Theories, Lawvere introduced the idea that semantics, as a map from expressions to their meanings, should be a functor between categories. This has been generalized in many directions, and the same idea works for double categories. So, we describe our semantics for open Petri nets as a map
from our double category of open Petri nets to a double category of relations. This map sends any open Petri net to its ‘reachability relation’.
In Petri net theory, a marking of a set is a finite multisubset of We can think of this as a way of placing finitely ‘tokens’—little black dots—on the elements of A Petri net lets us start with some marking of its places and then repeatedly change the marking by moving tokens around, using the transitions. This is how Petri nets describe processes!
For example, here’s a Petri net from chemistry:
Here’s a marking of its places:
But using the transitions, we can repeatedly change the marking. We started with one atom of carbon, one molecule of oxygen, one molecule of sodium hydroxide and one molecule of hydrochloric acid. But they can turn into one molecule of carbon dioxide, one molecule of sodium hydroxide and one molecule of hydrochloric acid:
These can then turn into one molecule of sodium bicarbonate and one molecule of hydrochloric acid:
Then these can turn into one molecule of carbon dioxide, one molecule of water and one molecule of sodium chloride:
People say one marking is reachable from another if you can get it using a finite sequence of transitions in this manner. (Our paper explains this well-known notion more formally.) In this example every marking has 0 or 1 tokens in each place. But that’s not typical: in general we could have any natural number of tokens in each place, so long as the total number of tokens is finite.
Our paper adapts the concept of reachability to open Petri nets. Let denote the set of markings of the set Given an open Petri net there is a reachability relation
This relation holds when we can take a given marking of feed those tokens into the Petri net move them around using transitions in and have them pop out and give a certain marking of leaving no tokens behind.
For example, consider this open Petri net
Here is a marking of
We can feed these tokens into and move them around using transitions in
They can then pop out into leaving none behind:
This gives a marking of that is ‘reachable’ from the original marking of
The main result of our paper is that the map sending an open Petri net to its reachability relation extends to a ‘lax double functor’
where is a double category having open Petri nets as horizontal 1-cells and is a double category having relations as horizontal 1-cells.
I can give you a bit more detail on those double categories, and also give you a clue about what ‘lax’ means, without it becoming too stressful.
Last time I said the double category has:
• sets as objects,
• functions as vertical 1-morphisms,
• open Petri nets as horizontal 1-cells—they look like this:
• morphisms between open Petri nets as 2-morphisms—an example would be the visually obvious map from this open Petri net:
to this one:
What about This double category has
• sets as objects,
• functions as vertical 1-morphisms,
• relations as horizontal 1-cells from to and
• maps between relations as 2-morphisms. Here a map between relations is a square
So, the idea of the reachability semantics is that it maps:
• any set to the set consisting of all markings of that set.
• any function to the obvious function
(Yes, is a really a functor.)
• any open Petri net to its reachability relation
• any morphism between Petri nets to the obvious map between their reachability relations.
Especially if you draw some examples, all this seems quite reasonable and nice. But it’s important to note that is a lax double functor. This means that it does not send a composite open Petri net to the composite of the reachability relations for and So, we do not have
Instead, we just have
It’s easy to see why. Take to be this open Petri net:
and take to be this one:
Then their composite is this:
It’s easy to see that is a proper subset of In a token can move all the way from point 1 to point 5. But it does not do so by first moving through and then moving through It has to take a more complicated zig-zag path where it first leaves and enters then comes back into and then goes to
In our paper, Jade and I conjecture that we get
if we restrict the reachability semantics to a certain specific sub-double category of consisting of ‘one-way’ open Petri nets.
Finally, besides showing that
is a lax double functor, we also show that it’s symmetric monoidal. This means that the reachability semantics works as you’d expect when you run two open Petri nets ‘in parallel’.
In a way, the most important thing about our paper is that it illustrates some methods to study semantics for symmetric monoidal double categories. Kenny Courser and I will describe these methods more generally in our paper “Structured cospans.” They can be applied to timed Petri nets, colored Petri nets, and various other kinds of Petri nets. One can also develop a reachability semantics for open Petri nets that are glued together along transitions as well as places.
I hear that the company Statebox wants these and other generalizations. We aim to please—so we’d like to give it a try.
Next time I’ll wrap up this little series of posts by explaining how Petri nets give symmetric monoidal categories.
• 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.