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.

July 27, 2020

Linear Logic Flavoured Composition of Petri Nets

Posted by John Baez

guest post by Elena Di Lavore and Xiaoyan Li

Petri nets are a mathematical model for systems in which processes, when activated, consume some resources and produce others. They can be used to model, among many others, business processes, chemical reactions, gene activation or parallel computations. There are different approaches to define a categorical model for Petri nets, for example, Petri nets are monoids, nets with boundaries and open Petri nets.

This first post of the Applied Category Theory Adjoint School 2020 presents the approach of Carolyn Brown and Doug Gurr in the paper A Categorical Linear Framework for Petri Nets, which is based on Valeria de Paiva’s dialectica categories. The interesting aspect of this approach is the fact that it combines linear logic and category theory to model different ways of composing Petri nets.

Elementary Petri nets are the objects of a category N𝒞\mathbf{N}\mathcal{C} whose morphisms can represent simulations or refinements of them. The interpretations of the linear logic connectives of the dialectica category G𝒞\mathbf{G}\mathcal{C} can be lifted to the category N𝒞\mathbf{N}\mathcal{C} and used to define compound nets. Each connective gives a different interpretation to the corresponding compound net, based on its meaning in intuitionistic linear logic.

The scope of the paper is wider and it covers markings, a definition of a category of arbitrary Petri nets and the description of N𝒞\mathbf{N}\mathcal{C} for some 𝒞\mathcal{C} different from Set\mathbf{Set}. We will focus on the aspect of composition of Petri nets via logical connectives giving a concrete example for each one of them and trying to give an interpretation to their corresponding constructs on Petri nets.

Preliminary definitions

Petri nets

We start by introducing Petri nets and elementary Petri nets, which will be the focus of this post.

Petri nets describe systems where some processes, called events, can be fired when all their preconditions are marked with at least the amount of tokens indicated by the weight of each arrow. After an event has been fired, the markings of all postconditions of this event will be increased by the weight of each arrow. We will represent events with rectangles and conditions with circles. The following figure represents the firing of the event e 1e_1. Its preconditions, b 0b_0 and b 1b_1, are indicated with an incoming arrow together with a weight. Similarly, its postconditions, b 0b_0 and b 2b_2, are indicated with an outgoing arrow together with a weight. The firing of e 1e_1 consumes a token from b 0b_0 and two tokens from b 1b_1 and produces one token in b 0b_0 and three tokens in b 2b_2.

A Petri net 𝒩=(E,B,pre,post)\mathcal{N}= (E,B, \mathit{pre}, \mathit{post}) is given by two sets E,BE, B and two multirelations pre,post:E mB\mathit{pre},\mathit{post} \colon E \rightarrow _m B. The set EE represents the events that are possible in the net 𝒩\mathcal{N} while the set BB represents the conditions around the events in EE. The multirelation pre\mathit{pre} keeps track of ”how many times” a condition is needed in order to fire an event. Similarly, the multirelation post\mathit{post} keeps track of ”how many times” a condition is produced after firing an event.

We will write pre(e)\mathit{pre}(e) and post(e)\mathit{post}(e) to indicate the multisets of preconditions and postconditions of an event ee.

In this post, we will focus on Petri nets whose pre\mathit{pre} and post\mathit{post} multirelations are ordinary relations and, thus, correspond to subsets of E×BE \times B. These are called elementary Petri nets.

In general, the weight of each condition can be an integer. In the case of elementary Petri nets, only nets whose arrows have weight one are considered (thus, the weight is omitted).

The category of elementary Petri nets N𝒞\mathbf{N} \mathcal{C}

We can define the category of elementary Petri nets N𝒞\mathbf{N} \mathcal{C} based on the dialectica category G𝒞\mathbf{G}\mathcal{C}. Objects and morphisms in N𝒞\mathbf{N} \mathcal{C} are defined from objects and morphisms in G𝒞\mathbf{G} \mathcal{C}.

Let 𝒞\mathcal{C} be a category with finite limits, then there is a category N𝒞\mathbf{N} \mathcal{C} defined as follows.

  • An object is a pair 𝒩=(pre,post)\mathcal{N}=(\mathit{pre}, \mathit{post}), where pre\mathit{pre} and post\mathit{post} are objects in G𝒞\mathbf{G}\mathcal{C}.

  • A morphism from 𝒩=(pre,post)\mathcal{N}=(\mathit{pre}, \mathit{post}) to 𝒩=(pre,post)\mathcal{N}'=(\mathit{pre}', \mathit{post}') is a pair of morphisms (f,F)(f, F) in 𝒞\mathcal{C} such that (f,F)(f, F) is a morphism from pre\mathit{pre} to pre\mathit{pre}' and from post\mathit{post} to post\mathit{post}' in G𝒞\mathbf{G} \mathcal{C}.

