An Approach to the Category of Net Computations

Vladimiro Sassone^{∘}

BRICS^{∗} – Computer Science Dept., University of Aarhus

\underline{Abstract}. We introduce the notion of strong concatenable process as a refinement of concatenable processes [3] which can be expressed axiomatically via a functor Q[ ] from the category of Petri nets to an appropriate category of symmetric strict monoidal categories, in the precise sense that, for each net N, the strong concatenable processes of N are isomorphic to the arrows of Q[N]. In addition, we identify a coreflection right adjoint to Q[ ] and characterize its replete image, thus yielding an axiomatization of the category of net computations.

Introduction

Petri nets, introduced by C.A. Petri in [8] (see also [10]), are unanimously considered among the most representative models for concurrency, since they are a fairly simple and natural model of concurrent and distributed computations. However, Petri nets are, in our opinion, not yet completely understood.

Among the semantics proposed for Petri nets, a relevant role is played by the various notions of process [9, 4, 1], whose merit is to provide a faithful account of computations involving many different transitions and of the causal connections between the events occurring in a computation. However, process models, at least in their standard forms, fail to bring to the foreground the algebraic structure of nets and their computations. Since such a structure is relevant to the understanding of nets, they fail, in our view, to give a comprehensive account of net behaviours.

The idea of looking at nets as algebraic structures [10, 7, 13, 14, 2] has been given an original interpretation by considering monoidal categories as a suitable framework [6]. In fact, in [6, 3] the authors have shown that the semantics of Petri nets can be understood in terms of symmetric monoidal categories— where objects are states, arrows processes, and the tensor product and the arrow composition model, respectively, the operations of parallel and sequential composition of processes. In particular, [3] introduced concatenable processes—the slightest variation of Goltz-Reisig processes [4] on which sequential composition can be defined—and structured the concatenable processes of a Petri net N as the arrows of the symmetric strict monoidal category P[N]. This yields an axiomatization of the causal behaviour of a net as an essentially algebraic theory and thus provides a unification of the process and the algebraic view of net computations.

However, also this construction is somehow unsatisfactory, since it is not functorial. More strongly, given a morphism between two nets, i.e., a simulation between them, it may not be possible to identify a corresponding monoidal functor between the respective categories of computations. This fact, besides showing that our understanding of the algebraic structure of Petri nets is still incomplete, prevents us from identifying the category (of the categories) of net computations, i.e., from axiomatizing the behaviour of Petri nets ‘in the large’.

* Basic Research in Computer Science, Centre of the Danish National Research Foundation.

∘ Supported by EU Human Capital and Mobility grant ERBCHBGCT920005.

This paper presents an analysis of this issue and a solution based on the new notion of strongly concatenable processes, introduced in Section 4. These are a slight refinement of concatenable processes which are still rather close to the standard notion of process: they are Goltz-Reisig processes whose minimal and maximal places are linearly ordered. In the paper we show that, similarly to concatenable processes, also this new notion can be axiomatized as an algebraic construction on N by providing an abstract symmetric strict monoidal category Q[N] whose arrows are in one-to-one correspondence with the strongly concatenable processes of N. The category Q[N] constitutes our proposed axiomatization of the behaviour of N in categorical terms.

Corresponding directly to the linear ordering of pre- and post-sets which characterizes strongly concatenable processes, the key feature of Q[ ] is that, differently from P[ ], it associates to the net N a monoidal category whose objects form a free non-commutative monoid. The reason for renouncing to commutativity when passing from P[ ] to Q[ ], a choice that at first may seem odd, is explained in Section 2, where the following negative result is proved: under very reasonable assumptions, no mapping from nets to symmetric strict monoidal categories whose monoids of objects are commutative can be lifted to a functor, since there exists a morphism of nets which cannot be extended to a monoidal functor between the appropriate categories. Thus, abandoning the commutativity of the monoids of objects and considering strings as representatives of multisets, i.e., considering strongly concatenable processes, seem to be a choice forced upon us by the aim of a functorial algebraic semantics of nets. As a consequence of this choice, any transition of N has many corresponding arrows in Q[N], actually one for each linearization of its pre-set and of its post-set. However, such arrows are ‘related’ to each other by a naturality condition, in the precise sense that, when collected together, they form a natural transformation between appropriate functors. This naturality axiom is the second relevant feature of Q[ ] and it is actually the key to keep the computational interpretation of the new category Q[N], i.e., the strongly concatenable processes, surprisingly close to that of P[N], i.e., the concatenable processes.

Concerning our main issue, viz. functoriality, in Section 3 we introduce a category \underline{TSSMC}^{⊗} of symmetric strict monoidal categories with free noncommutative monoids of objects, called symmetric Petri categories, whose arrows are equivalence classes—accounting for our view of strings as representatives of multisets—of those symmetric strict monoidal functors which preserve some further structure related to nets, and we show that Q[ ] is a functor from \underline{Petri}, a rich category of nets introduced in [6], to \underline{TSSMC}^{⊗}. In addition, we prove that Q[ ] has a coreflection right adjoint N [ ]: \underline{TSSMC}^{⊗} → \underline{Petri}. This implies, by general reasons, that \underline{Petri} is equivalent to an easily identified coreflective subcategory of \underline{TSSMC}^{⊗}, namely the replete image of Q[ ]. The category \underline{TSSMC}^{⊗}, together with the functors Q[ ] and N [ ], constitutes our proposed axiomatization (‘in the large’) of Petri net computations in categorical terms.

