A compositional framework for Petri nets
Serge Lechenne1,2 , Clovis Eberhart2,3 , and Ichiro Hasuo2,41École normale supérieure Paris-Saclay, Gif-sur-Yvette, France
2
National Institute of Informatics (NII), Tokyo, Japan
3
Japanese-French Laboratory for Informatics, IRL 3527, Tokyo, Japan
4
SOKENDAI (The Graduate University for Advanced Studies), Hayama, Japan

Abstract. We define a bidirectional compositional framework for Petrinets based on a line of work about compositionally defining games andcomputation models. This relies on defining structures with open ends
that form interfaces they can be composed along. Together with this
syntactic construction, we give a graphical language of morphisms in a
PROP and a semantic category that describes the evolution of markingsin a Petri net. Compared to previous work, the novelty is that computations in a Petri net are stateful, requiring specific care. This framework
allows us to solve reachability compositionally.
Keywords: Petri Nets · Category Theory · Compositionality

1

Introduction

Petri nets [13,15,16] are a graph theoretical formalisation of concurrency andparallel programming. Agents are represented by places and communication between agents by transitions. The main question in this formalism is how information circulates between agents. This information is represented by tokens thatare contained in places and transmitted to other places by transitions.
A crucial problem on Petri nets is reachability [16]: Given an initial marking(a number of tokens in each place), is there a sequence of transitions that reaches
a given final marking? In this paper, we develop a compositional framework for
Petri nets that we call open Petri nets. The idea is that we equip Petri nets with
open ends, which are interfaces along which two Petri nets can be composed. The
reachability problem naturally becomes an open-reachability problem [19], where
the question is to know whether, starting from a given marking on the entry
interface of the open Petri net, a given marking on its exit interface is reachable.
We then define a graphic language for Petri nets based on PROPs, a categoricalframework that has been successfully used to model many different graphicalstructures [1,5,6,7]. It abstracts away all the complexity of the definition of open
Petri nets by defining a syntax based on generators and equations. Finally, tosolve the open-reachability problem, we define a semantic category into which
open Petri nets can be interpreted and where open-reachability can be solved.
The base idea is that this semantic category is morally a category of relations

2

Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

between entry markings (markings on the entry interface) and exit markings(markings on the exit interface).
This development follows previous work on different open structures: open
parity games [20], open Markov decision processes [21], and open mean-payoff
games [22]. However, there are several fundamental differences between previous
work and the current article. The first one is that the nature of the structurestudied here is different from those of the games studied before. All the games
previously studied are sequential in the sense that they are games that consistof passing around a single token. Therefore, when studying a game composed ofmany sub-games, only one sub-game may play: the game that currently contains
the token. In Petri nets, there are many tokens passed around, and the nature of
the structure is, therefore, completely concurrent. This means that the semantic
composition of Petri nets should be different from those of previous structures.
Another difference is that all the structures we have previously studied arememoryless, in the sense that solving problems on those structures only require
the knowledge of which place the token is in. This means that most of thestructure can be abstracted away in the semantics. In an open Petri net, apossible exit marking is dependent on the entry marking, but also on the internal
state of the Petri net, which is therefore relevant to our approach. In this sense,
we may say that the properties studied in the previous papers in this line ofwork were static, while we study a dynamic property here. For these reasons,the semantic category of open Petri nets differs from those of the previous papers.
One advantage of our approach is that we derive a complex bidirectionalframework, expressed in the language of compact closed categories (CompCCs),
from a simpler unidirectional framework, expressed in the language of traced
symmetric monoidal categories (TSMCs). This is done for free using the wellknown Int-construction [10]. On the level of Petri nets, this means that we derivea category oPN of open Petri nets from a category roPN of rightward open Petrinets where all open ends point towards the right. We do the same at the levelof semantics, the semantic category Sr for the unidirectional framework is lifted
to S in the bidirectional framework using the same construction. Moreover, theInt-construction also lifts the interpretation of open Petri nets into the semantic
category from the unidirectional level (Sr ) to the bidirectional one (S). This is
the result of Lemma 6, which is illustrated in Figure 1.

roPN

Sr
Sr

oPN = Int(roPN)

S = Int(Sr )S = Int(Sr )Fig. 1. Lifting from the unidirectional framework to the bidirectional framework

Related Work As previously mentioned, this work is a continuation of a line ofwork on compositional structures [20,21,22], which aims at using compositionality to design faster algorithms to compute properties of structures.

A compositional framework for Petri nets

3

Our graphical language is based on PROPs, which are a specific type oftraced symmetric monoidal categories. Many lines of work have used TSMCs asgraphical languages. This dates back to [12], see [17] for a survey. For graph-likestructures, [8] considers acyclic graphs. In recent years, PROPs have been used
to study many graphical structures such as networks [1], signal flow diagrams [5],and quantum graphic calculi [6,7].
Many other works describe compositional approaches to Petri nets. In [3,2],
open Petri nets are defined as cospans and composed by pushout. While thisis close to our presentation, the fact that open Petri nets are cospans meansthat they are not exactly graphical objects. In [4], the authors define a graphicallanguage for linear systems. By interpreting this language in the right category,they can encode Petri nets. While their approach is also based on string diagrams,
it is a bit farther from graphical intuition than ours, as places, transitions, andtheir interactions, are encoded as non-trivial string diagrams.
In [19,18], the authors develop a compositional approach to Petri nets, called“Petri nets with boundaries”. One advantage is that the categorical structure canbe used to derive efficient algorithms. Petri nets with boundaries, in the fashionof a compositional approach, simplify model checking by applying a “divide andconquer” approach, as explained in [14]. We here present a systematic derivationof a compositional Petri net framework, separating the essence of Petri nets
with boundaries from specific details. Our framework, called “open Petri nets”,
is derived systematically, while Petri nets with boundaries were derived in asomewhat ad hoc manner. This approach is the closest to ours, and we offer amore thorough comparison in the article.