An object 𝒩=(pre,post)\mathcal{N}=(\mathit{pre}, \mathit{post}) of NSet\mathbf{NSet} represents an elementary Petri net whose precondition and postcondition relations are given by pre\mathit{pre} and post\mathit{post}. Taking 𝒞=Set\mathcal{C} = \mathbf{Set} lets us explicit the conditions for (f,F)(f,F) to be a morphism of Petri nets. We obtain that

epreF(b) f(e)preb epostF(b) f(e)postb \begin{aligned} e \ \mathit{pre} \ F(b') & \Rightarrow f(e) \ \mathit{pre}' \ b'\\ e \ \mathit{post} \ F(b') & \Rightarrow f(e) \ \mathit{post}' \ b'\\ \end{aligned}

This means that the net 𝒩\mathcal{N} is a refinement of 𝒩\mathcal{N}'. Intuitively, this means that 𝒩\mathcal{N} consumes and produces at least as many resources as 𝒩\mathcal{N}'.

This is not the only way one can define morphisms of Petri net. It is possible to reverse the direction of the unique morphism kk for one or both the components pre\mathit{pre} and post\mathit{post} of a Petri net. It is also possible to consider morphisms that give an if and only if in the condition above. All these variants have interpretations that is worth investigating. We shortly discuss the intuitions behind these variants in the last section.

The dialectica category G𝒞\mathbf{G} \mathcal{C}

We briefly give the definition of dialectica category that is necessary to define N𝒞\mathbf{N}\mathcal{C}. The reader already familiar with this work is invited to skip to the next section.

Given a category 𝒞\mathcal{C} with finite limits, we define the dialectica category G𝒞\mathbf{G} \mathcal{C} as follows.

  • Objects are relations on objects of 𝒞\mathcal{C}. They are given by monics α:AE×B \alpha \colon A \to E \times B in 𝒞\mathcal{C}. We indicate them with α:EB\alpha \colon E \nleftarrow B .

  • A morphism (f,F):αα(f,F) \colon \alpha \to \alpha' between two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' is given by a pair of morphisms f:EEf \colon E \rightarrow E' and F:BBF \colon B' \rightarrow B in 𝒞\mathcal{C} such that there exists a (necessarily unique and monic) morphism kk such that the following triangle commutes.

Theorem (de Paiva): If 𝒞\mathcal{C} is a locally cartesian closed category with finite disjoint coproducts, then G𝒞\mathbf{G}\mathcal{C} is a model of intuitionistic linear logic.

The structure of G𝒞\mathbf{G}\mathcal{C} that interprets the linear logic connectives can be lifted to the category of elementary Petri nets and used to define composites of Petri nets relying on the intuition of the linear logic connectives.

Composing Petri nets

In this section, we define how the constructs of linear logic are interpreted in G𝒞\mathbf{G} \mathcal{C} and, consequently, in N𝒞\mathbf{N}\mathcal{C}. We give concrete examples in NSet\mathbf{NSet} to try to explain the intuitive meaning of these constructs on Petri nets.

Cartesian product

The cartesian product of two nets 𝒩\mathcal{N} and 𝒩\mathcal{N}' is a Petri net where events are pairs e,e\langle e,e' \rangle that represent both the events ee, in 𝒩\mathcal{N}, and ee', in 𝒩\mathcal{N}', happening at the same time. Conditions in the product net are conditions in 𝒩\mathcal{N} or in 𝒩\mathcal{N}'.

To give a concrete example, consider two Petri nets representing interactions among genes (we took this example from a paper that uses open Petri nets for gene regulatory networks). The first one represents a gene b 0b_0 that, deactivating itself, can activate gene b 1b_1 or gene b 2b_2, and the second one represents a gene b 0b_0' that can deactivate b 1b_1'.

Their cartesian product represents the concurrent activation of b 1b_1 or b 2b_2 by b 0b_0 and deactivation of b 1b_1' by b 0b_0'. In fact, in order to be able to activate b 1b_1 and deactivate b 1b_1' simultaneously, all the preconditions of e 1e_1 in 𝒩 1\mathcal{N}_1 and all the preconditions of ee' in 𝒩 2\mathcal{N}_2 must be marked.

More formally, the conditions on the precondition and postcondition relations for the product 𝒩&𝒩\mathcal{N} \ \& \ \mathcal{N}' in NSet\mathbf{NSet} are given by the union of the preconditions and postconditions in the component nets.

pre &(e,e) =i B(pre(e))i B(pre(e)) post &(e,e) =i B(post(e))i B(post(e)) \begin{aligned} \mathit{pre}_{\&}(\langle e,e' \rangle ) & = i_{B}(\mathit{pre}(e)) \cup i_{B'}(\mathit{pre}'(e'))\\ \mathit{post}_{\&}(\langle e,e' \rangle ) & = i_{B}(\mathit{post}(e)) \cup i_{B'}(\mathit{post}'(e'))\\ \end{aligned}