Although this contribution is a first attempt towards the aims of a functorial algebraic semantics for nets and of an axiomatization of net behaviours ‘in the large’, we think that the results given here help to deepen the understanding of the subject. We remark that the refinement of concatenable processes into strongly concatenable processes is similar and comparable to the one which brought from Goltz-Reisig processes to them, and that the result of Section 2 makes strongly concatenable processes ‘unavoidable’ if a functorial construction is desired. In addition, from the categorical viewpoint, our approach is quite natural, since it is the one which simply observes that multisets are equivalence classes of strings and then takes into account the categorical paradigm, following which one always prefers to add suitable isomorphisms between objects rather than considering explicitly equivalence classes of them. Finally, concerning the use of category theory in semantics, and in particular in this paper, it may be appropriate to observe here that the categorical framework made it possible to discover and amend an ‘anomaly’ of P[ ] significant and of general relevance which could have not been noticed in other frameworks.

Due to the extended abstract nature of this paper, most of the proofs are omitted. Some preliminary related results appear also in [11].

\underline{Notation}. When dealing with a category \underline{C} in which arrows are meant to represent computations, in order to stress its computational interpretation, we write arrow composition from left to right, i.e., in the diagrammatic order, and we denote it by ; . The reader is referred to [5] for the categorical concepts used. \underline{Acknowledgements}. I wish to thank José Meseguer and Ugo Montanari to whom I am indebted for several discussions on the subject. Thanks to Mogens Nielsen, Claudio Hermida and Jaap Van Oosten for their valuable comments on an early version of this paper.

1 Concatenable Processes

In this section we recall the notion of concatenable processes [3].

\underline{Notation}. Given a set S, we denote by S^{⊕} the set of finite multisets of S, i.e., the set of all functions from S to the set ω of natural numbers which yield nonzero values only on finitely many s ∈ S. We recall that S^{⊕} is a commutative monoid, actually the free commutative monoid on S, under the operation of multiset union, in the following denoted by ⊕, with unit element the empty multiset 0.

Definition 1.1 (Petri Nets) A Petri net is a structure N = (∂_{N}^{0}, ∂_{N}^{1}: T_{N} → S_{N}^{⊕}), where T_{N} is a set of transitions, S_{N} is a set of places, and ∂_{N}^{0} and ∂_{N}^{1} are functions. A morphism of Petri nets from N_{0} to N_{1} is a pair ⟨f, g⟩, where f: T_{N_{0}} → T_{N_{1}} is a function and g: S_{N_{0}}^{⊕} → S_{N_{1}}^{⊕} is a monoid homomorphism such that ⟨f, g⟩ respects source and target, i.e., ∂_{N_{1}}^{i} ∘ f = g ∘ ∂_{N_{0}}^{i}, for i = 0, 1. This defines the category \underline{Petri} of Petri nets.

This describes a Petri net precisely as a graph whose set of nodes is a free commutative monoid, i.e., the set of finite multisets on a given set of places. The source and target of an arc, here called a transition, are meant to represent, respectively, the markings consumed and produced by the firing of the transition.

Definition 1.2 (Process Nets and Processes) A process net is a finite, acyclic net Θ such that for all t ∈ T_{Θ}, ∂_{Θ}^{0}(t) and ∂_{Θ}^{1}(t) are sets (as opposed to multisets), and for all t_{0} ≠ t_{1} ∈ T_{Θ}, ∂_{Θ}^{i}(t_{0})∩∂_{Θ}^{i}(t_{1}) = ∅, for i = 0, 1. Given N ∈ \underline{Petri}, a process of N is a morphism π: Θ → N, where Θ is a process net and π is a net morphism which maps places to places (as opposed to morphisms which map places to markings).

We consider as identical process nets which are isomorphic. Consequently, we shall make no distinction between two processes π: Θ → N and π′: Θ′ → N for which there exists an isomorphism φ: Θ → Θ′ such that π′ ∘ φ = π.

The equivalence of the following definition of P[N] with the original one in [3] has been proved in [12]. The reader is referred to the cited works for a more explicit description of P[N], a wider discussion, and for related examples.

Definition 1.3 The category P[N] is the monoidal quotient of ℱ(N), the symmetric strict monoidal category whose monoid of objects is S_{N}^{⊕} and whose arrows are freely generated from the transitions of N, modulo the axioms

γ_{a,b} = id_{a⊕b} if a, b ∈ S_{N} and a ≠ b,
t; (id ⊗ γ_{a,a} ⊗ id) = t  if t ∈ T_{N} and a ∈ S_{N},
(id ⊗ γ_{a,a} ⊗ id); t = t  if t ∈ T_{N} and a ∈ S_{N},

where γ is the symmetry isomorphism of ℱ(N).

The arrows of P[N] have a nice computational interpretation as concatenable processes, a slight refinement of the classical notion of process consisting of a suitable labelling of the minimal and the maximal places of process nets which distinguishes among the different instances of a place in a process of N. The role of the symmetries is to regulate the flow of causality between subprocesses by permuting instances of places appropriately, i.e., by exchanging causes. In this view, the first axiom says that permuting different places does not change the causal relationships, and the remaining two say that the same happens when permuting places in the pre- and in the post-set of a transition. Using the labels, it is easy to define an operation of concatenation of concatenable processes and, thus, a category CP[N] whose objects are the multisets S_{N}^{⊕} and whose arrows are the concatenable processes of N. It has been proved in [3] that CP[N] is a symmetric strict monoidal category and that the following result holds.

Theorem 1.4 CP[N] and P[N] are isomorphic.

2 A Negative Result about Functoriality

Among the primary requirements usually imposed on constructions like P[ ] there is that of functoriality. One of the main reasons supporting the choice of a categorical treatment of semantics is the need of specifying further the structure of the systems under analysis by giving explicitly the morphisms or, in other words, by specifying how the given systems simulate each other. This, in turn, means to choose precisely what the relevant (behavioural) structure of the systems is. It is then clear that such morphisms should be preserved at the semantic level. In our case, the functoriality of P[ ] means that if N can be mapped to N′ via a morphism ⟨f, g⟩, which by the very definition of net morphisms implies that N can be simulated by N′, there must be a way, namely P[⟨f, g⟩], to see the processes of N as processes of N′. However, this is not possible for P[ ]. The problem, as illustrated by the following example, is due to the first axiom in Definition 1.3 which, on the other hand, is exactly what makes P[N] capture quite precisely the notion of processes of N.