Plan In Section 2, we give some reminders on Petri nets and introduce rightward open Petri nets. Then, in Section 3, we study the structure of rightward
open Petri nets and show that they form a traced symmetric monoidal category(TSMC), and compare them to Petri nets with boundaries. Section 4 is dedicatedto defining the semantic category and proving that it is also a TSMC, as well as
the interpretation of rightward open Petri nets into the semantic category andprove that it respects the TSMC structure. Finally, we derive the bidirectionalframework in Section 5 as well as a syntax to inductively compute on open Petrinets, and use this to solve the open-reachability problem compositionally.

Notations and Prerequisites We assume that the reader is familiar with somebasic notions of category theory, especially monoidal categories. For all k ∈ N,
we write [k] for the set {1, 2, . . . , k}. Given a proposition P , we write δP for the
Kronecker symbol, i.e., δP = 1 if P holds, and δP = 0 otherwise. Given two
functions f : X → Y and f ′ : X ′ → Y ′ , we name f + f ′ : X + X ′ → Y + Y ′ thefunction obtained by universal property of coproduct. Given two pairs of natural
numbers n = (a, b) and m = (c, d), we write n + m for the pair (a + c, b + d).

4Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

2

Rightward Open Petri Nets

After some brief reminders on Petri nets, this section describes our first contribution, rightward open Petri nets, which are a compositional approach to Petrinets. For Petri nets, we follow the notations and definitions from [19].
2.1

Petri nets

Definition 1 (Petri nets). A Petri net is a tuple (P, T, • ( ), ( )• ) where– P (resp. T) is a set whose elements are called places (resp. transitions),– • ( ) and ( )• are functions T → P(P ).
Petri nets admit a graph-theoretical representation [13,15,16] where the places
are drawn as circles and the transitions as rectangles, sometimes with their labels
written around them. The function • ( ) is represented by arrows from place totransitions, and the function ( )• by arrows from transitions to places. For example, the Petri net with P = {p1 , p2 , p3 }, T = {t}, • t = {p1 }, and t• = {p2 , p3 }can be represented as on the left of Figure 2.

p1

t

p2

t

t

p3

Fig. 2. A Petri net, a marking of it, and the marking reached after firing transition t

The data, named tokens, is exchanged through the transitions from place toplace. Intuitively, the data does not represent any physical object but informationthat agents can freely exchange, create or destroy. This information circulating
in a network is modelled in the form of a marking function.
Definition 2 (marking). A marking function (or marking) on a Petri net isa function µ : P → N.
Information is transmitted between agents by selecting a transition t, consuming one token from every place leading to t (i.e., every place in • t) andplacing one token in every place reached by t (i.e., every place in t• ).
Definition 3 (enabling, firing). Given a Petri net, a transition t, and a marking µ, we say that t is enabled by µ if ∀x ∈ • t, µ(x) ≥ 1.
A transition t enabled by a marking µ can modify it into a new marking µ′
defined by µ′ (x) = µ(x) + δx∈t• − δx∈• t . This operation is called firing t, and istdenoted µ →− µ′ .

A compositional framework for Petri nets

5

In the definition above, µ′ removes one token from µ in all places in t• , andadds one to all places in • t.
We extend the notation of firing to sequences s = t1 , . . . , tn ∈ T ∗ and writesµ −→ µ′ to mean that each ti is enabled on the marking reached from µ after
firing all the previous tj ’s and that µ′ is reached after firing tn . We will also
write t(µ) the marking µ′ (or tN (µ) when the Petri net N is not explicit).
We now illustrate how the graphical representation accommodates markings
and firings of transitions. Tokens are represented as black dots, and a marking µ
is represented by placing µ(x) tokens in each place x. For example, remembering
the example Petri net on the left of Figure 2, the drawing in the middle of
Figure 2 represents the marking µ defined by µ(p1 ) = 2 and µ(p2 ) = µ(p3 ) = 0.
The transition t is enabled by µ in this net, and firing it outputs the marking
on the right of Figure 2.
2.2

Rightward Open Petri Nets

We now define rightward open Petri nets, which have open ends along which they
can be composed. We then adapt all the definitions of Petri nets to rightward
open Petri nets.
Definition 4 (rightward open Petri net). A rightward open Petri net is atuple N = (m, n, P, T, ◦ ( ), ( )◦ , • ( ), ( )• ) where– m = (mb , mr ) and n = (nb , nr ) are pairs of natural numbers called the ( left
and right) interfaces of N ,– P (resp. T ) is a set whose elements are called places (resp. transitions),– ◦ ( ) : mr → T + nr , mb → P + nb is a function such that ∀j ∈ [nb ] +[nr ], i1 , i2 ∈ [mb ] + [mr ], ◦ (i1 ) = j = ◦ (i2 ) ⇒ i1 = i2 ,– ( )◦ : P → P([nr ]), T → P([nb ]) is a function such that ∀t, t′ ∈ T ∪ P, (t)◦ ∩(t′ )◦ ̸= ∅ ⇒ t = t′ ,•– ( ) and ( )• are functions T → P(P ).

t1

p1

t2

p2
p3
t3

Fig. 3. A rightward open Petri net with interfaces (1, 1) and (1, 1)

We now explain in detail what each element of the tuple represents. First ofall, P , T , • ( ), and ( )• represent the same elements as for regular Petri nets.
The left and right interfaces, m and n, respectively, encode the number of open6

Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

