International Journal of Foundations of Computer Science 3, 4, (1992) 443-478.

PETRI NETS AND STEP TRANSITION SYSTEMS

MADHAVAN MUKUND School of Mathematics, SPIC Science Foundation 92, G. N. Chetty Road, T. Nagar Madras 600 017, INDIA

                             Email: madhavan@ssf.ernet.in

ABSTRACT Labelled transition systems are a simple yet powerful formalism for describing the operational behaviour of computing systems. They can be extended to model concurrency faithfully by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step.

Petri nets (or Place/Transition nets) give rise to such step transition systems in a natural way—the marking diagram of a Petri net is the canonical transition system associated with it. In this paper, we characterize the class of PN-transition systems, which are precisely those step transition systems generated by Petri nets.

We express the correspondence between PN-transition systems and Petri nets in terms of an adjunction between a category of PN-transition systems and a category of Petri nets in which the associated morphisms are behaviour-preserving in a strong and natural sense.

Keywords: Petri nets, models for concurrency, category theory

1. Introduction

Transition systems are an appealingly simple yet powerful formalism for describing the operational behaviour of models of concurrency. They provide a common framework for investigating the relationships between different models of distributed systems.

Nielsen, Rozenberg and Thiagarajan [14] have established a close correspondence between a class of transition systems called elementary transition systems and a basic model of net theory called elementary net systems. They describe this correspondence in terms of a coreflection between a category of elementary transition systems and a category of elementary net systems.

Here, we extend the results of [14] to a much richer model of net theory called Petri nets (also known as Place/Transition nets). Petri nets give rise to transition systems in a natural way—the reachability graph of a Petri net defines a canonical transition system associated with it. In this paper, we characterize a subclass of transition systems called PN-transition systems, which are precisely those transition systems generated by (unlabelled) Petri nets.

The results of [14] are established within the framework of conventional sequential transition systems, where the transitions are labelled by single events. Because of the relatively uncomplicated structure of elementary net systems, information about concurrency can be recovered from the sequential transition relation of an elementary transition system by checking local “diamond” properties.

However, when we move over to Petri nets, we need to introduce explicit information about concurrency into our transition systems. For instance, consider the two nets in Figure 1. Both give rise to the same sequential transition system, shown on the right. However, in the first net a and b can occur concurrently, while in the second net a and b can occur only sequentially (though in any order).

Thus, to represent concurrency faithfully, we shall enrich the transition relation by permitting one state to be transformed to another in a single step consisting of a finite multiset of actions. (We have to permit multisets and not just sets because of autoconcurrency.)

We call this new class of transition systems step transition systems. PNtransition systems are defined as a subclass of step transition systems which satisfy certain restrictions that ensure that the steps are “consistent”.

As in [14], we describe the connection between Petri nets and PN-transition systems using the language of category theory. We first define a category PNts whose objects are PN-transition systems and whose arrows are standard transition system morphisms, extended to respect steps. We then construct a category PNet of Petri nets. The morphisms we define between nets are a smooth generalization of the morphisms defined between elementary net systems in [14]. These morphisms are strengthened versions of the morphisms defined by Winskel [18]. They preserve the dynamic behaviour of nets in a strong way.

There is a natural functor NT : PNet → PNts which maps each Petri net to the transition system associated with its marking diagram. Our main result is the construction of a functor TN : PNts → PNet which is left adjoint to NT. In fact, the unit of the adjunction is a natural isomorphism, so we actually have a coreflection between this pair of functors.

To construct a Petri net corresponding to a PN-transition system, we have to construct places which appropriately constrain the behaviour of the net. To do this, we generalize the notion of a region.

Regions are used by Nielsen, Rozenberg and Thiagarajan in [14] to define the conditions of an elementary net system corresponding to a given elementary transition system. Their notion can be generalized in several ways to characterize classes

[figure: •; •; a; b; •; •; •; a; b; ◯; ◯; ◯; ◯; b; b; a; a] Figure 1:

of transition systems corresponding to different models of concurrency. For instance, Winskel and Nielsen [20] use a version of regions to establish a coreflection between a special class of asynchronous transition systems [1, 17] and 1-safe Petri nets. On a slightly different track, Hoogers, Kleijn and Thiagarajan [5] use regions to obtain a language-theoretic characterization of the non-sequential behaviour of Petri nets in terms of a generalized version of Mazurkiewicz trace languages. We shall discuss the relationship between our regions and these other notions in the concluding section.

The paper is organized as follows. We begin with the definition of step transition systems, followed by a brief introduction to Petri nets. In Section 4, we describe the class of PN-transition systems and construct the category PNts in Section 5. Next, we show how to define a category PNet of Petri nets. In Section 7, we construct the functor NT : PNet → PNts which serves as the right adjoint of the adjunction described in Section 8. In section 9, we discuss the existence of universal constructions such as products and coproducts in the categories PNts and PNet. In the concluding section, we tie up some loose ends and discuss possible extensions of our work. We also compare our categories PNts and PNet with related formalisms described in the literature.

2. Step Transition Systems

A transition system is usually defined as a quadruple T S = (Q, Σ, →, q_{in}), where Q is a set of states and → ⊆ Q × Σ × Q is a (sequential) transition relation which describes how the system evolves from state to state by performing actions from Σ, beginning with the initial state q_{in}.

We enrich the transition relation by permitting one state to be transformed to another in a single step consisting of a finite multiset of actions. Later, we shall define the class of PN-transition systems as a subclass of this new class of transition systems which satisfies some simple axioms ensuring that all the steps in the system are “consistent”.

We first fix some terminology and notation regarding multisets.

Definition 1. Let A be a set.

• A multiset u over A is a function u : A → N_{0}, where N_{0} is the set of natural numbers {0, 1, 2, …}. The set of all multisets over A is denoted by MS(A).

• For u ∈ MS(A), let |u|, the size of u, be given by ∑_{a∈A} u(a). u is finite iff |u| is finite. The set of all finite multisets over A is denoted by MS_{fin}(A).

• The empty multiset over A is the unique function O_{A} : A → N_{0} such that ∀a ∈ A. O_{A}(a) = 0. If A is clear from the context, we shall often use just O to mean O_{A}.

• Let u, v ∈ MS(A). Then u is a submultiset of v, written u ⊆_{MS} v, in case ∀a ∈ A. u(a) ≤ v(a).

Thus, if u is a multiset over A, for each a ∈ A, u(a) is the number of occurrences of a in u. Abusing notation, we shall write a ∈ u to signify that u(a) ≥ 1. For simplicity, we shall usually write out multisets as sets with multiplicities—for instance, if a, b ∈ A, then {a, a, b} denotes the multiset u over A which assigns u(a) = 2, u(b) = 1 and u(c) = 0 for all c ∈ A such that c ≠ a and c ≠ b.

Multisets can be added and subtracted pointwise — if u and v are two multisets over A, then u + v and u − v are defined as follows:

∀a ∈ A. (u + v)(a) = u(a) + v(a).

If v ⊆_{MS} u then ∀a ∈ A. (u − v)(a) = u(a) − v(a).

Given a partial function f : A ⇀ B between sets, f can be extended in a natural way to a (total) function f̂: MS_{fin}(A) → MS_{fin}(B) as follows:

∀u ∈ MS_{fin}(A). ∀b ∈ B. f̂(u)(b) = ∑_{{a∈A|f(a)=b}} u(a).

By convention, f̂(u) = O_{B} in case f(a) is undefined for all a ∈ u.

For convenience, we shall denote both f and its extension f̂ to multisets by f.

Definition 2. A step transition system is a structure T S = (Q, E, →, q_{in}), where

• Q is a countable set of states, with q_{in} ∈ Q as the initial state.

• E is a countable set of events.

• → ⊆ Q × MS_{fin}(E) × Q is the transition relation.

We shall often write q →^{u} q′ instead of (q, u, q′) ∈ →. We also write q →^{u} to denote that u is enabled at q—i.e. ∃q′ ∈ Q. (q, u, q′) ∈ →.

We can extend → to a relation →^{∗} over step sequences in the usual way. Let ρ = u_{1}u_{2} … u_{n} ∈ (MS_{fin}(E))^{∗} be a sequence of steps. Then (q, ρ, q′) ∈ →^{∗} iff

∃q_{0}, q_{1}, …, q_{n}. q_{0} = q, q_{n} = q′ and q_{i−1} →^{u_{i}} q_{i} for 1 ≤ i ≤ n.

We put two basic restrictions on transition systems. We first introduce idling transitions, represented by the empty multiset, as self loops at each state and demand that these special transitions occur only as self loops. We also ensure that all states in a transition system are reachable from the initial state. Formally, we have the following basic axioms.

(A1) ∀q, q′ ∈ Q. q \underrightarrow{O_{E}} q′ iff q = q′.

(A2) ∀q ∈ Q. ∃ρ ∈ (MS_{fin}(E))^{∗}. (q_{in}, ρ, q) ∈ →^{∗}.

Henceforth, we shall assume that every step transition system we consider satisfies axioms (A1) and (A2).

Notice that (A1) does not rule out the presence of non-trivial self-loops of the

form q →^{u} q.

Axioms (A1) and (A2) are fairly weak. In particular, we have not introduced any “step axioms” to ensure that the multisets which label the transitions actually represent concurrent steps. Later, when we introduce additional axioms for PNtransition systems, we shall see how the steps are constrained.

[figure: ◯; ◯; ◯; ◯; b; a; a; {a, a}]

Figure 2: A step transition system

Figure 2 is an example of a step transition system. As usual we graphically represent a transition system by a directed graph whose nodes are the states and whose arrows, labelled by multisets over E, denote the relation →. The initial state is marked out specially. The trivial self-loops at each state are not explicitly drawn, to avoid cluttering up the picture.

Before introducing the characteristic axioms for PN-transition systems, let us take a look at Petri nets.

3. Petri Nets

We give a brief introduction to Place/Transition nets, which are often simply called Petri nets. A more detailed discussion of this class of nets can be found in [16].

Definition 3. A Petri net is a quadruple PN = (S, T, W, M_{in}), where:

• S is set of places, T is a set of transitions and S ∩ T = ∅. T is assumed to be countable.

• W : (S × T) ∪ (T × S) → N_{0} is the weight function.

• M_{in} : S → N_{0} is the initial marking.

For t ∈ T, let ^{•}t = {s ∈ S | W (s, t) > 0} and t^{•} = {s ∈ S | W (t, s) > 0}. Similarly, for s ∈ S, let ^{•}s = {t ∈ T | W (t, s) > 0} and s^{•} = {t ∈ T | W (s, t) > 0}.

Figure 3 is an example of a Petri net. We follow the usual graphical notation for nets—places are denoted by circles, transitions are denoted by boxes. An arrow is drawn from a place s to a transition t (from t to s) iff W (s, t) > 0 (W (t, s) > 0) and is labelled by the value of W (s, t) (W (t, s)). By convention, an arrow without a label corresponds to the case where W (s, t) = 1 (W (t, s) = 1). The initial marking is denoted by drawing dots in the places. Thus if M_{in}(s) = n, we draw n dots (or tokens) in the circle corresponding to s.

The places of a Petri net intuitively correspond to local states of the system. A global state, called a marking, is a multiset M : S → N_{0}. If M(s) = n, then s is said to be assigned n tokens by M.