Example 2.1 Consider the nets N and N̄ in the picture below, where we use the standard graphical representation of nets in which circles are places, boxes are transitions, and sources and targets are directed arcs. We have S_{N} = {a_{0}, a_{1}, b_{0}, b_{1}} and T_{N} consisting of the transitions t_{0}: a_{0} → b_{0} and t_{1}: a_{1} → b_{1}, while SN̄ = {ā, b̄_{0}, b̄_{1}} and TN̄ contains t̄_{0}: ā → b̄_{0} and t̄_{1}: ā → b̄_{1}.

[figure: \begin{matrix}a_{0} & a_{1} & & ā \\ t_{0} & t_{1} & t̄_{0} & & t̄_{1} \\ b_{0} & b_{1} & b̄_{0} & & b̄_{1} \end{matrix}]

Consider now the net morphism ⟨f, g⟩ where f(t_{i}) = t̄_{i}, g(a_{i}) = ā and g(b_{i}) = b̄_{i}, for i = 0, 1. We claim that ⟨f, g⟩ cannot be extended to a monoidal functor P[⟨f, g⟩] from P[N] to P[N̄]. Suppose in fact that F is such an extension. Then, it must be F(t_{0} ⊗ t_{1}) = F(t_{0}) ⊗ F(t_{1}) = t̄_{0} ⊗ t̄_{1}. Moreover, since t_{0} ⊗ t_{1} = t_{1} ⊗ t_{0}, we would have

t̄_{0} ⊗ t̄_{1} = F(t_{1} ⊗ t_{0}) = t̄_{1} ⊗ t̄_{0},

which is impossible since the leftmost and the rightmost terms above are different processes in P[N̄].

Formally speaking, the problem is that the category of symmetries sitting inside P[N], say Sym_{N}, is not free. Moreover, it is easy to verify that as soon as one imposes axioms on P[N] which guarantee to get a functor, one annihilates all the symmetries and, therefore, destroys the ability of P[N] of dealing with causality. It is important to observe that it would be definitely meaningless to try to overcome the problem simply by dropping from \underline{Petri} the morphisms which ‘behave badly’: the morphism ⟨f, g⟩ of Example 2.1, for instance, is clearly a simulation and, as such, it should definitely be allowed by any serious attempt to formulate a definition of net morphisms. The following result shows that the problem illustrated in Example 2.1 is serious, actually deep enough to prevent any naive modification of P[ ] from being functorial.

Theorem 2.2 Let X [ ] be a function which assigns to each net N a symmetric strict monoidal category whose monoid of objects is commutative and contains the places of N. Suppose that the group of symmetries at any object of X [N] is finite and suppose that there exists a net N with a place a ∈ N such that, for each n > 1, we have that the components at (na, na) of the symmetry isomorphism of X [N] is not an identity. Then, there exists a Petri net morphism ⟨f, g⟩: N_{0} → N_{1} which cannot be extended to a symmetric strict monoidal functor from X [N_{0}] to X [N_{1}].

Proof. (Sketch.) Let N′ be a net such that, for each n, we have c′_{na,na} ≠ id, where c′ is the symmetry natural isomorphism of X [N′], and let N be a net with two distinct places a and b and with no transitions, and let c′ be the symmetry natural isomorphism of X [N]. Since the group of symmetries at ab is finite, there is a cyclic subgroup generated by c_{a,b}, i.e., there exists k > 1, the order of the subgroup, such that (c_{a,b})^{k} = id and (c_{a,b})^{n} ≠ id for any 1 ≤ n < k. Let p be any prime number greater than k. Then, exploiting general properties of monoidal categories and reasoning as in Example 2.1, one sees that the Petri net morphism ⟨f, g⟩: N → N′, where f is the function ∅ → T_{N′} and g is the monoid homomorphism such that g(b) = (p − 1)a and g is the identity on the other places of N, cannot be extended to a symmetric strict monoidal functor F: X [N] → X [N′]. ✓

The contents of the previous proposition may be restated in different terms by saying that in the free category of symmetries on a commutative monoid M there are infinite homsets. This means that dropping axiom γ_{a,b} = id_{a⊕b} in the definition of P[N] causes an ‘explosion’ of the structure of the symmetries. More precisely, if we omit that axiom we can find some object u such that the group of symmetries on u has infinite order. Of course, since symmetries represent causality, and as such they are integral parts of processes, this makes the category so obtained completely useless for the application we have in mind.

The hypothesis of Theorem 2.2 can be certainly weakened in several ways, at the expense of complicating the proof. However, we avoided such complications since the conditions stated above are already weak enough if one wants to regard X [N] as a category of processes of N. In fact, since places represent the atomic bricks of which states are built, one needs to consider them in X [N], since symmetries regulate the ‘flow of causality’, there will be c_{na,na} different from the identity, and since in a computation we can have only finitely many ‘causality streams’, there will not be categories with infinite groups of symmetries. Therefore, the given result means that there is no chance to have a functorial construction of the processes of N along the lines of P[N] whose objects form a commutative monoid.

3 The Category Q[N]

In this section we introduce the symmetric strict monoidal category Q[N] which is meant to represent the processes of the Petri net N and which supports a functorial construction. This will allow us to characterize the category of the categories of net behaviours, i.e., to axiomatize net behaviours ‘in the large’.

