Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 28, 2019

Generalized Petri Nets

Posted by John Baez

guest post by Jade Master

I just finished a paper which uses Lawvere theories to generalize Petri nets. I can think of two reasons why people might be interested in this:

  • Category theorists love Lawvere theories and are in awe of their power. However, it can be hard to find instances where Lawvere theories are used to get something specific and practical accomplished.

  • There are lots of papers on Petri nets and their variants. The bibliography on Petri nets world has over 8500 citations. This generalization puts some of the more popular variants under a common framework and allows for exploration of the relationships between them.

This is a blog for category theory so I figured I’d tell you what a Petri net is.

Definition: A Petri net is a pair of functions

(s,t:T[S]) (s,t \colon T \to \mathbb{N}[S])

where :SetSet\mathbb{N} \colon \mathsf{Set} \to \mathsf{Set} is the free commutative monoid monad which sends a set to (the underlying set of) the free commutative monoid on that set. A Petri net can be thought of as a graph whose vertices are elements of a free commutative monoid. TT is called the set of transitions, SS is the set of places, and ss and tt are the source and target functions. The idea is that each place can hold a natural number of tokens which can be shuffled around by a transition in proportions given by its source and target.

There is a classical result which says that every Lawvere theory Q\mathsf{Q} gives a monad M Q:SetSetM_{\mathsf{Q}} \colon \mathsf{Set} \to \mathsf{Set}. This generalizes the monad \mathbb{N}. We use this to generalize Petri nets into Q\mathsf{Q}-nets.

Definition A Q\mathsf{Q}-net PP is a pair of functions

(s,t:TM QS) (s,t \colon T \to M_{\mathsf{Q}} S)

A morphism from PP to a Q\mathsf{Q}-net

