BRICS RS-94-33 V. Sassone: Strong Concatenable Processes

BRICS

Basic Research in Computer Science

Strong Concatenable Processes: An Approach to the Category of Petri Net Computations

Vladimiro Sassone

BRICS Report Series RS-94-33 ISSN 0909-0878 October 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

Strong Concatenable Processes: An Approach to the Category of Petri Net Computations

Vladimiro Sassone

BRICS^{∗} – Computer Science Department University of Aarhus, Denmark

\underline{Abstract}. We introduce the notion of strong concatenable process for Petri nets as the least refinement of non-sequential (concatenable) processes which can be expressed abstractly by means of a functor Q[ ] from the category of Petri nets to an appropriate category of symmetric strict monoidal categories with free non-commutative monoids of objects, in the precise sense that, for each net N, the strong concatenable processes of N are isomorphic to the arrows of Q[N]. This yields an axiomatization of the causal behaviour of Petri nets in terms of symmetric strict monoidal categories. In addition, we identify a coreflection right adjoint to Q[ ] and we characterize its replete image in the category of symmetric monoidal categories, thus yielding an abstract description of the category of net computations.

Introduction

Petri nets, introduced by C.A. Petri in [17] (see also [18, 20]), are unanimously considered among the most representative models for concurrency, since they are a fairly simple and natural model of concurrent and distributed computation. 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 [19, 9, 2], 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.

Strong Concatenable Processes

The idea of looking at nets as algebraic structures [20, 16, 23, 24, 3, 4, 15], has been given an original interpretation by considering monoidal categories as a suitable framework [13]. In fact, in [13, 6] 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, [6] introduced concatenable processes—the slightest variation of Goltz-Reisig processes [9] on which sequential composition can be defined—and structured 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.

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

The author was supported by EU Human Capital and Mobility grant ERBCHBGCT920005.

This work was partly carried out during the author’s doctorate at Università di Pisa.

However, also this construction is somehow unsatisfactory, since it is not functorial. More strongly, as illustrated in Section 2, given a morphism between two nets—which is nothing but a simulation—it may not be possible to identify a corresponding monoidal functor between the respective categories of computations. This situation, besides showing that our understanding of the structure of nets is still incomplete, has also other drawbacks, the most relevant of which is probably that it prevents us to identify the category (of the categories) of net computations, i.e., to axiomatize the behaviour of Petri nets “in the large”.

This paper presents an analysis of this issue and a solution based on the new notion of strong 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: namely, they are Goltz-Reisig processes whose minimal and maximal places are linearly ordered. In the paper we show that, similarly to concatenable processes, the strong concatenable processes of N can be axiomatized as an algebraic construction on N by providing an abstract symmetric strict monoidal category Q[N] whose arrows are isomorphic to the strong concatenable processes of N. The category Q[N] constitutes our proposed axiomatization of the behaviour of N in categorical terms.

The key feature of Q[ ] is that, differently from P[ ], it associates to net N a monoidal category whose objects form a free, non-commutative monoid. The reason for renouncing to commutativity, a choice that at first glance 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 seems to be a price that has to be paid in order to obtain a functorial version of the algebraic semantics of nets given in [6]. Then, bringing such a condition at the level of nets, instead of taking multisets of places as sources and targets of computations, we consider strings of places, a choice which leads us directly to strong concatenable processes.

Correspondingly, a transition of N is represented by many arrows in Q[N], one for each different “linearization” of its pre-set and its post-set. However, such arrows are “linked” 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] surprisingly close to the category P[N] of concatenable processes.

Concerning functoriality, in Section 3 we introduce \underline{TSSMC}^{⊗}, a category of symmetric strict monoidal categories with free non-commutative monoids of objects, called symmetric Petri categories, whose arrows are equivalence classes 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 [13], 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 given by strong concatenable processes is similar and comparable to the one which brought from Goltz-Reisig processes to them. Clearly, the passage here is less obvious on intuitive grounds, since it brings us to model Petri nets, which after all are just multiset rewriting systems, using strings. It is important, however, to remind that the result of Section 2 makes strong 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 prefer to add suitable isomorphisms between objects rather than considering explicitly equivalence classes of them.

Some preliminary related results appear also in [21].

\underline{Notation}. Given a category \underline{C}, we denote the composition of arrows in \underline{C} by the usual symbol ∘ and follow the usual right to left order. The identity of c ∈ \underline{C} is written as id_{c}. However, we make the following exception. When dealing with a category in which arrows are meant to represent computations, in order to stress this, we write arrow composition from left to right, i.e., in the diagrammatic order, and we denote it by ; . Moreover, when no ambiguity arises, id_{c} is simply written as c. We shall use \underline{SSMC} to indicate the category of (small) symmetric strict monoidal categories and symmetric strict monoidal functors. Since the monoidal categories considered in the paper are always strict monoidal and (non-strictly) symmetric, we may sometimes omit to mention all the attributes without causing misunderstandings.

The reader is referred to [12] for the categorical concepts used in the paper. The basic definitions concerning monads and symmetric strict monoidal categories are summarized, respectively, in Appendices A and B.

\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 process [6] and we give the definitions which will be used in the rest of the paper.

\underline{Notation}. Given a function ν from a set S to the set of natural numbers ω, its support is the subset of S consisting of those elements s such that μ(s) > 0. We denote by S^{⊕} the set of finite multisets of S, i.e., the set of all functions from S to ω with finite support. We shall represent a finite multiset ν ∈ S^{⊕} as a formal sum ⨁_{i∈I} n_{i}s_{i} where {s_{i} | i ∈ I} is the support of ν and n_{i} = ν(s_{i}), i.e., as a sum whose summands are all nonzero.

\underline{Remark}. We recall that S^{⊕} is a commutative monoid, actually the free commutative monoid on S, under the operation of multiset union with unit element the empty multiset 0. Clearly, ⊕ can be extended to an endofunctor ( )^{⊕} on \underline{Set}, the category of (small) sets and functions, by taking, for each f: S_{0} → S_{1}, the monoid homomorphism f^{⊕}: S_{0}^{⊕} → S_{1}^{⊕} defined by f^{⊕}(⨁_{i∈I} n_{i}s_{i}) = ⨁_{i∈I} n_{i}f(s_{i}). This gives a monad (see Appendix A) (( )^{⊕}, η, μ) on \underline{Set}, where η_{S}: S → S^{⊕} is the function which maps s ∈ S to the singleton multiset s, and μ_{S}: (S^{⊕})^{⊕} → S^{⊕} is the monoid homomorphism which sends a multiset of multisets ν to the multiset ⨁ ν obtained as union of the elements of ν. Of course, the ( )^{⊕}-algebras are exactly the commutative monoids and the ( )^{⊕}-homomorphisms are the monoid homomorphisms.

Definition 1.1 (Petri Nets) A Place/Transition Petri (PT) 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, ∂_{N}^{0} and ∂_{N}^{1} are functions.

A morphism of PT 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., they make the two rectangles obtained by choosing the upper or lower arrows in the parallel pairs of the diagram below commute.

[figure: \begin{matrix}T_{N_{0}} & S_{N_{0}}^{⊕} \\ T_{N_{1}} & S_{N_{1}}^{⊕} \end{matrix}; ∂_{N_{0}}^{0}; ∂_{N_{0}}^{1}; f; g; ∂_{N_{1}}^{0}; ∂_{N_{1}}^{1}]

This, with the obvious componentwise composition of morphisms, defines the category \underline{Petri} of PT nets.

1. Concatenable Processes

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

i) for all t ∈ T_{Θ}, ∂_{Θ}^{0}(t) and ∂_{Θ}^{1}(t) are non-empty sets (as opposed to possibly empty multisets);

ii) for all pairs 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).

For the purpose of defining processes at the right level of abstraction, we need to make some identifications. Of course, we shall consider as identical process nets which are isomorphic and, consequently, we shall make no distinction between two processes π: Θ → N and π′: Θ′ → N for which there exists an isomorphism φ: Θ → Θ′ such that π′ ∘ φ = π. Observe that the constraint on π is relevant, since we certainly want process morphisms to map a single component of the process net to a single component of N. Otherwise said, process are nothing but labellings of Θ, which in turn is essentially a partial ordering of transitions, with an appropriate element of N.

The equivalence of the following definition of P[N] with the original one in [6] has been proved in [22].

Definition 1.3 The category P[N] is the monoidal quotient (see Appendix B) of ℱ(N), the free symmetric strict monoidal category generated by 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 in terms of a slight refinement of the classical notion of process consisting of a suitable layer of labels to the minimal and to the maximal places of process nets in order to distinguish among different istances of a place in a process of N.

Definition 1.4 ( f-indexed orderings) Given the sets A and B together with a function f: A → B, an f-indexed ordering of A is a family {ℓ_{b} | b ∈ B} of bijections ℓ_{b}: f^{−1}(b) → {1, …, |f^{−1}(b)|}, f^{−1}(b) being as usual the set {a ∈ A | f(a) = b}.

Informally, an f-indexed ordering of A is a family of total orderings, one for each of the partitions of A induced by f. In the following, given a process net Θ, let min(Θ) and max(Θ) denote, respectively, its minimal and maximal elements, which must be places.

Definition 1.5 (Concatenable Processes) A concatenable process of N is a triple CP = (π, ℓ, L) where

• π: Θ → N is a process of N;

• ℓ is a π-indexed ordering of min(Θ);

• L is a π-indexed ordering of max(Θ).

Two concatenable processes CP and CP′ are isomorphic if their underlying processes are isomorphic via an isomorphism φ which respects the ordering, i.e., such that ℓ′_{π′(φ(a))}(φ(a)) = ℓ_{π(a)}(a) and L′_{π′(φ(b))}(φ(b)) = L_{π(b)}(b) for all a ∈ min(Θ) and b ∈ max(Θ). As in the case of processes, we identify isomorphic concatenable processes.

Clearly, it is possible to define an operation of concatenation of concatenable processes, whence their name. We can associate a source and a target in S_{N}^{⊕} to any concatenable process CP, namely by taking the image through π of, respectively, min(Θ) and max(Θ), where Θ is the underlying process net of CP. Then, the concatenation of concatenable processes (π_{0}: Θ_{0} → N, ℓ_{0}, L_{0}): u → v and (π_{1}: Θ_{1} → N, ℓ_{1}, L_{1}): v → w is realized by merging the maximal places of Θ_{0} and the minimal places of Θ_{1} using both the values of π_{0} and π_{1} and the labellings to match those places one-to-one. Under this operation of sequential composition, the concatenable processes of N form a category CP[N] with identities those processes consisting only of places, which therefore are both minimal and maximal, and such that ℓ = L.

Concatenable processes admit also a tensor operation ⊗ which can be though of as the operation of putting two processes side by side and reorganizing the labelling from left to right. The concatenable processes consisting only of places are the symmetries which make CP[N] into a symmetric strict monoidal category; this clarifies that the role of the symmetries in a process is that of regulating the flow of causality between subprocesses by permuting tokens appropriately.

Proposition 1.6 CP[N] and P[N] are isomorphic. Proof. See [6]. ✓

2. A Negative Result about Functoriality

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 therefore 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′.

Unfortunately, this is not possible for P[ ]. More precisely, although it might be possible to extend P[ ] to net morphisms, it is definitely not possible to associates to a net morphism a symmetric monoidal functor, i.e., a functor which respects the monoidal structure of processes, which is certainly what is to be done in our case. The problem, as illustrated by the following example, is due to the particular shape of the symmetries of P[N] 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}]

The morphism ⟨f, g⟩, where f(t_{i}) = t̄_{i}, g(a_{i}) = ā and g(b_{i}) = b̄_{i}, i = 0, 1, cannot be extended to a monoidal functor P[⟨f, g⟩]: P[N] → 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}.