Theorem 2.2 shows that, necessarily, there is a price to be payed. Here, the idea is to renounce to the commutativity of the monoids of objects. More precisely, we build the arrows of Q[N] starting from the Sym_{N}^{∗}, the ‘free’ category of symmetries over the set S_{N} of places of N. This choice makes each transition of N have many corresponding arrows in Q[N]; however, the arrows of Q[N] which differ only by being instances of the same transition are linked together by a ‘naturality’ condition which guarantees that Q[N] remains close to the category P[N] of concatenable processes. Namely, the arrows of Q[N] correspond to Goltz-Reisig processes in which the minimal and the maximal places are linearly ordered.

Similarly to Sym_{N}, Sym_{N}^{∗} serves a double purpose: from the categorical point of view it provides the symmetry isomorphism of a symmetric monoidal category, while from a semantic perspective it regulates the flow of causal dependency. Generally speaking, a symmetry in Q[N] should be interpreted as a ‘reorganization’ of the tokens in the global state of the net which, when reorganizing multiple instances of the same place, yields a exchange of causes exactly as Sym_{N} does for P[N].

\underline{Notation}. In the following, we use S^{⊗} to indicate the set of (finite) strings on set S, more commonly denoted by S^{∗}. In the same way, we use ⊗ to denote string concatenation, while 0 denotes the empty string. As usual, for u ∈ S^{⊗}, we indicate by |u| the lenght of u and by u_{i} its i-th element.

Definition 3.1 (The Category of Permutations) Let S be a set. The category Sym_{S}^{∗} has for objects the strings S^{⊗} and an arrow p: u → v if and only if p is a permutation of |u| elements, and v is the string obtained by applying the permutation p to u, i.e., v_{p(i)} = u_{i}. Arrows composition in Sym_{S}^{∗} is obviously given by the product of permutations, i.e., their composition as functions, here and in the following denoted by ; .

Graphically, we represent an arrow p: u → v in Sym_{S}^{∗} by drawing a line between u_{i} and v_{p(i)}, as for example in Figure 1. Of course, it is possible to define a tensor product on Sym_{S}^{∗} together with interchange permutations which make it a symmetric monoidal category (see also Figure 1 where γ is the permutation {1 → 2, 2 → 1}).

Definition 3.2 (Operations on Permutations) Given the permutations p: u → v and p′: u′ → v′ in Sym_{S}^{∗} their parallel composition p ⊗ p′: u ⊗ u′ → v ⊗ v′ is the permutation such that