(P=s,t:TM QS) (P' = s',t' \colon T' \to M_{\mathsf{Q}} S')

is a pair of functions f:TT,g:SS f\colon T \to T',g \colon S \to S' that respect the source and target functions of PP and PP'. This defines a category Q\mathsf{Q}-net.

This category depends functorially on the Lawvere theory Q\mathbf{Q}. Indeed there is a functor

()-Net:LawCat(-)\text{-}\mathsf{Net} \colon \mathsf{Law} \to \mathsf{Cat}

A classical result says that morphisms of Lawvere theories give nice morphisms of the monads they induce. This relationship is used to define the functors in the image of ()(-)-Net\mathsf{Net}.

Functoriality is nice. We have the following diagram of Lawvere theories:


  • SEMILAT\mathsf{SEMILAT} is the Lawvere theory of semi-lattices i.e. idempotent commutative monoids,

  • CMON\mathsf{CMON} is the Lawvere theory of commutative monoids,

  • MON\mathsf{MON} is the Lawvere theory of monoids,

  • ABGRP\mathsf{ABGRP} is the Lawvere theory of abelian groups and,

  • GRP\mathsf{GRP} is the Lawvere theory of groups.

I won’t say what the functors in this diagram are except that they are the most natural functors of their type; I refer you to my paper to see what they actually are. This diagram induces the following diagram of categories using the functor ()(-)-Net\mathsf{Net}:

Many of the categories here are familiar to the Petri net community.

  • SEMILAT\mathsf{SEMILAT}-Net\mathsf{Net} is the category of elementary net systems. These are Petri nets which can have a maximum of one token in each place. Elementary net systems are used to represent non-concurrent programs; the location of the token represents how far along the computer is in execution.

  • Petri\mathsf{Petri} is the good old category of Petri nets.

  • PreNet\mathsf{PreNet} is the category of pre-nets; Petri nets which are equipped with an ordering of the places on their input and output. These are useful for keeping track of causality in sequences of processes.

  • \mathbb{Z}-Net\mathsf{Net} is the category of integer nets. These are lending Petri nets without a few properties. Integer nets and lending Petri nets are useful for modeling credit and borrowing. Places can hold negative tokens which represent debt.

Some of the functors in this diagram are known. cc-Net\mathsf{Net} and ee-Net\mathsf{Net} are commonly referred to as abelianization. This is because the cc-Net\mathsf{Net} sends a pre-net to the Petri net with an abelianized free monoid of places by forgetting about the ordering on the input and output of each species. ee-Net\mathsf{Net} is an analogous functor for \mathbb{Z}-Net\mathsf{Net} and their non-commutative cousin GRP\mathsf{GRP}-Net\mathsf{Net}.

This all sounds great but definitions are cheap. To justify a generalization can show that in its examples familiar consequences follow. Petri nets present free commutative monoidal categories: i.e., there is a meaningful adjunction between the category of Petri nets and a category where the objects are commutative monoidal categories. Commutative monoidal categories are symmetric monoidal categories whose symmetries are given by the identity. If you prefer, you can think of commutative monoidal categories categories as commutative monoid objects in Cat\mathsf{Cat}.

This statement can be seen as a justification of the usefulness of Petri nets, because symmetric monoidal categories are the language of processes which can be done in sequence and in parallel. This adjunction makes precise the way in which Petri nets represent processes and gives a mathematical description of the way transitions shuffle tokens around in a Petri net. For a Petri net PP, the free commutative monoidal category on PP is a category where the objects are all possible token configurations and the morphisms are all possible processes which bring one token configuration to another.

If the definition of Q\mathsf{Q}-Net\mathsf{Net} is any good we should have a similar statement for Q\mathsf{Q}-nets. Indeed, Q\mathsf{Q}-nets present free models of Q\mathsf{Q} in Cat\mathsf{Cat}. There is an adjunction

F QU Q:Q-NetQ-CatF_{\mathsf{Q}} \dashv U_{\mathsf{Q}} \colon\mathsf{Q}\text{-}\mathsf{Net} \to \mathsf{Q}\text{-}\mathsf{Cat}

where Q\mathsf{Q}-Cat\mathsf{Cat} is the subcategory of Mod(Q,Cat)\mathsf{Mod( Q, Cat)} consisting of

  • categories which have a free model of Q\mathsf{Q} of objects, and

  • functors whose object component is the unique extension of a function between the generating sets.

This may seem like an ugly category, but I’m convinced it’s necessary. The freeness of the objects of the objects in Q\mathsf{Q}-Cat\mathsf{Cat} arise because Q\mathsf{Q}-nets have a free model of Q\mathsf{Q} of species. Just like Petri nets, for a Q\mathsf{Q}-net PP, F QPF_{\mathsf{Q}} P is a category where the morphisms represent all possible process which can be built using the transitions of PP, the operations of Q\mathsf{Q}, and composition.

Although I don’t do this yet, this formalism can be used to efficiently generate new variants of Petri nets which follow some set of algebraic rules. The above adjunction means that these nets are equipped with an out of the box description of their operational semantics. I’m just starting to explore Q\mathsf{Q}-nets and I’m excited to see what else they can do.

Posted at April 28, 2019 3:36 AM UTC

TrackBack URL for this Entry:

12 Comments & 0 Trackbacks

Re: Generalized Petri Nets

I may have some questions, just to make sure that I’m following, but if I am following to some extent, then the set-up is somewhat reminiscent of computads (of various flavors).

An ordinary computad is a device used to present 22-categories. It is given by sets F,E,VF, E, V (think faces, edges, vertices) together with

  • Source and target maps s,t:EVs, t: E \rightrightarrows V, giving a directed graph GG, and
  • Source and target maps s,t:FPath(G)s', t': F \rightrightarrows Path(G) where Path(G)Path(G) is the set of directed paths in the graph GG.

In slightly different terms, Path(G)Path(G) is the set of morphisms in the free category generated by GG. One can now think of the faces ϕF\phi \in F as “2-cells”, and consider the 2-category that is freely generated by pasting together such 2-cells. This type of thing comes up when we describe 2-categories using string diagrams.

As a matter of fact, a special case of computad is a MonMon-net. In the Joyal-Street language of string diagrams (see their Geometry of Tensor Calculus), they call it a tensor scheme. It’s the special type of computad where VV consists of a single element. In this case, Path(G)Path(G) may be identified with E *E^\ast, the free monoid generated by EE. Then they go on to describe the free (strict) monoidal category generated by the tensor scheme/MonMon-net, and it smells like you’re considering the same type of thing here, where you construct a MonMon-category from a MonMon-net, or more generally a QQ-category from a QQ-net.

Is this on the right track? There are still other versions of this type of thing, involving not monads just on SetSet but on CatCat, and this comes up in the formalism of pros, props, and related things.

Posted by: Todd Trimble on April 28, 2019 11:00 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Yes! I do think you’re on the right track. Thanks for noticing this connection. One thing is that Mon\mathsf{Mon}-nets are more commonly called Pre-nets.

I’m sort of confused right now actually because it seems like the way that Joyal and Street generate these free strict monoidal categories gives an adjunction

FU:PreNetSMC F \vdash U \colon \mathsf{PreNet} \to \mathsf{SMC}

where SMC\mathsf{SMC} is the category of strict monoidal categories and functors. For me this didn’t work because pre-nets have a free monoid of species. I could get an adjunction in SMC\mathsf{SMC} by changing the definition so pre-nets have an arbitrary monoid of species.

Posted by: Jade Master on April 29, 2019 6:04 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Yes, a main focus in the Joyal-Street paper is on symmetric monoidal categories generated by tensor schemes, etc., but string diagrams can be used to treat monoidal categories generated by such data as well. I thought they also treated this case as a warm-up to the more involved case of SM categories, but even if they didn’t, you can still do that.

A remark on the word “species”. For category theorists, this word is often used in the context of Joyal species which are functors whose domain is the groupoid of finite sets and bijections between them. It sounds like species has a different meaning here. You spoke of “input and output” of species. Transitions have inputs and outputs (sources and targets), so a wild guess is that “species” refers to transitions, but I’m not at all confident that could be right.

Posted by: Todd Trimble on April 29, 2019 7:12 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Jade knows a bit about species in Joyal’s sense (and my student Joe is more deep into those), but in Petri net theory that word is used in another sense.

A Petri net is a pair of functions

f:T[S] f: T \to \mathbb{N}[S]

where TT is a set and [S]\mathbb{N}[S] is the underlying set of the free commutative monoid on the set SS.

Some people call SS the set of places and TT the set of transitions, and indeed some people call a Petri net a P/T net.

But often we think of SS as a set of ‘different kinds of things’, rather than different places where things can be. And in applications of Petri nets to chemistry, SS is called a set of species. You see, in chemistry, a species can be a type of molecule, or ion, etc.

The word ‘species’ is nice here, because another application of Petri nets is to population biology, where the species may be biological species!

Since I’ve done a lot of work on applications of Petri nets to chemistry, and a bit on population biology too, I call elements of SS species and elements of TT transitions. In these contexts using the word ‘places’ would confuse readers.

In this terminology, a transition has a finite \mathbb{N}-linear combination of species as its source, and a finite \mathbb{N}-linear combination of species as its target.

I see in this post Jade called SS a set of ‘places’, but in her last comment she switched to calling them ‘species’, out of force of habit.

Posted by: John Baez on April 29, 2019 9:38 PM | Permalink | Reply to this

Re: Generalized Petri Nets

In the computadic world, the objects are definitely free on the left and not on the right. This means the definition of the right adjoint has to be different: rather than taking the same underlying (free) monoid of objects, you take the monoid of objects in an SMCSMC as the generators of a free monoid of objects for a pre-net, and then pull back the morphisms along the counit of the free-monoid adjunction to get the transitions in your pre-net.

Posted by: Mike Shulman on April 29, 2019 6:48 PM | Permalink | Reply to this

Re: Generalized Petri nets

Just to make sure I understand. The right adjoint takes the pullback over

s:MorCObCs \colon \mathrm{Mor} C \to \mathrm{Ob} C


ϵ:ObC *ObC\epsilon \colon \mathrm{Ob} C^* \to \mathrm{Ob} C

to get a new (larger) set of transitions. The new source function is given by the map from this pullback to ObC *\mathrm{Ob} C^*?

Posted by: Jade Master on April 29, 2019 7:36 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Almost; it’s the pullback of (s,t):MorCObC×ObC(s,t) : Mor C \to Ob C \times Ob C along ϵ×ϵ:ObC *×ObC *ObC×ObC\epsilon\times \epsilon : Ob C^\ast \times Ob C^\ast \to Ob C \times Ob C. (Sorry if my “free on the left and not on the right” confused you; by “the left” I meant in PreNetPreNet and “the right” I meant in SMCSMC.)

Posted by: Mike Shulman on April 30, 2019 10:04 AM | Permalink | Reply to this

Re: Generalized Petri Nets

Okay thanks so much! I’m gonna be busy rewriting my paper to take this into account.

Do you remember where you learned this fact? I can’t seem to find it in The Geometry of Tensor Calculus.

Posted by: Jade Master on April 30, 2019 5:29 PM | Permalink | Reply to this

Re: Generalized Petri Nets

It’s kind of hidden in GoTC. They don’t even define morphisms of tensor schemes explictly. But if you give the obvious such definition, and then look at their definition of the category [𝒟,𝒱][\mathcal{D},\mathcal{V}] after Definition 1.4, where 𝒟\mathcal{D} is a tensor scheme and 𝒱\mathcal{V} a monoidal category, you can see that the objects of [𝒟,𝒱][\mathcal{D},\mathcal{V}] are equivalently the morphisms of tensor schemes 𝒟U𝒱\mathcal{D} \to U\mathcal{V}, where UU is the right adjoint as I described it. Then their remark at the end of chapter 1 (page 73) that [𝒟,𝒱][\mathcal{D},\mathcal{V}] is isomorphic to the category of strict monoidal functors F𝒟𝒱F\mathcal{D}\to \mathcal{V} implies, upon forgetting the 2-cells, that FUF\dashv U as 1-functors between the 1-category of tensor schemes and the 1-category of monoidal categories (and strict monoidal functors).

I believe the reason they work with [𝒟,𝒱][\mathcal{D},\mathcal{V}] instead of phrasing the theorem in this way is that using [𝒟,𝒱][\mathcal{D},\mathcal{V}] they can also give a universal property of F𝒟F\mathcal{D} relative to 2-cells and pseudo monoidal functors. The latter can’t obviously be expressed as any kind of adjunction, since tensor schemes don’t form a 2-category. But the simpler adjunction of 1-categories is also useful to know!

Posted by: Mike Shulman on April 30, 2019 11:36 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Todd mentioned “pros, props, and related things”. One day I’d like to see a general version of such “related things”, analogous to generalized multicategories but where both domain and codomain are parametrized by a monad. The first step in that direction was Garner’s observation that a polycategory can naturally be defined abstractly from two copies of the free-monoid monad and a pseudo-distributive law between them, but as far as I know no one has taken that any further. Your QQ-nets would be the generating data for one of these things where both monads are M QM_Q (and, I guess, the distributive law could be arbitrary).

Posted by: Mike Shulman on April 29, 2019 6:52 PM | Permalink | Reply to this

Re: Generalized Petri Nets

I am slightly disturbed that I haven’t needed distributive laws for this. Section 7.3 of Petri Nets are Monoids by Meseguer and Montanari describe a way of generalizing Petri nets in a way that seems more like the construction for polycategories. They start with a morphism of commutative monads on Set\mathsf{Set}, TTT \Rightarrow T'. Then they construct a monad on Grph\mathsf{Grph} which sends a graph

s,t:EVs,t \colon E \to V

to the graph with source (and target) given by

TEα ETETsTVT E \xrightarrow{\alpha_E} T' E \xrightarrow{T's} T'V

I didn’t need this level of generality because in most applications the structure you want to generate on the transitions is the same as the structure you want on the morphisms. The reason that they want these monads to be commutative is to ensure that the category of algebras of this monad is symmetric monoidal closed.

Posted by: Jade Master on April 30, 2019 6:01 PM | Permalink | Reply to this

Re: Generalized Petri Nets

Note that the distributive law used by Garner lives in ProfProf, not in CatCat. When I spent some time playing around with this a bit a while ago, I convinced myself that for a sufficiently nice monad TT, the composite of the representable and corepresentable profunctors corresponding to its monad multiplication TTXTXTTXT T X ⇸ T X ⇸ T T X ought to be a distributive law of TT over itself in ProfProf, and that the corresponding notion of “generalized polycategory” would be a sort of “generalized prop” (and in particular would be ordinary props when TT is the free symmetric monoidal category monad). So if you’re thinking only about that case, then the distributive law might not appear explicitly.

Posted by: Mike Shulman on April 30, 2019 11:41 PM | Permalink | Reply to this

Post a New Comment