Open Petri Nets (Part 2)

I’d like to continue talking about this paper:

• John Baez and Jade Master, Open Petri nets, Mathematical Structures in Computer Science, 30 (2020), 314–341.

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

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

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 X is a finite multisubset of X. We can think of this as a way of placing finitely ‘tokens’—little black dots—on the elements of X. 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 \mathbb{N}[X] denote the set of markings of the set X. Given an open Petri net P \colon X \nrightarrow Y there is a reachability relation

\blacksquare P \subseteq \mathbb{N}[X] \times \mathbb{N}[Y]

This relation holds when we can take a given marking of X, feed those tokens into the Petri net P, move them around using transitions in P, and have them pop out and give a certain marking of Y, leaving no tokens behind.

For example, consider this open Petri net P \colon X \nrightarrow Y:

Here is a marking of X:

We can feed these tokens into P and move them around using transitions in P:

They can then pop out into Y, leaving none behind:

This gives a marking of Y that is ‘reachable’ from the original marking of X.

The main result of our paper is that the map sending an open Petri net P to its reachability relation \blacksquare P extends to a ‘lax double functor’

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

where \mathbb{O}\mathbf{pen}(\mathrm{Petri}) is a double category having open Petri nets as horizontal 1-cells and \mathbb{R}\mathbf{el} 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 \mathbb{O}\mathbf{pen}(\mathrm{Petri}) has:

• sets X, Y, Z, \dots as objects,

• functions f \colon X \to Y as vertical 1-morphisms,

• open Petri nets P \colon X \nrightarrow Y 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 \mathbb{R}\mathbf{el}? This double category has

• sets X, Y, Z, \dots as objects,

• functions f \colon X \to Y as vertical 1-morphisms,

• relations R \subseteq X \times Y as horizontal 1-cells from X to Y, and

• maps between relations as 2-morphisms. Here a map between relations is a square

that obeys

(f \times g) R \subseteq S

So, the idea of the reachability semantics is that it maps:

• any set X to the set \mathbb{N}[X] consisting of all markings of that set.

• any function f \colon X \to Y to the obvious function

\mathbb{N}(f) \colon \mathbb{N}[X] \to \mathbb{N}[Y]

(Yes, \mathbb{N} is a really a functor.)

• any open Petri net P \colon X \nrightarrow Y to its reachability relation

\blacksquare P \colon \mathbb{N}[X] \to \mathbb{N}[Y]

• 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 \blacksquare is a lax double functor. This means that it does not send a composite open Petri net PQ to the composite of the reachability relations for P and Q. So, we do not have

\blacksquare Q \; \blacksquare P = \blacksquare (QP)

Instead, we just have

\blacksquare Q \; \blacksquare P \subseteq \blacksquare (QP)

It’s easy to see why. Take P \colon X \nrightarrow Y to be this open Petri net:

and take Q \colon Y \nrightarrow Z to be this one:

Then their composite QP \colon X \nrightarrow Y is this:

It’s easy to see that \blacksquare (QP) is a proper subset of \blacksquare Q \; \blacksquare P. In QP a token can move all the way from point 1 to point 5. But it does not do so by first moving through P and then moving through Q! It has to take a more complicated zig-zag path where it first leaves P and enters Q, then comes back into P, and then goes to Q.

In our paper, Jade and I conjecture that we get

\blacksquare Q \; \blacksquare P = \blacksquare (QP)

if we restrict the reachability semantics to a certain specific sub-double category of \mathbb{O}\mathbf{pen}(\mathrm{Petri}) consisting of ‘one-way’ open Petri nets.

Finally, besides showing that

\blacksquare \colon \mathbb{O}\mathbf{pen}(\mathrm{Petri}) \to \mathbb{R}\mathbf{el}

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.

This entry was posted on Saturday, August 18th, 2018 at 9:00 am and is filed under computer science, mathematics, networks. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