i ↦ \{ \begin{matrix}p(i) & if 0 < i ≤ |u| \\ p′(i − |u|) + |u| & if |u| < i ≤ |u| + |u′| \end{matrix}

Given a permutation π of m elements and the strings u_{i} ∈ S^{⊗}, i = 1, …, m, the interchange permutation π(u_{1}, …, u_{m}) is the permutation p such that

p(i) = i − ∑_{j=1}^{h−1} |u_{j}| + ∑_{π(j)<π(h)} |u_{j}| if ∑_{j=1}^{h−1} |u_{j}| < i ≤ ∑_{j=1}^{h} |u_{j}|.

[figure: \begin{matrix}a & a & a & b & b \\ a & a & a & b & b \end{matrix}] ⊗ [figure: \begin{matrix}a & a & b \\ a & a & b \end{matrix}] = [figure: \begin{matrix}a & a & a & b & b & a & a & b \\ a & a & a & b & b & a & a & b \end{matrix}]

γ([figure: a a b] ,[figure: a a a b b]) = [figure: \begin{matrix}a & a & b & a & a & a & b & b \\ a & a & a & b & b & a & a & b \end{matrix}]

Figure 1: The monoidal structure of Sym_{S}^{∗}

It is easy to see that ⊗ extends to a functor ⊗: Sym_{S}^{∗} × Sym_{S}^{∗} → Sym_{S}^{∗} making Sym_{S}^{∗} a strict monoidal category. Moreover, the family of interchange permutations γ = {γ(u, v)}_{u,v∈Sym_{S}^{∗}} provides the symmetry isomorphism which makes Sym_{S}^{∗} a symmetric strict monoidal category.

Theorem 3.3 Let S be a set, let \underline{C} be a symmetric strict monoidal category and let F be a function from S to the set of objects of \underline{C}. Then, there exists a unique symmetric strict monoidal functor F: Sym_{S}^{∗} → \underline{C} extending F.

The preceding result proves that the mapping S ↦ Sym_{S}^{∗} extends to a left adjoint functor from \underline{Set}, the category of sets, to \underline{SSMC}, the category of symmetric strict monoidal categories. Equivalently, Sym_{S}^{∗} is the free symmetric strict monoidal category on the set S, which is the key point about Sym_{S}^{∗}.

In the following, given a string u ∈ S^{⊗}, let M(u) denote the multiset corresponding to u, and, given a net N, let Sym_{N}^{∗} the category Sym_{S_{N}}^{∗}.

Definition 3.4 ( The category Q[N]) Let N be a net in \underline{Petri}. Then Q[N] is the category which includes Sym_{N}^{∗} as subcategory and has as additional arrows those defined by the following inference rules:

\frac{t: M(u) → M(v) in T_{N}}{t_{u,v}: u → v in Q[N]}

\frac{α: u → v and β: u′ → v′ in Q[N]}{α ⊗ β: u ⊗ u′ → v ⊗ v′ in Q[N]}  \frac{α: u → v and β: v → w in Q[N]}{α ; β: u → w in Q[N]}

plus the axioms expressing the fact that Q[N] is a symmetric strict monoidal category with symmetry isomorphism γ, and the following axiom involving transitions and symmetries.

p ; t_{u′,v′} = t_{u,v} ; q where p: u → u′ in Sym_{N}^{∗} and q: v → v′ in Sym_{N}^{∗}. (Φ)

Exploiting the freeness of Sym_{N}^{∗}, it is easy to prove the following completely axiomatic description of Q[N], which can be useful in many contexts.

Proposition 3.5 Q[N] is (isomorphic to) the category \underline{C} whose objects are the elements of S_{N}^{⊗} and whose arrows are generated by the inference rules

\frac{u ∈ S_{N}^{⊗}}{id_{u}: u → u in \underline{C}} \frac{u, v in S_{N}^{⊗}}{c_{u,v}: u ⊗ v → v ⊗ u in \underline{C}} \frac{t: M(u) → M(v) in T_{N}}{t_{u,v}: u → v in \underline{C}}
\frac{α: u → v and β: u′ → v′ in \underline{C}}{α ⊗ β: u ⊗ u′ → v ⊗ v′ in \underline{C}} \frac{α: u → v and β: v → w in \underline{C}}{α; β: u → w in \underline{C}}

modulo the axioms expressing that \underline{C} is a strict monoidal category, namely,

α; id_{v} = α = id_{u}; α and (α; β); δ = α; (β; δ),
(α ⊗ β) ⊗ δ = α ⊗ (β ⊗ δ) and id_{0} ⊗ α = α = α ⊗ id_{0},
id_{u} ⊗ id_{v} = id_{u⊗v} and (α ⊗ α′); (β ⊗ β′) = (α; β) ⊗ (α′; β′),

the latter whenever the righthand term is defined, the following axioms expressing that \underline{C} is symmetric with symmetry isomorphism c

c_{u,v⊗w} = (c_{u,v} ⊗ id_{w}); (id_{v} ⊗ c_{u,w}),
c_{u,u′}; (β ⊗ α) = (α ⊗ β); c_{v,v′} for α: u → v, β: u′ → v′,
c_{u,v}; c_{v,u} = id_{u⊗v},

and the following axiom corresponding to axiom (Φ)

p ; t_{u′,v′} ; q = t_{u,v} where p: u → u′ and q: v′ → v are symmetries.

We show next that Q[ ] can be lifted to a functor from the category of Petri nets to an appropriate category of symmetric strict monoidal categories and equivalence classes of symmetric strict monoidal functors. The role of such an equivalence is to take into account that we look at the strings of S_{N}^{⊗} as concrete representatives of the multisets of S_{N}^{⊕} and, therefore, we want to consider perfectly equal those functors which differ only by picking different, yet compatible, linearizations of multisets.

Definition 3.6 (Symmetric Petri Categories) A symmetric Petri category is a symmetric strict monoidal category \underline{C} in \underline{SSMC} whose monoid of objects is the free monoid S^{⊗} for some set S.

For any pair \underline{C} and \underline{D} of symmetric Petri categories, consider the binary relation ℛ_{\underline{C},\underline{D}} on the symmetric strict monoidal functors from \underline{C} to \underline{D} defined as F ℛ_{\underline{C},\underline{D}} G if and only if there exists a monoidal natural isomorphism σ: F ≅ G whose components are all symmetries. Clearly, ℛ_{\underline{C},\underline{D}} is an equivalence relation and the family ℛ = \{ℛ_{\underline{C},\underline{D}}\}_{\underline{C},\underline{D} ∈\underline{SSMC}} is a congruence with respect to functor composition. Therefore, the following definition makes sense.

Definition 3.7 (The category \underline{SSMC}^{⊗}) Let \underline{SSMC}^{⊗} be the quotient of the full subcategory of \underline{SSMC} consisting of the symmetric Petri categories modulo the congruence ℛ.

Theorem 3.8 (Q[ ]: \underline{Petri} → \underline{SSMC}^{⊗}) Q[ ] extends to a functor from \underline{Petri} to \underline{SSMC}^{⊗}.

Proof. (Sketch.) Let ⟨f, g⟩: N_{0} → N_{1} be a morphism of Petri nets. In order define Q[⟨f, g⟩] we need to be able to embed N in Q[N]. To this end, consider any function in_{N_{1}}: S_{N_{1}}^{⊕} → S_{N_{1}}^{⊗} such that M(in_{N_{1}}(ν)) = ν. Since g is a monoid homomorphism from the free monoid S_{N_{0}}^{⊕} to S_{N_{1}}^{⊕}, it corresponds to a unique function g′ from S_{N_{0}} to S_{N_{1}}^{⊕}, whence we obtain ĝ = in_{N_{1}} ∘ g′: S_{N_{0}} → S_{N_{1}}^{⊗}, i.e., a function from S_{N_{0}} to the set of objects of Q[N_{1}]. Then, from Theorem 3.3, we have the symmetric strict monoidal functor F′: Sym_{S_{N_{0}}} → Q[N_{1}]. Finally, we extend F′ to a functor Q[⟨f, g⟩] from Q[N_{0}] to Q[N_{1}] by considering the symmetric strict monoidal functor F which coincides with F′ on Sym_{N_{0}} and maps t_{u,v}: u → v to f(t)_{F(u),F(v)}: F(u) → F(v). Since monoidal functors map symmetries to symmetries, and since f(t) is transition of N_{1}, it follows immediately that F preserves axiom (Φ), i.e., that F is well defined. Moreover, since a different choice of in_{N_{1}} would clearly give a functor G such that F ℛ G, we have that Q[ ] does not depend on in_{N_{1}}. It is easy to check that this definition makes Q[ ] into a functor. ✓

However, the category \underline{SSMC}^{⊗} is still too general for our purpose. In particular, it is easily noticed that Q[ ] is not full. This signifies that \underline{SSMC}^{⊗} has too little structure to represent net behaviours precisely enough; equivalently, since the structure of the objects of a category \underline{C} is ‘encoded’ in the morphisms of \underline{C}, it signifies that the morphisms of \underline{SSMC}^{⊗} do not capture the structure of symmetric Petri categories precisely enough. Specifically, the transitions, which are definitely primary components of nets, and as such are treated by the morphisms in \underline{Petri}, have no corresponding notion in \underline{SSMC}^{⊗}: we need to identify such a notion and refine the choice of the category of net computations accordingly.

The key to accomplish our task is the following observation about axiom (Φ) in Definition 3.4: as already mentioned, it simply expresses that the collection of the arrows t_{u,v} of Q[N], for t ∈ T_{N} and u, v ∈ S_{N}^{⊗}, is a natural transformation. Namely, for \underline{C} a symmetric Petri category with objects S^{⊗}, and ν a multiset in S^{⊕}, let Sym_{\underline{C},ν} be the subcategory of \underline{C} consisting of those objects u ∈ S^{⊗} such that M(u) = ν and the symmetries between them, and let in_{\underline{C},ν} be the inclusion of Sym_{\underline{C},ν} in \underline{C}. Then, for ν, ν′ ∈ S^{⊕}, one obtains a pair of parallel functors π_{\underline{C},ν} and π_{\underline{C},ν′} by composing in_{\underline{C},ν} and in_{\underline{C},ν′} respectively with the first and with the second projection of Sym_{\underline{C},ν} × Sym_{\underline{C},ν′}.

Sym_{\underline{C},ν}
Sym_{\underline{C},ν} × Sym_{\underline{C},ν′}  \underline{C}
Sym_{\underline{C},ν′}

in_{\underline{C} ,ν} [figure]

π_{0}

[figure]

π_{\underline{C} ,ν} [figure]

π_{\underline{C} ,ν′} [figure]

π_{1}

[figure] in_{\underline{C} ,ν′} [figure]

It follows directly from the definitions that, when \underline{C} is Q[N], axiom (Φ) states exactly that, for all t: ν → ν′ ∈ T_{N}, the set {t_{u,v} | M(u) = ν, M(v) = ν′} is a natural transformation from π_{Q[N],ν} to π_{Q[N],ν′}.

A further very relevant property of the transitions of N when considered as arrows of Q[N] is that of being decomposable as a tensor only trivially and as a composition only by means of symmetries. This is easily captured by the following notion of primitive arrow.

Definition 3.9 (Primitive Arrows) Let \underline{C} be a symmetric Petri category. An arrow τ in \underline{C} is primitive if

i) τ is not a symmetry;