A transition t can occur at a marking M if for all s ∈ S, M(s) ≥ W (s, t). We say that t is enabled at M and denote this by M[t⟩.

[figure: •; •; a; b; 2]

Figure 3: A Petri net

When a transition t occurs at a marking M, a new marking M′ is generated according to the following rule:

∀s ∈ S. M′(s) = M(s) − W (s, t) + W (t, s).

We denote the fact that M evolves to M′ via t by M[t⟩M′.

Suppose t_{1} and t_{2} are two transitions and M is a marking such that ∀s ∈ S. M(s) ≥ W (s, t_{1}) + W (s, t_{2}). Then t_{1} and t_{2} can both occur independently at M and are thus concurrently enabled. In such a situation, M can evolve in a single step by the occurrence of both t_{1} and t_{2} to a marking M′ where

∀s ∈ S. M′(s) = M(s) − W (s, t_{1}) − W (s, t_{2}) + W (t_{1}, s) + W (t_{2}, s).

We can thus extend the transition relation associated with a Petri net to permit steps of actions between a pair of markings. In general, such a step will be a multiset over T rather than a subset of T because a transition may be concurrent with itself (a phenomenon called autoconcurrency). For instance, in Figure 3, two copies of the transition a are enabled at the initial marking.

Let u ∈ MS_{fin}(T). u is enabled at a marking M, denoted M[u⟩, if for all s ∈ S, M(s) ≥ ∑_{t∈T} u(t) · W (s, t). (Recall that u(t) denotes the number of occurrences of t in u). When u occurs, M is transformed to M′ (denoted M[u⟩M′) where

∀s ∈ S. M′(s) = M(s) + ∑_{t∈T} u(t) · (W (t, s) − W (s, t)).

The set of all markings reachable from a marking M is denoted by [M⟩. [M⟩ is the smallest set of markings such that:

• M ∈ [M⟩.

• If M′ ∈ [M⟩ and ∃u ∈ MS_{fin}(T). M′[u⟩M′′ then M′′ ∈ [M⟩.

Notice that if M′ ∈ [M⟩, we can always find a step sequence leading from M to M′ where each step in the sequence is a singleton step—i.e. the multiset of transitions constituting each step is actually a singleton set.

Given a Petri net PN = (S, T, W, M_{in}), we can associate a transition relation ⇒_{P N} ⊆ [M_{in}⟩ × MS_{fin}(T) × [M_{in}⟩ with P N as follows.

⇒_{P N} = {(M, u, M′) | M ∈ [M_{in}⟩ and M[u⟩M′}.

Just as we extended → to →^{∗} for transition systems, we extend ⇒_{P N} to a relation ⇒_{P N}^{∗} over step sequences. Let ρ = u_{1}u_{2} … u_{n} ∈ (MS_{fin}(T))^{∗} be a sequence of steps. Then (M, ρ, M′) ∈ ⇒_{P N}^{∗} iff M ∈ [M_{in}⟩ and ∃M_{0}, M_{1}, …, M_{n}. M_{0} = M, M_{n} = M′ and M_{i−1}[u_{i}⟩M_{i} for 1 ≤ i ≤ n.

Thus, given a Petri net PN = (S, T, W, M_{in}), we can associate a step transition system T S_{P N} = ([M_{in}⟩, T, ⇒_{P N}, M_{in}) which describes the operational behaviour of the net P N. For example, it is easy to see that the transition system of Figure 2 is the step transition system associated with the Petri net of Figure 3. It is straightforward to verify that for any Petri net PN = (S, T, W, M_{in}), T S_{P N} satisfies the two axioms we have introduced for step transition systems in the previous section.

The main aim of this paper is to characterize those step transition systems which arise out of describing the behaviour of Petri nets. As mentioned in the introduction, this characterization will be described using the language of category theory in terms of an adjunction between the category of Petri nets and the category of a subclass of step transition systems called PN-transition systems.

Before constructing these two categories, we must first define PN-transition systems.

4. PN-transition systems

To describe PN-transition systems, we need to introduce the notion of a region. Regions have originally been defined in the context of sequential transition systems by Ehrenfeucht and Rozenberg [4] as a transition system counterpart of the notion of a condition in an elementary net system. Using regions, they characterize the class of elementary transition systems which represent the behaviour of elementary net systems. This characterization is extended to a coreflection between elementary transition systems and elementary net systems in [14].

Here we generalize regions to capture the notion of a place of a Petri net.

Definition 4. Let T S = (Q, E, →, q_{in}) be a step transition system. A region is a pair of functions r = (r_{Q}, r_{E}) such that:

(i) r_{Q} : Q → N_{0}.

(ii) r_{E} : E → N_{0} × N_{0}.

For convenience, we denote the first component of r_{E}(e) as ^{r}e and the second component of r_{E}(e) as e^{r}. In other words, if r_{E}(e) = (n_{1}, n_{2}), then ^{r}e = n_{1} and e^{r} = n_{2}.

(iii) ∀(q, u, q′) ∈ → . \begin{matrix}r_{Q}(q) ≥ ∑_{e∈E} u(e) ·^{r}e and \\ r_{Q}(q′) = r_{Q}(q) + ∑_{e∈E} u(e) · (e^{r} −^{r}e). \end{matrix}

We shall denote both r_{Q} and r_{E} by r, unless it is unclear from the context which component we are referring to. Thus, normally we shall write r(q) for r_{Q}(q) and r(e) for r_{E}(e),

So, a region r corresponds to a place of the Petri net which we would like to associate with a given step transition system. Recall that for a Petri net P N, the associated transition system T S_{P N} has as its states the reachable markings of P N and as its events the transitions of P N. We specify the number of tokens on the “place” r at the “marking” q by r(q). For each e ∈ E, r(e) specifies the “weights” W (r, e) and W (e, r). The last condition in the definition of a region ensures that r_{Q} is consistent with the overall behaviour of the net—for every transition q →^{u} q′ present in the system, r(q) must have enough “tokens” to permit u to occur and r(q′) must contain the correct number of “tokens” as specified by the normal firing rule of a Petri net.

We disregard regions r which are “disconnected” from all the events—i.e. r such that r(e) = (0, 0) for all e ∈ E. These trivial regions correspond to isolated places in a Petri net and do not contribute in any way to characterizing the behaviour of the system.

Definition 5. Let T S = (Q, E, →, q_{in}) be a step transition system. A region r is non-trivial iff for some e ∈ E, r(e) ≠ (0, 0). We denote the set of non-trivial regions of T S by R_{T S}.

Henceforth, whenever we make a statement referring to all regions, we assume that we are only considering non-trivial regions (unless explicitly stated otherwise).

PN-transition systems are characterized by two “regional” axioms in addition to the basic axioms (A1) and (A2):

(A3) Let q, q′ ∈ Q. If ∀r ∈ R_{T S}. r(q) = r(q′) then q = q′. (Separation)

(A4) ∀q ∈ Q. ∀u ∈ MS_{fin}(E).

If ∀r ∈ R_{T S}. r(q) ≥ ∑_{e∈E} u(e) ·^{r}e then ∃q′ ∈ Q. q →^{u} q′. (Forward closure)

Axiom (A3) says that any pair of distinct states in Q will be distinguished by at least one (non-trivial) region. Axiom (A4) captures the fundamental idea underlying the dynamic behaviour of a Petri net. It says that whenever a multiset of actions u is enabled at a state q of the system by all regions, it must be possible to perform u and reach some state q′ in the system. In other words, if the system cannot perform a step labelled by u at the state q then there must be some region r which does not have enough “tokens” at q to permit u to occur.

Definition 6. A PN-transition system is a step transition system T S = (Q, E, →, q_{in}) which satisfies axioms (A1) to (A4).

Figure 4 shows two step transition systems that are not PN-transition systems. The transition system on the left violates (A3)—it is easy to see that for any region r,

r(q_{2}) = r(q_{in}) −^{r}a + a^{r} −^{r}b + b^{r} = r(q′_{2}),

[figure: ◯; ◯; ◯; ◯; ◯; q_{in}; q_{1}; q′_{1}; q_{2}; q′_{2}; a; b; b; a; ◯; ◯; ◯; q_{in}; q_{1}; q_{2}; a; b; {a, b}]

Figure 4: Step transition systems which are not PN-transition systems

and so q_{2} really denotes the same state as q′_{2} from a “regional” point of view.

The transition system on the right violates (A4). At q_{in}, the step {a, b} is enabled. This means that every region must also allow the step consisting of just {b} at q_{in}, but there is no transition corresponding to this step present in →.

A crucial observation about PN-transition systems is that they are deterministic. T S = (Q, E, →, q_{in}) is said to be a deterministic step transition system in case the following is true:

∀q ∈ Q. ∀u ∈ MS_{fin}(E). (q, u, q′) ∈ → and (q, u, q′′) ∈ → implies q′ = q′′.

Proposition 7. Every PN-transition system is deterministic.

Proof. Let T S = (Q, E, →, q_{in}) be a PN-transition system. Suppose that there exists q ∈ Q and u ∈ MS_{fin}(E) such that q →^{u} q′ and q →^{u} q′′. Then, for every region r, we know that

r(q′) = r(q) + ∑_{e∈E} u(e)(e^{r} −^{r}e) = r(q′′).

Thus, by axiom (A3), q′ = q′′. □

As we had mentioned earlier, we have to ensure that the steps in a step transition system actually represent concurrent actions. For instance, Lodaya, Ramanujam and Thiagarajan [7] define distributed transition systems, which are basically step transition systems with a “step axiom” which insists that for every step, all substeps must be present and combine together in a consistent way.

For PN-transition systems, the required step axiom is a straightforward consequence of (A3) and (A4).

Proposition 8. Let T S = (Q, E, →, q_{in}) be a PN-transition system and let (q, u, q′) ∈ →. Then, for every v ⊆_{MS} u, there exists q′′ ∈ Q such that (q, v, q′′) ∈ → and (q′′, u − v, q′) ∈ →.

Proof. From (A4) it follows that if a step u is permitted by all regions, so is every substep v of u. So we know that ∃q′′. q →^{v} q′′. It is easy to compute that u − v must still be enabled at q′′, so there exists a q′′′ such that q′′ ⟶^{u−v} q′′′. So, all we have to show is that q′′′ is the same as q′.

Consider any region r. We know that

r(q′′′) = r(q′′) + ∑_{e∈E}(u − v)(e)(e^{r} −^{r}e),

and that

r(q′′) = r(q) + ∑_{e∈E} v(e)(e^{r} −^{r}e).

From this it follows that

r(q′′′) = r(q) + ∑_{e∈E} v(e)(e^{r} −^{r}e) + ∑_{e∈E}(u − v)(e)(e^{r} −^{r}e),

and therefore

r(q′′′) = r(q) + ∑_{e∈E} u(e)(e^{r} −^{r}e) = r(q′).

Since q′′′ and q′ agree on all regions, it follows from (A3) that q′′′ = q′ and we are done. □

The step axiom formulated in [7] is actually much more subtle than the one described by Proposition 8 because distributed transition systems are, in general, non-deterministic. In the presence of determinacy, however, their step axiom reduces to the simple condition stated in Proposition 8.

5. PNts—A Category of PN-transition Systems

To construct a category of PN-transition systems, we now define morphisms between PN-transition systems. These morphisms are essentially the G-morphisms of [14]. They capture a notion of simulation which preserves concurrency.

Definition 9. Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems. A transition system morphism f from T S_{1} to T S_{2} is a pair of functions f = (f_{Q}, f_{E}) where:

(i) f_{Q} : Q_{1} → Q_{2} is a total function such that f_{Q}(q_{in}^{1}) = q_{in}^{2}.

(ii) f_{E} : E_{1} ⇀ E_{2} is a partial function.

(iii) If (q, u, q′) ∈ →_{1} then (f_{Q}(q), f_{E}(u), f_{Q}(q′)) ∈ →_{2}.

As with regions, we shall denote both f_{Q} and f_{E} by f, unless it is unclear from the context which component we are referring to. Thus, normally we shall write f(q) for f_{Q}(q) and f(e) for f_{E}(e).

Notice that the last clause ensures that if a step u is hidden by f then every transition (q, u, q′) ∈ →_{1} results in q and q′ being mapped to the same state in Q_{2}; i.e. if for all e ∈ u, f(e) is undefined, then (q, u, q′) ∈ →_{1} implies (f(q), O_{E_{2}}, f(q′)) ∈ →_{2}, which by axiom (A1) forces f(q) = f(q′).

Figure 5 shows two examples of transition system morphisms. It is important to notice that clause (iii) in Definition 9 describes a simulation requirement for all

[figure: ◯; ◯; ◯; q_{in}; q_{1}; q_{2}; a; b; ◯; ◯; q′_{in}; q′_{1}; a′; ◯; ◯; ◯; ◯; q_{0}; q_{1}; q_{2}; q_{3}; a; b; b; a; ◯; ◯; ◯; ◯; q′_{0}; q′_{1}; q′_{2}; q′_{3}; a′; b′; b′; a′; {a′, b′}]

Figure 5: Some examples of transition system morphisms

multisets between pairs of states mapped by the morphism. Thus, for the last pair of systems shown in Figure 5, there can be no morphism going in the opposite direction that is defined for both a′ and b′ because there is no matching step in the

first system corresponding to the step q′_{0} ⟶^{{a′,b′}} q′_{3} in the second system.

Given a PN-transition system T S = (Q, E, →, q_{in}), let 1_{T S} = (id_{Q}, id_{E}) denote the identity morphism where id_{Q} : Q → Q and id_{E} : E → E are the (total) identity functions. Let f^{1} = (f_{Q}^{1}, f_{E}^{1}) : T S_{1} → T S_{2} and f^{2} = (f_{Q}^{2}, f_{E}^{2}) : T S_{2} → T S_{3} be two transition system morphisms. The composition f^{2} ∘ f^{1} : T S_{1} → T S_{3} is defined as the pair (f_{Q}^{2} ∘ f_{Q}^{1}, f_{E}^{2} ∘ f_{E}^{1}) (where the composition on the first component is normal functional composition and composition on the second component is the obvious composition operation on partial functions).

It is easy to see that PN-transition systems with transition system morphisms form a category. Let us call this category PNts.

The rest of the section is devoted to establishing some results concerning transition system morphisms.

Our first observation is that these morphisms preserve regions in the reverse direction.

Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems, f : T S_{1} → T S_{2} be a morphism and r be a region in T S_{2}. Define r^{−1} as follows:

∀q ∈ Q_{1}. r^{−1}(q) = r(f(q)) and

∀e ∈ E_{1}. r^{−1}(e) = \{ \begin{matrix}r(f(e)) & if f(e) is defined \\ (0, 0) & otherwise \end{matrix}

Proposition 10. Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems, f : T S_{1} → T S_{2} a morphism and r ∈ R_{T S_{2}}. Then r^{−1} is a (possibly trivial) region in T S_{1}.

Proof. We only have to check that:

∀(q, u, q′) ∈ →_{1} . \begin{matrix}r^{−1}(q) ≥ ∑_{e_{1}∈E_{1}} u(e_{1}) ·^{r^{−1}}e_{1} \\ and \\ r^{−1}(q′) = r^{−1}(q) + ∑_{e_{1}∈E_{1}} u(e_{1}) · (e_{1}^{r^{−1}} −^{r^{−1}}e_{1}) \end{matrix}

Let E′_{1} ⊆ E_{1} be the set of events over which f has a defined value. We know by definition that r^{−1}(e) = (0, 0) for e ∈ (E_{1} \ E′_{1}), so what we actually have to check is that:

∀(q, u, q′) ∈ →_{1} . \begin{matrix}r^{−1}(q) ≥ ∑_{e′_{1}∈E′_{1}} u(e′_{1}) ·^{r^{−1}}e′_{1} \\ and \\ r^{−1}(q′) = r^{−1}(q) + ∑_{e′_{1}∈E′_{1}} u(e) · (e′_{1}^{r^{−1}} −^{r^{−1}}e′_{1}) \end{matrix}

Rewriting r^{−1} in terms of r we must show that:

∀(q, u, q′) ∈ →_{1} . \begin{matrix}r(f(q)) ≥ ∑_{e′_{1}∈E′_{1}} u(e′_{1}) ·^{r}f(e′_{1}) \\ and \\ r(f(q′)) = r(f(q)) + ∑_{e′_{1}∈E′_{1}} u(e′_{1}) · (f(e′_{1})^{r} −^{r}f(e′_{1})) \end{matrix}

Since f is a morphism, (q, u, q′) ∈ →_{1} implies that (f(q), f(u), f(q′)) ∈ →_{2}. r is a region in T S_{2}, so we know that the following holds:

∀(q, u, q′) ∈ →_{1} . \begin{matrix}r(f(q)) ≥ ∑_{e_{2}∈E_{2}}f(u)(e_{2}) ·^{r}e_{2} \\ and \\ r(f(q′)) = r(f(q)) + ∑_{e_{2}∈E_{2}}f(u)(e_{2}) · (e_{2}^{r} −^{r}e_{2}) \end{matrix}

Since f(u)(e_{2}) = ∑_{{e′_{1}∈E′_{1}|f(e′_{1})=e_{2}}} u(e′_{1}) for every e_{2} ∈ E_{2}, it is straightforward to

verify that the result follows.

□

Notice that r^{−1} will be trivial in case r(e_{2}) = (0, 0) for every e_{2} in the range of f. Otherwise r^{−1} ∈ R_{T S_{1}}.

Our next observation about transition system morphisms exploits determinacy. For PN-transition systems, it turns out that morphisms are completely characterized by the way they map events.

Lemma 11. Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems and let f^{1} and f^{2} be two morphisms from T S_{1} to T S_{2}. If f_{E}^{1} = f_{E}^{2} then f^{1} = f^{2}.

Proof. We have to show that f^{1}(q) = f^{2}(q) for every q ∈ Q_{1}. We know that q is reachable by a finite step sequence from q_{in}^{1}. Let ρ = u_{1}u_{2} … u_{k} be a sequence of steps such that q_{in}^{1} →^{ρ}_{1}^{∗} q. We proceed by induction on k = |ρ| (where by |ρ| we mean the number of steps in the sequence ρ).

k = 0: Then q = q_{in}^{1} and so f^{1}(q) = q_{in}^{2} = f^{2}(q).

k > 0: Then we can write ρ as ρ′u_{k} where |ρ′| = k−1. We thus have q_{in}^{1} →^{ρ′}_{1}^{∗} q_{1} →^{u_{k}}_{1} q. By the induction hypothesis, we know that f^{1}(q_{1}) = f^{2}(q_{1}).

By the definition of a morphism, we must have (f^{1}(q_{1}), f^{1}(u_{k}), f^{1}(q)) ∈ →_{2} and (f^{2}(q_{1}), f^{2}(u_{k}), f^{2}(q)) ∈ →_{2}. Since f_{E}^{1} = f_{E}^{2}, we have f^{1}(u_{k}) = f^{2}(u_{k}). We already know that f^{1}(q_{1}) = f^{2}(q_{1}). Since T S_{2} is a PN-transition system, it must be deterministic. So it follows that f^{1}(q) = f^{2}(q) and we are done. □

6. PNet—A Category of Petri Nets

Next, we construct a category of Petri nets. To do so, we have to define a suitable notion of morphism.

Definition 12. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets. A net morphism from P N_{1} to P N_{2} is a pair ϕ = (ϕ_{S}, ϕ_{T}) where:

(i) ϕ_{S} : S_{2} ⇀ S_{1} is a partial function. (Notice that ϕ_{S} is a map from S_{2} to S_{1} and not from S_{1} to S_{2}. Thus, in the “forward” direction, ϕ_{S}^{−1} ⊆ S_{1} × S_{2} is a relation. For X ⊆ S_{1}, ϕ_{S}^{−1}(X) denotes the set {y ∈ S_{2} | ϕ_{S}(y) ∈ X}.)

(ii) ϕ_{T} : T_{1} ⇀ T_{2} is a partial function.

(iii) ∀s_{1} ∈ S_{1}. ∀s_{2} ∈ S_{2}. If s_{1} = ϕ_{S}(s_{2}) then M_{in}^{1}(s_{1}) = M_{in}^{2}(s_{2}).

(iv) ∀t_{1} ∈ T_{1}. If ϕ_{T} (t_{1}) is undefined then ϕ_{S}^{−1}(^{•}t_{1}) = ϕ_{S}^{−1}(t_{1}^{•}) = ∅.

(v) ∀t_{1} ∈ T_{1}. If ϕ_{T} (t_{1}) = t_{2} then:

– ϕ_{S}^{−1}(^{•}t_{1}) = ^{•}t_{2} and ϕ_{S}^{−1}(t_{1}^{•}) = t_{2}^{•}.

– ∀s ∈ ^{•}t_{2}. W_{1}(ϕ_{S}(s), t_{1}) = W_{2}(s, t_{2}).

– ∀s ∈ t_{2}^{•}. W_{1}(t_{1}, ϕ_{S}(s)) = W_{2}(t_{2}, s).

Following [2], we have directly defined the map on places as a partial function in the reverse direction, rather than as a relation in the forward direction whose inverse is a partial function (as in [14]).

[figure: •; •; •; s_{1}; s_{3}; s_{2}; t_{1}; t_{2}; •; •; s′_{1}; s′_{2}; t′_{1}; t′_{2}; •; •; •; s_{1}; s_{5}; s_{3}; s_{2}; s_{4}; t_{1}; t_{2}; •; •; s′_{1}; s′_{3}; s′_{2}; s′_{4}; t′_{1}; t′_{2}]

Figure 6: Some examples of net morphisms

As with transition system morphisms, we shall denote both ϕ_{S} and ϕ_{T} by ϕ, unless it is unclear from the context which component we are referring to. Thus, normally we shall write ϕ(s) for ϕ_{S}(s) and ϕ(t) for ϕ_{T} (t).

Figure 6 shows two examples of net morphisms. Notice that in the first example, if we omit the place s_{1} we can no longer construct a morphism mapping t_{1} to t′_{1}, though the behaviour of the first net remains unchanged. This is a problem with all structurally defined notions of net morphisms—they are very sensitive to the choice of Petri net for “implementing” a given behaviour.

Quite a few different types of morphisms on Petri nets have been defined in the literature. Our morphisms are closest in spirit to the morphisms defined by Winskel [18]. The main difference is that, following [14], we insist that the map on the places be a partial function in the reverse direction, whereas Winskel only requires the forward map to be a relation (actually, a multirelation) which preserves the initial marking and the neighbourhoods of defined events. We shall discuss the connection between our net morphisms and those studied by others in greater detail in the concluding section.

For each object PN = (S, T, W, M_{in}), let 1_{P N} = (id_{S}, id_{T}) be the identity morphism where id_{S} : S → S and id_{T} : T → T are the (total) identity functions. Let (ϕ_{S}^{1}, ϕ_{T}^{1} ) : P N_{1} → P N_{2} and (ϕ_{S}^{2}, ϕ_{T}^{2} ) : P N_{2} → P N_{3} be two net morphisms. Define the composition (ϕ_{S}^{2}, ϕ_{T}^{2} ) ∘ (ϕ_{S}^{1}, ϕ_{T}^{1} ) of these two morphisms as (ϕ_{S}^{1} ∘ ϕ_{S}^{2}, ϕ_{T}^{2} ∘ ϕ_{T}^{1} ).

It follows easily that Petri nets equipped with net morphisms form a category. Let us call this category PNet.

In the rest of this section, we shall prove some useful properties of net morphisms. We first show that net morphisms preserve concurrent behaviour in a strong way. This follows from the following result.

Lemma 13. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets and let ϕ be a net morphism from P N_{1} to P N_{2}. For each M ∈ [M_{in}^{1}⟩, define M_{ϕ} : S_{2} → N_{0} as follows:

∀s ∈ S_{2}. M_{ϕ}(s) = \{ \begin{matrix}M(ϕ(s)) & if ϕ(s) exists \\ M_{in}^{2}(s) & otherwise \end{matrix}

We then have the following:

(i) ∀M ∈ [M_{in}^{1}⟩. M_{ϕ} ∈ [M_{in}^{2}⟩.

(ii) Suppose that (M, u, M′) ∈ ⇒_{P N_{1}}. Then (M_{ϕ}, ϕ(u), M′_{ϕ}) ∈ ⇒_{P N_{2}}.

Proof.

(i) Since M ∈ [M_{in}^{1}⟩, we know that there is a step sequence ρ = u_{1}u_{2} … u_{n} such that (M_{in}^{1}, ρ, M) ∈ ⇒_{P N_{1}}^{∗}. Without loss of generality, we can assume that |u_{i}| = 1 for 0 ≤ i ≤ n—i.e. ρ is actually a sequence of singleton steps. We proceed by induction on k = |ρ|.

k = 0: Then M = M_{in}^{1} and by condition (iii) of net morphisms, (M_{in}^{1})_{ϕ} = M_{in}^{2} ∈ [M_{in}^{2}⟩.

k > 0: We can write ρ as ρ′t where |ρ′| = k − 1. Then there exists a marking M′ such that (M_{in}^{1}, ρ′, M′) ∈ ⇒_{P N_{1}}^{∗} and M′[t⟩_{1}M. By the induction hypothesis, M′_{ϕ} ∈ [M_{in}^{2}⟩.

Suppose that ϕ(t) is undefined. Then ϕ^{−1}(^{•}t) = ϕ^{−1}(t^{•}) = ∅ so the places in S_{1} whose marking changes in going from M′ to M do not have ϕ^{−1} images in S_{2}. As a result, M_{ϕ} = M′_{ϕ} ∈ [M_{in}^{2}⟩.

On the other hand, if ϕ(t) = t′ then ϕ^{−1}(^{•}t) = ^{•}t′ and ϕ^{−1}(t^{•}) = t′^{•}. Consider any s ∈ ^{•}t′. We know that M′_{ϕ}(s) = M′(ϕ(s)). Furthermore, W_{2}(s, t′) = W_{1}(ϕ(s), t) by the definition of net morphisms. Since M′[t⟩ we know that M′(ϕ(s)) ≥ W_{1}(ϕ(s), t) and so M′_{ϕ}(s) ≥ W_{2}(s, t′). This holds for all s ∈ •t′, so we have M′_{ϕ}[t′⟩ as well. Let M′_{ϕ}[t′⟩_{2}M′′. Using the definition of net morphisms, it is straightforward to check that M′′ = M_{ϕ}.

(ii) Suppose that M ∈ [M_{in}^{1}⟩ and M[u⟩_{1}. By part (i) of this lemma, we know that M_{ϕ} ∈ [M_{in}^{2}⟩. By the definition of M_{ϕ} and the definition of a net morphism it is straightforward to compute that M_{ϕ}[ϕ(u)⟩_{2} and that (M, u, M′) ∈ ⇒_{P N_{1}} and (M_{ϕ}, ϕ(u), M′′) ∈ ⇒_{P N_{2}} implies that M′′ = M′_{ϕ}.

□

Corollary 14. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets and let ϕ be a net morphism from P N_{1} to P N_{2}. Then (M_{in}^{1}, ρ, M) ∈ ⇒_{P N_{1}}^{∗} implies (M_{in}^{2}, ϕ(ρ), M_{ϕ}) ∈ ⇒_{P N_{2}}^{∗}, where ρ is a step sequence over T_{1} and M_{ϕ} is defined as in the previous lemma. (By abuse of notation, we have denoted the obvious extension of ϕ_{T} to step sequences also as ϕ.)

In certain restricted cases, it turns out that net morphisms, like transition system morphisms, are characterized by the way they map transitions.

To establish this result, we need to restrict our attention to morphisms whose source nets are simple with respect to places.

Definition 15. Let PN = (S, T, W, M_{in}) be a Petri net. P N is simple with respect to S in case

∀s_{1}, s_{2} ∈ S. If M_{in}(s_{1}) = M_{in}(s_{2}) and ∀t ∈ T. W (s_{1}, t) = W (s_{2}, t) and W (t, s_{1}) = W (t, s_{2}) then s_{1} = s_{2}.

Lemma 16. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets, such that P N_{1} is simple with respect to S_{1} and has no isolated places (i.e. ∀s_{1} ∈ S_{1}. ∃t_{1} ∈ T_{1}. s_{1} ∈ ^{•}t_{1} ∪ t_{1}^{•}). Let ϕ^{1} = (ϕ_{S}^{1}, ϕ_{T}^{1} ) and ϕ^{2} = (ϕ_{S}^{2}, ϕ_{T}^{2} ) be two net morphisms from P N_{1} to P N_{2}. If ϕ_{T}^{1} = ϕ_{T}^{2} then ϕ^{1} = ϕ^{2}.

Proof. We have to establish that ϕ_{S}^{1} = ϕ_{S}^{2}. We first show that if s_{1} = ϕ_{S}^{1}(s_{2}) then s_{1} = ϕ_{S}^{2}(s_{2}) as well.

Suppose s_{1} = ϕ_{S}^{1}(s_{2}). Since P N_{1} has no isolated places, there exists t_{1} ∈ T_{1} such that s_{1} ∈ ^{•}t_{1} or s_{1} ∈ t_{1}^{•}. Then ϕ_{T}^{1} (t_{1}) must be defined—suppose that ϕ_{T}^{1} (t_{1}) = t_{2}. Assume, without loss of generality, that s_{1} ∈ t_{1}^{•}. Then, since (ϕ_{S}^{1})^{−1}(t_{1}^{•}) = t_{2}^{•}, we must have s_{2} ∈ t_{2}^{•}. Since ϕ_{T}^{1} = ϕ_{T}^{2} , we have s_{2} ∈ ϕ_{T}^{2} (t_{1})^{•} as well, which implies that ϕ_{S}^{2}(s_{2}) exists and furthermore ϕ_{S}^{2}(s_{2}) = s′_{1} ∈ t_{1}^{•}. To establish that s′_{1} = s_{1} it suffices to establish the following:

Claim. M_{in}^{1}(s_{1}) = M_{in}^{1}(s′_{1}) and ∀t ∈ T_{1}. W_{1}(s_{1}, t) = W_{1}(s′_{1}, t) and W_{1}(t, s_{1}) = W_{1}(t, s′_{1}). Proof of Claim.

We know that M_{in}^{1}(s_{1}) = M_{in}^{2}(s_{2}) since s_{1} = ϕ_{S}^{1}(s_{2}). M_{in}^{1}(s′_{1}) = M_{in}^{2}(s_{2}) as well since s′_{1} = ϕ_{S}^{2}(s_{2}). So M_{in}^{1}(s_{1}) = M_{in}^{1}(s′_{1}).

Suppose t ∈ ^{•}s_{1}. Then, since s_{1} = ϕ_{S}^{1}(s_{2}), ϕ_{T}^{1} (t) is defined. Further, W_{1}(t, s_{1}) = W_{2}(ϕ_{T}^{1} (t), s_{2}). Since ϕ_{T}^{2} = ϕ_{T}^{1} and s′_{1} = ϕ_{S}^{2}(s_{2}), W_{1}(t, s′_{1}) = W_{2}(ϕ_{T}^{2} (t), s_{2}) = W_{2}(ϕ_{T}^{1} (t), s_{2}). Thus W_{1}(t, s_{1}) = W_{1}(t, s′_{1}).

A symmetric argument can be used to show that for each t ∈ ^{•}s′_{1}, W_{1}(t, s′_{1}) = W_{1}(t, s_{1}).

Similarly, we can establish that for each t ∈ T_{1}, W_{1}(s_{1}, t) = W_{1}(s′_{1}, t), thus establishing the claim.

Returning to the main proof, since P N_{1} was assumed to be simple with respect to places, we can conclude that s_{1} = s′_{1}. Hence s_{1} = ϕ_{S}^{1}(s_{2}) implies that s_{1} = ϕ_{S}^{2}(s_{2}) as well.

By a symmetric argument we can show that s_{1} = ϕ_{S}^{2}(s_{2}) implies that s_{1} = ϕ_{S}^{1}(s_{2}). Thus ϕ_{S}^{1} = ϕ_{S}^{2} and so ϕ^{1} = ϕ^{2}. □

7. From Petri nets to PN-transition systems

We now construct a functor NT from the category PNet of Petri nets to the category PNts of PN-transition systems.

NT maps objects in the obvious way—each Petri net P N is mapped to its associated transition system T S_{P N}. Let PN = (S, T, W, M_{in}) be a Petri net. Then

NT(P N) = ([M_{in}⟩, T, ⇒_{P N}, M_{in})

where, as usual, [M_{in}⟩ is the set of markings reachable from M_{in} in P N, T is the set of transitions of P N, ⇒_{P N} is the step transition relation for Petri nets defined in Section 3 and M_{in} is the initial marking of P N.

Next we define how NT maps arrows. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets and let ϕ = (ϕ_{S}, ϕ_{T}) be a net morphism from P N_{1} to P N_{2}. Then, NT(ϕ) = f^{ϕ} is defined as follows:

• ∀t ∈ T_{1}. f_{E}^{ϕ}(t) = ϕ_{T} (t).

• ∀M ∈ [M_{in}^{1}⟩. f_{Q}^{ϕ}(M) = M_{ϕ}.

(Recall that ∀s ∈ S_{2}. M_{ϕ}(s) = \{ \begin{matrix}M(ϕ_{S}(s)) & if ϕ_{S}(s) exists \\ M_{in}^{2}(s) & otherwise \end{matrix} )

Proposition 17. Let PN = (S, T, W, M_{in}) be a Petri net. Then NT(P N) = ([M_{in}⟩, T, ⇒_{P N}, M_{in}) is a PN-transition system.

Proof. T is countable by assumption. To establish that [M_{in}⟩ is countable, we first observe that the free monoid T^{∗} is countable. Each marking M ∈ [M_{in}⟩ is reachable by some sequence of transitions t_{1}t_{2} … t_{n} ∈ T^{∗}. Further, T S_{P N} is deterministic—a given sequence of transitions can lead to only one marking. From this, it follows that the cardinality of [M_{in}⟩ is less than or equal to the cardinality of T^{∗} and so [M_{in}⟩ must be countable.

Since M[O_{T} ⟩M′ in P N iff M = M′, clearly NT(P N) satisfies axiom (A1). The fact that NT(P N) satisfies (A2) follows directly from the definition of [M_{in}⟩.

To verify (A3) we have to show that distinct states in NT(P N) can be separated by non-trivial regions. For each s ∈ S, it is easy to check that r_{s} is a region where

∀M ∈ [M_{in}⟩. r_{s}(M) = M(s) and ∀t ∈ T. r_{s}(t) = (W (s, t), W (t, s)).

For M, M′ ∈ [M_{in}⟩, if M ≠ M′, there must be a non-isolated place s ∈ S such that M(s) ≠ M′(s). Then clearly r_{s} is a non-trivial region that separates M from M′ in NT(P N).

Finally, consider (A4). Suppose M ∈ [M_{in}⟩ and u ∈ MS_{fin}(T), and for every region r in NT(P N) it is the case that r(M) ≥ ∑_{t∈T} u(t) · ^{r}t. Then we have to show that there exists M′ ∈ [M_{in}⟩ such that (M, u, M′) ∈ ⇒_{P N}.

We know that for every s ∈ S, r_{s} (as defined above) is a region in NT(P N). Since r_{s}(M) = M(s) and ^{rs}t = W (s, t) it follows that for every s ∈ S we have M(s) ≥ ∑_{t∈T} u(t) · W (s, t). But then, we know that M[u⟩M′ where, for each s ∈ S, M′(s) = M(s) + ∑_{t∈T} u(t) · (W (t, s) − W (s, t)). So, by the definition of ⇒_{P N}, (M, u, M′) ∈ ⇒_{P N} and we are done. □

Proposition 18. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets and let ϕ be a morphism from P N_{1} to P N_{2}. Then NT(ϕ) = f^{ϕ} is a transition system morphism from NT(P N_{1}) to NT(P N_{2}).

Proof. Recall that ∀t ∈ T_{1}. f_{E}^{ϕ}(t) = ϕ_{T} (t) and ∀M ∈ [M_{in}^{1}⟩. f_{Q}^{ϕ}(M) = M_{ϕ}. By Lemma 13, we know that for each M ∈ [M_{in}^{1}⟩, M_{ϕ} ∈ [M_{in}^{2}⟩, so f_{Q}^{ϕ} is a total function from [M_{in}^{1}⟩ into [M_{in}^{2}⟩ as required. By definition, we know that f_{E}^{ϕ} is a partial function from T_{1} into T_{2}.

We have to show that if (M, u, M′) ∈ ⇒_{P N_{1}} then (f_{Q}^{ϕ}(M), f_{E}^{ϕ}(u), f_{Q}^{ϕ}(M′)) ∈ ⇒_{P N_{2}}. This follows directly from the second part of Lemma 13 which says that (M, u, M′) ∈ ⇒_{P N_{1}} implies that (M_{ϕ}, ϕ_{T} (u), M′_{ϕ}) ∈ ⇒_{P N_{2}}. □

Theorem 19. NT : PNet → PNts is a functor.

Proof. We have already verified that NT maps objects and arrows in PNet to objects and arrows in PNts correctly. We only have to verify that NT preserves the identity arrows and respects composition.

For every net PN = (S, T, W, M_{in}) ∈ PNet, the identity arrow is given by 1_{P N} = (id_{S}, id_{T}) where id_{S} and id_{T} are the (total) identity functions. Clearly f_{E}^{1_{P N}} (t) = t for every t ∈ T and f_{Q}^{1_{P N}} (M) = M_{id_{S}} = M for every M ∈ [M_{in}⟩ and so f^{1_{P N}} is the identity arrow for NT(P N).

Let ϕ^{1} : P N_{1} → P N_{2} and ϕ^{2} : P N_{2} → P N_{3} be a pair of net morphisms. Let f^{i} = NT(ϕ^{i}), i = 1, 2, and let f^{2∘1} = NT(ϕ^{2} ∘ ϕ^{1}). We have to show that f^{2} ∘ f^{1} = f^{2∘1}. Clearly, f_{E}^{2∘1}(t) = ϕ_{T}^{2} ∘ ϕ_{T}^{1} (t) for all t ∈ T_{1}. But, (f^{2} ∘ f^{1})_{E}(t) is again equal to ϕ_{T}^{2} ∘ ϕ_{T}^{1} (t) for all t ∈ T_{1}. Since f_{E}^{2∘1} = (f^{2} ∘ f^{1})_{E}, by Lemma 11 we must have f^{2∘1} = f^{2} ∘ f^{1} and we are done. □

8. The adjunction

Having constructed the functor NT from PNet to PNts, we want to show that it has a left adjoint TN : PNts → PNet. According to Mac Lane [8], it suffices to construct a map TN_{O} mapping objects in PNts to objects in PNet so that the diagram shown in Figure 7 commutes. The object map TN_{O} can then be extended uniquely to a functor TN : PNts → PNet which is the left adjoint of NT.

In other words, we have to first construct a universal transition system morphism η in PNts (which will serve as the unit of the adjunction). We then have to prove that for any object T S in PNts and any object P N in PNet, if there is a transition system morphism f : T S → NT(P N) then there is a unique net morphism ϕ : TN_{O}(T S) → P N such that f = NT(ϕ) ∘ η_{T S}.

[figure: T S; NT(P N); NT ∘ TN_{O}(T S); η_{T S}; f; NT(ϕ); TN_{O}(T S); P N; ϕ]

Figure 7: The adjunction

We first describe the object map TN_{O}. Let T S = (Q, E, →, q_{in}) be a PNtransition system. Then

TN_{O}(T S) = (R_{T S}, E, W_{T S}, M_{in}^{T S})

where W_{T S}(r, e) = ^{r}e and W_{T S}(e, r) = e^{r} for each r ∈ R_{T S} and e ∈ E and M_{in}^{T S}(r) = r(q_{in}) for each r ∈ R_{T S}.

Proposition 20. Let T S = (Q, E, →, q_{in}) be a PN-transition system. Then TN_{O}(T S) = (R_{T S}, E, W^{T S}, M_{in}^{T S}) is a Petri net. Moreover, TN_{O}(T S) is simple with respect to places and has no isolated places.

Proof. Checking that TN_{O}(T S) is a Petri net is straightforward. We know that E is countable, so the set of transitions of TN_{O}(T S) is countable. Notice that if E is infinite, R_{T S} may well be uncountable. In verifying that the places and transitions of TN_{O}(T S) are disjoint, a small problem arises in the (pathological) case where R_{T S} and E are not disjoint! We shall ignore this possiblity by noting that we can always construct TN_{O}(T S) with disjoint sets of places and transitions by using a suitable coding technique.

The regions in R_{T S} are “simple” by definition (any two distinct regions either differ in their value at q_{in} or in their value for some e ∈ E). Since we create exactly one place in TN_{O}(T S) for each region from R_{T S}, it is clear that the net TN_{O}(T S) is also simple with respect to places.

Finally, since R_{T S} has only non-trivial regions, TN_{O}(T S) has no isolated places. □

Next we describe how to construct η, the unit of the adjunction. We first need the following lemma.

Lemma 21. Let T S = (Q, E, →, q_{in}) be a PN-transition system and let TN_{O}(T S) = (R_{T S}, E, W_{T S}, M_{in}^{T S}). Then we have:

(i) ∀M ∈ [M_{in}^{T S}⟩. ∃!q ∈ Q such that ∀r ∈ R_{T S}. M(r) = r(q). We denote this state by q_{M}.

(ii) ∀q ∈ Q. ∃!M ∈ [M_{in}^{T S}⟩ such that ∀r ∈ R_{T S}. M(r) = r(q). We denote this marking by M_{q}.

(iii) ⇒_{TN_{O}(T S)}= {(M_{q}, u, M′_{q}) | (q, u, q′) ∈ →}.

Proof.

(i) For each M ∈ M_{in}^{T S}, we show that there is at least one q ∈ Q such that ∀r ∈ R_{T S}. M(r) = r(q). Let ρ be a step sequence u_{1}u_{2} … u_{k} such that (M_{in}^{T S}, ρ, M) ∈ ⇒_{P N}^{∗}. We proceed by induction on k = |ρ|.

k = 0: Then M = M_{in}^{T S} and by the definition of M_{in}^{T S}, q_{in} satisfies the given requirement.

k > 0: Then write ρ = ρ′u_{k} where |ρ′| < k. We know that ∃M′. (M_{in}^{T S}, ρ′, M′) ∈ ⇒_{P N}^{∗} and M′[u_{k}⟩M. By the induction hypothesis, there exists q′ ∈ Q such that ∀r ∈ R_{T S}. M′(r) = r(q′). Since M′[u_{k}⟩M, we know that r(q′) ≥ ∑_{e∈E} u(e)^{r}e for all r ∈ R_{T S}. Therefore, by axiom (A4), ∃q. q′ ⟶^{u_{k}} q. It is straightforward to compute that ∀r ∈ R_{T S}. M(r) = r(q). Having established that there is at least one candidate for q_{M} for every marking M, we now have to show that there is exactly one choice for q_{M}. Suppose q and q′ are both states in Q such that ∀r ∈ R_{T S}. M(r) = r(q) = r(q′). Then, by axiom (A3), we know that q = q′ since they agree on all regions.

(ii) Similar to (i), by induction on q_{in} →^{ρ}^{∗} q.

(iii) Follows in a straightforward way from (i) and (ii).

□

Lemma 22. Let T S = (Q, E, →, q_{in}) be a PN-transition system and let TN_{O}(T S) = (R_{T S}, E, W_{T S}, M_{in}^{T S}). Then the map η_{T S} : T S → NT ∘ TN_{O}(T S) given by

∀q ∈ Q. η_{T S}(q) = M_{q} and ∀e ∈ E. η_{T S}(e) = e

is a transition system isomorphism.

Proof. From the previous lemma, it follows that η_{T S} is a transition system morphism. To check that it is in fact an isomorphism, we show that we can construct a transition system morphism η′_{T S} such that η_{T S} ∘ η′_{T S} = 1_{NT∘TN_{O}(T S)} and η′_{T S} ∘ η_{T S} = 1_{T S}.

Define η′_{T S} : NT ∘ TN_{O}(T S) → T S as follows:

∀M ∈ [M_{in}^{T S}⟩. η′_{T S}(M) = q_{M} and ∀e ∈ E. η′_{T S}(e) = e

By the previous lemma, it is easy to verify that η′_{T S} is also a transition system morphism. Since q_{M_{q}} = q for all q ∈ Q and M_{q_{M}} = M for all M ∈ [M_{in}^{T S}⟩, it follows that η′_{T S} ∘ η_{T S} = 1_{T S} and η_{T S} ∘ η′_{T S} = 1_{NT∘TN_{O}(T S)}. □

We can now prove our main result.

Theorem 23. There exists a functor TN : PNts → PNet such that TN and NT form an adjunction (coreflection) with TN as the left adjoint and η as the unit.

Proof. We have to show that the diagram shown in Figure 7 commutes.

Let T S = (Q, E, →, q_{in}) and PN = (S, T, W, M_{in}). Then TN_{O}(T S) = (R_{T S}, E, W_{T S}, M_{in}^{T S}) and NT(P N) = ([M_{in}⟩, T, ⇒_{P N}, M_{in}). Define ϕ as follows:

ϕ_{S} : S ⇀ R_{T S} is given by

∀s ∈ S. ϕ_{S}(s) = \{ \begin{matrix}r_{s}^{−1} & if r_{s}^{−1} ∈ R_{T S} \\ undefined & otherwise \end{matrix}

ϕ_{T} = f_{E},

where for each s ∈ S, r_{s} ∈ R_{NT(P N)} is the region defined in the proof of Proposition 17. In other words,

∀M ∈ [M_{in}⟩. r_{s}(M) = M(s) and ∀t ∈ T. r_{s}(t) = (W (s, t), W (t, s)).

Also, recall that for r_{s} ∈ R_{NT(P N)}, r_{s}^{−1} is the inverse of r_{s} through f, as defined in Section 5.

Claim A. ϕ is a net morphism.

Proof of claim.

Suppose that r = ϕ_{S}(s). We have to check that M_{in}^{T S}(r) = M_{in}(s). We know that M_{in}^{T S}(r) = r(q_{in}) and that M_{in}(s) = r_{s}(M_{in}). Since r = r_{s}^{−1}, it follows that r(q_{in}) = r_{s}(f(q_{in})) = r_{s}(M_{in}).

Suppose that e ∈ E and ϕ_{T} (e) is undefined. We have to show that ϕ_{S}^{−1}(^{•}e) = ϕ_{S}^{−1}(e^{•}) = ∅. Consider any r ∈ ^{•}e such that r = ϕ_{S}(s), for some s ∈ S. Then W_{T S}(r, e) = ^{r}e. But, since r = r_{s}^{−1} and f(e) = ϕ_{T} (e) is undefined, we must have r(e) = (0, 0), and therefore W_{T S}(r, e) = 0, which contradicts r ∈ ^{•}e. Thus, ϕ_{S}^{−1}(^{•}e) = ∅. Similarly, we can show that ϕ_{S}^{−1}(e^{•}) = ∅.

On the other hand, suppose that e ∈ E and ϕ_{T} (e) = t. Then, we have to show that ϕ_{S}^{−1}(^{•}e) = ^{•}t and ϕ_{S}^{−1}(e^{•}) = t^{•}. We also have to establish that for each s ∈ ^{•}t, W (s, t) = W_{T S}(ϕ_{S}(s), e), and for each s ∈ t^{•}, W (t, s) = W_{T S}(e, ϕ_{S}(s)).

We first show that ϕ_{S}^{−1}(^{•}e) ⊆ ^{•}t. Let r ∈ ^{•}e and let s ∈ ϕ_{S}^{−1}(r). Since r = r_{s}^{−1} and f(e) = ϕ_{T} (e) is defined, we must have r(e) = r_{s}(f(e)) = r_{s}(t) and so W_{T S}(r, e) = ^{r}e = ^{rs}t = W (s, t). Thus, if r ∈ ^{•}e then s ∈ ^{•}t.

Conversely, we show that ^{•}t ⊆ ϕ_{S}^{−1}(^{•}e). Suppose that s ∈ ^{•}t. Since f(e) is defined and r_{s}(f(e)) ≠ (0, 0), r_{s}^{−1} is a non-trivial region r ∈ R_{T S}. Thus, ϕ_{S}(s) = r and by the definition of r_{s}^{−1}, r(e) = r_{s}(t) and so W (s, t) = ^{rs}t = ^{r}e = W_{T S}(r, e). Thus s ∈ ^{•}t implies ϕ_{S}(s) = r ∈ ^{•}e.

From this it follows that ϕ_{S}^{−1}(^{•}e) = ^{•}t. Similarly, we can establish that ϕ_{S}^{−1}(e^{•}) = t^{•}.

The fact that for each s ∈ ^{•}t, W (s, t) = W_{T S}(ϕ_{S}(s), e) and for each s ∈ t^{•}, W (t, s) = W_{T S}(e, ϕ_{S}(s)) again follows easily from the definition of r_{s}^{−1}.

Claim B. NT(ϕ) ∘ η_{T S} = f.

Proof of claim. Let f′ = NT(ϕ)∘η_{T S}. Then f′_{E} = NT(ϕ)_{E} ∘id_{E} = NT(ϕ)_{E} = ϕ_{T}. But, ϕ_{T} = f_{E} by definition. Hence f′_{E} = f_{E} and so, by Lemma 11, f′ = f and we are done.

Claim C. ϕ is unique.

Proof of claim. We have to show that if ϕ′ : TN_{O}(T S) → P N is any net morphism such that NT(ϕ′) ∘ η_{T S} = f, then ϕ′ = ϕ.

We know that f_{E} = ϕ_{T} ∘ η_{T S}_{E} = ϕ′_{T} ∘ η_{T S}_{E}. Since η_{T S}_{E} = id_{E}, we have f_{E} = ϕ_{T} = ϕ′_{T}. But, we know that TN_{O}(T S) is simple with respect to places and has no isolated places (by Proposition 20). So, by Lemma 16, we have ϕ_{S} = ϕ′_{S} as well.

Returning to the main proof, Claims A, B and C establish that the diagram shown in Figure 7 commutes. From [8], it then follows that TN_{O} can be uniquely extended to a functor TN from PNts to PNet which is the left adjoint of NT.

Since η, the unit of the adjunction, is an isomorphism, we have, in fact, a coreflection between TN and NT. □

If we work out the way TN maps morphisms, it turns out to be the following. Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems and let f :

T S_{1} → T S_{2} be a transition system morphism. Then TN(f) is the map ϕ^{f} where

ϕ_{S}^{f} : R_{T S_{2}} ⇀ R_{T S_{1}} is given by

∀r_{2} ∈ R_{T S_{2}}. ϕ_{S}^{f}(r_{2}) = \{ \begin{matrix}r_{2}^{−1} & if r_{2}^{−1} ∈ R_{T S_{1}} \\ undefined & otherwise \end{matrix}

ϕ_{T}^{f} : E_{1} ⇀ E_{2} = f_{E}.

9. Universal Constructions

Having established the coreflection between the categories PNts and PNet, we now look at some universal constructions in these categories.

It is easy to verify that the trivial transition system T S = ({q_{in}}, ∅, →, q_{in}), where →= {(q_{in}, O_{∅}, q_{in})}, is both an initial and a terminal object in PNts. Similarly, its image in PNet, the empty net P N = (∅, ∅, ∅, O_{∅}), is the initial and terminal object in PNet.

The standard product construction goes through for both PN-transition systems and Petri nets. For Petri nets, the product of two nets is the synchronized parallel composition of the two nets.

Definition 24. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets. Define the Petri net PN_{1×2} = (S_{1×2}, T_{1×2}, W_{1×2}, M_{in}^{1×2}) as follows.

• S_{1×2} = (S_{1} × {∗}) ∪ ({∗} × S_{2}), where ∗ ∉ S_{1} ∪ S_{2}.

• T_{1×2} = (T_{1} × T_{2}) ∪ (T_{1} × {∗}) ∪ ({∗} × T_{2}), where ∗ ∉ T_{1} ∪ T_{2}.

• ∀s ∈ S_{1×2}. ∀t ∈ T_{1×2}. W_{1×2}(s, t) = \{ \begin{matrix}W_{1}(s_{1}, t_{1}) & if s = (s_{1}, ∗) and \\ & t = (t_{1}, ∗) or t = (t_{1}, t_{2}) \\ W_{2}(s_{2}, t_{2}) & if s = (∗, s_{2}) and \\ & t = (∗, t_{2}) or t = (t_{1}, t_{2}) \\ 0 & otherwise \end{matrix}

• ∀s ∈ S_{1×2}. ∀t ∈ T_{1×2}. W_{1×2}(t, s) = \{ \begin{matrix}W_{1}(t_{1}, s_{1}) & if s = (s_{1}, ∗) and \\ & t = (t_{1}, ∗) or t = (t_{1}, t_{2}) \\ W_{2}(t_{2}, s_{2}) & if s = (∗, s_{2}) and \\ & t = (∗, t_{2}) or t = (t_{1}, t_{2}) \\ 0 & otherwise \end{matrix}

• ∀s ∈ S_{1×2}. M_{in}^{1×2}(s) = \{ \begin{matrix}M_{in}^{1}(s_{1}) & if s = (s_{1}, ∗) \\ M_{in}^{2}(s_{2}) & if s = (∗, s_{2}) \end{matrix}

Define morphisms π_{i} : PN_{1×2} → PN_{i}, i = 1, 2, as follows:

• \begin{matrix}∀s ∈ S_{1}. & π_{1_{S}}(s) = (s, ∗). \\ ∀t ∈ T_{1×2}. & π_{1_{T}} (t) = t_{1} if t = (t_{1}, ∗) or t = (t_{1}, t_{2}). \end{matrix}

• \begin{matrix}∀s ∈ S_{2}. & π_{2_{S}}(s) = (∗, s). \\ ∀t ∈ T_{1×2}. & π_{2_{T}} (t) = t_{2} if t = (∗, t_{2}) or t = (t_{1}, t_{2}). \end{matrix}

Lemma 25. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets. The product of these two nets is the Petri net PN_{1×2} = (S_{1×2}, T_{1×2}, W_{1×2}, M_{in}^{1×2}) equipped with the projections π_{i}, i = 1, 2, defined above.

Proof. It is easy to verify that π_{1} and π_{2} are PN-morphisms from PN_{1×2} to PN_{1} and PN_{2} respectively.

To prove that PN_{1×2} together with π_{1} and π_{2} actually is the product of PN_{1} and PN_{2}, we have to establish the following.

Claim. For any other net PN = (S, T, W, M_{in}) such that there exist morphisms f_{i} : PN → PN_{i}, i = 1, 2, there is a unique morphism g : PN → PN_{1×2} such that f_{i} = π_{i} ∘ g, i = 1, 2.

Proof of claim.

It is convenient to first define total functions f̂_{i} : T → (T_{i} ∪ {∗}), i = 1, 2, as follows.

∀t ∈ T. f̂_{i}(t) = \{ \begin{matrix}f_{i}(t) & if f_{i}(t) defined \\ ∗ & otherwise \end{matrix}

Now, define g : PN → PN_{1×2} as follows.

∀s ∈ S_{1×2}. g_{S}(s) = \{ \begin{matrix}f_{1}(s_{1}) \\ f_{2}(s_{2}) \\ undefined \end{matrix}

if s = (s_{1}, ∗) and f_{1}(s_{1}) defined if s = (∗, s_{2}) and f_{2}(s_{2}) defined otherwise

∀t ∈ T. g_{T} (t) = \{ \begin{matrix}undefined \\ (f̂_{1}(t), f̂_{2}(t)) \end{matrix} if f̂_{1}(t) = f̂_{2}(t) = ∗ otherwise

It is easy to verify that g is a PN-morphism and that f_{i} = π_{i} ∘ g, i = 1, 2, and, furthermore, that it is the unique map from PN to PN_{1×2} with this property. □

Since the right adjoint preserves limits, and, further, every PN-transition system in PNts is the image of some net in PNet, we know that PNts has products as well. It is straightforward to verify that the product of two PN-transition systems T S_{1} and T S_{2} is the transition system T S_{1×2} equipped with projections π_{1} and π_{2} as defined below.

Definition 26. Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be two PN-transition systems. Let the transition system T S_{1×2} = (Q_{1×2}, E_{1×2}, →_{1×2}, q_{in}^{1×2}) be defined as follows:

• Q_{1×2} = Q_{1} × Q_{2}.

• E_{1×2} = (E_{1} × E_{2}) ∪ (E_{1} × {∗}) ∪ ({∗} × E_{2}).

• →_{1×2}= \{((q_{1}, q_{2}), u, (q′_{1}, q′_{2})) | \begin{matrix}where u ∈ MS_{fin}(E_{1×2}) and there exists \\ u_{i} ∈ MS_{fin}(E_{i}), i = 1, 2, such that: \end{matrix}

− (q_{i}, u_{i}, q′_{i}) ∈ →_{i}.

− ∀e_{1} ∈ E_{1}. u_{1}(e_{1}) = u((e_{1}, ∗)) + ∑_{e_{2}∈E_{2}}u((e_{1}, e_{2})).

− ∀e_{2} ∈ E_{2}. u_{2}(e_{2}) = u((∗, e_{2})) + ∑_{e_{1}∈E_{1}}u((e_{1}, e_{2})).

}.

Define morphisms π_{i} : T S_{1×2} → T S_{i}, i = 1, 2, as follows:

• \begin{matrix}π_{1_{Q}}((q_{1}, q_{2})) = q_{1}. \\ π_{1_{E}}((e_{1}, ∗)) = π_{1_{E}}((e_{1}, e_{2})) = e_{1}. \end{matrix}

• \begin{matrix}π_{2_{Q}}((q_{1}, q_{2})) = q_{2}. \\ π_{2_{E}}((∗, e_{2})) = π_{2_{E}}((e_{1}, e_{2})) = e_{2}. \end{matrix}

It turns out that PNet also has coproducts. If the initial markings of the two nets are reasonably similar, then the sum of the two nets represents nondeterministic choice. If the initial markings are dissimilar, then the sum corresponds to the asynchronous parallel composition of the two nets.

Definition 27. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets. Define the Petri net PN_{1+2} = (S_{1+2}, T_{1+2}, W_{1+2}, M_{in}^{1+2}) as follows.

• S_{1+2} = (S_{1} × {∗}) ∪ ({∗} × S_{2}) ∪ {(s_{1}, s_{2})|s_{1} ∈ S_{1}, s_{2} ∈ S_{2}, M_{in}^{1}(s_{1}) = M_{in}^{2}(s_{2})}, where ∗ ∉ S_{1} ∪ S_{2}.

• T_{1+2} = (T_{1} × {∗}) ∪ ({∗} × T_{2}), where ∗ ∉ T_{1} ∪ T_{2}.

• ∀s ∈ S_{1+2}. ∀t ∈ T_{1+2}. W_{1+2}(s, t) = \{ \begin{matrix}W_{1}(s_{1}, t_{1}) & if t = (t_{1}, ∗) and \\ & s = (s_{1}, ∗) or s = (s_{1}, s_{2}) \\ W_{2}(s_{2}, t_{2}) & if t = (∗, t_{2}) and \\ & s = (∗, s_{2}) or s = (s_{1}, s_{2}) \\ 0 & otherwise \end{matrix}

• ∀s ∈ S_{1+2}. ∀t ∈ T_{1+2}. W_{1+2}(t, s) = \{ \begin{matrix}W_{1}(t_{1}, s_{1}) & if t = (t_{1}, ∗) and \\ & s = (s_{1}, ∗) or s = (s_{1}, s_{2}) \\ W_{2}(t_{2}, s_{2}) & if t = (∗, t_{2}) and \\ & s = (∗, s_{2}) or s = (s_{1}, s_{2}) \\ 0 & otherwise \end{matrix}

• ∀s ∈ S_{1+2}. M_{in}^{1+2}(s) = \{ \begin{matrix}M_{in}^{1}(s_{1}) & if s = (s_{1}, ∗) or s = (s_{1}, s_{2}) \\ M_{in}^{2}(s_{2}) & if s = (∗, s_{2}) \end{matrix}

Define morphisms in_{i} : PN_{i} → PN_{1+2}, i = 1, 2, as follows:

• \begin{matrix}∀s ∈ S_{1+2}. & in_{1_{S}}(s) = s_{1} if s = (s_{1}, ∗) or s = (s_{1}, s_{2}). \\ ∀t ∈ T_{1}. & in_{1_{T}} (t) = (t, ∗). \end{matrix}

• \begin{matrix}∀s ∈ S_{1+2}. & in_{2_{S}}(s) = s_{2} if s = (∗, s_{2}) or s = (s_{1}, s_{2}). \\ ∀t ∈ T_{2}. & in_{2_{T}} (t) = (∗, t). \end{matrix}

So, given transitions t_{1} ∈ T_{1} and t_{2} ∈ T_{2} that are enabled at the initial markings M_{in}^{1} and M_{in}^{2} respectively, PN_{1+2} will have a common input place for t_{1} and t_{2} provided there is an s_{1} ∈ ^{•}t_{1} and an s_{2} ∈ ^{•}t_{2} such that M_{in}^{1}(s_{1}) = M_{in}^{2}(s_{2}). This represents a kind of non-deterministic choice between (t_{1}, ∗) and (∗, t_{2}) in the composite net PN_{1+2}. On the other hand, if we cannot find s_{1} ∈ ^{•}t_{1} and s_{2} ∈ ^{•}t_{2} such that M_{in}^{1}(s_{1}) = M_{in}^{2}(s_{2}), then both (t_{1}, ∗) and (∗, t_{2}) will be independently enabled at the initial marking M_{in}^{1+2} in PN_{1+2}, corresponding to the asynchronous parallel composition of t_{1} and t_{2}.

Lemma 28. Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be two Petri nets. The coproduct of these two nets is the Petri net PN_{1+2} = (S_{1+2}, T_{1+2}, W_{1+2}, M_{in}^{1+2}) equipped with the injections in_{i}, i = 1, 2, defined above.

Proof. It is easy to verify that in_{1} and in_{2} are PN-morphisms from PN_{1} to PN_{1+2} and PN_{2} to PN_{1+2} respectively.

To prove that PN_{1+2} together with in_{1} and in_{2} actually is the coproduct of PN_{1} and PN_{2}, we have to establish the following.

Claim. For any other net PN = (S, T, W, M_{in}) such that there exist morphisms f_{i} : PN_{i} → PN , i = 1, 2, there is a unique morphism g : PN_{1+2} → PN such that f_{i} = g ∘ in_{i}, i = 1, 2.

Proof of Claim.

For convenience, we first define total functions f̂_{i} : S → (S_{i} ∪ {∗}), i = 1, 2, as follows.

∀s ∈ S. f̂_{i}(s) = \{ \begin{matrix}f_{i}(s) & if f_{i}(s) defined \\ ∗ & otherwise \end{matrix}

Now, define g : PN_{1+2} → P N as follows.

∀s ∈ S. g_{S}(s) = \{ \begin{matrix}undefined \\ (f̂_{1}(s), f̂_{2}(s)) \end{matrix} if f̂_{1}(s) = f̂_{2}(s) = ∗ otherwise

∀t ∈ T_{1+2}. g_{T} (t) = \{ \begin{matrix}f_{1}(t_{1}) \\ f_{2}(t_{2}) \\ undefined \end{matrix}

if t = (t_{1}, ∗) and f_{1}(t_{1}) defined if t = (∗, t_{2}) and f_{2}(t_{2}) defined otherwise

We first verify that g is a PN-morphism. It is straightforward to check that

∀s ∈ S. ∀s′ ∈ S_{1+2}. g(s) = s′ implies M_{in}(s) = M_{in}^{1+2}(s′).

Next, suppose g(t′) is undefined for t′ ∈ T_{1+2}. We have to show that g^{−1}(^{•}t′) = g^{−1}(t′^{•}) = ∅. Let s′ ∈ ^{•}t′. Without loss of generality, let t′ = (t_{1}, ∗). Then it is clear that s′ is of the form (s_{1}, x), where s_{1} ∈ ^{•}t_{1} in PN_{1} and x ∈ S_{2} ∪ {∗}. If s′ = g(s) for some s ∈ S, then this implies that s_{1} = f_{1}(s). But we know that f_{1}(t_{1}) is undefined as well and so f_{1}^{−1}(^{•}t_{1}) = ∅. In particular, f_{1}^{−1}(s_{1}) = ∅ and so g^{−1}(s′) = ∅ as well. Since s′ was an arbitrary place in ^{•}t′ it follows that g^{−1}(^{•}t′) = ∅. By a similar argument, g^{−1}(t′^{•}) = ∅ as well.

On the other hand suppose that g(t′) = t for t′ ∈ T_{1+2} and t ∈ T. Then, we have to show that g^{−1}(^{•}t′) = ^{•}t and g^{−1}(t′^{•}) = t^{•}. We also have to establish that for each s ∈ ^{•}t, W (s, t) = W_{1+2}(g(s), t′) and for each s ∈ t^{•}, W (t, s) = W_{1+2}(t′, g(s)).

Without loss of generality, assume that t′ is of the form (t_{1}, ∗).

We first show that g^{−1}(^{•}t′) ⊆ ^{•}t. Let s′ ∈ ^{•}t′. Clearly s′ must be of the form (s_{1}, x), where s_{1} ∈ ^{•}t_{1} in PN_{1} and x ∈ S_{2} ∪ {∗}. Then, s ∈ g^{−1}(s′) implies s ∈ f_{1}^{−1}(s_{1}). But f_{1}(t_{1}) = t′ and so f_{1}^{−1}(^{•}t_{1}) = ^{•}t. Hence, it follows that if s_{1} ∈ ^{•}t_{1} then s ∈ ^{•}t. So s ∈ g^{−1}(^{•}t′) implies s ∈ ^{•}t.

Conversely, let s ∈ ^{•}t. Then, since f_{1}(t_{1}) = t, we know that f_{1}(s) = s_{1} for some s_{1} ∈ ^{•}t_{1} in PN_{1}. It follows that g(s) = (s_{1}, x), where x = f̂_{2}(s) and (s_{1}, x) ∈ •(t_{1}, ∗). So ^{•}t ⊆ g^{−1}(^{•}t′).

So we have shown that g^{−1}(^{•}t′) = ^{•}t. A similar argument establishes that g^{−1}(t′^{•}) = t^{•}.

The fact that for each s ∈ ^{•}t, W (s, t) = W_{1+2}(g(s), t′) and for each s ∈ t^{•}, W (t, s) = W_{1+2}(t′, g(s)) follow easily from the definition of g and W_{1+2}.

To show that g is the unique map from PN_{1+2} → PN such that f_{i} = g ∘ in_{i}, i = 1, 2, we establish that g_{S} : S → S_{1+2} is the unique map such that f_{i_{S}} = in_{i_{S}} ∘ g_{S}, i = 1, 2, and g_{T} : T_{1+2} → T is the unique map such that f_{i_{T}} = g_{T} ∘ in_{i_{T}}, i = 1, 2.

First define the maps în_{i} : S_{1+2} → S_{i} ∪ {∗}, i = 1, 2, as follows.

∀s ∈ S_{1+2}. în_{i}(s) = \{ \begin{matrix}in_{i}(s) & if in_{i}(s) defined \\ ∗ & otherwise \end{matrix}

Now define the maps ⟨in_{1_{S}}, in_{2_{S}}⟩ : S_{1+2} → (S_{1}∪{∗})×(S_{2}∪{∗}) and ⟨f_{1_{S}}, f_{2_{S}}⟩ : S → (S_{1} ∪ {∗}) × (S_{2} ∪ {∗}) such that

\begin{aligned}∀s ∈ S_{1+2}. & ⟨in_{1_{S}}, in_{2_{S}}⟩(s) & = & (în_{1}(s), în_{2}(s)). \\ ∀s ∈ S. & ⟨f_{1_{S}}, f_{2_{S}}⟩(s) & = & (f̂_{1}(s), f̂_{2}(s)). \end{aligned}

[figure: ◯; ◯; e_{1}; T S_{1}; ◯; ◯; ◯; ◯; e_{2}; e_{2}; e_{2}; e_{2}; ⋯; T S_{2}; •; e_{1}; P N_{1}; •; e_{2}; P N_{2}; ◯; ◯; ◯; ◯; ◯; s_{0}; s_{1}; s_{2}; s_{3}; s′_{1}; e_{1}; e_{2}; e_{2}; e_{2}; e_{2}; ⋯; T S_{1+2}]

Figure 8: A Naïve Coproduct Construction in PNts

To establish that g_{S} is the unique map such that f_{i_{S}} = in_{i_{S}} ∘ g_{S}, i = 1, 2, it suffices to show that g_{S} is the unique map such that ⟨f_{1_{S}}, f_{2_{S}}⟩ = ⟨in_{1_{S}}, in_{2_{S}}⟩ ∘ g_{S}. Suppose that there is some other g′_{S} such that ⟨f_{1_{S}}, f_{2_{S}}⟩ = ⟨in_{1_{S}}, in_{2_{S}}⟩ ∘ g′_{S} = ⟨in_{1_{S}}, in_{2_{S}}⟩ ∘ g_{S}. Since ⟨in_{1_{S}}, in_{2_{S}}⟩ is an injective total function from S_{1+2} to (S_{1} ∪ {∗}) × (S_{2} ∪ {∗}) , it follows that g′_{S} = g_{S}.

To show that g_{T} is the unique map such that f_{i_{T}} = g_{T} ∘ in_{i_{T}}, i = 1, 2, define maps ⟨f_{1_{T}} + f_{2_{T}} ⟩ : T_{1} ⊎ T_{2} → T and ⟨in_{1_{T}} + in_{2_{T}} ⟩ : T_{1} ⊎ T_{2} → T_{1+2} as follows

∀t ∈ T_{1} ⊎ T_{2}. ⟨f_{1_{T}} + f_{2_{T}} ⟩(t) = \{ \begin{matrix}f_{1}(t) \\ f_{2}(t) \end{matrix}  if t ∈ T_{1} ; otherwise
∀t ∈ T_{1} ⊎ T_{2}. ⟨in_{1_{T}} + in_{2_{T}} ⟩(t) = \{ \begin{matrix}in_{1}(t) \\ in_{2}(t) \end{matrix}  if t ∈ T_{1} ; otherwise

It then suffices to show that g_{T} is the unique map such that ⟨f_{1_{T}} + f_{2_{T}} ⟩ = g_{T} ∘ ⟨in_{1_{T}} + in_{2_{T}} ⟩. Suppose that there is some other g′_{T} such that ⟨f_{1_{T}} + f_{2_{T}} ⟩ = g′_{T} ∘ ⟨in_{1_{T}} + in_{2_{T}} ⟩ = g_{T} ∘ ⟨in_{1_{T}} + in_{2_{T}} ⟩. Since ⟨in_{1_{T}} + in_{2_{T}} ⟩ is a surjective function from T_{1} ⊎ T_{2} to T_{1+2} , it follows that g′_{T} = g_{T}. □

On the other hand, for PN-transition systems, the situation regarding the existence of coproducts is not so straightforward.

For transition systems in general, there is a canonical way to form the coproduct— given T S_{1} and T S_{2}, the transition system T S_{1} + T S_{2} is obtained by identifying the initial states of T S_{1} and T S_{2}.

This operation is well behaved for various special classes of transition systems— for instance, the sum of two elementary transition systems defined in this manner is also an elementary transition system [14] and the sum of two asynchronous transition systems is also an asynchronous transition system [20].

Unfortunately, it turns out that for PN-transition systems, this is not the case. In other words, it is possible to define two PN-transition systems T S_{1} and T S_{2} such that the transition system obtained by identifying their initial states is not a PN-transition system.

Consider the transition systems shown in Figure 8. T S_{1} is generated by P N_{1} and T S_{2} is generated by P N_{2} so both T S_{1} and T S_{2} are PN-transition systems.

On the other hand the transition system T S_{1+2}, obtained by forming the normal coproduct of T S_{1} and T S_{2}, is not a PN-transition system. To see this, observe that for any region r in T S_{1+2}, r(s_{i+1}) ≥ r(s_{i}) for all i ∈ N_{0}.

For, suppose there is some r′ such that r′(s_{i+1}) < r′(s_{i}) for some i ∈ N_{0}. Then it must be the case that ^{r′}e_{2} > e_{2}^{r′} and in fact r′(s_{i+1}) < r′(s_{i}) for every i ∈ N_{0}. Since r′(s_{0}) is finite, there must be some j ∈ N_{0} where r′(s_{j}) < ^{r′}e_{2}, which contradicts the fact that e_{2} is enabled at all s_{i}, i ∈ N_{0}.

As a result, it follows that for all regions r, for all i ∈ N_{0}, r(s_{i}) ≥ r(s_{0}) ≥ ^{r}e_{1}, since e_{1} is enabled at s_{0}. In other words, the states s_{i}, i ∈ {1, 2, …}, do not satisfy axiom (A4) of PN-transition systems, because e_{1} is enabled by all regions at these states and there is no e_{1} transition out of these states.

However, we can show, indirectly, that PNts does have coproducts.

Lemma 29. The category PNts has coproducts.

Proof. Let T S_{1} and T S_{2} be two PN-transition systems. We want to find a PNtransition system T S_{1+2} and two maps in_{i} : T S_{i} → T S_{1+2}, i = 1, 2, such that T S_{1+2} equipped with the injection morphisms in_{1} and in_{2} is a coproduct of T S_{1} and T S_{2}.

Let P N_{1} = TN(T S_{1}) and P N_{2} = TN(T S_{2}). Since PNet has coproducts, we can define a net P N_{1+2} which, when equipped with injections in′_{i} : P N_{i} → P N_{1+2}, i = 1, 2, constitutes a coproduct of P N_{1} and P N_{2}.

The result we are after hinges on the following:

Claim. P N_{1+2} ≃ TN ∘ NT(P N_{1+2}).

Assuming the claim for the moment, let ϕ : P N_{1+2} → TN ∘ NT(P N_{1+2}) denote one direction of the isomorphism. We can conclude that TN ∘ NT(P N_{1+2}) equipped with injections ϕ ∘ in′_{i} : P N_{i} → TN ∘ NT(P N_{1+2}), i = 1, 2, is also a coproduct of P N_{1} and P N_{2}.

It follows from the fact that we have a coreflection between TN and NT that the left adjoint, TN, is full and faithful. So, we can find maps in_{i} : T S_{i} → NT(P N_{1+2}) such that TN(in_{i}) = ϕ ∘ in′_{i} for i = 1, 2.

It is straightforward to show that full and faithful functors reflect coproduct diagrams. Since the coproduct diagram consisting of P N_{1}, P N_{2}, TN ∘ NT(P N_{1+2}) and the two injection maps ϕ ∘ in′_{i}, i = 1, 2, lies within the range of TN, it follows that the corresponding diagram in PNts consisting of T S_{1}, T S_{2}, NT(P N_{1+2}) and the maps in_{i}, i = 1, 2, constitutes a coproduct diagram as well, and we are done.

[figure: T S_{1} ≃ NT(P N_{1}); T S_{2} ≃ NT(P N_{2}); NT(P N_{1+2}); NT(in′_{1}); NT(in′_{2}); TN(T S_{1}) = P N_{1}; TN(T S_{2}) = P N_{2}; ≃; ≃; TN ∘ NT(P N_{1}); TN ∘ NT(P N_{2}); P N_{1+2}; TN ∘ NT(P N_{1+2}); in′_{1}; in′_{2}; TN∘NT(in′_{1}); TN∘NT(in′_{2}); ϕ; ε_{P N_{1+2}}; TN; NT]

Figure 9:

To complete the proof, we have to establish the claim that P N_{1+2} is isomorphic to TN ∘ NT(P N_{1+2}).

Proof of claim.

By the coreflection between TN and NT, we know that T S_{i} is isomorphic to NT(P N_{i}), i = 1, 2 (recall that P N_{i} abbreviates TN(T S_{i}), i = 1, 2).

Since TN is full and faithful, it preserves isomorphisms and thus P N_{i} ≃ TN ∘ NT(P N_{i}), i = 1, 2.

Combining this isomorphism with TN ∘ NT(in′_{i}), we have maps from P N_{i} to TN ∘ NT(P N_{1+2}) (see Figure 9). Since P N_{1+2} equipped with the injections in′_{1} and in′_{2} is a coproduct of P N_{1} and P N_{2}, we have a unique map ϕ : P N_{1+2} → TN ∘ NT(P N_{1+2}) such that ϕ ∘ in′_{i} = TN ∘ NT(in′_{i}), i = 1, 2 (where we ignore the isomorphism between P N_{i} and TN ∘ NT(P N_{i}), i = 1, 2, from now on).

From the way the adjunction is defined, it follows that the set of transitions of P N_{1+2}, T_{P N_{1+2}}, is the same as the set of transitions of TN∘NT(P N_{1+2}). Similarly, T_{P N_{i}} = T_{TN∘NT(P N_{i})}, for i = 1, 2.

As in the proof of Lemma 28, we can define maps ⟨in′_{1_{T}} + in′_{2_{T}} ⟩ and ⟨(TN ∘ NT(in′_{1}))_{T} + (TN ∘ NT(in′_{2}))_{T} ⟩ from T_{P N_{1}} ⊎ T_{P N_{2}} → T_{P N_{1+2}}. It follows from the way the functors NT and TN are defined that ⟨in′_{1_{T}} + in′_{2_{T}} ⟩ = ⟨(TN ∘ NT(in′_{1}))_{T} + (TN ∘ NT(in′_{2}))_{T} ⟩.

We know that ϕ_{T} ∘ ⟨in′_{1_{T}} + in′_{2_{T}} ⟩ = ⟨(TN ∘ NT(in′_{1}))_{T} + (TN ∘ NT(in′_{2}))_{T} ⟩. Since ⟨in′_{1_{T}} + in′_{2_{T}} ⟩ is a surjective map onto T_{1+2}, it must be the case that ϕ_{T} is the identity map on T_{P N_{1+2}}.

In the other direction, the counit of the adjunction defines a map ε_{P N_{1+2}} from TN ∘ NT(P N_{1+2}) to P N_{1+2}. It follows from the way the adjunction is defined that

[figure: ◯; ◯; ◯; ◯; ◯; ◯; ◯; ◯; ⋯; ⋯; s_{0}; s_{1}; s_{2}; s_{3}; s′_{0}; s′_{1}; s′_{2}; s′_{3}; e_{2}; e_{2}; e_{2}; e_{2}; e_{1}; e_{1}; e_{1}; e_{1}]

Figure 10: The coproduct of T S_{1} and T S_{2} (from Figure 8)

(ε_{P N_{1+2}})_{T} is the identity map on T_{P N_{1+2}} as well.

Thus, (ϕ ∘ ε_{P N_{1+2}})_{T} is the identity map on T_{P N_{1+2}}. We know that TN ∘ NT(P N_{1+2}) is simple with respect to places and has no isolated places. Hence, from Lemma 16, we can conclude that that ϕ ∘ ε_{P N_{1+2}} = id_{TN∘NT(P N_{1+2})} since the two morphisms agree on the way they map transitions.

Similarly, (ε_{P N_{1+2}} ∘ ϕ)_{T} is the identity map on T_{P N_{1+2}}. Since P N_{1} and P N_{2} are both simple respect to places and have no isolated places, it is not difficult to show, from Definition 27, that P N_{1+2} is also simple with respect to places and has no isolated places. Hence, we can appeal to Lemma 16 once again to conclude that ε_{P N_{1+2}} ∘ ϕ = id_{P N_{1+2}}.

Thus, we have established that ϕ and ε_{P N_{1+2}} constitute an isomorphism between P N_{1+2} and TN ∘ NT(P N_{1+2}) and we are done.

□

Using Lemma 29, we can show that the transition system shown in Figure 10, together with the obvious injection maps, is the coproduct of the transition systems T S_{1} and T S_{2} shown in Figure 8.

10. Discussion

In this paper, we have established a coreflection between the category PNts of PN-transition systems and the category PNet of Petri nets.

This coreflection essentially means that the category PNts can be embedded in PNet—in other words, PN-transition systems can be viewed as a sub-model of Petri nets. One crucial advantage of having coreflections between different models of concurrency is that we can automatically translate results from one model to another. For instance, to obtain a non-interleaved model for a process calculus such as CCS [9], it is intuitively easier to enrich the standard interleaved transition system semantics to obtain a more faithful representation of concurrency, rather than providing a semantics directly in terms of nets [3, 15] or event structures [19]. So, for example, we can use a very simple extension of the standard operational semantics for CCS to provide a non-interleaved semantics for a rich subclass of the language in terms of asynchronous transtition systems [13]. These asynchronous transition systems belong to the special subcategory shown to correspond closely to safe nets in [20]. This implies that we obtain “for free” a net semantics for this language.

An advantage of working with categories is that many interesting operations that one defines on these models can be captured as universal categorical constructions. For instance, parallel composition corresponds to a notion of categorical product, while nondeterministic choice can be described in terms of coproducts. Thus, by relating categories of models, we can also compare how these constructions behave in different models. This issue is discussed in some detail in [20], where a number of relationships between models for concurrency are established in a categorical setting, spanning the spectrum of linear-time, branching-time and partial-order approaches to modelling the behaviour of concurrent systems.

In establishing our coreflection, we have placed no restrictions on the nets in PNet. In particular, we permit isolated transitions in our nets. Behaviourally, isolated transitions have the unpleasant side-effect of introducing unbounded concurrency into the system. Thus, a useful restriction to place on nets is that every transition has an input place. The corresponding restriction on PN-transition systems is that the steps enabled at any state should be bounded. By introducing these restrictions, we obtain full subcategories of PNts and PNet which are also related by a coreflection.

We have also removed the restriction imposed by Nielsen, Rozenberg and Thiagarajan [14] in constructing their category of elementary net systems that the nets be simple. This restriction is crucially used by them to establish the equivalent of Lemma 16 for elementary net systems. However, as we have observed here, it is sufficient to ensure that in going from PN-transition systems (elementary transition systems) to Petri nets (elementary net systems), the nets that one constructs are simple. So, the coreflection between elementary transition systems and elementary net systems established in [14] continues to hold even when their category of elementary net systems is extended to permit non-simple nets.

Our construction of a Petri net from a PN-transition system always gives rise to an infinite net (except in the case of the trivial transition system). This is because any non-negative linear combination of regions is also a region and we saturate the net with all possible non-trivial regions. So, it would be interesting to try and characterize those PN-transition systems which can be described in terms of a finite basis set of regions.

For elementary transition systems, it is straightforward to see that a given transition system can be represented as a finite elementary net system if and only if the set of states and the set of events of the transition system are finite.

However, since Petri nets can have places which are unbounded, a finite Petri net can give rise to an infinite PN-transition system.

Since we are dealing with unlabelled structures, the set of events of a PNtransition system is the same as the set of transitions of the Petri net whose behaviour it represents. Thus, for a PN-transition system to have a representation as a finite net, it is necessary for its set of events to be finite.

Unfortunately, this condition is not sufficient. In [11], we show an example of a Petri net that has a finite number of transitions but an infinite number of (unbounded) places whose behaviour cannot be simulated by any finite net.

However, it is the case that if both the set of events and the set of states of a PN-transition system are finite, then we can construct a finite Petri net whose behaviour is the same as that of the original transition system.

We turn now to other categories of Petri nets that have been described in the literature—notably those of Winskel [18] and Meseguer and Montanari [10].

Our definition of net morphisms is a strengthened version of the one used by Winskel in [18]. Winskel permits the map on places to be an arbitrary relation (actually a multirelation) in the forward direction which preserves the initial marking and neighbourhoods of transitions. The main reason for this is to permit morphisms between the unfolding of a net and the original net (for 1-safe nets). However, as has been pointed out in [14], this relaxation does not permit us to establish an adjunction between transition systems and nets. The essential problem is that we can, in general, find more than one of Winskel’s morphisms between a pair of nets describing the same behavioural morphism between the corresponding transition systems. This destroys the bijection between hom(TN(T S), PN ) and hom(T S, NT(PN )) which is required for an adjunction. The observation in [14] is made with respect to elementary transition systems, but it holds for PN-transition systems as well.

Meseguer and Montanari [10] define a variety of categories based on Petri nets. They regard multisets of places and transitions as commutative monoids and, in the most general case, define their net morphisms to be monoid homomorphisms over both places and transitions which respect the neighbourhoods of the transitions. Their category MPetri_{0}, where maps on places are monoid homomorphisms and maps on transitions are partial functions, is closest in spirit to our category PNet. Once again, we cannot obtain an adjunction using their net morphisms because there can be more than one such net morphism corresponding to the same transition system morphism. Also, in MPetri_{0} initial markings are restricted to sets of places (rather than multisets) in order for coproducts to exist. Given this restriction, coproducts in MPetri_{0} correspond to non-deterministic choice. In PNet no such restriction is necessary to obtain coproducts, and, as we have noted in the previous section, for nets satisfying such a restriction on the initial marking, our coproducts would also always correspond to non-deterministic choice.

Admittedly, our net morphisms appear to be fairly restrictive when compared to those of [18] or [10]. However, the restrictions we impose on net morphisms seem essential for establishing the correspondence we would like between nets and transition systems, given our “free” construction of a net TN(T S) from a PN-transition system T S, where all non-trivial regions are included as places in TN(T S). One possible way to relax the notion of a net morphism and still obtain a coreflection between PN-transition systems and nets is to tighten up the construction of a net PN from a PN-transition system T S to include, say, only a basis set of regions as places in PN , rather than all non-trivial regions.

Despite the restricted nature of our net morphisms, our coreflection does offer a solution to a general problem with net morphisms. Ideally, a morphism should exist between nets PN_{1} and PN_{2} iff PN_{2} can simulate the behaviour of PN_{1}. However, the structure of PN_{1} and PN_{2} will often rule out such a morphism, even when the behaviours of the two nets can be related. This is true even in the more generous setup of [18] or [10] and is a consequence of the fact that nets are too concrete a representation of system behaviour. Our coreflection gives us a way to get around this difficulty. Suppose we have two nets PN_{1} and PN_{2} such that there is a transition system morphism from NT(PN_{1}) to NT(PN_{2}), but there is no net morphism from PN_{1} to PN_{2}. We can construct the net TN ∘ NT(PN_{1}), which is the “canonical” representation of PN_{1}. The coreflection then guarantees that a net morphism exists between TN ∘ NT(PN_{1}) and PN_{2}. In fact, we do not even need the entire net TN ∘ NT(PN_{1}) to obtain a morphism to PN_{2}. If f is the map between NT(PN_{1}) and NT(PN_{2}), it is sufficient to construct a net PN ′_{1} from PN_{1} by adding to PN_{1} those places which are inverse images via f of the special regions r_{s} in NT(PN_{2}) (recall that for each place s in PN_{2}, we can associate a region r_{s} in NT(PN_{2})).

Another way that Meseguer and Montanari [10] generalize their net morphisms is by permitting a single event in the source net to map to a “computation” of the target net. In fact, in [18], Winskel also generalizes his morphisms to permit an event to be mapped to a multiset of events rather than a single event. This corresponds to a sort of refinement operation. It would be interesting to see if such an idea could be transported to our setup—this would also require us to define a more sophisticated notion of transition system morphism.

As we had mentioned in the introduction, our work is a generalization of the results described in [14] dealing with elementary net systems. In addition, Winskel and Nielsen [20] have established a similar result relating a subclass of asynchronous transition systems to 1-safe Petri nets.

By tuning our regions appropriately, we can fit the results of [14] and [20] neatly into our framework [12]. To begin with, for a region r, we can restrict the range of r_{Q} to {0, 1} and the range of r_{E} to {(0, 0), (0, 1), (1, 0), (1, 1)}. If we enforce the regional axioms (A3) and (A4) for step transition systems in terms of this restricted class of regions, we obtain a full subcategory of PNts consisting of safe PN-transition systems, which corresponds to 1-safe Petri nets. For all transition systems in this subcategory, it turns out that the steps in the transition relation consist of only sets of events and not multisets because autoconcurrency is ruled out.

Winskel and Nielsen have established a coreflection between a subcategory of asynchronous transition systems and safe nets [20]. In an asynchronous transition system, information about concurrency is incorporated in terms of a binary independence relation on the events, rather than by adding structure to the labels of the transitions as we have done here. At first sight, it appears that the category of safe PN-transition systems should coincide with the subcategory of asynchronous transition systems studied in [20]. However, we can show that there is only a coreflection between these two categories [12], indicating that asynchronous transition systems are a slightly more “concrete” model than safe PN-transition systems (though still a more abstract model than safe nets). This “concreteness” arises from the fact that the independence relation can specify that two events are concurrent in an asynchronous transition system even when there is no state at which the concurrency is actually exhibited in the behaviour of the system.

By further restricting the range of r_{E} to exclude (1, 1), we obtain a full subcategory of PNts called elementary PN-transition systems, corresponding to elementary net systems. In [12], we establish an equivalence between our category of elementary PN-transition systems and the category of elementary net systems of Nielsen, Rozenberg and Thiagarajan [14]. Since elementary transition systems are a subclass of conventional sequential transition systems, this categorical equivalence offers an alternative proof of the result of Hoogeboom and Rozenberg [6]

Elementary net systems  Safe nets  ↪  Petri nets
⇑
⇑

Asynchronous transition systems (Winskel, Nielsen)

⇑
⇑

Elementary PN-transition systems

↪

Safe PN-transition systems

↪

PN-transition systems

≅

Elementary transition systems (Nielsen, Rozenberg, Thiagarajan)

Figure 11: Relating various models for concurrency

that for elementary transition systems, no information about concurrency is lost by restricting one’s attention to sequential transition systems.

The relationship between these different models is summarized in Figure 11. The vertical arrows (⇑) indicate coreflections; the arrow indicates the direction of the left adjoint.

It also turns out that if we are interested only in the sequential behaviour of Petri nets, we can characterize Petri nets using conventional transition systems. Suppose we consider purely sequential transition systems (thereby restricting our attention to the sequential firing sequences of Petri nets). We then get an obvious sequential definition of a region and we can impose the corresponding regional axioms to obtain a category of sequential PN-transition systems. Somewhat surprisingly, it turns out that we can establish a coreflection between this category of sequential PN-transition systems and the category PNet[12]. In this setup, every net P N will have a canonical representation TN ∘ NT(N) which is purely sequential—i.e. there will be a place s in TN ∘ NT(N) such that for every transition t in TN ∘ NT(N), W (s, t) = W (t, s) = 1.

The observation that we can use both sequential and step transition systems to characterize Petri nets seems to indicate that we can use objects like PN-transition systems to bridge the gap between interleaving and non-interleaving models of concurrency in a smooth way.

We conclude by pointing out a major issue which we have ignored in our study— that of labelling. In the theory of Petri nets, abstraction is achieved by adding a set of labels which can be associated with the underlying events of the system. This is crucial for using nets to provide, say, a semantics for CCS-like langages. In [20], labelling is introduced into the categorical treatment of different models of concurrency by means of fibrations and cofibrations. Though they point out some problems in defining these constructions over categories of nets, it does not seem to prevent the coreflection between unlabelled transition systems and unlabelled nets from being extended to the corresponding labelled categories. So, while we have not explicitly handled labelling in our framework, we are confident that we can follow the route set out in [20] without too much difficulty.

Acknowledgments P. S. Thiagarajan’s suggestions and criticism have greatly influenced the formulation and presentation of this work. I also thank Douglas Gurr, Peter Hoogers, Jetty Kleijn, Mogens Nielsen, Vladimiro Sassone and Glynn Winskel, as well as an anonymous referee, for constructive comments on preliminary versions of this work.

Part of the work reported here was done while visiting the Computer Science Department, Aarhus University, Denmark. The author’s stay in Denmark was supported by a grant from the Aarhus University Research Foundation.

References

1. M.A. Bednarczyk, “Categories of Asynchronous Systems”, PhD Thesis, Report 1/88, Computer Science, University of Sussex, Brighton, UK (1988).

2. C. Brown, D. Gurr, “A Categorical Linear Framework for Petri Nets”, Proc. 5th Ann. IEEE Symp. on Logic in Computer Science, Philadelphia, USA, 1990, pp. 208–218.

3. P. Degano, R. de Nicola, U. Montanari, “A Distributed Operational Semantics for CCS based on Condition/Event Systems”, Acta Inf. 26 (1988) 59–91.

4. A. Ehrenfeucht, G. Rozenberg, “Partial 2-structures; Part II, State Spaces of Concurrent Systems”, Acta Inf. 27 (1990) 348–368.

5. P. Hoogers, H.C.M. Kleijn, P.S. Thiagarajan, “A Trace Semantics for Petri Nets”, Report 92-03, Department of Computer Science, Leiden University, Leiden, The Netherlands (1992) (extended abstract appears in Proc. ICALP ’92).

6. H.J. Hoogeboom, G. Rozenberg, “Diamond Properties of Elementary Net Systems”, Fund. Inf. XIV (1991) 287–300.

7. K. Lodaya, R. Ramanujam, P.S. Thiagarajan, “A Logic for Distributed Transition Systems”, Springer Lect. Notes in Comput. Sci. 354 (1989) 508–522.

8. S. Mac Lane, Categories for the Working Mathematician, (Springer-Verlag, New York/Berlin, 1971).

9. R. Milner, Communication and Concurrency, (Prentice-Hall, London, 1989).

10. J. Meseguer, U. Montanari, “Petri Nets are Monoids”, Inf. Comput. 88 (1990) 105– 155.

11. M. Mukund, “A Transition System Characterization of Petri Nets”, Report TCS-91-2, School of Mathematics, SPIC Science Foundation, Madras, India (1991).

12. M. Mukund, “Transition System Models for Concurrency”, Report DAIMI-PB-399, Computer Science Department, Aarhus University, Aarhus, Denmark (1992).

13. M. Mukund, M. Nielsen, “CCS, Locations and Asynchronous Transition Systems”, Report DAIMI-PB-395, Computer Science Department, Aarhus University, Aarhus, Denmark (1992).

14. M. Nielsen, G. Rozenberg, P.S. Thiagarajan, “Elementary Transition Systems”, Theor. Comput. Sci. 96(1)(1992) 3–33.

15. E.-R. Olderog, Nets, Terms and Formulas, (Cambridge University Press, Cambridge, 1991).

16. W. Reisig, Petri Nets, (Springer-Verlag, Berlin, 1985).

17. M.W. Shields, “Concurrent Machines”, Computer Journal, 28 (1985) 449–465.

18. G. Winskel, “Petri Nets, Algebras, Morphisms and Compositionality”, Inf. Comput. 72 (1987) 197–238.

19. G. Winskel, “Event Structure Semantics of CCS and Related Languages”, Springer Lect. Notes in Comput. Sci., 140 (1982) 561–577.

20. G. Winskel, M. Nielsen, “Models for Concurrency”, (to appear in S. Abramsky, D.M. Gabbay, T.S.E. Maibaum eds., Handbook of Logic in Computer Science).