But this is impossible, since the leftmost and the rightmost terms of the chain of equalities above are different arrows of P[N̄].

The problem can be explained formally by saying that the category of symmetries sitting inside P[N], say Sym_{N}, is not free, and this is why we cannot find an extension to P[N] of the morphism ⟨f, g⟩: N → N̄ ↪ P[N̄]. In fact, Definition 1.3 states that Sym_{N} is generated modulo the axiom

γ_{a,b} = id_{a⊕b} if a ≠ b in S_{N}.

Clearly, it is exactly this conditional axiom with a negative premise which prevents Sym_{N} from being free. To make things worse, the theory illustrated extensively in [6, 21] makes it clear that, in order for P[N] to have the interesting computational meaning it has, such an axiom is strictly needed. Moreover, it is easy to observe that as soon as one imposes further 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.

There does not seem to be an easy and satisfactory solution to the functoriality problem for P[ ]. A possible solution which comes naturally to the mind would consist of looking for a non strict monoidal functor, i.e., a functor F together with a natural transformation φ: F (x_{1}) ⊗ F (x_{2}) →^{▪} F (x_{1} ⊗ x_{2}) which substitutes the equality required by strict functors. However, simple examples show that this idea does not lead anywhere, at least unless P[ ] is heavily modified also on the objects, since it is not possible to choose the components of φ “naturally”.

The following proposition shows that the problem illustrated in Example 2.1 is serious, actually deep enough to prevent any naive modification of P[ ] to be functorial.

Proposition 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 S_{N}, the places of N. Suppose further that the group of symmetries at any object of X [N] is finite. Finally, suppose that there exists a net N with a place a ∈ N such that, for each n > 1, we have that the component 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. The key of the proof is the following observation about monoidal categories. Let \underline{C} be a symmetric strict monoidal category with symmetry isomorphism c. Then, for all a ∈ \underline{C} and for all n ≥ 1, we have (c_{a,(n−1)a})^{n} = id, where, in order to simplify the notation, throughout the proof we write na and c_{x,y}^{n} to denote, respectively, the tensor product of n copies of a and the sequential composition of n copies of c_{x,y}. To show that the above identity holds, consider for i = 1, …, n the functor F_{i} from \underline{C}^{n}, the cartesian product of n copies of \underline{C}, to \underline{C} defined as follows.

[figure: \begin{matrix}(x_{1}, …, x_{n}) & x_{i} ⋯ x_{n} ⋯ x_{i+1} \\ (y_{1}, …, y_{n}) & y_{i} ⋯ y_{n} ⋯ y_{i+1} \end{matrix}; (f_{1},...,f_{n}); (f_{i}···f_{n}f_{1}···f_{i+1}); \underline{C}; ^{\underline{C}^{n}}; F_{i}]

Moreover, consider the natural transformations ϕ_{i}: F_{i} →^{▪} F_{i+1}, i = 1, …, n − 1 and ϕ_{n}: F_{n} → F_{1} whose components at x_{1}, …, x_{n} are, respectively, c_{x_{i},x_{i+1}···x_{n}x_{1}···x_{i−1}} and c_{x_{n},x_{1}···x_{n−1}}. Finally, let ϕ be the sequential composition of ϕ_{1}, …, ϕ_{n}. Then, ϕ is a natural transformation x_{1} ⋯ x_{n} →^{▪} x_{1} ⋯ x_{n} built up only from components of c. From the Kelly-MacLane coherence theorem [11, 10] (see also Appendix B) we know that there is at most one natural transformation consting only of identities and components of c, and since the identity of F_{1} is one such transformation, we have that ϕ = id_{F_{1}}. Then, instantiating each variable with a, we obtain (c_{a,(n−1)a})^{n} = id_{na}, as required.

It may be worth observing that the above property holds also for n = 0, provided we define 0a = e and c_{x,y}^{0} = id.

It is now easy to conclude the proof. 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. We claim that the Petri net morphism ⟨f, g⟩: N → N′, where f is the (unique) 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′]. In fact, from the first part of this proof, we know that (c_{a,(p−1)a})^{p} = 1. Moreover, by general results of group theory, the order of the cyclic subgroup generated by c_{a,(p−1)a} must be a factor of p and then, in this case, 1 or p. In other words, either c_{a,(p−1)a} = id or (c_{a,(p−1)a})^{n} ≠ id for all 1 ≤ n < p. If the second situation occurs, then we have F((c_{a,b})^{k}) = id and also F((c_{a,b})^{k}) = (c′_{F(a),F(b)})^{k} = (c′_{a,(p−1)a})^{k} ≠ id, i.e., F cannot exists. Thus, in order to conclude the proof, we only need to show that, in our hypothesis, c′_{a,(p−1)a} ≠ id. For this, it is enough to observe that c′_{a,(p−1)a} = id implies c′_{na,na} = id for n = p − 1, which is against our hypothesis on N′. In fact, c′_{ka,(p−1)a} = ac′_{(k−1)a,(p−1)a} ; c′_{a,(p−1)a}na, whence it follows directly that c′_{(p−1)a,(p−1)a} = id. ✓

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 kind of application we have in mind.

The hypothesis of Proposition 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 on 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 on the line 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 categories of net behaviours, i.e., to axiomatize the behaviour of nets “in the large”. In fact, although [13] and [6] clarify how the behaviour of a single net can be captured by a symmetric strict monoidal category, because of the missing functoriality of P[ ], nothing is said about what the semantic domain for Petri net behaviours should be.

Proposition 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 makes transitions have many corresponding arrows in Q[N]; however, all the arrows of Q[N] which differ only by being instances of the same transition are linked together by a “naturality” condition whose role is to guarantee 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 totally ordered.

3. The Category Q[N]

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 the semantics viewpoint it regulates the flow of causal dependency. It should be noticed, however, that here the point of view is strictly more concrete than in the case of Sym_{N}. In fact, generally speaking, a symmetry in Q[N] must be interpreted as a “reorganization” of the tokens in the global state of the net which, when reorganizing multiple instances of the same place, as a by-product, 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 the 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. \underline{Remark}. The construction of S^{⊗}, which under the operation of string concatenation is the free monoid on S, admits a corresponding monad (( )^{⊗}, η, μ) on \underline{Set}. In this case ( )^{⊗} is the functor which associates to each set S the monoid S^{⊗} and to each f: S_{0} → S_{1} the monoid homomorphism f^{⊗}: S_{0}^{⊗} → S_{1}^{⊗} such that f^{⊗}(u) = ⨂_{i} f(u_{i}), η_{S}: S → S^{⊗} is the injection

of S in S^{⊗}, and μ_{S}: S^{⊗^{2}} → S^{⊗} is the obvious monoid homomorphism mapping a string of elements of S^{⊗} to the concatenation of its component strings. Recall that the algebras for such a monad are the monoids and the homomorphisms are the monoids homomorphisms. \underline{Remark}. A permutation of n elements is an automorphism of the segment of the first n positive natural numbers. The set Π(n) of the n! permutations of n elements is a group under the operation of composition of functions. The neutral element of Π(n) is the identity function on {1, …, n} and the inverse of σ is its inverse function σ^{−1}. The group Π(n) is called the symmetric group on n elements, or of order n!. Due to its triviality, the notion of permutation of zero elements is never considered. However, to simplify notations, we shall assume that the empty function ∅: ∅ → ∅ is the (unique) permutation of zero elements. A permutation σ leaves i fixed if σ(i) = i. A transposition is a permutation which leaves all the elements fixed but two, say i and j, which are exchanged. We shall denote such a σ simply as (i j). Transpositions are a relevant kind of permutations, since each permutation can be written as a composition of transpositions. Moreover, since any transposition (i j) can be expressed as the composition of “swappings” of adjacent integers, we have that the n − 1 transpositions on adjacent integers (1 2), (2 3), … (n − 1 n) generate the group Π(n). In view of this fact, in the following we shall use the term transposition to indicate exclusively permutations of the kind (i i + 1).

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 ∈ Π(|u|), i.e., 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)).

[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}^{∗}

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 π ∈ Π(m) and m strings u_{i} in 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}|.

Clearly, ⊗ so defined is associative and furthermore a simple calculation shows that it satisfies the equations

(p ⊗ p′) ; (q ⊗ q′) = (p ; q) ⊗ (p′ ; q′) and id_{u} ⊗ id_{v} = id_{u⊗v}.

It follows easily that the mapping ⊗: Sym_{S}^{∗} × Sym_{S}^{∗} → Sym_{S}^{∗} defined by

[figure: \begin{matrix}(u, u′) & u ⊗ v \\ (v, v′) & v ⊗ v′ \end{matrix}; (p,p′); (p⊗p′); ^{Sym∗ S}; Sym_{S}^{∗} × Sym_{S}^{∗}; ⊗]

is a functor making Sym_{S}^{∗} a strict monoidal category. Finally, the symmetric structure of Sym_{S}^{∗} is made explicit through the interchange permutations.

Proposition 3.3 ( Sym_{S}^{∗} is symmetric strict monoidal) For any set S, the family γ = {γ(u, v)}_{u,v∈Sym_{S}^{∗}} provides the symmetry isomorphism endowing Sym_{S}^{∗} with a symmetric monoidal structure.

Proof. Recall that γ(u, v) is the interchange permutation defined from the permutation γ = (1 2) in Π(2). It is just a matter of performing a few calculations to verify that, for any p: u → u′ and p′: v → v′, the equations defining a symmetry isomorphism i.e., equations (6) in Appendix B which in the current case reduce to

(γ(u, v) ⊗ w) ; (v ⊗ γ(u, w)) = γ(u, v ⊗ w)
γ(u, v) ; (p′ ⊗ p) = (p ⊗ p′) ; γ(u′, v′)
γ(u, v) ; γ(v, u) = u ⊗ v

hold. Observe that, in fact,