ii) τ = α; β implies α is a symmetry and β is primitive, or viceversa;

iii) τ = α ⊗ β implies α = id_{0} and β is primitive, or viceversa.

A simple inspection of Definition 3.4 shows that the only primitive arrows in Q[N] are the arrows t_{u,v}, for t: M(u) → M(v) a transition of N. As a consequence, the natural transformations τ: π_{Q[N],ν} →^{▪} π_{Q[N],ν′} whose components are primitive are in one-to-one correspondence with the transitions of N. Following the usual categorical paradigm, we then use the properties that characterize the transitions of N in Q[N], expressed in abstract categorical terms, to define the notion of transition in any symmetric Petri category.

Definition 3.10 (Transitions of Symmetric Petri Categories) Let \underline{C} be a symmetric Petri category and let S^{⊗} be its monoid of objects. A transition of \underline{C} is a natural transformation τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}, for ν, ν′ in S^{⊕}, whose components τ_{u,v} are primitive arrows of \underline{C}.

It is clear now what the extra structure required in \underline{SSMC}^{⊗} is: transitions must be preserved by morphisms of symmetric Petri categories. Formally, for \underline{C} and \underline{D} in \underline{SSMC}^{⊗} and F: \underline{C} → \underline{D} in \underline{SSMC}, F respects transitions if, for each transition τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′} of \underline{C}, there exists a transition τ′: π_{\underline{D} ,ν̄} →^{▪} π_{\underline{D} ,ν̄′} of \underline{D} such that F(τ_{u,v}) = τ′_{F(u),F(v)} for all (u, v) in Sym_{\underline{C},ν} × Sym_{\underline{C},ν′}; in this case, we say that τ′ corresponds to τ via F.

The following lemma shows that a symmetric strict monoidal functor which preserves transitions defines a mapping between sets of transitions and that, moreover, this property extends to the arrows of \underline{SSMC}^{⊗}. It follows immediately that Definition 3.12 is well given.

Lemma 3.11 If F: \underline{C} → \underline{D} respects transitions, then for any transition τ of \underline{C}, there exists a unique transition τ′ of \underline{D} which corresponds to τ via F. If F ℛ G, then F respects transitions if and and only if G does so, and then τ′ corresponds to τ via F if and only if τ′ corresponds to τ via G.

Definition 3.12 (Symmetric Petri Morphisms and the Category \underline{TSSMC}^{⊗}) A morphism of symmetric Petri category is an arrow in \underline{SSMC}^{⊗} which respects transitions. We shall use \underline{TSSMC}^{⊗} denote the (lluf) subcategory of \underline{SSMC}^{⊗} whose arrows are the morphisms of symmetric Petri categories.

Finally, it is easy to prove that Q[ ] is actually a functor to \underline{TSSMC}^{⊗}.

Proposition 3.13 ( Q[ ]: \underline{Petri} → \underline{TSSMC}^{⊗}) The functor Q[ ] restricts to a functor from \underline{Petri} to \underline{TSSMC}^{⊗}.

Proof. It is enough to verify that, for any morphism ⟨f, g⟩: N_{0} → N_{1} in \underline{Petri}, a representative F of Q[⟨f, g⟩] respects transitions. This follows at once, since f is a function T_{N_{0}} → T_{N_{1}}, F(t_{u,v}) = f(t)_{F(u),F(v)}, and the transitions of Q[N_{i}] are exactly the natural transformations {t_{u,v} | M(u) = ν, M(v) = ν′} for t: ν → ν′ ∈ T_{N_{i}}. ✓