These conditions come from the more general definition of the product in the category N𝒞\mathbf{N}\mathcal{C}. In the category N𝒞\mathbf{N}\mathcal{C}, the cartesian product of two nets is defined by component-wise products. 𝒩&𝒩=(pre&pre,post&post)\mathcal{N} \ \& \ \mathcal{N}' = (\mathit{pre} \ \& \ \mathit{pre}', \mathit{post}\ \& \ \mathit{post}') where pre&pre\mathit{pre} \ \& \ \mathit{pre}' and post&post\mathit{post}\ \& \ \mathit{post}' indicate cartesian products in G𝒞\mathbf{G}\mathcal{C}.

For the more interested reader, we present the formal definition of cartesian product in the dialectica category G𝒞\mathbf{G}\mathcal{C}. The cartesian product of two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' in G𝒞\mathbf{G} \mathcal{C} is the relation α&α:E×EB+B\alpha \ \& \ \alpha' \colon E \times E' \nleftarrow B + B' given by α&α=(α×𝟙 E)+(α×𝟙 E)\alpha \ \& \ \alpha' = (\alpha \times \mathbb{1}_{E'})+(\alpha' \times \mathbb{1}_E) where ×\times and ++ indicate the product and coproduct in the category 𝒞\mathcal{C}. The projections are given by the morphisms (π E,i B)(\pi_{E},i_{B}) and (π E,i B)(\pi_{E'},i_{B'}).

By the universal property of the product, when 𝒞=Set\mathcal{C}=\mathbf{Set}, we obtain the following condition for the product relation, which directly gives the conditions for the product of Petri nets that we presented above.

e,e(α&α)i B(b) eαb e,e(α&α)i B(b) eαb \begin{aligned} \langle e,e' \rangle (\alpha \ \& \ \alpha')i_{B}(b) &\Leftrightarrow e \ \alpha \ b\\ \langle e,e' \rangle (\alpha \ \& \ \alpha')i_{B'}(b') &\Leftrightarrow e' \ \alpha' \ b'\\ \end{aligned}

Coproduct

The behaviour of a coproduct net is to be able to fire either an event in the first net or one in the second. Thus, events in the coproduct net are events from the first net or the second. Conditions are pairs of conditions in the first and second net, respectively. When a condition b,b\langle b,b' \rangle in the coproduct is marked, it is interpreted as one of the two conditions, bb or bb', is marked. We will show this through a concrete example. Consider the first of the Petri nets introduced above.

Its behaviour is to activate either b 1b_1 or b 2b_2 by deactivating b 0b_0. This behaviour seems the one of a coproduct net as we just described it. In fact, we can see that the coproduct of the two nets 𝒩 1\mathcal{N}_1, representing the activation of b 1b_1, and 𝒩 2\mathcal{N}_2, representing the activation of b 2b_2, below is refined by the net 𝒩\mathcal{N}.

In fact, a refinement of 𝒩 1𝒩 2\mathcal{N}_1 \oplus \mathcal{N}_2 by 𝒩\mathcal{N} is the morphism of elementary nets (f,F):𝒩 1𝒩 2𝒩(f,F) \colon \mathcal{N}_1 \oplus \mathcal{N}_2 \to \mathcal{N} given by

f:E 1+E 2 E F:B B 1×B 2 e 1 e 1 b 0 b 0,b 0 e 2 e 2 b 1 b 1,b 2 b 2 b 1,b 2 \begin{aligned} f \colon E_1 + E_2 & \to E & F \colon B & \to B_1 \times B_2 \\ e_1 & \mapsto e_1 & b_0 & \mapsto \langle b_0,b_0 \rangle \\ e_2 & \mapsto e_2 & b_1 & \mapsto \langle b_1,b_2 \rangle \\ & & b_2 & \mapsto \langle b_1,b_2 \rangle \\ \end{aligned}

The conditions for the coproduct of two nets 𝒩𝒩\mathcal{N} \oplus \mathcal{N}' in NSet\mathbf{NSet} can be given explicitly.

pre (i E(e)) =π B 1(pre(e)) pre (i E(e)) =π B 1(pre(e)) post (i E(e)) =π B 1(post(e)) post (i E(e)) =π B 1(post(e)) \begin{aligned} \mathit{pre}_{\oplus}(i_{E}(e)) & = \pi_{B}^{-1}(\mathit{pre}(e)) \\ \mathit{pre}_{\oplus}(i_{E'}(e')) & = \pi_{B'}^{-1}(\mathit{pre}'(e')) \\ \mathit{post}_{\oplus}(i_{E}(e)) & = \pi_{B}^{-1}(\mathit{post}(e)) \\ \mathit{post}_{\oplus}(i_{E'}(e')) & = \pi_{B'}^{-1}(\mathit{post}'(e')) \\ \end{aligned}