ends on the left-hand and right-hand side of the rightward open Petri net. They
are pairs of numbers because open ends that point to places are different fromopen ends that point to transitions; mb and nb represent open ends that point
to places, while mr and nr represent open ends that point to transitions. The
subscripts b and r stand for “black” and “red” respectively, corresponding to thegraphical representation we show below. The constraints on ◦ ( ) and ( )◦ meanthat there is at most one arrow pointing to each open end on the right.
The function ◦ ( ) (which is formally two functions, but for which we use
the same symbol) encodes how each open end on the left (in [mb ] or [mr ]) is
connected to a place, a transition, or an open end on the right (i.e., in [nb ]or [nr ]). The type of the function ensures that black open ends only point toeither places or black open ends on the right, and red open ends only to eithertransitions or red open ends on the right.
The function ( )◦ (which is again formally two functions) encodes the connection of places and transitions to open ends on the right.
We also adapt the graphical representation of Petri nets to rightward open
Petri nets by graphically drawing ◦ ( ) as arrows coming from the left open ends
and leading to places, transitions, or to the right open ends. We draw ( )◦ similarly from places and transitions to right open ends. Figure 3 shows an exampleof the graphic representation of a rightward open Petri net. It describes therightward open Petri net with m = n = (1, 1), P = {p1 , p2 , p3 }, T = {t1 , t2 , t3 },◦1b = p2 , ◦ 1r = t1 , p◦1 = p◦2 = t◦1 = t◦3 = ∅, p◦2 = 1r , t◦3 = 1b , • t1 = ∅, • t2 = {p1 },•t3 = {p3 }, t•1 = {p1 }, t•2 = {p2 , p3 }, and t•3 = ∅, where 1b , 1r are used to distinguish between black and red open ends (even though it is unambiguous even
without this distinction because of the typing).
Open ends are numbered, and verticality in the graphical representation encodes the order between open ends. Note that we always draw black open ends
above red ones for interfaces, but that is just a graphical convention: there is noorder between open ends of different colours.
We can now define configurations, which are the counterparts of markings for
traditional Petri nets. We can then define the way roPN configurations evolve.
Like Petri nets, they evolve through firing transitions. The main difference withtraditional Petri nets is that they can also evolve by tokens “sliding” from theentry interface to the exit interface.
Definition 5 (Markings, configurations). Given a rightward open Petri net
with interfaces m and n and a set P of places, a marking is a function µ : P → N,an entry marking is a function µi : [mb ] + [mr ] → N, and an exit marking isa function µo : [nb ] + [nr ] → N. A configuration is an element (µi , µ, µo ) of
Nmb +mr × NP × Nmb +mr .
Definition 6 (firing, sliding). Given a rightward open Petri net N , a configuration c = (µi , µ, µo ), and a transition t, we say that t is enabled on c if for allplaces p ∈ • t, µ(p) > 0, and for all entries i ∈ [mr ] such that ◦ i = t, µi (i) > 0.
Similarly, an entry i ∈ [nb ] is enabled on c if µ(i) > 0, and an exit j ∈ [mr ], forwhich there exists p ∈ P with j ∈ p◦ , is enabled if µ(p) > 0.

A compositional framework for Petri nets

7

The firing of t enabled on c turns it into (µ′i , µ′ , µ′o ) such that µ′i (i) = µi (i) −δ◦ i=t , µ′ (p) = µ(p) − δp∈• t + δp∈t• t , and µ′o (j) = µo (j) + δj∈t◦ .
The sliding of entry i enabled on c turns it into (µ′i , µ′ , µ′o ) with µ′i (i′ ) =µi (i′ ) − δi′ =i , µ′ (p) = µ(p) + δ◦ i=p , µ′o (j) = µo (j) + δ◦ i=j .
The sliding of exit j enabled on c turns it (µ′i , µ′ , µ′o ) with µ′i = µi , µ′ (p) =µ(p) − δp◦ = j, and µ′o (j ′ ) = µo (j ′ ) + δj=j ′ .
In this definition, sliding is rather straightforward: tokens may slide freely
between open ends and places (as these correspond to transitions being fired
outside of the open Petri net). To fire a transition, all arrows pointing to it must
contain at least one token: both from places and from open ends.
We denote by t(c) the configuration obtained by firing transition t from c.
Similarly, we denote by li (c) (resp. rj (c)) the configuration obtained by sliding
the ith entry (resp. jth exit) from c.

3

The Categorical Structure of roPN

We now move on to explicitating the categorical structure of rightward open
Petri nets, viewed as arrows between interfaces. We explicitate the categoricalstructure of rightward open Petri nets, using the language of monoidal categories [11,9]. We will then compare our approach and the work done in [19,18].
3.1

The Category of Rightward Open Petri Nets