Interestingly enough, we can identify a functor from \underline{TSSMC}^{⊗} to \underline{Petri} which is a coreflection right adjoint to Q[ ]. It is worth remarking that this answers to a possible legitimate doubt about the category \underline{TSSMC}^{⊗}: in principle, in fact, the functoriality of Q[ ] could be due to a very tight choice of the target category, e.g., the congruence ℛ could induce too many isomorphisms of categories and Q[ ] make undesirable identifications of nets. The existence of a coreflection right adjoint to Q[ ] is, of course, the best possible proof of the adequacy of \underline{TSSMC}^{⊗}: it implies that \underline{Petri} is embedded in it fully and faithfully as a coreflective subcategory. This result supports our claim that \underline{TSSMC}^{⊗} is an axiomatization of the category of net computations.

Theorem 3.14 ( Q[ ] ⊣ N [ ]: \underline{Petri} → \underline{TSSMC}^{⊗} ) Let \underline{C} be a symmetric Petri category, and let S^{⊗} be its monoid of objects. Define N [\underline{C}] to be the Petri net (∂^{0}, ∂^{1}: T → S^{⊕}), where

• T is the set of transitions τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′} of \underline{C};

• ∂^{0}(τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}) = ν and ∂^{1}(τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}) = ν′.

Then, N [ ] extends to a functor \underline{TSSMC}^{⊗} → \underline{Petri} which is right adjoint to Q[ ]. In addition, since the unit is an isomorphism, the adjunction is a coreflection.

Proof. For any symmetric Petri category \underline{C}, there is a (unique) symmetric strict monoidal functor ε\underline{C}: QN [\underline{C}] → \underline{C} which is the identity on the objects and which sends the component at (u, v) of the transition τ: ν → ν′ of N [\underline{C}] to the component τ_{u,v} of the natural transformation τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}: Sym_{\underline{C},ν} ×Sym_{\underline{C},ν′} → \underline{C}. Since it clearly preserves transitions, we have that ε\underline{C} is a (representative of a) morphism of symmetric Petri categories. It is not difficult to prove that ε\underline{C} enjoys the couniversal property making it the counit of the adjunction. The unit η_{N}: N → N Q[N] is the morphism ⟨f, id⟩, where f sends t ∈ T_{N} to {t_{u,v}} ∈ T_{N Q[N]}, which is an iso. ✓

We end this section by identifying the replete image of Q[ ] in \underline{TSSMC}^{⊗}, i.e., the full subcategory of \underline{TSSMC}^{⊗} consisting of those symmetric Petri categories isomorphic to Q[N], for some N in \underline{Petri}.

Theorem 3.15 ( \underline{Petri} ≅ \underline{PSSMC}) Let \underline{PSSMC} be the full subcategory of \underline{TSSMC}^{⊗} consisting of those symmetric Petri categories \underline{C} whose arrows can be generated by tensor and composition from symmetries, and components of transitions of \underline{C}, uniquely up to the axioms of symmetric strict monoidal categories, i.e., the axioms in Proposition 3.5, and the naturality of transitions, i.e., axiom (Φ). Then, \underline{PSSMC} and \underline{Petri} are equivalent.

Proof. By general results in category theory, it is enough to show that \underline{C} belongs to \underline{PSSMC} if and only if ε\underline{C}: QN [\underline{C}] → \underline{C} is an isomorphism, which is easy. ✓

4 Strongly Concatenable Processes

In this section we introduce a slight refinement of concatenable processes and we show that they are abstractly represented by the arrows of the category Q[N]. In other words, we find a process-like representation for the arrows of Q[N]. This yields a functorial construction for the category of the processes of a net N.

Definition 4.1 (Strongly Concatenable Processes) Given a petri net N in \underline{Petri}, a strongly concatenable process of N is a tuple (π, ℓ, L) where π: Θ → N is a process of N, and ℓ: min(Θ) → {1, …, | min(Θ)|} and L: max(Θ) → {1, …, | max(Θ)|} are isomorphisms, i.e., total orderings of, respectively, the minimal and the maximal places of Θ. An isomorphism of strongly concatenable processes is an isomorphism of the underlying processes which, in addition, preserves the orderings ℓ and L. As usual, we identify isomorphic strongly concatenable processes.

As in the case of concatenable processes, it is easy to define an operation of concatenation of strongly concatenable processes. We associate a source and a target in S_{N}^{⊗} to each strongly concatenable process by taking the string corresponding to the linear ordering of, respectively, min(Θ) and max(Θ). Then, the concatenation of (π_{0}: Θ_{0} → N, ℓ_{0}, L_{0}): u → v and (π_{1}: Θ_{1} → N, ℓ_{1}, L_{1}): v → w is the strongly concatenable process u → w obtained by merging the maximal places of Θ_{0} and the minimal of Θ_{1} according to L_{0} and ℓ_{1}. (See Figure 2, where we enrich the usual representation of non-sequential processes by labelling the minimal and the maximal places with the values of, respectively, ℓ and L.)

Proposition 4.2 Under the above defined operation of sequential composition, the strongly concatenable processes of N form a category CQ[N] whose identities are those processes consisting only of places, which therefore are both minimal and maximal, and such that ℓ = L.

Strongly concatenable processes admit a tensor product ⊗ such that, given SCP = (π_{0}: Θ_{0} → N, ℓ_{0}, L_{0}): u → v and SCP′ = (π_{1}: Θ_{1} → N, ℓ_{1}, L_{1}): u′ → v′, SCP⊗SCP′ is the strongly concatenable process (π: Θ → N, ℓ, L): u⊗u′ → v⊗v′ given below (see also Figure 2), where +, besides the usual sum of natural numbers, denotes also the disjoint union of sets and functions, and in_{0} and in_{1} the corresponding injections.

• Θ = (∂_{Θ_{0}}^{0} + ∂_{Θ_{1}}^{0}, ∂_{Θ_{0}}^{1} + ∂_{Θ_{1}}^{1}: T_{Θ_{0}} + T_{Θ_{1}} → (S_{Θ_{0}} + S_{Θ_{1}})^{⊕});

• π = π_{0} + π_{1};