The coproduct of two nets is given by component-wise coproducts. 𝒩𝒩=(prepre,postpost)\mathcal{N} \oplus \mathcal{N}' = (\mathit{pre} \oplus \mathit{pre}', \mathit{post}\oplus \mathit{post}') where prepre\mathit{pre} \oplus \mathit{pre}' and postpost\mathit{post}\oplus \mathit{post}' are coproducts in G𝒞\mathbf{G}\mathcal{C}.

We define the coproduct of two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' in G𝒞\mathbf{G} \mathcal{C}. It is the relation αα:E+EB×B\alpha \oplus \alpha' \colon E+E' \nleftarrow B \times B' given by αα=(α×𝟙 B)+(α×𝟙 B)\alpha \oplus \alpha' = (\alpha \times \mathbb{1}_{B'})+(\alpha' \times \mathbb{1}_B) where ×\times and ++ indicate the product and coproduct in the category 𝒞\mathcal{C}. The inclusions are the morphisms (i E,π B)(i_{E},\pi_{B}) and (i E,π B)(i_{E'},\pi_{B'}).

By the universal property of the coproduct, when 𝒞=Set\mathcal{C}=\mathbf{Set}, we can express the coproduct relation in terms of the component relations. This gives the conditions in NSet\mathbf{NSet} written above.

i E(e)(αα)b,b eαb i E(e)(αα)b,b eαb \begin{aligned} i_{E} (e) (\alpha \oplus \alpha') \langle b,b' \rangle &\Leftrightarrow e \ \alpha \ b\\ i_{E'}(e') (\alpha \oplus \alpha') \langle b,b' \rangle &\Leftrightarrow e' \ \alpha' \ b'\\ \end{aligned}

Monoidal product

The monoidal product also represents the concurrent firing of events in the two nets but, contrary to the cartesian product, it keeps track of the necessary channels of communication between events in one net and conditions in the other for the concurrent event to happen. Thus, events in 𝒩𝒩\mathcal{N} \otimes \mathcal{N}' are going to be again pairs of events e,e\langle e,e' \rangle, with ee an event in 𝒩\mathcal{N} and ee' an event in 𝒩\mathcal{N}'. However, conditions are going to be pairs of functions f,f\langle f,f' \rangle from events in one net to conditions in the other, so that ff represents a channel from the events in 𝒩\mathcal{N}' to the conditions in 𝒩\mathcal{N} and ff' a channel from the events in 𝒩\mathcal{N} to the conditions in 𝒩\mathcal{N}'. Consider the monoidal product of the Petri nets shown above 𝒩\mathcal{N} and 𝒩\mathcal{N}'.

On the right hand side, we indicate with b ib_i the function from EE' to BB that sends ee' to b ib_i. We indicate with 𝟙,lnot,! 0,! 1\mathbb{1}, \lnot, !_0, !_1 the functions from EE to BB' that send e ie_i to b i1b'_{i-1}, e 1e_1 to b 1b'_1 and e 2e_2 to b 0b'_0, e ie_i to b 0b_0, and e ie_i to b 1b_1, respectively.

The preconditions for the synchronous event e 1,e\langle e_1,e' \rangle are all those channels that, whenever e 1e_1 can fire, enable the preconditions of ee' and all those channels that, whenever ee' can fire, enable the preconditions of e 1e_1. This means that the preconditions of e 1,e\langle e_1,e' \rangle are pairs of functions f,f\langle f,f' \rangle such that f(e)=b 0f(e')=b_0 and f(e 1)=b 0f'(e_1) = b_0' or f(e 1)=b 1f'(e_1) = b_1'. Similarly, after firing e 1,e\langle e_1,e' \rangle, the channels f,f\langle f,f' \rangle such that f(e)=b 1f(e')=b_1 and f(e 1)=b 0f'(e_1)=b_0'.

In NSet\mathbf{NSet}, the conditions on the preconditions and postconditions sets can be given explicitly.

e,epre f,f epref(e) and epref(e) e,epost f,f epostf(e) and epostf(e) \begin{aligned} \langle e, e' \rangle \ \mathit{pre}_{\otimes} \ \langle f,f' \rangle &\Leftrightarrow e \ \mathit{pre} \ f(e') \ \text{ and } \ e' \ \mathit{pre}' \ f'(e) \\ \langle e, e' \rangle \ \mathit{post}_{\otimes} \ \langle f,f' \rangle &\Leftrightarrow e \ \mathit{post} \ f(e') \ \text{ and } \ e' \ \mathit{post}' \ f'(e) \\ \end{aligned}

More generally, in N𝒞\mathbf{N}\mathcal{C}, the monoidal product of two nets is given by the component-wise monoidal product 𝒩𝒩=(prepre,postpost)\mathcal{N} \otimes \mathcal{N}' = (\mathit{pre} \otimes \mathit{pre}', \mathit{post}\otimes \mathit{post}') where prepre\mathit{pre} \otimes \mathit{pre}' and postpost\mathit{post}\otimes \mathit{post}' are monoidal products in G𝒞\mathbf{G}\mathcal{C}.

For the details of this definition, we need to define the monoidal product of two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' in G𝒞\mathbf{G} \mathcal{C}. It is the relation αα:E×EB E ×B E\alpha \otimes \alpha' \colon E \times E' \nleftarrow B^{E^'} \times B'^E given by αα=(𝟙 E×(π;ev E)) 1(α)(𝟙 E×(π;ev E)) 1(α)\alpha \otimes \alpha' = (\mathbb{1}_{E'} \times (\pi' ; \mathit{ev}_E))^{-1}(\alpha') \wedge (\mathbb{1}_{E} \times (\pi ; \mathit{ev}_{E'}))^{-1}(\alpha) where f 1(g)f^{-1}(g) indicates the pullback of gg along ff in the category 𝒞\mathcal{C} and fff \wedge f' indicates the pullback of ff and ff'.

By taking 𝒞=Set\mathcal{C} = \mathbf{Set}, these conditions can be explicitly stated as follows.

e,e(αα)f,feαf(e) and eαf(e)\langle e, e' \rangle (\alpha \otimes \alpha') \langle f,f' \rangle \Leftrightarrow e \ \alpha \ f(e') \ \text{ and } \ e' \ \alpha' \ f'(e)