γ(u, v)(i) = \{ \begin{matrix}i + |v| & if 0 < i ≤ |u| \\ i − |u| & if |u| < i ≤ |u| + |v| \end{matrix}

which shows the second equation. Moreover, it implies that (γ(u, v) ; (p′ ⊗p))(i) is equal to p(i) + |v| if 0 < i ≤ |u|, and is equal to p′(i − |u|) if |u| < i ≤ |u| + |v|. On the other hand, we have that ((p⊗p′) ; γ(u′, v′))(i) is equal to p(i)+|v′| = p(i)+|v| if 0 < i ≤ |u| and p′(i − |u|) + |u| − |u| = p′(i − |u|) if |u| < i ≤ |u| + |v|. Therefore, the first equation holds. Concerning the last equation, we have that

(γ(u, v) ⊗ w)(i) = \{ \begin{matrix}i + |v| & if 0 < i ≤ |u| \\ i − |u| & if |u| < i ≤ |u| + |v| \\ i & if |u| + |v| < i ≤ |u| + |v| + |w| \end{matrix}

and, since

(v ⊗ γ(u, w))(i) = \{ \begin{matrix}i & if 0 < i ≤ |v| \\ i + |w| & if |v| < i ≤ |v| + |u| \\ i − |u| & if |v| + |u| < i ≤ |v| + |u| + |w|, \end{matrix}

we have the required equality. ✓

The previous proposition justifies the use of the name symmetries for the arrows of the groupoid Sym_{S}^{∗}. The key point about Sym_{S}^{∗} is that it is a free construction. In order to show it, we need the following lemma [14, 5].

Lemma 3.4 The symmetric group Π(n) is (isomorphic to) the group G freely generated from the set {τ_{i} | 1 ≤ i < n}, modulo the equations (see also Figure 2)

τ_{i}τ_{i+1}τ_{i} = τ_{i+1}τ_{i}τ_{i+1};
τ_{i}τ_{j} = τ_{j}τ_{i} if |i − j| ≥ 1;  (1)
τ_{i}τ_{i} = e;

where e is the neutral element of the group.

[figure: 1 2 3 1 2 3 1 2 3 1 2 3] = [figure: 1 2 3 1 2 3 1 2 3 1 2 3] [figure: 1 2 3 4 1 2 3 4 1 2 3 4] = [figure: 1 2 3 4 1 2 3 4 1 2 3 4]

[figure: 1 2 1 2 1 2] = [figure: 1 2 1 2]

Figure 2: Some instances of the axioms of permutations

Proof. The proof is by induction on n. First of all, observe that for n = 0 and n = 1 the set of generators is empty and the equations are vacuous. Hence, G is the free group on the empty set of generators, i.e., the group consisting only of the neutral element, which is (isomorphic to) Π(0) and Π(1).

Suppose now that the thesis holds for n ≥ 1 and let us prove it for n + 1. It is immediately evident that the permutations of n + 1 elements are generated by the n transpositions, i.e., by those pemutations which leave all the elements fixed but two adjacent ones, which are exchanged. Moreover, the transpositions satisfy axioms (1), as a quick look to Figure 2 shows. It follows that the order of G must not be smaller than the order of Π(n + 1), i.e., |G| ≥ (n + 1)!, where | | is the cardinality function. Moreover, there is a group homomorphism h: G → Π(n + 1) which sends τ_{i} to the transposition (i i + 1), and since the transpositions generate Π(n+1), we have that h is surjective. Thus, in order to conclude the proof, we only need to show that h injective, which clearly follows if we show that |G| = (n + 1)!.

Let H be the subgroup of G generated by {τ_{1}, τ_{2}, …, τ_{n−1}} and consider the n + 1 cosets H_{1}, …, H_{n+1}, where H_{i} = Hτ_{n} ⋯ τ_{i} = {xτ_{n} ⋯ τ_{i} | x ∈ H}, 1 ≤ i ≤ n, and H_{n+1} = H. Then, for 1 ≤ i ≤ n + 1 and 1 ≤ j ≤ n, consider H_{i}τ_{j}. The following cases are possible.

\underline{i > j + 1}. By the second of axioms (1), τ_{j} is permutable with each of τ_{i}, …, τ_{n} and, therefore,

H_{i}τ_{j} = Hτ_{n} ⋯ τ_{i}τ_{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 \\ a & a & a & b & b & a & a & b \end{matrix}]

Figure 3: The parallel composition of permutations

= Hτ_{j}τ_{n} ⋯ τ_{i}
= Hτ_{n} ⋯ τ_{i} = H_{i}.

\underline{i < j}. Again by the second of (1), τ_{j} is permutable with each of τ_{i}, …, τ_{j−2} and, therefore,

H_{i}τ_{j} = Hτ_{n} ⋯ τ_{i}τ_{j}
= Hτ_{n} ⋯ τ_{j+1}τ_{j}τ_{j−1}τ_{j} ⋯ τ_{i}
= Hτ_{n} ⋯ τ_{j+1}τ_{j−1}τ_{j}τ_{j−1} ⋯ τ_{i} by the first of (1)
= Hτ_{j−1}τ_{n} ⋯ τ_{j+1}τ_{j}τ_{j−1} ⋯ τ_{i} by the second of (1)
= Hτ_{n} ⋯ τ_{i} = H_{i}.

\underline{i = j}. Then H_{j}τ_{j} = Hτ_{n} ⋯ τ_{j}τ_{j} which, by the third of (1), is Hτ_{n} ⋯ τ_{j+1} = H_{j+1}. \underline{i = j + 1}. Then H_{j+1}τ_{j} = Hτ_{n} ⋯ τ_{j+1}τ_{j} = H_{j}.

In other words, for 1 ≤ j ≤ n, the sets H_{1} … H_{n+1} remain all unchanged by postmultiplication by τ_{j}, except for H_{j} and H_{j+1} which are exchanged with each other. Now, since each element of G is a product τ_{i_{1}} ⋯ τ_{i_{k}}, it belongs to Hτ_{i_{1}} ⋯ τ_{i_{k}}, i.e., to one of the H_{i}. Hence, G is contained in the union of the H_{i}’s. It follows immediately that, if H is finite, we have that |G| ≤ (n + 1) · |H|. However, by induction hypothesis, H is (isomorphic to) Π(n), and thus H is finite and |H| = n!. Therefore, |G| ≤ (n + 1)!, which concludes the proof. ✓

We are now ready to show the announced fact about Sym_{S}^{∗}.

Proposition 3.5 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.

Proof. Let ⊗ be the tensor product, e the unit object, and γ: x_{1} ⊗x_{2} ⟶^{∼} x_{2} ⊗x_{1} the symmetry natural isomorphism in \underline{C}. There is of course a choice forced upon us for the behaviour of F on objects: the monoidal extension of F, i.e., the mapping

F(0) = e and F(u ⊗ v) = F(u) ⊗ F(v) for u, v ∈ S^{⊗}.

Concerning morphisms, we know by Lemma 3.4 that each arrow in Sym_{S}^{∗} can be written as a composition of transpositions. Moreover, observe that the transposition (i i+1): u⊗a⊗b⊗v → u⊗b⊗a⊗v, where u is a string of length i−1, coincides in Sym_{S}^{∗} with the tensor of γ(a, b): a⊗b → b⊗a with appropriate identities, namely (u ⊗ γ(a, b) ⊗ v). Thus, recalling also that 0 ⊗ γ(a, b) = γ(a, b) = γ(a, b) ⊗ 0, the following definition defines F on all the arrows of Sym_{S}^{∗}.

F(u ⊗ γ(a, b) ⊗ v) = F(u) ⊗ γ_{F(a),F(b)} ⊗ F(v) a, b ∈ S, u, v ∈ S^{⊗};
F(p ; p′) = F(p′) ∘ F(p).  (2)

Observe that both the equations (2) are forced by the definition of symmetric strict monoidal functor (see axioms (7) in Appendix B). It follows that the extension of F to a strict monoidal functor, if it exists, is unique and must be given by (2). Then, in order to conclude the proof, we only need to show that F is well-defined and that it is a symmetric monoidal functor. We first show that F is well-defined. For this, it is enough to show that the axioms (1) of Lemma 3.4 are preserved by F. In fact, this implies that applying the definition of F to two different factorizations of p actually yields the same result, i.e., it implies that F is well-defined. Concering axioms (1), the third one matches directly with the fact that the inverse of γ_{F(a),F(b)} is γ_{F(b),F(a)}, while the second one follows easily from the fact that ⊗ is a functor. In fact, in the hypothesis, we have τ_{i} = (u ⊗ γ(a, b) ⊗ v ⊗ c ⊗ d ⊗ w) and τ_{j} = (u ⊗ b ⊗ a ⊗ v ⊗ γ(c, d) ⊗ w). Thus, we have that

F(τ_{i} ; τ_{j}) = (F(u) ⊗ F(b) ⊗ F(a) ⊗ F(v) ⊗ γ_{F(c),F(d)} ⊗ F(w)) ∘
(F(u) ⊗ γ_{F(a),F(b)} ⊗ F(v) ⊗ F(c) ⊗ F(d) ⊗ F(w))
= (F(u) ⊗ γ_{F(a),F(b)} ⊗ F(v) ⊗ γ_{F(c),F(d)} ⊗ F(w))
= (F(u) ⊗ γ_{F(a),F(b)} ⊗ F(v) ⊗ F(d) ⊗ F(c) ⊗ F(w)) ∘
(F(u) ⊗ F(a) ⊗ F(b) ⊗ F(v) ⊗ γ_{F(c),F(d)} ⊗ F(w))
= F(τ_{j} ; τ_{i})

Finally, concerning the first axiom, we have

F(τ_{i} ; τ_{i+1} ; τ_{i}) = (F(u) ⊗ γ_{F(b),F(c)} ⊗ F(a) ⊗ F(v)) ∘

(F(u) ⊗ F(b) ⊗ γ_{F(a),F(c)} ⊗ F(v)) ∘ (F(u) ⊗ γ_{F(a),F(b)} ⊗ F(c) ⊗ F(v))

= (F(u) ⊗ F(b) ⊗ γ_{F(a),F(c)} ⊗ F(v)) ∘

(F(u) ⊗ γ_{F(a),F(b)⊗F(c)} ⊗ F(v))

= (F(u) ⊗ γ_{F(a),F(c)⊗F(b)} ⊗ F(v)) ∘

(F(u) ⊗ F(a) ⊗ γ_{F(b),F(c)} ⊗ F(v))

= (F(u) ⊗ F(c) ⊗ γ_{F(a),F(b)} ⊗ F(v)) ∘

(F(u) ⊗ γ_{F(a),F(c)} ⊗ F(b) ⊗ F(v)) ∘ (F(u) ⊗ F(a) ⊗ γ_{F(b),F(c)} ⊗ F(v))

= F(τ_{i+1} ; τ_{i} ; τ_{i+1})

where the third equation is by naturality of γ and the others follow from the coherence axiom for γ.

Let us prove that F is a symmetric monoidal functor. Since \underline{C} is a symmetric strict monoidal category, we have γ_{e,x} = γ_{e⊗e,x} = γ_{e,x} ⊗ e ∘ e ⊗ γ_{e,x} = γ_{e,x} ∘ γ_{e,x}, and since γ_{e,x} is invertible, it follows that γ_{e,x} = id_{x}. Of course, the same holds for every symmetric strict monoidal category. Therefore, since F(id_{u}) = F(γ(0, u)) and γ_{e,F(u)} = id_{F(u)}, we have that F(id_{u}) = id_{F(u)}. This, together with the second of the equations (2), means that F is a functor.

Observe further that for permutations p: u → v and p′: u′ → v′ in Sym_{S}^{∗} we have p ⊗ p′ = (p ⊗ u′) ; (v ⊗ p′) (see also Figure 3). Then, we have that

F(p ⊗ p′) = F(v ⊗ p′) ∘ F(p ⊗ u′) = (F(v) ⊗ F(p′)) ∘ (F(p) ⊗ F(u′)) = F(p) ⊗ F(p′),

i.e., F is a strict monoidal functor.

Finally, thanks to the coherence axiom for symmetries, i.e., the first of axioms (6),^{1} we have that γ(a, b ⊗ c) = (γ(a, b) ⊗ c) ; (b ⊗ γ(a, c)) and thus, by the aforesaid axiom and by the coherence of γ,

F(γ(a, b ⊗ c)) = F((γ(a, b) ⊗ c) ; (b ⊗ γ(a, c)))
= (F (b) ⊗ γ_{F (a),F (c)}) ∘ (γ_{F (a),F (b)} ⊗ F (c))
= γ_{F (a),F (b)⊗F (c)} = γ_{F(a),F(b⊗c)}.

Now, by considering the inverses of the arrows appearing in the coherence axiom, we have that γ(a ⊗ b, c) = (a ⊗ γ(b, c)) ; (γ(a, c) ⊗ b) and that γ_{F(a⊗b),F(c)} = (γ_{F(a),F(c)}⊗ F(b)) ∘ (F(a) ⊗ γ_{F(b),F(c)}). Therefore, it follows easily by induction that F(γ(u, v)) = γ_{F(u),F(v)}. Then, F maps each component of the symmetry natural isomorphism of Sym_{S}^{∗} to the corresponding component of γ, i.e., F is a symmetric monoidal functor. ✓

This result proves that the mapping S ↦ Sym_{S}^{∗} extends to a left adjoint functor from \underline{Set} to \underline{SSMC}, the standard category of symmetric strict monoidal (small) categories and symmetric strict monoidal functors. Equivalently, we can say that Sym_{S}^{∗} is the free symmetric strict monoidal category on the set S.

Corollary 3.6 Let \underline{S} be the symmetric strict monoidal category whose monoid of objects is S^{⊗}, the free monoid on S, and whose arrows are freely generated from a family of arrows c_{u,v}: u⊗v → v⊗u, for u, v ∈ S^{⊗}, subject to the axioms (6) in Appendix B (with γ properly replaced by c). Then \underline{S} and Sym_{S}^{∗} are isomorphic.

1Strictly speaking, the first and the third of (6) are the coherence axioms for symmetries.

However, by abuse of language, we shall often refer to the first of (6) as the coherence axiom.

Proof. By definition, \underline{S} is the free monoidal category on S. In fact, since the axioms (6) which define \underline{S} hold in all symmetric strict monoidal categories, it is immediate to verify that \underline{S} enjoys the universal property stated in Proposition 3.5. Then, exploiting in the usual way the uniqueness condition in this universal property, we have that the functors F: Sym_{S}^{∗} → \underline{S} and G: \underline{S} → Sym_{S}^{∗} which are the identity on the objects and which map, respectively, γ(u, v) to c_{u,v} and c_{u,v} to γ(u, v) are inverse to each other. ✓

Now, we can define of Q[N]. 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}^{∗} denote the category Sym_{S_{N}}^{∗}.

Definition 3.7 ( 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 γ (see Appendix B), 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}^{∗}. (Φ)

It is worth noticing that axiom (Φ) entails, as a particular case, the last two axioms in the Definition 1.3 of P[N], called axioms (Ψ) in [6], whenever they make sense in Q[N]. In fact, axiom (Φ) asserts that any diagram of the kind

[figure: \begin{matrix}u & u_{′} \\ v & v_{′} \end{matrix}; p; t_{u,v}; t_{u′,v′}; q]

commutes. Now, fixed u = u′ and v = v′, choosing p = id, respectively q = id, one obtains the first, respectively the second of axioms (Ψ). Of course, when v ≠ v′ one rather obtains t_{u,v} ; q = t_{u,v′}, and when u ≠ u′ one has p ; t_{u,v} = t_{u′,v}.

Exploiting Corollary 3.6, it is easy to prove that the following is an alternative description of Q[N].

Proposition 3.8 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},  (3)
id_{u} ⊗ id_{v} = id_{u⊗v} and (α ⊗ α′); (β ⊗ β′) = (α; β) ⊗ (α′; β′),

the latter whenever the righthand term is defined, the following axioms corresponding to axioms (6) 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′,  (4)
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.

Proof. It is enough to observe that the definition of \underline{C} is simply the definition of Q[N] enriched with the axiomatization of Sym_{N}^{∗} provided by Corollary 3.6. ✓

The previous proposition is relevant, since it gives a completely axiomatic description of the structure of Q[N] which can be useful in many contexts. In the following, we shall at each time use as definitions of Q[N] and Sym_{N}^{∗} those versions best suited for the actual application.

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 issue is not very difficult now, since most of the work has been done in the proof of Proposition 3.5. We start by showing that Q[ ] is a pseudo-functor from \underline{Petri} to \underline{SSMC} in the sense made explicit by Proposition 3.9 below. More precisely, we extend Q[ ] to a mapping from Petri net morphisms to symmetric strict monoidal functors in such a way that identities are preserved strictly, while net morphism composition is preserved only up to a monoidal natural isomorphism. In order to do that, the key point which is still missing is to be able to embed N into Q[N]. To achieve this, we assume for each set S a function in_{S}: S^{⊕} → S^{⊗} such that M(in_{S}(ν)) = ν, i.e., a function which chooses a “linearization” of each ν ∈ S^{⊕}. Clearly, corresponding to different choices of the functions in_{S}, we shall have a different—yet equivalent—extension of Q[ ] to a pseudo-functor. We would like to remark that this apparent arbitrariness of Q[ ] is not at all a concern, since the relevant fact we want to show now is that such an extension exists. Moreover, we shall see shortly that introducing the category \underline{SSMC}^{⊗} one can completely dispense with the functions in_{S}. In the following, given a net N, we shall use in_{N} to denote in_{S_{N}}.

\underline{Remark}. An elegant way to express the idea of “linearization” of a multiset, would be to look for a morphism of monads in: ( )^{⊕} →^{▪} ( )^{⊗}. This would indeed simplify the following formal development and would make Q[ ] be a functor \underline{Petri} → \underline{SSMC}. However, such a morphism does not exist. It is worth noticing that this is because it is not possibile to choose the functions in_{N} “naturally”.

Proposition 3.9 (Q[ ]: \underline{Petri} → \underline{SSMC}) Let ⟨f, g⟩: N_{0} → N_{1} be a morphism in \underline{Petri}. Then, there exists a symmetric strict monoidal functor Q[⟨f, g⟩]: Q[N_{0}] → Q[N_{1}] which extends ⟨f, g⟩. Moreover, Q[id_{N}] = id_{Q[N]} and Q[⟨f_{1}, g_{1}⟩ ∘ ⟨f_{0}, g_{0}⟩] ≅ Q[⟨f_{1}, g_{1}⟩] ∘ Q[⟨f_{0}, g_{0}⟩].

Proof. Let ⟨f, g⟩: N_{0} → N_{1} be a morphism of Petri nets. Since g is a monoid homomorphism from the free monoid S_{N_{0}}^{⊕} to S_{N_{1}}^{⊕}, it corresponds to a unique function g ∘ η_{S_{N_{0}}} from S_{N_{0}} to S_{N_{1}}^{⊕}, where η is the unit of the “commutative monoid” monad. Then, we obtain ĝ = in_{N_{1}} ∘ g ∘ η_{S_{N_{0}}} : 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 Proposition 3.5, we have the symmetric strict monoidal functor F′: Sym_{S_{N_{0}}} → Q[N_{1}]. Clearly, the objects component of F′ is μ̄_{S_{N_{1}}} ∘ ĝ^{⊗}, where μ̄ is the multiplication of the “monoid” monad. Finally, we extend F′ to a functor F from Q[N_{0}] to Q[N_{1}] by considering the symmetric strict monoidal functor 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 a transition of N_{1}, it follows immediately that F preserves axiom (Φ), i.e., that F is well defined. We show next that the above definition makes Q[ ] into a pseudo-functor. First of all, observe that whatever the choice of in_{N}, the function S_{N} ↪ S_{N}^{⊕} →^{in_{N}} S_{N}^{⊗} is the inclusion of S_{N} in S_{N}^{⊗}. It follows from the uniqueness part of the universal property stated in Proposition 3.5 that Q[id_{N}]: Q[N] → Q[N] is the identity functor. Now consider ⟨f_{0}, g_{0}⟩: N_{0} → N_{1} and ⟨f_{1}, g_{1}⟩: N_{1} → N_{2} and, for i = 0, 1, let F_{i} be Q[⟨f_{i}, g_{i}⟩]: Q[N_{i}] → Q[N_{i+1}] and let F be Q[⟨f_{1} ∘f_{0}, g_{1} ∘g_{0}⟩]. We have to show that F ≅ F_{1}F_{0}. Let u ∈ S_{N_{0}}^{⊗}. By definition, we have that F(u_{i}) = in_{N_{2}} ∘ g_{1} ∘ g_{0}(u_{i}) is a permutation of F_{1}F_{0}(u_{i}) = μ̄_{S_{N_{2}}} ∘ĝ_{1}^{⊗}∘ĝ_{0}(u_{i}) and, therefore, there exists a symmetry s_{i}: F(u_{i}) → F_{1}F_{0}(u_{i}) in Q[N_{2}]. Then, we take s_{u} to be s_{1}⊗⋯⊗s_{n}: F(u) → F_{1}F_{0}(u), where n is the lenght of the string u. We shall prove that the family of the s_{u}, for u ∈ S_{N_{0}}^{⊗} is a natural transformation F →^{▪} F_{1}F_{0}. Since s is clearly a monoidal transformation and each s_{u} is an isomorphism, this concludes the proof.

We must show that for any α: u → v in Q[N_{0}] we have F(α) ; s_{v} = s_{u} ; F_{1}F_{0}(α). Exploiting the characterization of Q[N_{0}] given by Proposition 3.8, we proceed by induction on the structure of α. The key to the proof is that s is monoidal, i.e., s_{u⊗v} = s_{u} ⊗ s_{v}, as a simple inspection of the definition shows. If α is an identity, then the claim is obvious. Moreover, if α is a transition t_{u,v}, then we have F(α) = f_{1} ∘f_{0}(t)_{F(u),F(v)} and F_{1}F_{0}(α) = f_{1}(f_{0}(t))_{F_{1}F_{0}(u),F_{1}F_{0}(v)} and the thesis follows immediately from axiom (Φ). Let us consider now α = γ(u, v). Since F and F_{1}F_{0} are symmetric strict monoidal functors, the equation we have to prove reduces to γ(F(u), F(v)) ; s_{v}⊗s_{u} = s_{u}⊗s_{v} ; γ(F_{1}F_{0}(u), F_{1}F_{0}(v)), which certainly holds since {γ(u, v)}_{u,v∈S_{0}^{⊗}} is a natural transformation x_{1}⊗x_{2} →^{▪} x_{2}⊗x_{1}. If α = α′⊗α′′, where α′: u′ → v′ and α′′: u′′ → v′′ then, by induction, we have F(α′) ; s_{v′} = s_{u′} ; F_{1}F_{0}(α′) and F(α′′) ; s_{v′′} = s_{u′′} ; F_{1}F_{0}(α′′). Then, we deduce

F(α′) ⊗ F(α′′) ; s_{v′} ⊗ s_{v′′} = s_{u′} ⊗ s_{u′′} ; F_{1}F_{0}(α′) ⊗ F_{1}F_{0}(α′′),

which is F(α) ; s_{v} = s_{u} ; F_{1}F_{0}(α). Finally, in the case α = α′ ; α′′, where α′: u → v and α′′: u → w, the induction is mantained by pasting the two commutative squares in the following diagrams, which exist by the induction hypothesis

[figure: \begin{matrix}F(u) & F_{1}F_{0}(u) \\ F(v) & F_{1}F_{0}(v) \\ F(w) & F_{1}F_{0}(w) \end{matrix}; F(α′); s_{u}; F_{1}F_{0}(α′); F(α′′); s_{v}; F_{1}F_{0}(α′′); s_{w}]

Thus, F(α) ; s_{v} = s_{u} ; F_{1}F_{0}(α), which concludes the proof. ✓

Therefore, due to technical reasons concerned with the lack of naturality of the functions in_{N}, Q[ ] fails to be a functor from \underline{Petri} to \underline{SSMC}. It is only a pseudo-functor. However, it is worth remarking that this failure is intrinsically different from the situation for P[ ], and that the pseudo-functoriality of Q[ ] is already a valuable result. In fact, in the case of P[ ], we cannot lift net morphisms to functors between the categories of processes, a failure which may possibly rise doubts on the structure chosen to represent the processes of the single net, while in the case of Q[ ], we just cannot define arrow composition better that “up to isomorphism”. This simply brings us to the conclusion that \underline{SSMC} is not the correct target category for the functorial construction we are looking for. Indeed, as we shall see in the following, it is easy to identify a category \underline{SSMC}^{⊗} of symmetric strict monoidal categories such that Q[ ] is a functor \underline{Petri} → \underline{SSMC}^{⊗}. Actually, this construction is already implicit in Proposition 3.9 and corresponds to taking an appropriate quotient of \underline{SSMC}.

Definition 3.10 (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. Moreover, if F′: \underline{C}′ → \underline{C} and G′: \underline{D} → \underline{D}′ are symmetric strict monoidal functors, then whenever F ℛ_{\underline{C},\underline{D}} G we have G′FF′ ℛ_{\underline{C}′,\underline{D}′} G′GF′. In fact, if σ: F ≅ G then G′σF′: F′FG′ ≅ F′GG′, where G′σF′ is clearly monoidal and all its components are symmetries. In other words, the family ℛ is a congruence with respect to functor composition. Therefore, the following definition makes sense.

Definition 3.11 (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 ℛ.

Of course, concerning \underline{SSMC}^{⊗} there is the following easy result.

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

Proof. For ⟨f, g⟩: N_{0} → N_{1}, let Q[⟨, f, g⟩] be the equivalence class of the functor in \underline{SSMC} from Q[N_{0}] to Q[N_{1}] described in Proposition 3.9.

Then, by the cited proposition, for any PT net N, we have that Q[id_{N}] = [id_{Q[N]}]_{ℛ} , which is the identity of Q[N]. Moreover, we have proved that, for ⟨f_{0}, g_{0}⟩: N_{0} → N_{1} and ⟨f_{1}, g_{1}⟩: N_{1} → N_{2} in \underline{Petri}, there exists a monoidal natural isomorphism s: Q[⟨f_{1} ∘ f_{0}, g_{1} ∘ g_{0}⟩] ≅ Q[⟨f_{1}, g_{1}⟩] ∘ Q[⟨f_{0}, g_{0}⟩] whose components are symmetries. Then, Q[⟨f_{1} ∘f_{0}, g_{1} ∘g_{0}⟩] = Q[⟨f_{1}, g_{1}⟩]∘Q[⟨f_{0}, g_{0}⟩] in \underline{SSMC}^{⊗}, i.e., Q[ ] is a functor from \underline{Petri} to \underline{SSMC}^{⊗}. ✓

Observe that, when describing Q[⟨f, g⟩] in \underline{SSMC}^{⊗}, there is no need to consider the family of functions in, since the extensions of ⟨f, g⟩ to a symmetric strict monoidal functor corresponding to different choices of in_{S} yield the same functor in \underline{SSMC}^{⊗}.

However, the category \underline{SSMC}^{⊗} is still too general for our purpose. In particular, it is easily noticed that Q[ ] is not full (though faithful), i.e., that that there are functors from Q[N_{0}] to Q[N_{1}] in \underline{SSMC}^{⊗} which do not correspond to any morphism from N_{0} to N_{1} in \underline{Petri}. This signifies that \underline{SSMC}^{⊗} has too little structure to represent net behaviours precisely enough; in other terms, since the structure of the objects of a category \underline{C} is “encoded” in the morphisms of \underline{C}, it

22 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.

\underline{Notation}. Given a symmetric monoidal category \underline{C}, we use Sym\underline{C} to indicate the subcategory of \underline{C} consisting of the symmetries, i.e., of those arrows which are build up from identities and components of symmetry isomorphism of \underline{C}.

The key to accomplish our task is the following observation about axiom (Φ) in Definition 3.7: 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 full subcategory of Sym\underline{C} consisting of those objects u ∈ S^{⊗} such that M(u) = ν, 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.13 (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.7 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.14 (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.

Lemma 3.15 If F: \underline{C} → \underline{D} preserves transitions, then for any transition τ of \underline{C}, there exists a unique transition τ′ of \underline{D} which corresponds to τ via F.

Proof. First observe that, for any symmetric Petri category \underline{C} and any pair of natural transformations τ, τ′: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′} whenever τ_{u,v} = τ′_{u,v} for some u and v, then τ = τ′. In fact, for any u′ and v′ there exists (s, s′): (u′, v) → (u, v′) in Sym_{\underline{C},ν} × Sym_{\underline{C},ν′}, and then τ_{u′,v′} = s; τ_{u,v}; s′ = s; τ′_{u,v}; s′ = τ′_{u′,v′}.

Now consider the transitions τ′ and τ′′ of \underline{D} and suppose that they both correspond to τ via F. Then, F(τ_{u,v}) = τ′_{F(u),F(v)} = τ′′_{F(u),F(v)}, which implies τ′ = τ′′. ✓

The previous lemma shows that any symmetric strict monoidal functor which preserves transitions defines a mapping between the respective sets of transitions. Then next lemma proves that this extends to the arrows of \underline{SSMC}^{⊗}.

Lemma 3.16 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.

Proof. Let σ: F →^{▪} G: \underline{C} → \underline{D} be a monoidal natural isomorphism whose components are symmetries, suppose that F respects transitions, and consider a transition τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}. By hypothesis, there exists a transition τ′: π_{\underline{D} ,ν̄} →^{▪} π_{\underline{D} ,ν̄′} of \underline{D} such that F(τ_{u,v}) = τ′_{F(u),F(v)} for all (u, v) ∈ Sym_{\underline{C},ν} × Sym_{\underline{C},ν′}. Then, by naturality of σ, G(τ_{u,v}) = σ_{u}^{−1}; τ′_{F(u),F(v)}; σ_{v}, and therefore, by naturality of τ′, G(τ_{u,v}) = τ′_{G(u),G(v)} and the proof is concluded. ✓

It follows now from Lemma 3.16 that the next definition is well given.

Definition 3.17 (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.18 ( 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. But this follows at once, since f is a function from T_{N_{0}} to T_{N_{1}}, since F(t_{u,v}) = f(t)_{F(u),F(v)}, and since 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. More precisely, \underline{Petri} is (equivalent to) a coreflective subcategory of \underline{TSSMC}^{⊗}. This result supports our claim that \underline{TSSMC}^{⊗} is an axiomatization of the category of net computations.

Proposition 3.19 ( 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},ν′}) = ν;

• ∂^{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. Given 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}], in the following denoted by [τ]_{u,v}, to the component τ_{u,v} of the corresponding natural transformation τ: π_{\underline{C},ν} →^{▪} π_{\underline{C},ν′}: Sym_{\underline{C},ν} × Sym_{\underline{C},ν′} → \underline{C}. In fact, by naturality of τ, we have that s; τ_{u′,v′} = τ_{u,v}; s′ for any symmetries s: u → u′ and s′: v → v′ in Sym\underline{C}. It follows then directly from Definition 3.7 that the conditions above define ε\underline{C} (uniquely) as a symmetric strict monoidal functor from QN [\underline{C}] to \underline{C}. In addition, since it clearly preserves transitions, we have that ε\underline{C} is a (representative of a) morphism of symmetric Petri categories. We shall prove that ε\underline{C} enjoys the following couniversal property: for each K: Q[N] → \underline{C} in \underline{TSSMC}^{⊗}, there exists a unique morphism ⟨f, g⟩: N → N [C] in \underline{Petri} such that the following diagram commutes.

[figure: \begin{matrix}QN [\underline{C}] & \underline{C} \\ Q[N] \end{matrix}; ε\underline{C}; Q[⟨f,g⟩]; K]

This proves that N [ ] is right adjoint to Q[ ], in symbols, Q[ ] ⊣ N [ ].

Let S^{⊗} denote the monoid of objects of \underline{C}, and let (∂^{0}, ∂^{1}: T → S^{⊕}) be N [\underline{C}] and F any representative of K. Since the object component of F is a monoid homomorphism, we have M(F(u)) = M(F(v)) whenever M(u) = M(v). Then, the function g: S_{N}^{⊕} → S^{⊕} which sends ν to M(F(u_{ν})), for u_{ν} any linearization of ν, is a well defined monoid homomorphism. Moreover, g does not depend on the chosen representative of K, for if F ℛ F′ then, for all u ∈ S^{⊗}, there is a symmetry σ_{u}: F(u) → F′(u), whence M(F(u)) = M(F′(u)). Concerning the transitions, consider f: T_{N} → T defined as f(t) = τ, where τ is the transition of \underline{C} corresponding via F to the transition \{t_{u,v}\} of Q[N]. By Lemma 3.15, f is well-defined, and by Lemma 3.16, it does not depend on the representative of K. Moreover, since f(t: ν → ν′) = τ implies that τ: π_{\underline{C},g(ν)} →^{▪} π_{\underline{C},g(ν′)}, we have that ⟨f, g⟩: N → N [\underline{C}] is a morphism in \underline{Petri}.

We have to prove that ε\underline{C} ∘ Q[⟨f, g⟩] = K in \underline{TSSMC}^{⊗}. Without loss of generality, exploiting the fact that ℛ is a congruence, we prove that ε ∘ G = F for choosen representatives ε of ε\underline{C}, G of Q[⟨f, g⟩], and F of K. In particular, we can assume that ε is the identity on the objects and that G(u) = F(u) for all u ∈ S_{N}^{⊗}. Then, εG(t_{u,v}) = ε([f(t)]_{G(u),G(v)} ) = f(t)_{G(u),G(v)} = τ_{F(u),F(v)} = F(t_{u,v}), the last equality being since τ is the transition of \underline{C} corresponding to \{t_{u,v}\} via F. The required equality of functors follows now directly from Definition 3.7. Finally, the uniqueness of ⟨f, g⟩ follows immediately, since if the diagram has to commute, then both the definitions of f and g are forced.

By general results in category theory, the component η_{N}: N → N Q[N] of the unit of Q[ ] ⊣ N [ ] is the unique arrow which makes the diagram commute when \underline{C} is Q[N] and K is the (equivalence class of the) identity of Q[ ]. Applying the previous part of the proof, we have that η_{N} = ⟨f, g⟩, where g is the identity of S_{N}^{⊕} and f sends t ∈ T_{N} to {t_{u,v}} ∈ T_{N Q[N]}. Since by the definitions of N [ ] and of transition of Q[N] we know that f is an isomorphism, we conclude that η_{N} is such. ✓

4. Strong Concatenable Processes

We end this section by characterizing the replete image of Q[ ] in \underline{TSSMC}^{⊗}.

Proposition 3.20 ( \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., axioms (3) and (4), 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 the component ε\underline{C}: QN [\underline{C}] → \underline{C} of the counit of Q[ ] ⊣ N [ ] is an isomorphism. Let ε be a representative of ε\underline{C}. Clearly, ε\underline{C} is iso if and only if ε is such. Moreover, since ε is an isomorphism on the objects, it is iso if and only if it is an isomorphism on each homset. Then the result follows, since each arrow of \underline{C} can be written as tensor and composition of symmetries and component of transitions if and only if ε is surjective on each homset, and this can be done uniquely (up to the equalities that necessarily hold in any symmetric Petri category) if and only if ε is injective on each homset. ✓

4 Strong 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. Once again most of the work has already been done in the proof of Proposition 3.5 and therefore our task is now easy.

Definition 4.1 (Strong Concatenable Processes) Given a petri net N in \underline{Petri}, a strong 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 strong concatenable processes is an isomorphism of the underlying processes which, in addition, preserves the orderings ℓ and L. As usual, we identify isomorphic strong concatenable processes.

So, a strong concatenable process is a non-sequential process where the minimal and maximal places are linearly ordered. Graphically, we shall represent strong concatenable processes by using the usual representation of nonsequential processes enriched by labelling the minimal and the maximal places with the value of, respectively, ℓ and L. An example is shown in Figure 4.

[figure: \begin{matrix}ā & ā \\ t_{0} & t_{1} \\ b̄_{0} & b̄_{1} \end{matrix}; 1; 2; 2; 1]

Figure 4: A strong concatenable process for the net of Example 2.1

As in the case of concatenable processes, it is easy to define an operation of concatenation of strong concatenable processes. We associate a source and a target in S_{N}^{⊗} to each strong 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 concatenable process (π: Θ → N, ℓ, L): u → w defined as follows (see also Figure 5), where, in order to simplify notations, we assume that S_{Θ_{0}} and S_{Θ_{1}} are disjoint.

• Let A be the set of pairs (x, y) such that x ∈ max(Θ_{0}), y ∈ min(Θ_{1}) and ℓ(y) = L(x). By the definitions of concatenable processes and of their sources and targets, each element of max(Θ_{0}) belongs exactly to one pair of A, and of course the same happens to min(Θ_{1}). Consider S_{0} = S_{Θ_{0}} \max(Θ_{0}) and S_{1} = S_{Θ_{1}} \min(Θ_{1}). Then, let in_{0}: S_{Θ_{0}} → S_{0} ∪A be the function which is the identity on x ∈ S_{0} and maps x ∈ max(Θ_{1}) to the corresponding pair in A. Define in_{1}: S_{Θ_{1}} → S_{1} ∪A analogously. Then,

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

where + denotes the disjoint union of sets and functions, and

– ∂^{0} = in_{0}^{⊕} ∘ ∂_{Θ_{0}}^{0} + in_{1}^{⊕} ∘ ∂_{Θ_{1}}^{0};

– ∂^{1} = in_{0}^{⊕} ∘ ∂_{Θ_{0}}^{1} + in_{1}^{⊕} ∘ ∂_{Θ_{1}}^{1};

• Suppose π_{i} = ⟨f_{i}, g_{i}⟩, for i = 0, 1, and consider the function g(a) = g_{i}(a) if a ∈ S_{i} and g((x, y)) = g_{0}(x) = g_{1}(y) otherwise. Then π = ⟨f_{0} + f_{1}, g⟩.

• ℓ(a) = ℓ_{0}(a) if a ∈ min(Θ_{0}) and ℓ((x, y)) = ℓ_{0}(x) if (x, y) ∈ min(Θ).

• L(a) = L_{1}(a) if a ∈ max(Θ_{1}) and L((x, y)) = L_{1}(y) if (x, y) ∈ max(Θ).

[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 5: An example of the algebra of strong concatenable processes

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

Strong concatenable processes admit a tensor operation ⊗ such that, given SCP_{0} = (π_{0}: Θ_{0} → N, ℓ_{0}, L_{0}): u → v and SCP_{1} = (π_{1}: Θ_{1} → N, ℓ_{1}, L_{1}): u′ → v′, SCP_{0}⊗SCP_{1} is the strong concatenable process (π: Θ → N, ℓ, L): u⊗u′ → v⊗v′ given below (see also Figure 5).

• Θ = (∂_{Θ_{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).

It is easy to verify that ⊗ is a functor ⊗: CQ[N] × CQ[N] → CQ[N]. The strong concatenable processes consisting only of places are analogous in CQ[N] of the permutations of Q[N]. In particular, for any u, v ∈ S^{⊗}, the strong 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 6).

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}^{⊗}}. Moroever, the subcategory of CQ[N] consisting of the processes with only places is the category of symmetries of CQ[N] and is isomorphic to Sym_{N}^{∗}.

Proof. Concerning the first claim, it is enough to verify that CQ[N] satisfies the axioms (6) with respect to ⊗ and the symmetries γ̄(u, v) defined above. The task is really immediate and thus omitted.

Let Sym be the subcategory of the processes consisting only of places of CQ[N]. Since ⊗ restricts to a functor Sym × Sym → Sym, we have that Sym is a symmetric strict monoidal category with symmetry isomorphism {γ̄(u, v)}_{u,v∈S_{N}^{⊗}}. Then, by Proposition 3.5, there exists a functor F from Sym_{N}^{∗} to Sym, corresponding to the identity function on S_{N}^{⊗}, which is the identity on the objects and such that F(γ(u, v)) = γ̄(u, v). Moreover, since for any u, v ∈ S_{N}^{⊗} the strong concatenable processes from u to v in Sym are clearly isomorphic to the permutations p: u → v in Sym_{N}^{∗}, it follows easily that F is full and faithful. Therefore, F is an isomorphism. This means that Sym is generated via composition and tensor product from the symmetries γ̄(u, v) and from the identities, i.e., that Sym is the category of symmetries of CQ[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 6).

We can show the announced correspondence between CQ[N] and Q[N].

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

Proof. First of all observe that CQ[N] satisfies axiom (Φ) of Definition 3.7, the symmetries and the (instances of) transitions being as explained above. In order to prove this claim, let T_{u,v} = (π_{0}: Θ_{0} → N, ℓ_{0}, L_{0}) and T_{u′,v′} = (π_{1}: Θ_{1} → N, ℓ_{1}, L_{1}) be different instances of some transition t, and let S: u → u′ and S′: v → v′ be symmetries of CQ[N]. Moreover, suppose that S^{−1} and S′ correspond, respectively,

[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 6: A transitions t_{u,v}: u → v and the symmetry γ(u, v) in CQ[N]

to the permutations p: u′ → u and q: v → v′ in Q[N]. Then, S^{−1} ; T_{u,v} ; S is (isomorphic to) (π_{0}: Θ_{0} → N, p ∘ ℓ_{0}, q ∘ L_{0}). Consider the function g: S_{Θ_{0}} → S_{Θ_{1}} such that g(x) = ℓ_{1}^{−1}(p(ℓ_{0}(x))) if x ∈ min(Θ_{0}) and g(x) = L_{1}^{−1}(q(L_{0}(x))) if x ∈ max(Θ_{1}). Clearly, by definition of Θ_{0} and Θ_{1}, g is an isomorphism. Moreover, since for each x ∈ min(Θ_{0}) and y ∈ max(Θ_{0}) we have that u_{ℓ_{0}(x)} = u′_{p(ℓ_{0}(x))} and v_{L_{0}(y)} = u′_{q(L_{1}(y))}, it follows that π_{1}(g(x)) = u′_{ℓ_{1}(g(x))} = u′_{p(ℓ_{0}(x))} = u_{ℓ_{0}(x)} = π_{0}(x) and that π_{1}(g(y)) = u′_{L_{1}(g(y))} = u′_{q(L_{0}(y))} = u_{L_{0}(y)} = π_{0}(y). Therefore, we have an isomorphism ⟨f, g^{⊗}⟩: Θ_{0} → Θ_{1}, where g^{⊗}: S_{Θ_{0}}^{⊗} → S_{Θ_{1}}^{⊗} is the free monoidal extension of g and f is the function which maps the unique transition in Θ_{0} to the unique transition in Θ_{1}. Then, S^{−1} ; T_{u,v} ; S′ = T_{u′,v′}, i.e., (Φ) holds.

Thus, since by definition Q[N] is the free symmetric strict monoidal category built on Sym_{N}^{∗} plus the additional arrows in T_{N} and which satisfies axiom (Φ), there is a strict monoidal functor H: Q[N] → CQ[N] which is the identity on the objects and sends the generators, i.e., symmetries and transitions, to the corresponding strong concatenable processes. We want to show that H is an isomorphism. Observe that, by Proposition 4.3, we already know that H is an isomorphism between the corresponding categories of symmetries.

\underline{fullness}. It is completely trivial to see that any strong concatenable process SCP may be obtained as a concatenation SCP_{0} ; …; SCP_{n} of strong concatenable processes SCP_{i} of depth one. Now, each of these SCP_{i} may be split into the concatenation of a symmetry S_{0}^{i}, the tensor of the (processes representing the) transitions which appear in it plus some identities, say u_{i} ⊗ ⨂_{j} T_{j}^{i} and finally another symmetry S_{1}^{i}. The intuition about this factorization is as follows. We take the tensor of the transitions which appear in SCP_{i} in any order and multiply the result by an identity concatenable process in order to get the correct source and target. Then, in general, we need a pre-concatenation and a post-concatenation with a symmetry in order to get the right indexing of minimal and maximal places. Then, we finally have

SCP = S_{0}^{0} ; (u_{1} ⊗ ⨂_{j} T_{j}^{1}) ; (S_{1}^{0} ; S_{0}^{1}) ; …; (S_{1}^{n−1} ; S_{0}^{n}) ; (u_{n} ⊗ ⨂_{j} T_{j}^{n}) ; S_{1}^{n}

which shows that every strong concatenable process is in the image of H.

\underline{faithfulness}. The arrows of Q[N] are equivalence classes, modulo the axioms stated in Definition 3.8, of terms built by applying tensor and sequential composition to the identities id_{u}, the symmetries c_{u,v}, and the transitions t_{u,v}. We have to show that, given two such terms α and β, whenever H(α) = H(β) we have α =_{E} β, where =_{E} is the equivalence induced by the axioms (3), (4) and (Φ).

First of all, observe that if H(α) is a strong process SCP of depth n, then α can be proved equal to a term

α′ = s_{0}; (id_{u_{1}} ⊗ ⨂_{j} τ_{j}^{1}); s_{1}; …; s_{n−1}; (id_{u_{n}} ⊗ ⨂_{j} τ_{j}^{n}); s_{n}

where, for 1 ≤ i ≤ n, τ_{j}^{i} = (t_{j}^{i})_{u_{j}^{i} ,v_{j}^{i}} and the transitions t_{j}^{i}, for 1 ≤ j ≤ n_{i}, are exactly the transitions of SCP at depth i and where s_{0}, …, s_{n} are symmetries. Moreover, we can assume that in the i-th tensor product ⨂_{j} τ_{j}^{i} the transitions are indexed according to a global ordering ≤ of T_{N} assumed for the purpose of this proof, i.e., t_{1}^{i} ≤ ⋯ ≤ t_{n_{i}}^{i}, for 1 ≤ i ≤ n. Let us prove our claim. It is easily shown by induction on the structure of terms that using axioms (3) α can be rewritten as α_{1}; …; α_{h}, where α_{i} = ⨂_{k} ξ_{k}^{i} and ξ_{k}^{i} is either a transition or a symmetry. Now, observe that by functoriality of ⊗, for any α′: u′ → v′, α′′: u′′ → v′′ and s: u → u, we have α′ ⊗ s ⊗ α′′ = (id_{u′} ⊗ s ⊗ id_{u′′}); (α′ ⊗ id_{u} ⊗ α′′), and thus, by repeated applications of (3), we can prove that α is equivalent to s̄_{0}; ᾱ_{1}; s̄_{1} …; s̄_{h−1}; ᾱ_{h}, where s̄_{0}, …, s̄_{h−1} are symmetries and each ᾱ_{i} is a tensor ⨂_{k} ξ̄_{k}^{i} of transitions and identities. The fact that the transitions at depth i can be brought to the i-th tensor product, follows intuitively from the facts that they are “disjointly enabled”, i.e., concurrent to each other, and that they depend causally on some transition at depth i − 1. In particular, the sources of the transitions of depth 1 can be target only of symmetries. Therefore, reasoning formally as above, they can be pushed up to ᾱ_{1} exploiting axioms (3). Then, the same happens for the transitions of depth 2, which can be brought to ᾱ_{2}. Proceeding in this way, eventually we show that α is equivalent to the composition ¯ s̄_{0}; ¯ ᾱ_{1}; ¯ s̄_{1} …; ¯ s̄_{n−1}; ¯ ᾱ_{n}; ¯ s̄_{n} of the symmetries ¯s̄_{0}, …, ¯ s̄_{n} and the products ¯ ᾱ_{i} = ⨂_{k} ¯ ξ̄_{k}^{i} of transitions at depth i and identities.

Finally, the order of the ¯ ξ̄_{k}^{i} can be permuted in the way required by ≤. This is achieved by pre- and post-composing each product by appropriate interchange symmetries. More precisely, let σ be a permutation such that ⨂_{k} ¯ ξ̄_{σ(k)}^{i} coincides

with id_{u_{i}} ⊗ ⨂_{j} τ_{j}^{i}, suppose that ¯ ξ̄_{k}^{i}: u_{k}^{i} → v_{k}^{i}, for 1 ≤ k ≤ k_{i}. Then, by definition of interchange permutation in Sym_{N}^{∗}, we have that

σ(u_{1}^{i}, …, u_{k_{i}}^{i}); (⨂_{k} ¯ ξ̄_{σ(k)}^{i}) = (⨂_{k} ¯ ξ̄_{k}^{i}); σ(v_{1}^{i}, …, v_{k_{i}}^{i}),

and then, since σ(u_{1}^{i}, …, u_{k_{i}}^{i}) is an isomorphism, we have that

(id_{u_{i}} ⊗ ⨂_{j} τ_{j}^{i}) = σ(u_{1}^{i}, …, u_{k_{i}}^{i})^{−1}; (⨂_{k} ¯ ξ̄_{k}^{i}); σ(v_{1}^{i}, …, v_{k_{i}}^{i}).

Now, applying the same argument to β, one proves that it is equivalent to a term β′ = p_{0}; β_{0}; p_{1}; … p_{n−1}; β_{n}; p_{n}, where p_{0}, …, p_{n} are symmetries and β_{i} is the product of (instances of) the transitions at depth i in H(β) and of identities.

Then, since H(α) = H(β), and since the transitions occurring in β_{i} are indexed in a predetermined way, we conclude that β_{i} = (id_{u_{i}} ⊗ ⨂_{j} τ̄_{j}^{i}), where τ̄_{j}^{i} = (t_{j}^{i})_{ū_{j}^{i} ,v̄_{j}^{i}} i.e.,

α′ = s_{0}; (id_{u_{1}} ⊗ ⨂_{j}(t_{j}^{1})_{u_{j}^{1},v_{j}^{1}}); s_{1}; …; s_{n−1}; (id_{u_{n}} ⊗ ⨂_{j}(t_{j}^{n})_{u_{j}^{n},v_{j}^{n}}); s_{n}
β′ = p_{0}; (id_{u_{1}} ⊗ ⨂_{j}(t_{j}^{1})_{ū_{j}^{1},v̄_{j}^{1}}); p_{1}; …; p_{n−1}; (id_{u_{n}} ⊗ ⨂_{j}(t_{j}^{n})_{ū_{j}^{n},v̄_{j}^{n}}); p_{n}. (5)

In other words, the only possible differences between α′ and β′ are the symmetries and the sources and targets of the corresponding instances of transitions. Observe now that the steps which led from α to α′ and from β to β′ have been performed by using the axioms which define Q[N] and since such axioms hold in CQ[N] as well and H preserves them, we have that H(α′) = H(α) = H(β) = H(β′). Thus, we conclude the proof by showing that, if α and β are terms of the form given in (5) which differ only by the intermediate symmetries and if H(α) = H(β), then α and β are equal in Q[N].

We proceed by induction on n. Observe that if n is zero then there is nothing to show: since we know that H is an isomorphism on the symmetries, s_{0} and p_{0}, and thus α and β, must coincide. To provide a correct basis for the induction, we need to prove the thesis also for n = 1.

\underline{depth 1}. In this case, we have

α = s_{0}; (id_{u} ⊗ ⨂_{j}(t_{j})_{u_{j} ,v_{j}}); s_{1}
β = p_{0}; (id_{u} ⊗ ⨂_{j}(t_{j})_{ū_{j} ,v̄_{j}}); p_{1}.

Without loss of generality we may assume that p_{0} and p_{1} are identities. In fact, we can multiply both terms by p_{0}^{−1} on the left and by p_{1}^{−1} on the right and obtain a pair of terms whose images through H still coincide and whose equality implies the equality in Q[N] of the original α and β.

Let (π: Θ → N, ℓ, L) and (π̄: Θ̄ → N, ℓ̄, L̄) be, respectively, the strong concatenable processes H(id_{u} ⊗⨂_{j}(t_{j})_{u_{j} ,v_{j}}) and H(id_{u} ⊗⨂_{j}(t_{j})_{ū_{j} ,v̄_{j}}). Clearly, we can assume that H(s_{0}) and H(s_{1}) are respectively (π_{0}: Θ_{0} → N, ℓ′, ℓ) and (π_{1}: Θ_{1} → N, L, L′), where Θ_{0} is min(Θ), Θ_{1} is max(Θ), π_{0} and π_{1} are the corresponding restrictions of π, and ℓ′ and L′ are the orderings respectively of the minimal and the maximal places of Θ.

Then, we have that H(s_{0}; (id_{u} ⊗ ⨂_{j}(t_{j})_{u_{j} ,v_{j}}); s_{1}) is (π: Θ → N, ℓ′, L′), and by hypothesis there is an isomorphism φ: Θ → Θ̄ such that π̄ ∘ φ = π and which respects all the orderings, i.e., ℓ̄(φ(a)) = ℓ′(a) and L̄(φ(b)) = L′(b), for all a ∈ Θ_{0} and b ∈ Θ_{1}. Let us write id_{u} ⊗ ⨂_{j}(t_{j})_{u_{j} ,v_{j}} as ⨂_{k} ξ_{k} and id_{u} ⊗ ⨂_{j}(t_{j})_{ū_{j} ,v̄_{j}} as ⨂_{k} ξ̄_{k}, where ξ_{k}, respectively ξ̄_{k}, is either a transition (t_{j})_{u_{j} ,v_{j}}, respectively (t_{j})_{ū_{j} ,v̄_{j}}, or the identity of a place in u. Clearly, φ induces a permutation, namely the permutation σ such that ξ̄_{σ(k)} = φ(ξ_{k}). In order for φ to be a morphism of nets, it must map the (places corresponding to the) pre-set, respectively postset, of (t_{j})_{u_{j} ,v_{j}} to (the places corresponding to the) pre-set, respectively post-set, of (t_{σ(j)})_{ū_{σ(j)},v̄_{σ(j)}}. It follows that (π_{1}: Θ_{1} → N, L, L′), which is H(s_{1}), must be a symmetry obtained by post-concatenating the image via H of the interchange symmetry σ(v̄_{1}, …, v̄_{k_{i}}) in CQ[N] with a tensor product ⨂_{j} S_{j}^{1} of symmetries, one for each t occurring in α, where S_{j}^{1}: v_{j} → v̄_{j}, whose role is to reorganize the tokens in the post-sets of each transitions. Reasoning along the same lines, we can conclude that (π_{0}: Θ_{0} → N, ℓ, ℓ′), which is H(s_{0})^{−1}, must be a symmetry obtained by concatenating a tensor product ⨂_{j} S_{j}^{0}, where S_{j}^{0}: u_{j} → ū_{j} is a symmetry, with the image via H of the interchange symmetry σ(ū_{1}, …, ū_{k_{i}}). Then, since H is an isomorphism between Sym_{Q[N]} and Sym_{CQ[N]}, s_{0} and s_{1} must necessarily be, respectively, σ(ū_{1}, …, ū_{k_{i}})^{−1}; (id_{u} ⊗⨂_{j} s_{j}^{0}), and (id_{u} ⊗⨂_{j} s_{j}^{1}); σ(v̄_{1}, …, v̄_{k_{i}}), where s_{j}^{0}: ū_{j} → u_{j} and s_{j}^{1}: v_{j} → v̄_{j} are symmetries.

Then, by distributing the tensor of symmetries on the transitions and using (Φ), we show that α = σ(ū_{1}, …, ū_{k_{i}})^{−1}; (id_{u} ⊗ ⨂_{j} s_{j}^{0}; (t_{j})_{u_{j} ,v_{j}}; s_{j}^{1}); σ(v̄_{1}, …, v̄_{k_{i}}) = σ(ū_{1}, …, ū_{k_{i}})^{−1}; (id_{u} ⊗ ⨂_{j}(t_{j})_{ū_{j} ,v̄_{j}}); σ(v̄_{1}, …, v̄_{k_{i}}), which, by definition of interchange symmetry, is (id_{u} ⊗ ⨂_{j}(t_{j})_{ū_{j} ,v̄_{j}}). Thus, we have α =_{E} β as required.

\underline{Inductive step}. Suppose that n > 1 and let α = α′; α′′ and β = β′; β′′, where

α′ = s_{0}; (id_{u_{1}} ⊗ ⨂_{j} τ_{j}^{1}); s_{1}; …; s_{n−1} and α′′ = (id_{u_{n}} ⊗ ⨂_{j} τ_{j}^{n}); s_{n}
β′ = p_{0}; (id_{u_{1}} ⊗ ⨂_{j} τ̄_{j}^{1}); p_{1}; …; p_{n−1} and β′′ = (id_{u_{n}} ⊗ ⨂_{j} τ̄_{j}^{n}); p_{n}

We show that there exists a symmetry s in Q[N] such that H(α′; s) = H(β′) and H(s^{−1}; α′′) = H(β′′). Then, by the induction hypothesis, we have (α′; s) =_{E} β′ and (s^{−1}; α′′) =_{E} β′′. Therefore, we conclude that (α′; s; s^{−1}; α′′) =_{E} (β′; β′′), i.e., that α = β in Q[N].

Let (π: Θ → N, ℓ, L) be the strong concatenable process H(α) = H(β). Without loss of generality we may assume that the strong processes H(α′) and H(β′) are, respectively, (π: Θ′ → N, ℓ′, L^{α′}) and (π′: Θ′ → N, ℓ′, L^{β′}), where Θ′ is the subnet of depth n − 1 of Θ, ℓ′ is the appropriate restriction of ℓ and finally L^{α′} and L^{β′} are orderings of the places at depth n − 1 of Θ. Consider the symmetry S = (π̄: Θ̄ → N, ℓ̄, L̄) in CQ[N], where

• Θ̄ is the process nets consisting of the maximal places of Θ′;

• π̄: Θ̄ → N is the restriction of π to Θ̄;

• ℓ̄= L^{α′};

• L̄ = L^{β′}.

Then, by definition, we have H(α′); S = H(β′). Let us consider now α′′ and β′′. We can assume that H(α′′) and H(β′′) are, respectively, (π′′: Θ′′ → N, ℓ^{α′′}, L′′) and (π′′: Θ′′ → N, ℓ^{β′′}, L′′), where Θ′′ is the process net obtained by removing from Θ the subnet Θ′, L′′ is the restriction of L to Θ′′, and ℓ^{α′′} and ℓ^{β′′} are orderings of the places at depth n − 1 of Θ. Now, in our hypothesis, it must be L^{α′} = ℓ^{α′′} and L^{β′} = ℓ^{β′′}, which shows directly that S^{−1}; H(α′′) = H(β′′). Then, s = H^{−1}(S) is the required symmetry of Q[N].

Then, since H is full and faithful and is an isomorphism on the objects, it is an isomorphism and the proof is concluded. ✓

Conclusions

In this paper we studied the issue of functoriality for the categorical/algebraic viewpoint of Petri net processes introduced in [6]. We gave a negative result showing that no naive modification of P[N] can be functorial. Then, we introduced the strong concatenable processes as the least modification of concatenable processes which takes such a result into account and we showed that the construction of the strong concatenable processes can be expressed via a functor Q[ ]. This shows that, in a sense, strong concatenable processes are the least extension of concatenable processes which yields functoriality, i.e., the least extension of Goltz-Reisig processes which yields an operation of concatenation and admits a functorial treatment.

In addition, the paper proposed \underline{TSSMC}^{⊗} as an axiomatization of the category of (categories of) net behaviours; the appropriateness of such a category to the purpose has been proved by showing that Q[ ] embeds coreflectively \underline{Petri} in \underline{TSSMC}^{⊗}.

The choice of the category of Petri nets studied in the paper, namely \underline{Petri} exactly as defined in [13] and used in [6], has been suggested by the existence of the open problem of functoriality of the process semantics. It is worth remarking, however, that such a category is rather general, in the precise sense of allowing all the reasonable morphisms, as introduced in [23, 24], which map transitions to transitions. Nevertheless, more general kinds of morphisms, e.g., mapping transitions to computations, have been occasionally proposed in the literature [24, 13]. A question which may be worth investigating in the future concerns the categorical axiomatizations of the behaviour of nets, analogous to the one presented here, when such morphisms are considered.

References

[1] J. Bénabou.

Categories with Multiplication. Comptes Rendue Académie Science Paris, n. 256, pp. 1887–1890, 1963.

[2] E. Best and R. Devillers.

Sequential and Concurrent Behaviour in Petri Net Theory. Theoretical Computer Science, n. 55, pp. 87–136, 1987.

[3] C. Brown and D. Gurr.

A Categorical Linear Framework for Petri Nets. In Proceedings of the 5th LICS Symposium, pp. 208–218, IEEE, 1990.

[4] C. Brown, D. Gurr, and V. de Paiva.

A Linear Specification Language for Petri Nets. Technical Report DAIMI PB-363, Computer Science Department, Aarhus University, 1991.

[5] W. Burnside.

Theory of Groups of Finite Order. Cambridge University Press, 1911.

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

[7] S. Eilenberg, and G.M. Kelly.

Closed Categories. In Proceedings of the Conference on Categorical Algebra, La Jolla, pp. 421–562, Springer, 1966.

[8] S. Eilenberg, and J.C. Moore.

Adjoints Functors and Triples. Illinois Journal of Mathematics, n. 9, pp. 381–398, 1965.

[9] U. Goltz and W. Reisig.

The Non-Sequential Behaviour of Petri Nets. Information and Computation, n. 57, pp. 125–147, 1983.

[10] G.M. Kelly. On MacLane’s Conditions for Coherence of Natural Associativities, Commutativities, etc. Journal of Algebra, n. 1, pp. 397–402, 1964.

[11] S. MacLane. Natural Associativity and Commutativity. Rice University Studies, n. 49, pp. 28–46, 1963.

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

\underline{References}

[13] J. Meseguer and U. Montanari.

Petri Nets are Monoids. Information and Computation, n. 88, pp. 105–154, Academic Press, 1990.

[14] E.H. Moore.

Concerning the abstract group of order k! isomorphic with the symmetric substitution group on k letters. Proceedings of the London Mathematical Society, n. 28, pp. 357–366, 1897.

[15] M. Mukund.

Petri Nets and Step Transition Systems. International Journal of Foundations of Computer Science, n. 3, pp. 443–478, World Scientific, 1992.

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

[17] C.A. Petri.

Kommunikation mit Automaten. PhD thesis, Institut für Instrumentelle Mathematik, Bonn, Germany, 1962.

[18] C.A. Petri.

Concepts of Net Theory. In Proceedings of MFCS ‘73, pp. 137–146, Mathematics Institute of the Slovak Academy of Science, 1973.

[19] C.A. Petri.

Non-Sequential Processes. Interner Bericht ISF–77–5, Gesellschaft für Mathematik und Datenverarbeitung, Bonn, Germany, 1977.

[20] W. Reisig.

Petri Nets. Springer-Verlag, 1985.

[21] V. Sassone.

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

[22] V. Sassone.

Some Remarks on Concatenable Processes. Technical Report TR 6/94, Dipartimento di Informatica, Università di Pisa, April 1994.

[23] G. Winskel.

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

[24] G. Winskel.

Petri Nets, Algebras, Morphisms and Compositionality. Information and Computation, n. 72, pp. 197–238, 1987.

A Monads

A monad [8, 12] on a category \underline{C} is a triple (T, η, μ), where T: \underline{C} → \underline{C} is an endofunctor, η: Id\underline{C} →^{▪} T is a natural transformation, called the unit of the monad, μ: T^{2} →^{▪} T is a natural transformation, called the multiplication of the monad, such that

μ ▪ ηT = 1_{T} = μ ▪ Tη (Unit law);
μ ▪ Tμ = μ ▪ μT  (Associative law).

Monads are strictly related to algebraic constructions. In order to appreciate this fact, one should think of T as being the “free construction”, in the precise sense of associating to each object c ∈ \underline{C} a “free algebra” Tc on c, one should think of η as the injection of c in the “free algebra” on it, and one should think of μ as providing the interpretation for the operations in Tc.

A T-algebra is a pair (c, h), where c ∈ \underline{C} and h: Tc → c is a morphism, called the structure map, such that

h ∘ η_{c} = id_{c}  (Unit);
h ∘ Th = h ∘ μ_{c} (Associativity).

Observe that for any c we have that (Tc, μ_{c}) is an algebra.

A morphism of T-algebras, or T-homomorphism, f: (c, h) → (c′, h′) is an arrow f: c → c′ in \underline{C} such that

h′ ∘ Tf = f ∘ h.

T-algebras and their morphisms define the category \underline{C}^{T}.

The well know fact that homomorphisms of algebras whose source is a free algebra Tc are uniquely identified by their behaviour on c has the following counterpart in the theory of monads: there is a bijection between the T-homomorphisms (Tc, μ_{c}) → (c′, h′) in \underline{C}^{T} and the arrows c → c′ in \underline{C}. Such one-to-one correspondence is expressed by following diagram.

[figure: _{Hom\underline{C}}(c, c′)  _{Hom_{\underline{C}_{T}}} ((Tc, μ_{c}), (c′, h_{c′})); h_{c′} ∘T( ); ∘η_{c}]

In fact, for each arrow f: c → c′ in \underline{C}, it follows from the naturality of η that h_{c′} ∘ Tf ∘ η_{c} = h_{c′} ∘ η_{c′} ∘ f, which, by the unit law of structure maps, is f. On the other hand, given a homomorphism g: (Tc, μ_{c}) → (c′, h_{c′}), we have that h_{c′} ∘T(g∘η_{c}) = g∘μ_{c} ∘Tη_{c} by definition of T-homomorphism, and g∘μ_{c} ∘Tη_{c} = g by the unit law of monads.

B. Symmetric Strict Monoidal Categories

B Symmetric Strict Monoidal Categories

A symmetric strict monoidal category [1, 7, 12] is a category \underline{C} together with a functor ⊗: \underline{C} × \underline{C} → \underline{C}, called the tensor product, and a selected object e ∈ \underline{C}, the unit object, such that ⊗, when viewed as a pair of operations respectively on objects and arrows of \underline{C}, forms two monoids whose units are e and id_{e}, and together with a family of arrows γ_{x,y}: x ⊗ y → y ⊗ x, for x and y objects of \underline{C}, such that, for each f: x → y and g: x′ → y′ in \underline{C},

(id_{y} ⊗ γ_{x,z}) ∘ (γ_{x,y} ⊗ id_{z}) = γ_{x,y⊗z}
(g ⊗ f) ∘ γ_{x,y} = γ_{x′,y′} ∘ (f ⊗ g);  (6)
γ_{y,x} ∘ γ_{x,y} = id_{x⊗y}

Notice that the equations above mean, respectively, that γ satisfies the relevant Kelly-MacLane [11, 10] coherence axiom, that γ = \{γ_{x,y}\}_{x,y∈\underline{C}} is a natural transformation ⊗ →^{▪} ⊗∘Δ, where Δ is the endofunctor on \underline{C}×\underline{C} which “swaps” its arguments, and that γ_{x,y} is an isomorphism with inverse γ_{y,x}. The role of γ is to express the commutativity “up to isomorphism” of the structure by giving explicitly the isomorphism, e.g., between x⊗y and y⊗x. Then, the axioms above guarantee the reasonable requirement that between two given objects there is at most one such structural isomorphism, i.e., they guarantee the coherence of the structural isomorphism γ.

Theorem [11, 10]. Every diagram of natural transformations each arrow of which is obtained by repeatedly applying ⊗ to “instances” of γ and identities, where in turn “instances” means components of the natural transformation at objects of \underline{C} obtained by repeated applications of ⊗ to e and to “variables”, commutes.

A symmetry in a symmetric monoidal category is any arrow obtained as composition and tensor of “instances” of γ and identities. We write Sym\underline{C} to denote the subcategory of a symmetric monoidal category \underline{C} whose objects are those of \underline{C} and whose arrows are the symmetries of \underline{C}.

A symmetric strict monoidal functor from (\underline{C}, ⊗, e, γ) to (\underline{D}, ⊗′, e′, γ′) is a functor F: \underline{C} → \underline{D} such that

F(e) = e′,
F(x ⊗ y) = F(x) ⊗′ F(y),  (7)
F(γ_{x,y}) = γ′_{Fx,Fy}.

These data define the category \underline{SSMC} of symmetric strict monoidal (small) categories and symmetric strict monoidal functors.

Given the symmetric strict monoidal categories \underline{C} and \underline{D} and the symmetric strict monoidal functors F: \underline{C} → \underline{D} and G: \underline{C} → \underline{D}, a monoidal transformation from F to G is a natural transformation σ: F →^{▪} G such that

σ_{e} = id_{e′},
σ_{u⊗v} = σ_{u} ⊗′ σ_{v}.  (8)

Given a (symmetric monoidal) category \underline{C} and a family ℛ of binary relations on the homsets of \underline{C} (in particular a set of equations E on parallel arrows of \underline{C}) the (monoidal) quotient of \underline{C} modulo ℛ, is the category \underline{C}/ℛ, whose objects are those of \underline{C} and whose arrows are the equivalence classes of the arrows of \underline{C} modulo the least equivalence closed with respect to arrow composition (and tensor product) which contains ℛ.

Recent Publications in the BRICS Report Series

RS-94-33 Vladimiro Sassone. Strong Concatenable Processes: An Approach to the Category of Petri Net Computations. October 1994. 40 pp.

RS-94-32 Alexander Aiken, Dexter Kozen, and Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. October 1994. 33 pp.

RS-94-31 Noam Nisan and Amnon Ta-Shma. Symmetric Logspace is Closed Under Complement. September 1994. 8 pp.

RS-94-30 Thore Husfeldt. Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink. September 1994. 26 pp.

RS-94-29 Ronald Cramer and Ivan Damg� ard. Secure Signature Schemes Based on Interactive Protocols. September 1994. 24 pp.

RS-94-28 Oded Goldreich. Probabilistic Proof Systems. September 1994. 19 pp.

RS-94-27 Torben Bra� uner. A Model of Intuitionistic Af�ne Logic from Stable Domain Theory (Revised and Expanded Version). September 1994. 19 pp. Full version of paper appearing in: ICALP ’94, LNCS 820, 1994.

RS-94-26 S�ren Riis. Count(q) versus the Pigeon-Hole Principle. August 1994. 3 pp.

RS-94-25 S�ren Riis. Bootstrapping the Primitive Recursive Functions by 47 Colors. August 1994. 5 pp.

RS-94-24 S�ren Riis. A Fractal which violates the Axiom of Determinacy. August 1994. 3 pp.

RS-94-23 S�ren Riis. Finitisation in Bounded Arithmetic. August 1994. 31 pp.

RS-94-22 Torben Bra� uner. A General Adequacy Result for a Linear Functional Language. August 1994. 39 pp. Presented at MFPS ’94.