We start by establishing their structure as a category by defining the identities
and composition. When a Petri net N has interfaces m and n, we write N : m →n. Indeed, in this section we define the category roPN or rightward open Petrinets whose objects are interfaces are morphisms are roPNs.
Definition 7 (composition). Given N : m → n and N ′ : n → k, we name
N ; N ′ : m → k the rightward open Petri net made from the following data:
PN ;N ′ = P ∪ P ′ , TN ;N ′ = T ∪ T ′ ,(••tN ;N ′ =•(tNtN ′ ∪ {p ∈ P | ∃j ∈ [mr ] .j ∈ p◦N ∧ ◦ jN ′ = t}

if t ∈ Totherwise,t•N ∪ {◦ jN ′ ∈ P ′ | j ∈ t◦N } if t ∈ Tt•N ′otherwise,(◦ ◦( iN )N ′ if ◦ iN ∈ [jb ]◦iN ;N ′ = ◦iNotherwise,(x◦N ′if ◦ (x◦N )N ′ ∈ P ∪ T
x◦N ;N ′ =◦◦{ jN ′ ∈ [kb ] + [kr ] | j ∈ xN } otherwise.
t•N ;N ′ =8Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

t1

p1

p2

t2

p3
t3

Fig. 4. Two roPNs with interfaces (1, 1) → (3, 0) and (3, 0) → (1, 1) respectively

Checking that ◦ ( )N ;N and ( )◦N ;N satisfy the condition is easy.
The definitions of ( )◦ , ◦ ( ), • ( ), and ( )• encode the fact that edges thatpoint to and from the middle interface get merged in the composition N ; N ′ .
Figure 4 shows two roPNs whose composition is the roPN in Figure 3.

idm

1
..
.

1 . . . mb

1
..
.

Cm,n

1 . . . nb

mb + 1 . . . mb + nb

nb + 1 . . . nb + mb

1..
.

1 . . . mr

1 . . . nr

mr

mr + 1 . . . mr + nr

nr + 1 . . . nr + mr

mb

mb

1
..
.
mr

Fig. 5. Identities and swaps

Definition 8 (identities, swaps). Given an interface m, the identity roPN
idm : m → m is given by the following data: P = T = ∅, ◦ i = i (the rest of thedata being trivial since P = T = ∅).
Given two interfaces m and n, the swap Cm,n : m + n → n + m is given by
the following data: P = T = ∅, ◦ i is i + mb if i ≤ mb and i − mb otherwise fori ∈ [mb + nb ], and ◦ i is i + mr if i ≤ mr and i − mr otherwise for i ∈ [mr + nr ].
The identities and swaps are illustrated in Figure 5. We can now organiserightward open Petri nets into a category roPN.
Definition 9 (roPN). We name roPN the category whose objects are pairs ofelements (mr , mb ) ∈ N × N and arrows N : (mr , mb ) → (nr , nb ) are rightward
open Petri nets with the corresponding numbers of open ends. Composition isdefined by ; and the identity of m ∈ N × N is the rightward open Petri net idm .
3.2

Monoidal Categorical Structure

We now further explore the categorical structure of roPN, showing that it is a
traced symmetric monoidal category.

A compositional framework for Petri nets

9

Fig. 6. An roPN with interfaces (4, 1) and (4, 1)

Definition 10 (tensor product). Given N : m → n and N ′ : m′ → n′ , wedefine N ⊗ N ′ : m + m′ → n + n′ the rightward open Petri net given by thefollowing data: PN ⊗N ′ = P ∪ P ′ , TN ⊗N ′ = T ∪ T ′ , ◦ ( )N ⊗N ′ = ◦ ( )N + ◦ ( )N ′ ,( )◦N ⊗N ′ = ( )◦N + ( )◦N ′ , • ( )N ⊗N ′ = • ( )N + • ( )N ′ , and ( )•N ⊗N ′ = ( )•N + ( )•N ′ .
Figure 6 shows the tensor product of the two roPNs from Figure 4. Note that thisgraphically corresponds to stacking the roPNs (except for the interfaces, where
the red ends are drawn below the black ones, but which is only a convention).
Lemma 1. roPN forms a symmetric monoidal category with + as tensor on
objects, and ⊗ on morphisms, and Cm,n as the symmetries.
3.3

Trace Operator

p2
p2
p3

p3
t3

t3

Fig. 7. The trace of the roPN on the right in Figure 4 along (1, 0) and a simpler
representation

Our goal is to derive a bidirectional framework from the unidirectional one.
To do this, we need to show that roPN is traced. We first introduce some notions,as defining the trace is trickier than for composition or tensor. Graphically, thetrace operator “loops” over the first black and red inputs and outputs of the
Petri net, as shown in Figure 7.

10Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

Fig. 8. An roPN with interfaces (4, 0) and (4, 0), traced along (2, 0), and a simpler
representation

This construction has to involve some form of recursive definition to connect
inputs and outputs. Figure 8 shows an example that illustrates that if something(a place, a transition, or a left open end) is connected to one of the right open
ends affected by the trace, simply looking at the value of the corresponding open
end by ( )◦ is not enough, since we can “stay” in the loop. In order to define the•(−) function on the first open end of the traced Petri net, we have to compute•(−) of the original Petri net on three different open ends. The first open end in
the trace corresponds to the third open end, which is connected to the second,which is connected to the first, which is finally connected to the fourth. In otherwords if we denote by • (−)′ the accessibility function of the traced Petri net
and • (−) that of the original Petri net, then the formula to compute • (1)′ is• • •( ( (1 + 2))) (where 2 is the number of black wires we trace over). In general,
this can take an arbitrary number of steps, which justifies the complexity of thedefinition.
Hence, given a rightward open Petri net N : (mb +p, mr +q) → (nb +p, nr +q),
we need to define functions ϕp (for the p black open ends that are looped) that
output the final open end that does not lead back to [p] (in the loop). To ensure
such a function ϕp can be defined, we must prove that such an exiting open end
exists. The following lemma ensures this.
Lemma 2. Let j ∈ [p], then there is at most one i ∈ [mb + p] such that ◦ iN = j.
This is easily proven using the conditions imposed over (x)◦N . Finally, because[p] is finite, we define ϕp (x) by induction: ϕp (x) = x if ◦ x ∈/ [p], and ϕp (x) =ϕp (◦ x) otherwise. This definition is well-founded because of Lemma 2 and thefact that [p] is finite. We define ϕq equivalently.
Definition 11 (Trace operator). Given a rightward open Petri net N : m +p → n + p, we define N ′ = Trpm,n (N ) : m → n as the rightward open Petri net
with the following data: P ′ = P , T ′ = T ,(◦ϕp (x) if x ∈ [mb ]◦′(x) = ◦
ϕq (x) if x ∈ [mr ],(x)◦′ = {◦ (ϕp (h) | h ∈ x◦ ∩ [p]} ∪ {◦ ϕq (h) | h ∈ x◦ ∩ [q]} ∪ (x◦ \ ([p] ∪ [q]))•(t)′ = {x ∈ P | ∃h ∈ [q], h ∈ x◦ ∧ ϕq (h) ∈ • t} ∪ • t•′(t) = {x ∈ P | ∃h ∈ [q] , h ∈ t◦ ∧ ◦ ϕp (h) = x} ∪ t• .

A compositional framework for Petri nets

11

Lemma 3 (trace). Trp,qm,n (−) defines a trace over roPN.
Theorem 1. roPN is a traced symmetric monoidal category (TSMC).
3.4

Comparison with Petri Nets with Boundaries

Now that the categorical structure is spelt out, we move on to pointing out thesyntactic and operational differences between roPN and PNB, the category of
Petri net with boundaries defined in [19].

Fig. 9. Some examples of Petri nets with boundaries

We first give out a quick summary of Petri net with boundaries. A Petrinet with boundaries is thought of as a Petri net with extra structure, namely
a net (P, T, • ( ), ( )• ) as defined in our work to which is added two finite ordinals that act as the interface, and two accessibility functions, called “in” and“out” (those are not the original notations introduced in [19]), encoding how theinterface is linked to transitions. Petri nets with boundaries admit a graphicalrepresentation, as shown in Figure 9 (taken from [19]), where the boundaries are
represented as black squares located on the edges of a box enclosing the Petrinet. The two accessibility functions are represented as regular edges, connecting
the black squares and the transition.
The first main difference, and the most important one, is that the boundaries
representing the interface are connected to transitions only, meaning they are
not leading in or out of the Petri net by default. Here, it is the function in(resp. out) that makes one boundary in the interface leading to or coming fromtransitions.
The fact that boundaries are only connected to transitions also affects thecomposition of Petri nets with boundaries: we have chosen our definition of arightward open Petri net to have an “implicit” interface, which allows us to follow
graphical intuition of fusing edges. In the Petri net with boundary framework,
the fusing is intuitively done on the boundaries, as demonstrated in the two
examples shown in Figure 10 (taken from [18]). However, when fusing the edges,
the transitions these edges are connected to also need to be fused (this is called12Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

Fig. 10. composing Petri net with boundaries

a minimal synchronisation in [19]). This fusing process is destructive in regard
to the structure of the Petri net, as transitions can be either created or deleted,like in the rightmost net in Figure 10. For example, the middle two Petri nets
with boundaries in Figure 9 are the categorical identities and crossing of thecategory PNB, and they only satisfy the required naturality equations up toisomorphism, making the categorical structure lax monoidal, contrary to roPN.
Another consequence of this fact is that by connecting two boundaries of thesame interface via a transition, one can create the counit of PNB (depicted as
the rightmost net in Figure 9). As the snake equation is satisfied, this meansthat PNB is a compact closed (lax) category, where the trace is defined by
the canonical construction described in [10]. In comparison, in the case of open
Petri nets, the compact closed structure is derived from the more primitive traced
symmetric monoidal structure that describes the unidirectional case.

4

The Semantic Structure

In this section, we define the semantic category Sr , prove that it has a traced
symmetric monoidal structure, define a semantic functor Sr : roPN → Sr andprove that it respects that traced symmetric monoidal structure.
4.1

The Semantic Category Sr

The main idea is that what can be observed of an open Petri net is how many
tokens enter and exit it through its interfaces. However, that is not enough tocharacterise the behaviour of an open Petri net. Indeed, some token can be left in
the net, therefore modifying the behaviour of said net. The marking acts like aninternal state to the Petri net, and that is how we represent it in the semantics.
Definition 12 (The semantic category Sr ). We denote by Sr the semantic
category. Its objects are pairs (nb , nr ) of natural numbers. The morphisms from(mb , mr ) to (nb , nr ) are pairs of a set Q (called the set of internal states) and afunction from Nmb +mr × Q × Nnb +nr to P(Nmb +mr × Q × Nnb +nr ) that satisfies
the following conditions– (reflexivity) (µi , q, µo ) ∈ f (µi , q, µo ),A compositional framework for Petri nets

13

– (transitivity) if (µ′i , q ′ , µ′o ) ∈ f (µi , q, µo ) and (µ′′i , q ′′ , µ′′o ) ∈ f (µ′i , q ′ , µ′o ), then(µ′′i , q ′′ , µ′′o ) ∈ f (µi , q, µo ),– (additivity) (µ′i , q, µ′o ) ∈ f (µi , q, µo ) iff (µ′i + µ̃i , q, µ′o + µ˜o ) ∈ f (µi + µ̃i , q, µo +µ˜o )– (monotonicity) if (µ′i , q, µ′o ) ∈ f (µi , q, µo ), then µ′i ≤ µi and µo ≤ µ′o .
For simplicity, we sometimes just write Nm for Nmb +mr . We write (µi , q, µo )for an element in Nm × Q × Nn , where µi represents the entry marking, q theinternal state, and µo the exit marking. Note that the function is equivalent to a
relation on Nm × Q × Nn , and we write (µi , q, µo ) →f (µ′i , q ′ , µ′o ) to denote thatthese two elements are related by f (i.e., that (µ′i , q ′ , µ′o ) ∈ f ((µi , q, µo ))).
The idea is that two elements (µi , q, µo ) and (µ′i , q ′ , µ′o ) are related by theinterpretation of a Petri net N if, starting with an entry marking µi in internal
state q, and assuming that N has already output µo , then there exists a sequenceof firings that consumes tokens from the entry marking until exactly µ′i is left,
modifying the internal state to q ′ , and outputting tokens to reach exactly µ′o .
There are two differences between the semantic category here and those ofprevious work. The first one is insignificant: in previous work, the objects were
natural numbers rather than pairs, as there was a single type of edges. More
importantly, in previous work, the semantic category was always defined via
a monad, but this is not the case here. The current definition may seem toocomplicated, but we argue that such complexity is necessary. We go throughseveral simpler ideas and explain why they fail.
As mentioned above, the internal state of the Petri net dynamically modifies
its behaviour, hence if we considered a morphism from m to n to only be afunction Nm → P(Nn ) (which would fall under the monad construction), it
would be impossible to interpret roPNs into this semantic category.
A second idea would then be to define morphisms as functions f : Nm × Q →P(Q × Nn ), which solves the problem of taking the internal state of the Petrinet into account, and it would be possible to interpret rightward-open Petri nets
into this semantic category. The problem lies with what it means for (q ′ , µo ) to
be in f (µi , q). It would mean that µo is reachable by consuming all the tokens
from µi . However, it would then be impossible to define a trace operator thatis compatible with that of roPNs, since some tokens should remain in the entry
marking between two loops in order to reach some exit markings. Hence, thisidea does not lead to a trace that is compatible with that of roPN.
This explains why we need to remember the entry marking even in the outputof the function. Technically, it is possible to define the semantics as a categoryof functions of type Nm × Q → P(Nm × Q × Nn ), but we chose to add the exit
marking to the argument of the function, making it symmetric and therefore,
equivalent to a category of relations.
To define Sr , we first need to define the identities and composition.
Definition 13 (Identities, composition of Sr ). The identity on n is idn : n →n defined as the set {∗} of internal states and the relation (µi , ∗, µo ) →idn(µ′i , ∗, µ′o ) if and only if µ′i ≤ µi and µi + µo = µ′i + µ′o .

14Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

Let f : n → m and g : m → p be two morphisms in Sr , we define their composition f ; g as having Qf ×Qg as its set of internal states, and (µi , (qf , qg ), µo ) →f ;g(µ′i , (qf′ , qg′ ), µ′o ) if and only if there exists µ∗ such that (µi , qf , 0m ) →f (µ′i , qf′ , µ∗ )and (µ∗ , qg , µo ) →g (0m , qg′ , µ′o ). With this data, Sr forms a category.
The idea of identities is that they connect each entry i to its corresponding
exit, and each wire can slide any number of tokens from the entry marking to
the exit one. Note that additivity and monotonicity are necessary to prove that
Sr forms a category.

qf
µi

f

qf′

qg
0

m

g

µo

µ′i

f

qf′

qg
µ

∗

g

µo

µ′i

f

qg ’
0m

g

µ′o

Fig. 11. Composition in the semantic category Sr

We depict how composition intuitively works in Figure 11. In the configuration on the left, before the Petri net starts evolving, there should be no “floating”
tokens on the interface between f and g. The execution starts from f , which gives
a new initial marking and internal states, as well as tokens on the interface between f and g, as depicted in the middle of Figure 11. Then g is executed, but
its execution should consume all the tokens on the interface, so that there are
no tokens floating on the interface after execution, as depicted on the right of
Figure 11.
4.2

The Monoidal Categorical Structure

We now show that Sr has a monoidal structure as a first step towards showingthat it is a TSMC.
Definition 14 (tensor product of Sr ). Given n, m ∈ N, we define ⊗ as
the addition. Given f1 : m1 → n1 and f2 : m2 → n2 , we define f1 ⊗ f2 : m1 +m2 → n1 + n2 as the morphism with the internal state Q1 × Q2 and (µi,1 ⊗µi,2 , (q1 , q2 ), µo,1 ⊗ µo,2 ) →f1 ⊗f2 (µ′i,1 ⊗ µ′i,2 , (q1′ , q2′ ), µ′o,1 ⊗ µ′o,2 ) if and only if(µi,i , qi µo,i ) →fi (µ′i,i , qi′ , µ′o,i ) for i ∈ {1, 2}.
Definition 15 (Symmetries of Sr ). Given two pairs of natural numbers mand n, we define the symmetry Cm,n : m+n → n+m as the morphism whose setof internal states is {∗} and such that (µi ⊗νi , ∗, νo ⊗µo ) →Cn,m (µ′i ⊗νi′ , ∗, νo′ ⊗µ′o )if and only if for all i ∈ [mb ] + [mr ], there exists k such that µ′i (i) = µi (i) − k
and µ′o (i) = µo (i) + k, and similarly for for all i ∈ [nb ] + [nr ], there exists k suchthat νi′ (i) = νi (i) − k and νo′ (i) = νo (i) + k.
Finally, Sr also possesses a trace operator, as defined inA compositional framework for Petri nets

15

Definition 16 (trace of Sr ). Given three pairs of natural numbers m, n, p anda morphism f : p + m → p + n, the trace Trpm,n (f ) of f along p is defined ashaving Q as its set of internal states, and (µi , q, µo ) →Trpm,n (f ) (µ′i , q ′ , µ′o ) if andonly if there exist (µ0i , q 0 , µ0o ), . . . , (µni , q n , µno ) such that
– µ0i = 0p ⊗ µi , q 0 = q, and µ0o = 0p ⊗ µo ,– µni = 0p ⊗ µ′i , q n = q ′ , and µno = 0p ⊗ µ′o , and→,j– for all j < n, (µ←,j, q j , µ→,j
) →f (µj+1, q j+1 , µj+1
= 0p ⊗oo ), where µo
i
i
←,j
j
j
j
j
µo|>p , µi
= (µi + µo )|≤p ⊗ µi |>p , and (µi )i<n |P = (µi )i<n∧P (i) is the
restriction of µ to those indices that satisfy P .
This definition is somewhat similar to that of trace on Rel [10], but taking theinternal state into account. It must also take into account the fact that the tokens
that have reached a looping exit must be made available in the corresponding
and µ←,j. They can be viewed as “reloading”
entry, which is encoded into µ→,joi
the Petri net by moving all tokens that have reached a looping exit to thehas no tokens on the first p exits and is equalcorresponding looping entry: µ→,jo
to µjo on the other ones, while µ←,j
is equal to µji + µjo on the looping entriesijj(gaining tokens from µo ) and to µi on the other ones.
Lemma 4. Sr is a traced symmetric monoidal category.
We need reflexivity and transitivity in Definition 12 to prove that Trpm,n (−)
is a trace operator.
4.3

The Semantic Functor Sr

We now define the semantic function Sr : roPN → Sr that interprets rightward
open Petri nets in the semantic category.
Definition 17 (the functor Sr ). We define the semantic functor Sr : roPN →Sr on objects by Sr (n) = n and on arrows N : m → n as Sr (N ) : m → n
whose set of internal states is Q = NP the set of all markings of N , and(µi , µ, µo ) →Sr (N ) (µ′i , µ′ , µ′o ) if and only if (µ′i , µ′ , µ′o ) is reachable from (µi , µ, µo )in N by a sequence of firings and slidings.
We aim to prove that S is a traced symmetric monoidal functor. The difficult points to prove are Sr (N ; N ′ ) = Sr (N ); Sr (N ′ ) and Sr (Trpm,n (N )) =Trpm,n (Sr (N )). We only give informal proof of these two identities.
We start by proving Sr (N ; N ′ ) = Sr (N ); Sr (N ′ ), which amounts to proving Sr (N ; N ′ )(c) = (Sr (N ); Sr (N ′ ))(c) for all c = (µi , µ, µo ). First, given two
sequences (µi , µN , 0n ) → . . . → (µ′i , µ′N , µ∗ ) in N and (µ∗ , µM , µo ) → . . . →(0n , µ′M , µ′o ), it is simple to build a sequence c → . . . → (µ′i , µ′ , µ′o ) in N ; N ′ byconcatenating the two sequences and turning pairs of transitions/slidings thattouch the middle interface to a single transition/sliding in N ; N ′ .
It is slightly more difficult to reconstruct µ∗ and the sequences on N and N ′from the sequence on N ; N ′ , for which the following lemma is convenient.

16Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

Lemma 5 (Priority). Given Petri nets N : m → n and N ′ : n → p, a configuration c for N ; N ′ , k ∈ T ∪(li )i∈[mb ]+ , k ′ ∈ T ′ ∪(rj )j∈[pr ] if k ′ is enabled on c andk is enabled on k ′ (c), then k is enabled on c, k ′ on k(c), and k ′ (k(c)) = k(k ′ (c)).
This lemma is crucial, as given a sequence of transitions and slidings in N ; N ′ ,it guarantees that all the sliding and transitions in N can be prioritised over theones in N ′ . This means we can always assume that all transitions and slidingof N are fired before those of N ′ . Given a sequence of transitions and slidingson N ; N ′ , we can permute all entry slidings and transitions in N first. We canthen rebuild µ∗ by counting how many tokens are output by the input slidings
and transitions in N , then reconstruct the sequence on N (resp. N ′ ) by copying
those slidings in the sequence on N ; N ′ that are in N (resp. N ′ ). This provesthat Sr (N ; N ′ ) = Sr (N ); Sr (N ′ ).
Finally, we move on to proving Sr (Trpm,n (N )) = Trpm,n (Sr (N )). Here again,
the idea is to turn sequences c → . . . → c′ in Trpm,n (N ) to sequences in N for the(semantic) trace and vice-versa. The only difficulty is managing tokens on thelooping part of the interface. Given a sequence c → . . . → c′ in Trpm,n (N ) whose
general term is (µji , µj , µjo ), we can recreate a sequence for the trace by copying
all transitions/slidings and “reloading” the net (see Definition 16) after eachmove max {ϕp (i) | i ∈ [p]} times, so that reloading moves no tokens anymore. Its
general term is (µ̃ji ⊗ µji , µj , µ̃jo ⊗ µjo ), and is a witness that c → . . . → c′ in the
trace. The other direction is simpler. Given a sequence of configurations suchthat (µ→,j, µj , µ→,j
) → (µj+1, µj+1 , µj+1oo ) in N , we can create a sequence foriipTrm,n (N ) by simply copying all firings/slidings.

5

The Semantic Interpretation Functor J.K

5.1

Moving to the Bidirectional Case

One idea of this line of work [21,20,22] is that the bidirectional framework can
be derived from the unidirectional one automatically using the Int-construction,
instead of being an ad hoc construction. Here, we define the category oPNof open Petri nets from that of rightward open Petri nets. This simplifies thedevelopment, readability, and conciseness of the ideas, in addition to giving acompact closed structure “for free” to oPN (and the semantic domain S).
The basic idea of the Int-construction [10] is that objects of Int(C) are pairs(X, Y ) of objects of C where X represents objects going “forward”, while Y represents objects going “backward”. Morphisms from (X, Y ) to (X ′ , Y ′ ) in Int(C)are morphisms X ⊗ Y ′ → Y ⊗ X ′ (notice that the Y ’s are reversed). In our case,this allows us to model open ends going leftward, allowing for simpler modelling
especially for looping structures, which do not need to use trace explicitly.
Definition 18. We define oPN = Int(roPN) and S := Int(Sr ) the categoryof open Petri nets and semantic category, respectively. Moreover, because Sr
respects the traced symmetric monoidal structure, the Int-construction applies to
it too, and we define S = Int(Sr ) : oPN → S.

A compositional framework for Petri nets

17

From the property of the Int-construction, it follows that :Lemma 6. oPN and S are compact closed categories and S is a compact closed
functor.
This lemma gives a formal meaning to the claim we have been making that thebidirectional framework is derived canonically from the unidirectional one, andgives meaning to Figure 1.
5.2

The Coloured Graphical PROP

Until now, we have considered oPN (or roPN) to be our syntax and S to be
our semantics. However, the definitions of the different elements of oPN suchas composition and trace are hard to read and to work with, and they obscuretheir graphical essences. In this section, we give a simpler syntax for open Petrinets based on free coloured PROPs.
PROPs are a categorical concept widely used in many works to describe various graphical structures and fit well to define a categorical syntax in the formof string diagrams. Precisely, a PROP is a symmetric monoidal category whose
objects are the elements of the free monoid on a single object. Concretely, the elements are built as the powers of a single base object; hence, every object admits
a unique decomposition. In particular, this allows us to draw string diagrams
where wires do not carry specific information.
This formalism is expanded upon by considering the free monoid on a finite
set C (called the set of colours) in an object called a coloured PROP [7]. Concretely, its objects are lists of elements of C. Here, the usage of coloured PROPs
is doubly beneficial: because of the nature of Petri nets, we need to consider twocolours (as explained before) for the arrows, and we have to double the numberof colours (going from 2 to 4) to encompass the bidirectional setting. We define
our syntax category as a free PROP on a set of generators ΣPCN and equations
EPCN . A similar approach is presented in [20,21,22], from which we will adapt
the results without fully detailing them.
Let C = {•L , •R , •L , •R } be the set of colours. The colour •L (resp. •R )correspond to red arrows going leftward (resp. red arrows going rightward), andanalogously for •L and •L . We now move on to defining the signature ΣPCN ,containing the generators. They are illustrated in Figure 12.
Definition 19 (ΣPCN ). We pose ΣPCN : C ∗ × C ∗ → Set the functor defined byC
ΣPCN (ϵ, •R •L ) = {ηb , t0,2 }, ΣPCN (•L •R , ϵ) = {ϵ b , p2,0 }, ΣP N (ϵ, •R∗•L ) = {ηr , p0,2∗ },CC
ΣP N (•L •R , ϵ) = {ϵr , t2,0 }, ΣP N (u, v) = p|u|,|v| if u ∈ •L and v ∈ •L ,
ΣPCN (u, v) = t|u|,|v| if u ∈ •∗L and v ∈ •∗L , and ΣPCN (u, v) = ∅ otherwise.
We define EPCN to be the set containing the equations (ϵb ⊗id•L )◦(id•L ⊗ηb ) =id•L , (id•R ⊗ϵb ) ◦ (ηb ⊗ id•R ) = id•R , (ϵr ⊗ id•L ) ◦ (id•L ⊗ηr ) = id•L , (id•R ⊗ϵr ) ◦(ηr ⊗ id•R ) = id•R , i.e. the black and red snake equations for ϵb , ϵr , ηb , ηr . Our
syntactic PROP is F(ΣPCN , EPCN ), where F is defined as the free construction
from signatures (pairs of generators and equations) to PROPs detailed in [7].

18Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo
ηb

pm,n

tn,m

ηr

ϵb

ϵr

Fig. 12. The generators in ΣPCN

The free property of F(ΣPCN , EPCN ) is that any valuation V of ΣPCN to a PROP
C (i.e., a pair of a set function from colours to objects of C and a set function
from ΣPCN to morphisms of C of the corresponding type) uniquely extends to a
PROP morphism F(ΣPCN , EPCN ) → C.
This freeness allows us to define the realisation functor R : F(ΣPCN , EPCN ) →oPN canonically, by considering the valuation V : ΣPCN → Int(roPN) definedby V (ϵb ) = V (ηb ) = id(1,0) , V (ϵr ) = V (ηr ) = id(0,1) , V (pm,n ) the open Petri net
m → n with a single place with n inputs and m outputs and no transitions, andV (tm,n ) the open Petri net m → n with no places and a single transition withn inputs and m outputs.
Not only is F(ΣPCN , EPCN ) the free PROP over (ΣPCN , EPCN ) by definition, it
also possesses a more interesting property here.
Lemma 7. There is a signature Σ such that F(ΣPCN , EPCN ) ∼= Int(Ftr (Σ)) the
free traced symmetric monoidal category over Σ.
The nature of the signature Σ is not useful on its own for this work but
is developed in [20]. This theorem allows us to consider the second universal
property of F(ΣPCN , EPCN ), as it is also a free compact closed category. First,
we take the valuation V defined earlier and name R the unique compact closed
functor that makes the leftmost triangle in Figure 13 commute. Second, we takethe valuation S ◦ V : ΣPCN → S, and and we name J.K : F(ΣPCN , EPCN ) → S theunique functor that makes the larger triangle in Figure 13 commute.

ΣPCN
η

V

oPN
R

S

S

J.K

F(ΣPCN , EPCN )Fig. 13. The construction of R and J.K

This means that both S◦R and J.K satisfies the lifting property of F(ΣPCN , EPCN )as the free compact closed category, hence the following result.
Theorem 2. J.K = S ◦ R.

A compositional framework for Petri nets

19

We could have defined J.K as S ◦ R, but this would have hidden the fact that
J.K is given by a freeness property and can thus be computed inductively. This
property is important to solve the open reachability problem inductively.

6

Conclusion and Future WorkIn this work, we have designed a compositional approach to Petri nets to solve
open reachability. To achieve such a result, we have defined a category of open
Petri nets, as well as a graphical language of string diagram and a semantic
domain in which open Petri nets can be interpreted.
Directions for future work include the bounded case, in which there is a finite
limit to the number of tokens present on places/open ends. However, semantic
composition is more complex in this case. Moreover, we could implement analgorithm in the bounded case. Finally, a general work on compositionality, following [20,21] and the current work, would prove useful to design frameworks
for open structures without starting from scratch every time.
Acknowledgments. The authors are supported by CREST ZT-IoT Project (No. JPMJCR21M3), ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and ASPIRE Grant No. JPMJAP2301, JST.

References
1. Baez, J.C., Coya, B., Rebro, F.: Props in network theory. Theory and Applicationsof Categories 33(25), 727–783 (2018)
2. Baez, J.C., Maste, J.: Open Petri nets. Mathematical Structures in Computer
Science 30(3), 314–341 (2020)
3. Baez, J.C., Pollard, B.S.: A compositional framework for reaction networks. Reviews in Mathematical Physics 29(09), 1750028 (2017)
4. Bonchi, F., Holland, J., Piedeleu, R., Sobociński, P., Zanasi, F.: Diagrammatic algebra: from linear to concurrent systems. Proceedings of the ACM on Programming
Languages 3(POPL), 1–28 (2019)
5. Bonchi, F., Sobociński, P., Zanasi, F.: Interacting Hopf algebras. Journal of Pureand Applied Algebra 221(1), 144–184 (2017)
6. Carette, T., Horsman, D., Perdrix, S.: Szx-calculus: Scalable graphical quantum
reasoning. In: 44th International Symposium on Mathematical Foundations ofComputer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany. vol. 138,
pp. 55:1–55:15 (2019)
7. Carette, T., Perdrix, S.: Colored props for large scale graphical reasoning (2020)
8. Fiore, M., Campos, M.D.: The algebra of directed acyclic graphs. In: Computation,
Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky,
pp. 37–51. Springer (2013)
9. Joyal, A., Street, R.: Braided tensor categories. Advances in Mathematics 102(1),
20–78 (1993)
10. Joyal, A., Street, R., Verity, D.: Traced monoidal categories. In: Mathematical proceedings of the cambridge philosophical society. vol. 119, pp. 447–468. Cambridge
University Press (1996)

20

Serge Lechenne, Clovis Eberhart, and Ichiro Hasuo

11. Mac Lane, S.: Categories for the working mathematician, vol. 5. Springer Science& Business Media (2013)12. Penrose, R.: Applications of negative dimensional tensors. Combinatorial mathematics and its applications 1, 221–244 (1971)
13. Peterson, J.L.: Petri nets. ACM Computing Surveys (CSUR) 9(3), 223–252 (1977)
14. Rathke, J., Sobociński, P., Stephens, O.: Compositional reachability in petri nets.
In: Reachability Problems: 8th International Workshop, RP 2014, Oxford, UK,
September 22-24, 2014. Proceedings 8. pp. 230–243. Springer (2014)
15. Reisig, W.: Petri nets: an introduction, vol. 4. Springer Science & Business Media(2012)
16. Reisig, W.: Understanding Petri nets. Springer (2016)17. Selinger, P.: A survey of graphical languages for monoidal categories. In: New
structures for physics, pp. 289–355. Springer (2010)18. Sobociński, P.: Compositional model checking of concurrent systems, with petri
nets. arXiv preprint arXiv:1603.00976 (2016)19. Stephens, O.: Compositional specification and reachability checking of net systems.
Ph.D. thesis, University of Southampton (2015)
20. Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: A compositional approach toparity games. arXiv preprint arXiv:2112.14058 (2021)
21. Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic
model checking with string diagrams of mdps. In: 35th International Conference
on Computer Aided Verification (CAV 2023) (2023)
22. Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional solution of mean
payoff games by string diagrams. arXiv preprint arXiv:2307.08034 (2023)