• ℓ(in_{0}(a)) = ℓ_{0}(a) and ℓ(in_{1}(a)) = | min(Θ_{0})| + ℓ_{1}(a);

• L(in_{0}(a)) = L_{0}(a) and L(in_{1}(a)) = | max(Θ_{1})| + L_{1}(a).

Observe that ⊗ is a functor ⊗: CQ[N] × CQ[N] → CQ[N]. The strongly concatenable processes consisting only of places are analogous in CQ[N] of the

[figure: \begin{matrix}a & a \\ t_{0} & t_{1} \\ a & a \end{matrix}; 1; 2; 2; 1; ;; \begin{matrix}a & a \\ t_{0} \\ a \end{matrix}; 1; 2; 1; 2] = [figure: \begin{aligned}a & a \\ t_{0} & t_{1} \\ a & a \\ & t_{0} \\ & a \end{aligned}; 1; 2; 1; 2] = [figure: \begin{matrix}a \\ t_{0} \\ a \end{matrix}; 1; 1] ⊗ [figure: \begin{matrix}a \\ t_{1} \\ a \\ t_{0} \\ a \end{matrix}; 1; 1]

Figure 2: An example of the algebra of concatenable processes

[figure: \begin{aligned}u_{1} & ⋯ & u_{n} \\ & t \\ v_{1} & ⋯ & v_{m} \end{aligned}; 1; n; 1; m; u_{1} ⋯ u_{n} v_{1} ⋯ v_{m}; 1; m+1; n; m+n; n+1; 1; n+m; m]

Figure 3: A transitions t_{u,v}: u → v and the symmetry γ(u, v) in CQ[N]

permutations of Q[N]. In particular, for any u, v ∈ S^{⊗}, the strongly concatenable process γ̄(u, v) consisting of places in one-to-one correspondence with the elements of the string u ⊗ v mapped by π to the corresponding places of N, and such that ℓ(u_{i}) = i, ℓ(v_{i}) = |u| + i, L(u_{i}) = |v| + i and L(v_{i}) = i, plays in CQ[N] the role played by the permutation γ(u, v) in Q[N] (see also Figure 3).

Proposition 4.3 Under the above defined tensor product CQ[N] is a symmetric strict monoidal category whose symmetry isomorphism is the family {γ̄(u, v)}_{u,v∈S_{N}^{⊗}}.

The transitions t of N are faithfully represented in the obvious way by processes with a unique transition which is in the post-set of any minimal place and in the pre-set of any maximal place, minimal and maximal places being in one-to-one correspondence, respectively, with ∂_{N}^{0}(t) and ∂_{N}^{1}(t). Thus, varying ℓ and L on the process corresponding to a transition we obtain a representative in CQ[N] of each instance t_{u,v} of t in Q[N] (see also Figure 3).

Theorem 4.4 CQ[N] and Q[N] are isomorphic.

Proof. (Sketch.) Consider the following mapping F from the arrows of Q[N] to strongly concatenable processes.

• An instance t_{u,v} of a transition t of Q[N] is mapped to the strongly concatenable processes with a unique transition and two layers of places: the minimal, in one-to-one correspondence with ∂_{N}^{0}(t) and ordered by ℓ to form the string u, and the maximal, in one-to-one correspondence with ∂_{N}^{1}(t) and ordered to form v.

• The permutation γ(u, v) is sent to the strongly concatenable process γ̄(u, v).

• F is extended inductively to a generic term α of Q[N], i.e., α_{0} ⊗ α_{1} is mapped to F(α_{0}) ⊗ F(α_{1}) and α_{0} ; α_{1} to F(α_{0}); F(α_{1}).

Then, defining F to be the identity on the objects gives the required isomorphism F: Q[N] ≅ CQ[N]. ✓

References

[1] E. Best and R. Devillers. Sequential and Concurrent Behaviour in Petri Net Theory. Theoretical Computer Science, n. 55, pp. 87–136, 1987.

[2] C. Brown, D. Gurr, and V. de Paiva. A Linear Specification Language for Petri Nets. Technical Report DAIMI PB-363, Computer Science Dept., Aarhus University, 1991.

[3] P. Degano, J. Meseguer, and U. Montanari. Axiomatizing Net Computations and Processes. In Proceedings of the 4th LICS Symposium, pp. 175–185, IEEE, 1989.

[4] U. Goltz and W. Reisig. The Non-Sequential Behaviour of Petri Nets. Information and Computation, n. 57, pp. 125–147, 1983.

[5] S. MacLane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[6] J. Meseguer and U. Montanari. Petri Nets are Monoids. Information and Computation, n. 88, pp. 105–154, Academic Press, 1990.

[7] M. Nielsen, G. Plotkin, and G. Winskel. Petri Nets, Event Structures and Domains, Part 1. Theoretical Computer Science, n. 13, pp. 85–108, 1981.

[8] C.A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Bonn, Germany, 1962.

[9] C.A. Petri. Non-Sequential Processes. Interner Bericht ISF–77–5, Gesellschaft für Mathematik und Datenverarbeitung, Bonn, Germany, 1977.

[10] W. Reisig. Petri Nets. Springer-Verlag, 1985.

[11] V. Sassone. On the Semantics of Petri Nets: Processes, Unfoldings, and Infinite Computations. PhD Thesis TD 6/94, Dipartimento di Informatica, Università di Pisa, 1994.

[12] V. Sassone. Some Remarks on Concatenable Processes. Technical Report TR 6/94, Dipartimento di Informatica, Università di Pisa, 1994.

[13] G. Winskel. A New Definition of Morphism on Petri Nets. In Proceedings of STACS ‘84, LNCS, n. 166, pp. 140–150, Springer-Verlag, 1984.

[14] G. Winskel. Petri Nets, Algebras, Morphisms and Compositionality. Information and Computation, n. 72, pp. 197–238, 1987.