9 Responses to Open Petri Nets (Part 2)

  1. Lee Bloomquist says:
    18 August, 2018 at 10:13 pm

    How would you analyze a “self” loop, where an arrow from a transition goes to a place (self) thence back to the originating transition– with other arrows possible? (I had to do that once when simulating a factory system using diagrams of Petri nets automatically coded into Smalltalk80. Without the self loop, multiple parts entering the queue for a machine would spawn multiple instances of the transition in multiple threads, while in the factory the machine would only process one part at a time.)

    Reply
    • John Baez says:
      19 August, 2018 at 2:05 am

      A loop like this describes a transition where something turns into itself. Such transitions can be removed from a Petri net without affecting reachability.

      Reply
      • leebloomquist says:
        21 August, 2018 at 1:40 pm

        If reachability is our only concern, then certainly we can ignore self loops. But if thermodynamics is of any concern, self loops are a way to model a thermodynamic engine. In a factory, the engine doesn’t start when you put a part in the input queuing place to a transition that models a machine. The thermodynamic engine starts when you put a token in the “self” place. To stop the thermodynamic engine, remove the token from the “self” place. Regarding chemistry, that might be of interest for models of biological systems, which involve thermodynamics.

        Reply
  2. Toby Bartels says:
    19 August, 2018 at 6:13 am

    Unless I misunderstand reachability (which is quite possible), then the laxness should be \blacksquare Q \circ \blacksquare P \subseteq \blacksquare ( Q \circ P ) , rather than the other way around. That is, if something's reachable by going through Q after going through P , then it's reachable by going through Q \circ P , but additional zigzag reachings may also exist in \blacksquare ( Q \circ P ) .

    Also, shouldn't the chemistry diagrams have some nodes with more than mark in them? Not in the original diagram, but in the later ones, if each is supposed to be reachable from the previous one.

    Reply
    • John Baez says:
      19 August, 2018 at 6:57 am

      I should have written \blacksquare Q \circ \blacksquare P \subseteq \blacksquare ( Q \circ P ). I’ll fix that—thanks! I hope I didn’t get it twisted around in the actual paper.

      Also, shouldn’t the chemistry diagrams have some nodes with more than mark in them? Not in the original diagram, but in the later ones, if each is supposed to be reachable from the previous one.

      I don’t think so. We start with one atom of carbon, one molecule of oxygen, one molecule of sodium hydroxide and one molecule of hydrochloric acid:

      They turn into one molecule of carbon dioxide, one molecule of sodium hydroxide and one molecule of hydrochloric acid:

      These turn into one molecule of sodium bicarbonate and one molecule of hydrochloric acid:

      These turn into one molecule of carbon dioxide, one molecule of water and one molecule of sodium chloride:

      So, there’s always at most one token in each place in this story. That’s not true for all such stories, so this example is unrepresentative, but I think I’ve got the chemistry basically right: atoms of each kind are being conserved.

      Reply
  3. williamsharkey says:
    26 April, 2019 at 8:10 am

    I wonder if this is relevant to reasoning about dropping grains of sand on an Abelian sandpile. Ie could it show that all points on lattice are reachable from dropping grains on a single tile repeatedly, or more interestingly, would it be able to tell you things about interference patterns caused by dropping grains at two points separated by n cells simultaneously, etc. Would it cause an problem in applying these techniques if the lattice is infinite instead of a finite number of cells?

    Reply
  4. Structured Cospans and Petri Nets | Azimuth says:
    6 April, 2020 at 6:34 pm

    This talk on structured cospans and Petri nets is the second of a two-part series, but it should be understandable on its own. The first part is on structured cospans and double categories.

    You can see my talk live on YouTube here, with simultaneous discussion on the Category Theory Community Server. (To join this, click here.) The talk will be recorded and remain available on YouTube.

    You can already see the slides here.

    Structured cospans and Petri nets

    Abstract. “Structured cospans” are a general way to study networks with inputs and outputs. Here we illustrate this using a type of network popular in theoretical computer science: Petri nets. An “open” Petri net is one with certain places designated as inputs and outputs. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Using the formalism of structured cospans, open Petri nets can be treated as morphisms of a symmetric monoidal category—or better, a symmetric monoidal double category. We explain two forms of semantics for open Petri nets using symmetric monoidal double functors out of this double category. The first, an operational semantics, gives for each open Petri net a category whose morphisms are the processes that this net can carry out. The second, a “reachability” semantics, simply says what these processes can accomplish. This is joint work with Kenny Courser and Jade Master.

    Reply

You can use Markdown or HTML in your comments. You can also use LaTeX, like this: $latex E = m c^2 $. The word 'latex' comes right after the first dollar sign, with a space after it.

This site uses Akismet to reduce spam. Learn how your comment data is processed.