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)pre′b′ epostF(b′) ⇒f(e)post′b′ \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 $α:A→E×B \alpha \colon A \to E \times B$ in $𝒞\mathcal{C}$ . We indicate them with $α:E↚B\alpha \colon E \nleftarrow B$ .
A morphism $(f,F):α→α′(f,F) \colon \alpha \to \alpha'$ between two objects $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ is given by a pair of morphisms $f:E→E′f \colon E \rightarrow E'$ and $F:B′→BF \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 $e′e'$ , 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 0′b_0'$ that can deactivate $b 1′b_1'$ .

Their cartesian product represents the concurrent activation of $b 1b_1$ or $b 2b_2$ by $b 0b_0$ and deactivation of $b 1′b_1'$ by $b 0′b_0'$ . In fact, in order to be able to activate $b 1b_1$ and deactivate $b 1′b_1'$ simultaneously, all the preconditions of $e 1e_1$ in $𝒩 1\mathcal{N}_1$ and all the preconditions of $e′e'$ 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 $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ in $G𝒞\mathbf{G} \mathcal{C}$ is the relation $α&α′:E×E′↚B+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 $b′b'$ , 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. $𝒩⊕𝒩′=(pre⊕pre′,post⊕post′)\mathcal{N} \oplus \mathcal{N}' = (\mathit{pre} \oplus \mathit{pre}', \mathit{post}\oplus \mathit{post}')$ where $pre⊕pre′\mathit{pre} \oplus \mathit{pre}'$ and $post⊕post′\mathit{post}\oplus \mathit{post}'$ are coproducts in $G𝒞\mathbf{G}\mathcal{C}$ .

We define the coproduct of two objects $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ in $G𝒞\mathbf{G} \mathcal{C}$ . It is the relation $α⊕α′:E+E′↚B×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 $e′e'$ 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 $f′f'$ 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 $E′E'$ to $BB$ that sends $e′e'$ to $b ib_i$ . We indicate with $𝟙,lnot,! 0,! 1\mathbb{1}, \lnot, !_0, !_1$ the functions from $EE$ to $B′B'$ that send $e ie_i$ to $b′ i−1b'_{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 $e′e'$ and all those channels that, whenever $e′e'$ 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 0′f'(e_1) = b_0'$ or $f′(e 1)=b 1′f'(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 0′f'(e_1)=b_0'$ .

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

$⟨e,e′⟩pre ⊗⟨f,f′⟩ ⇔epref(e′) and e′pre′f′(e) ⟨e,e′⟩post ⊗⟨f,f′⟩ ⇔epostf(e′) and e′post′f′(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 $𝒩⊗𝒩′=(pre⊗pre′,post⊗post′)\mathcal{N} \otimes \mathcal{N}' = (\mathit{pre} \otimes \mathit{pre}', \mathit{post}\otimes \mathit{post}')$ where $pre⊗pre′\mathit{pre} \otimes \mathit{pre}'$ and $post⊗post′\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 $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ in $G𝒞\mathbf{G} \mathcal{C}$ . It is the relation $α⊗α′:E×E′↚B 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 $f∧f′f \wedge f'$ indicates the pullback of $ff$ and $f′f'$ .

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

$⟨e,e′⟩(α⊗α′)⟨f,f′⟩⇔eα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 $e∈Ee \in E$ and $b′∈B′b' \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 $B′B'$ to $BB$ that sends $b 0′b_0'$ to $b ib_i$ and with $!!$ the only function from $EE$ to $E′E'$ .

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)pre′b′ ⟨f,F⟩[post,post′]⟨e,b′⟩ ⇔ if epostF(b′) then f(e)post′b′ \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 $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ is the relation $[α,α′]:E′ E×B B′↚E×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×B′E'^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}$ , $fwedgef′f \wedgef'$ indicates the pullback of $ff$ and $f′f'$ 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 $b∈Bb \in B$ and $b′∈B′b' \in B'$ . We can see an example.

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

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

$⟨f,f′⟩pre ⅋⟨b,b′⟩ ⇔f(b′)preb or f′(b)pre′b′ ⟨f,f′⟩post ⅋⟨b,b′⟩ ⇔f(b′)postb or f′(b)post′b′ \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 $𝒩⅋𝒩′=(pre⅋pre′,post⅋post′)\mathcal{N} \invamp \mathcal{N}' = (\mathit{pre} \invamp \mathit{pre}', \mathit{post}\invamp \mathit{post}')$ where $pre⅋pre′\mathit{pre} \invamp \mathit{pre}'$ and $post⅋post′\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 $α:E↚B\alpha \colon E \nleftarrow B$ and $α′:E′↚B′\alpha' \colon E' \nleftarrow B'$ is the relation $α⅋α′:E B′×E′ B↚B×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 $f′f'$ .

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

$⟨f,f′⟩(α⅋α′)⟨b,b′⟩⇔f(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 $e′e'$ , 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:

$(f,F):pre→pre′(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}'$ in $G𝒞\mathbf{G} \mathcal{C}$ , and $(f,F):post→post′(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}'$ in $G𝒞\mathbf{G}\mathcal{C}$ .
$(f,F):pre→pre′(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}'$ in $G𝒞 co\mathbf{G}\mathcal{C}^{co}$ , and $(f,F):post→post′(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}'$ in $G𝒞\mathbf{G} \mathcal{C}$ .
$(f,F):pre→pre′(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}'$ in $G𝒞\mathbf{G} \mathcal{C}$ , and $(f,F):post→post′(f, F) \colon \ \mathit{post} \ \rightarrow \mathit{post}'$ in $G𝒞 co\mathbf{G}\mathcal{C}^{co}$ .
$(f,F):pre→pre′(f, F) \colon \mathit{pre} \rightarrow \mathit{pre}'$ in $G𝒞 co\mathbf{G}\mathcal{C}^{co}$ , and $(f,F):post→post′(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 $b′b'$ in $B′B'$ we get the following inequalities.

$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”.
$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”.
$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”.
$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 $E↚B×ℕ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.

from Hacker News https://ift.tt/2ZZDg9G

SymmetricalDataSecurity

Wednesday, July 29, 2020

Linear Logic Flavoured Composition of Petri Nets

Preliminary definitions

Petri nets

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

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

Composing Petri nets

Cartesian product

Coproduct

Monoidal product

Units

Exponential

Disjunctive monoidal product

Negation

Asynchronous events

Discussion

No comments:

Post a Comment

Blog Archive

Search This Blog

Total Pageviews

Wednesday, July 29, 2020

Linear Logic Flavoured Composition of Petri Nets

Preliminary definitions

Petri nets

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

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

Composing Petri nets

Cartesian product

Coproduct

Monoidal product

Units

Exponential

Disjunctive monoidal product

Negation

Asynchronous events

Discussion

No comments:

Post a Comment

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

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