nLab Petri net

Redirected from "Petri nets".
Contents

Contents

See also the Petri net in The Azimuth Project.

Introduction

Petri nets are a well known model of concurrent computation, generalising transition systems by using a built in notion of resource. Their use is widespread in modelling manufacturing systems, optimising control systems and in resource critical aspects of operational research, as well as being a useful model of computation. Because of this they exist in many variants : colored, algebraic, probabilistic, timed, …, and hence there are many forms of the basic definition, each thought best of that particular application.

The initial use, here, is for their links with transition systems, event structures, asynchronous automata etc., leading on to their comparison with higher dimensional automata? and higher dimensional transition systems, so the first definition we will use is that given by Winskel and Nielsen (see references below), but first we will attempt to give some idea of what a Petri net is and what it does.

Idea

The idea of a simple Petri net is based on a simple manufacturing shop. You have various ‘transitions’ or manufacturing ‘events’ that form part of the various process occurring in the ‘shop’. These typically take parts (of the final object), do something to them, such as combining two or more different parts to make a more complicated one, (for instance, putting the wheels on a car).

Parts, represented by ‘tokens’ are stored in ‘places’ and the assembly process are known, as above, as ‘events’ or ‘transitions’ (depending on the source being used for the theory). The relationships are typically represented graphically. For instance:

Layer 1 1 1 1 e A B C

represents a system with three places (labelled AA, BB, and CC) and one event/ transition (labelled ee). Shown is a situation represented by an initial ‘marking’ where there are two tokens in AA, one in BB, and none in CC. (The convention is that places are shown as circles and events as rectangles.)

Suppose that the ‘event’ takes one ‘part’ of type AA, one of type BB and produces one of type CC. (This is indicated on the diagram by the labels on the edges. Clearly with the available resources the even ee is able to be performed. (The usual Petri net jargon for this is that ‘ee is enabled’.) In this case, ee can be ‘fired’ and the result will yield a marking of one token in AA, none in BB and one in CC. This sort of structure gets abstracted as follows:

Definition

A Petri net NN consists of

  • a set PP of places;

  • an initial marking M 0 PM_0 \in \mathbb{N}^P, so M 0:PM_0 : P \to \mathbb{N};

  • a set EE of events; and

  • two functions

    • pre:P×Epre: P\times E\to \mathbb{N}, and

    • post:P×Epost: P\times E\to \mathbb{N}.

Categorical Semantics of Petri Nets

The functions prepre and postpost can be curried to write a Petri net as a pair of functions

where [P]\mathbb{N}[P] denotes the free commutative monoid on the set PP of places. Written this way, the analogy to graphs is clearer. The main difference is that now the source and target functions land in a free commutative monoid rather than just a set. Thus, Petri nets can be thought of as symmetric monoidal graphs because each edge is a multi-edge between a permutable sum of vertices. Just as graphs generate free categories, Petri nets should generate free symmetric monoidal categories. As Petri nets often model processes in various sciences, the free symmetric monoidal categories that they generate model the operational semantics of these processes. For a given Petri net PP, the free symmetric monoidal category FPFP that it generates should have objects given by possible markings of PP, and morphisms given by ways of composing the events in sequence and in parallel.

The first to explore this idea were Meseguer and Montanari who constructed an adjunction between Petri nets and a subcategory of the category CMCCMC of commutative monoidal categories. This adjunction was modified in Petri nets based on Lawvere theories to get

Although morally Petri nets generate free symmetric monoidal categories, it turns out that because they have a free commutative monoid of places, they more naturally generate commutative monoidal categories, symmetric monoidal categories of an unusually strict type. Commutative monoidal categories don’t show up often in nature because they aren’t the result of a coherence theorem for symmetric monoidal categories. Mac Lane's coherence theorem for symmetric monoidal categories says that every symmetric monoidal category is symmetric monoidally equivalent to a strict symmetric monoidal category which may have nontrivial symmetry morphisms. However, commutative monoidal categories have symmetry morphisms which are given by the identity so they aren’t the strictifications of symmetric monoidal categories.

Computer scientists also haven’t been satisfied with commutative monoidal categories as a categorical semantics for Petri nets. Commutative monoidal categories are said to exhibit the collective token philosophy (see e.g. Glabeek and Plotkin), where tokens do not have individual identities. On the other hand, symmetric monoidal categories are said to have the individual token philosophy where the individual identities of the tokens are retained. The easiest to see where an issue shows up is with a variation of the Eckmann-Hilton argument. Let CC be a commutative monoidal category and let f,g:aaf,g \colon a \to a be morphisms from an object a to itself. Then,

gf+1 a =gf+1 a1 a =(g+1 a)(f+1 a) =(g+1 a)(1 a+f) =g1 a+1 af =g+f\begin{aligned} g \circ f + 1_a & = g \circ f + 1_a \circ 1_a \\ &= (g+ 1_a)\circ (f + 1_a) \\ &= (g + 1_a) \circ (1_a + f) \\ & = g \circ 1_a + 1_a \circ f \\ &= g + f \end{aligned}

So in a commutative monoidal category gf+1 a=g+fg \circ f + 1_a = g+ f even though they have very different semantic interpretations: one represents sequential composition and the other represents parallel composition.

One possible fix to this is to change the definition of Petri net. In Functorial Models for Petri Nets the authors introduced pre-nets. A pre-net is a pair of functions from a set of events to the free monoid on a set of places. The key difference is that now every event is equipped with an ordering on the input and output of each transition. With pre-nets, there is a natural adjunction between the category PreNetPreNet of pre-nets and SMCSMC the category of strict monoidal categories

which can be composed with the adjunction which freely adds symmetries to a strict monoidal category to get an adjunction

where SSMCSSMC is the category of strict symmetric monoidal categories. This gives a categorical operational semantics for pre-nets which obeys the individual token philosophy and avoids the pitfall of the above computation. Pre-nets can be turned into Petri nets via abelianization. For a given Petri net PP, its abelianization forgets about the ordering on the input and output of each event. Therefore, to obtain a categorical semantics for a Petri net PP which obeys the individual token philosophy, a pre-net QQ can be chosen which abelianizes to PP. Then, the categorical semantics for PP can defined as the free strict symmetric monoidal category L(Q)L(Q).

References

For an introduction to Petri nets (en francais, which is very clear and accessible) look at

On the connection to linear logic:

On the categorical semantics of Petri nets:

  • José Meseguer and Ugo Montanari?, Petri nets are monoids, Information and Computation, Volume 88, Issue 2, Pages 105-155, 1990. journal, pdf

  • Jade Master, Petri nets based on Lawvere theories, Mathematical Structures in Computer Science 30, no. 7 (2020): 833-864. Available at journal

  • Roberto Bruni?, José Meseguer, Ugo Montanari?, and Vladimiro Sassone. Functorial models for Petri nets Information and Computation 170, no. 2 (2001): 207-236. pdf

  • Rob J. van Glabbeek?, and Gordon Plotkin. Configuration structures, event structures and Petri nets Theoretical Computer Science 410, no. 41 (2009): 4111-4159. Available at pdf

Last revised on March 6, 2024 at 15:39:35. See the history of this page for a list of all contributions to it.