Units

The units of the operations given so far are the terminal object, the initial object and the monoidal unit respectively.

The unit for the cartesian product is the empty relation from 00 to 11, the unit of the coproduct is the empty relation from 11 to 00 and the monoidal unit is the identity relation from 11 to 11, where 00 and 11 indicate the initial and terminal object of 𝒞\mathcal{C}, respectively.

Exponential

The exponential of two nets, as one might expect, gives information about the morphisms from one net to the other because morphisms from 𝒩\mathcal{N} to 𝒩\mathcal{N}' correspond to points of the exponential [𝒩,𝒩]\left[ \mathcal{N}, \mathcal{N}' \right]. Events in [𝒩,𝒩]\left[ \mathcal{N}, \mathcal{N}' \right] have the types of morphisms from 𝒩\mathcal{N} to 𝒩\mathcal{N}', and they correspond to morphisms precisely when they have all places in the exponential net as preconditions and postconditions. Places in the exponential are elements in which the events can be evaluated, namely, pairs e,b\langle e,b' \rangle with eEe \in E and bBb' \in B'. The following example shows that there is one possible morphism from the first net to the second one, the one corresponding to the coloured event !,b 0\langle ! , b_0 \rangle.

On the right hand side, we indicate with b ib_i the function from BB' to BB that sends b 0b_0' to b ib_i and with !! the only function from EE to EE'.

If the first net represents cooking pizza from the ingredients and the second net represents destroying the ingredients, then destroying the ingredients is a refinement of using the ingredients to cook a pizza and the refinement map is given by the pair of functions (!,b 0)(!,b_0) that sends cooking to destroying and the ingredients to the ingredients.

We can write the precondition and postcondition relations of the exponential of 𝒩\mathcal{N}' by 𝒩\mathcal{N} in terms of the ones in 𝒩\mathcal{N} and 𝒩\mathcal{N}'.

f,F[pre,pre]e,b if epreF(b) then f(e)preb f,F[post,post]e,b if epostF(b) then f(e)postb \begin{aligned} \langle f,F \rangle \left[ \mathit{pre}, \mathit{pre}' \right] \langle e,b' \rangle &\Leftrightarrow \ \text{ if } \ e \ \mathit{pre} \ F(b') \ \text{ then } \ f(e) \ \mathit{pre}' \ b' \\ \langle f,F \rangle \left[ \mathit{post}, \mathit{post}' \right] \langle e,b' \rangle &\Leftrightarrow \ \text{ if } \ e \ \mathit{post} \ F(b') \ \text{ then } \ f(e) \ \mathit{post}' \ b' \\ \end{aligned}

More generally, in the category N𝒞\mathbf{N}\mathcal{C}, the exponential of two nets is given by the component-wise exponential [𝒩,𝒩]=([pre,pre],[post,post])\left[ \mathcal{N}, \mathcal{N}' \right] = (\left[ \mathit{pre}, \mathit{pre}' \right], \left[ \mathit{post}, \mathit{post}' \right]) where [pre,pre]\left[ \mathit{pre}, \mathit{pre}' \right] and [post,post]\left[ \mathit{post}, \mathit{post}' \right] are exponentials in G𝒞\mathbf{G}\mathcal{C}.

In the category G𝒞\mathbf{G} \mathcal{C}, the exponential of two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' is the relation [α,α]:E E×B BE×B\left[ \alpha, \alpha' \right] \colon E'^E \times B^{B'} \nleftarrow E \times B' given by the greatest subobject [α,α]\left[ \alpha, \alpha' \right] of E E×B B×E×BE'^E \times B^{B'} \times E \times B' such that [α,α]γγ\left[ \alpha, \alpha' \right] \wedge \gamma \leq \gamma' with γ=((𝟙 E E×E×ev B);π) 1(α)\gamma = ((\mathbb{1}_{E'^E \times E} \times \mathit{ev}_{B'}); \pi)^{-1}(\alpha) and γ=((𝟙 B B×B×ev E);π) 1(α)\gamma' = ((\mathbb{1}_{B^{B'} \times B'} \times \mathit{ev}_{E}); \pi')^{-1}(\alpha'), where f 1(g)f^{-1}(g) indicates the pullback of gg along ff in the category 𝒞\mathcal{C}, fwedgeff \wedgef' indicates the pullback of ff and ff' and \leq indicates the inclusion of subobjects.

When 𝒞=Set\mathcal{C} = \mathbf{Set}, these conditions can be explicitly stated as follows.

f,F[α,α]e,b if eαF(b) then f(e)αb\langle f,F \rangle \left[ \alpha, \alpha' \right] \langle e,b' \rangle \Leftrightarrow \ \text{ if } \ e \ \alpha \ F(b') \ \text{ then } \ f(e) \ \alpha' \ b'

Disjunctive monoidal product

The disjunctive monoidal product is the interpretation of the par connective in linear logic, whose meaning is well known to be unintuitive. Its behaviour on Petri nets is similar to the one of \otimes but with disjunction instead of conjunction. Events in 𝒩𝒩\mathcal{N} \invamp \mathcal{N}' are pairs of functions from the conditions in one net to the events in the other, and places elements in which to evaluate the events, namely pairs b,b\langle b,b' \rangle with bBb \in B and bBb' \in B'. We can see an example.

On the right hand side, we indicate with e ie_i the function from BB' to EE that sends b 0b_0' to e ie_i and with !! the only function from BB to EE'.

In NSet\mathbf{NSet}, the conditions on the preconditions and postconditions of 𝒩𝒩\mathcal{N} \invamp \mathcal{N}' can be given explicitly.

f,fpre b,b f(b)preb or f(b)preb f,fpost b,b f(b)postb or f(b)postb \begin{aligned} \langle f, f' \rangle \ \mathit{pre}_{\invamp} \ \langle b,b' \rangle & \Leftrightarrow f(b') \ \mathit{pre} \ b \ \text{ or } \ f'(b) \ \mathit{pre}' \ b'\\ \langle f, f' \rangle \ \mathit{post}_{\invamp} \ \langle b,b' \rangle &\Leftrightarrow f(b') \ \mathit{post} \ b \ \text{ or } \ f'(b) \ \mathit{post}' \ b' \\ \end{aligned}

In the category N𝒞\mathbf{N}\mathcal{C}, the disjunctive monoidal product of two nets is given by the component-wise monoidal product 𝒩𝒩=(prepre,postpost)\mathcal{N} \invamp \mathcal{N}' = (\mathit{pre} \invamp \mathit{pre}', \mathit{post}\invamp \mathit{post}') where prepre\mathit{pre} \invamp \mathit{pre}' and postpost\mathit{post}\invamp \mathit{post}' are disjunctive monoidal products in G𝒞\mathbf{G}\mathcal{C}.

In G𝒞\mathbf{G} \mathcal{C}, the disjunctive monoidal product of two objects α:EB\alpha \colon E \nleftarrow B and α:EB\alpha' \colon E' \nleftarrow B' is the relation αα:E B×E BB×B\alpha \invamp \alpha' \colon E^{B'} \times E'^B \nleftarrow B \times B' given by αα=((𝟙 B×(π;ev B)) 1(α)(𝟙 B×(π;ev B)) 1(α))\alpha \invamp \alpha' = \binom{(\mathbb{1}_{B} \times (\pi' ; \mathit{ev}_B))^{-1}(\alpha')}{(\mathbb{1}_{B'} \times (\pi ; \mathit{ev}_{B}))^{-1}(\alpha)} where f 1(g)f^{-1}(g) indicates the pullback of gg along ff in the category 𝒞\mathcal{C} and (ff)\binom{f}{f'} indicates the unique map from the coproduct of the domains of ff and ff'.

By taking 𝒞=Set\mathcal{C} = \mathbf{Set}, these conditions can be explicitly stated as follows.

f,f(αα)b,bf(b)αb or f(b)αb\langle f,f' \rangle (\alpha \invamp \alpha') \langle b, b' \rangle \Leftrightarrow f(b') \ \alpha \ b \ \text{ or } \ f'(b) \ \alpha' \ b'

Negation

The unit for the disjunctive monoidal product is given by the net with one place and one event that are not related to each other.

The exponential [α,]\left[ {\alpha}, \perp \right] corresponds to the negation of the relation α\alpha. The same interpretation holds for the objects of NSet\mathbf{NSet}.

Asynchronous events

We have seen how to model events happening synchronously with the cartesian product. One may wonder how to account for the possibility for only one net to fire in the cartesian product. The idea is to allow both the nets to ”do nothing” by adding an extra ”empty” event to both the nets and, then, taking the cartesian product. This is obtained by taking the coproduct with the negation net. In fact, the net 𝒩\mathcal{N} \oplus \perp is the net 𝒩\mathcal{N} with one additional event that has no preconditions nor postconditions.

We take again the example of genes activating other genes to show how this works concretely. We compute (𝒩)&(𝒩)(\mathcal{N} \oplus \perp) \ \& \ (\mathcal{N}' \oplus \perp).

We see that the events in this net are pairs of events in 𝒩\mathcal{N} and 𝒩\mathcal{N}', with the same interpretation that they have in the cartesian product 𝒩&𝒩\mathcal{N} \ \& \ \mathcal{N}', or events, like e 1e_1, e 2e_2 and ee', that represent the asynchronous events gene b 0b_0 activates gene b 1b_1, gene b 0b_0 activates gene b 2b_2 and gene b 0b'_0 deactivates gene b 1b'_1, respectively, happening in one net while the other net ”does nothing”.

Discussion

The challenge of this framework is to understand how it can be useful in the numerous and diverse applications of Petri nets. In order to do this, it is worth investigating different twists in the definition of the category N𝒞\mathbf{N}\mathcal{C}. As mentioned above, it is possible to reverse the direction of the unique morphism kk (the one appearing in the definition of morphism in G𝒞\mathbf{G}\mathcal{C}) in either of the components pre\mathit{pre} or post\mathit{post} of a Petri net. Thus, we can get four variants of category N𝒞\mathbf{N}\mathcal{C}, based on the four different combinations for defining morphisms in this category. By changing the direction of the morphism kk in the definition of morphism in the category G𝒞\mathbf{G}\mathcal{C}, we obtain another category, isomorphic to G𝒞 op\mathbf{G}\mathcal{C}^{op}, called G𝒞 co\mathbf{G}\mathcal{C}^{co}. The four variants are as follows. A pair (f,F)(f, F) is a morphism of N𝒞\mathbf{N} \mathcal{C} such that:

  1. (f,F):prepre(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}' in G𝒞\mathbf{G} \mathcal{C}, and (f,F):postpost(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}' in G𝒞\mathbf{G}\mathcal{C}.

  2. (f,F):prepre(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}' in G𝒞 co\mathbf{G}\mathcal{C}^{co}, and (f,F):postpost(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}' in G𝒞\mathbf{G} \mathcal{C}.

  3. (f,F):prepre(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}' in G𝒞\mathbf{G} \mathcal{C}, and (f,F):postpost(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}' in G𝒞 co\mathbf{G}\mathcal{C}^{co}.

  4. (f,F):prepre(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}' in G𝒞 co\mathbf{G}\mathcal{C}^{co}, and (f,F):postpost(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}' in G𝒞 co\mathbf{G}\mathcal{C}^{co}.

We can explicit the conditions above in the case 𝒞=Set\mathcal{C} = \mathbf{Set}. For all ee in EE and all bb' in BB' we get the following inequalities.

  1. pre(e,Fb)pre(fe,b)\mathit{pre}(e, F b') \leq \mathit{pre}'(f e, b') and post(e,Fb)post(fe,b)\mathit{post}(e, F b') \leq \mathit{post}'(f e, b'). Intuitively, this can be summed up as ”more gives more”.

  2. pre(e,Fb)pre(fe,b)\mathit{pre}(e, F b') \geq \mathit{pre}'(f e, b') and post(e,Fb)post(fe,b)\mathit{post}(e, F b') \leq \mathit{post}'(f e, b'). Intuitively, this can be summed up as ”less gives more”.

  3. pre(e,Fb)pre(fe,b)\mathit{pre}(e, F b') \leq \mathit{pre}'(f e, b') and post(e,Fb)post(fe,b)\mathit{post}(e, F b') \geq \mathit{post}'(f e, b'). Intuitively, this can be summed up as ”more gives less”.

  4. pre(e,Fb)pre(fe,b)\mathit{pre}(e, F b') \geq \mathit{pre}'(f e, b') and post(e,Fb)post(fe,b)\mathit{post}(e, F b') \geq \mathit{post}'(f e, b'). Intuitively, this can be summed up as ”less gives less”.

The definition that we chose to present is the first one, given in the earlier version of the paper (where elementary Petri nets are called structurally safe), while the third variant is the same category defined in a later version of the paper. Morphisms in (1) represent refinements, while morphisms in (3) represent simulations.

It is also possible to generalise this construction to arbitrary Petri nets by taking pairs of objects of G𝒞\mathbf{G}\mathcal{C} of the form EB×E \nleftarrow B \times \mathbb{N} and we leave the detailed discussion of this definition as another aspect to investigate further.

We thank the organizers of the ACT school for making this blog post possible and our group, in particular our TA Jade Master for her helpful suggestions.

Posted at July 27, 2020 12:20 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3237

10 Comments & 0 Trackbacks

Re: Linear Logic Flavoured Composition of Petri Nets

This is great! Could some of this be generalized to full-fledged Petri nets? It could be very useful to have a richly structured category of Petri nets and morphisms between them.

And if can’t be generalized, why not?

Posted by: John Baez on July 27, 2020 8:33 PM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

On the Category Theory Community Server Valeria de Paiva writes:

Could some of this be generalized to full-fledged Petri nets?

well, yes, it has been generalized to arbitrary Petri nets. the mathematical basis is the paper that Wilmer Leal and Eigil Rischel were working over, “Categorical multirelations, linear logic and Petri nets” TR from Cambridge.

Posted by: John Baez on July 29, 2020 12:49 AM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

As Valeria de Paiva mentioned, this is possible by considering a slightly different definition of the Dialectica category. Objects in the original definition are (equivalence classes of) monos into products, α:AB×E\alpha \colon A \hookrightarrow B \times E. This is difficult to generalize to multirelations, for example; for this purpose, it is more convenient to think of relations as arrows into 22, α:B×E2\alpha \colon B \times E \to 2. By taking these as objects we can define a Dialectica category equivalent to the original one.

This definition can be easily generalized to model multirelations. We take an object LL of the base category 𝒞\mathcal{C} that is a lineale (a monoidal closed poset) – this will be the natural numbers in Set\mathit{Set} if we want to model multirelations – and we take arrows α:B×EL\alpha \colon B \times E \to L in 𝒞\mathcal{C} as objects of the generalized Dialectica category. This Dialectica category carries the same structure that we presented in this blogpost.

This is explained in details in the paper mentioned above and I believe there will also be a blogpost about it.

During the ACT school we started discussing a way of generalizing the original Dialectica category by taking as objects (equivalence classes of) arrows α:AB×E\alpha \colon A \to B \times E that are not necessarily monos. It is still unclear to us what is the relation between this construction and the generalized Dialectica category as above.

Posted by: Elena Di Lavore on July 31, 2020 8:35 AM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

Sounds to me like a mismatch between two different meanings of “multiset”. Does an element of a multiset simply have a number of times that it occurs, or does it have a whole set of such occurrences? If you don’t quotient the non-monos AB×EA\to B\times E in any way, the category or groupoid of such would be equivalent to maps into some classifying category/groupoid SetSet (or FinSetFinSet if you have finite fibers), instead of its decategorification \mathbb{N}.

Posted by: Mike Shulman on July 31, 2020 9:18 PM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

hi Mike,

Does an element of a multiset simply have a number of times that it occurs yes, I think so.

As far I am concerned there are no non-monos AE×BA\to E\times B. The original constructions insist on monos, always. this is why I say the categories are equivalent over Sets.

Elena wants to generalize it to non-monos AE×BA\to E\times B, and this is cool. I mentioned to her that this was a suggestion of the late Aurelio Carboni, who was also very fond of spans. I was and still am reluctant, as I think the asymmetry given by the ‘lax’ condition on morphisms is what makes the dialectica constructive. But we’re investigating!

Posted by: Valeria de Paiva on August 1, 2020 1:25 AM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

We took as definition of multiset the one with only a number of occurrences for each element. In fact, we considered equivalence classes of arrows AE×BA \to E \times B. But it would probably be interesting to investigate the other option as well.

Posted by: Elena Di Lavore on August 4, 2020 12:02 PM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

What is a “multirelation”?

Posted by: Mike Shulman on July 28, 2020 4:39 PM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

From p. 6 of the paper just mentioned by John above, a multirelation between UU and XX is a function U×XU \times X \to \mathbb{N}.

Posted by: David Corfield on July 29, 2020 8:35 AM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

An object is a pair 𝒩=(pre,post)\mathcal{N}=(\mathit{pre}, \mathit{post}), where pre\mathit{pre} and post\mathit{post} are objects in G𝒞\mathbf{G}\mathcal{C}.

That doesn’t seem right — don’t you have to require that the two objects of G𝒞\mathbf{G}\mathcal{C} have the same underlying pair of objects in 𝒞\mathcal{C}?

Posted by: Mike Shulman on July 29, 2020 5:48 PM | Permalink | Reply to this

Re: Linear Logic Flavoured Composition of Petri Nets

Yes, you are right. We forgot to specify that pre\mathit{pre} and post\mathit{post} need to have the same underlying objects of 𝒞\mathcal{C}. This is because pre\mathit{pre} and post\mathit{post} both relate the same sets of conditions BB and events EE of a Petri net.

Posted by: Elena Di Lavore on July 31, 2020 7:52 AM | Permalink | Reply to this

Post a New Comment