Internal Report  TCS-92-3

November, 1992

Transition System Models for Concurrency

Madhavan Mukund^{1} School of Mathematics SPIC Science Foundation 92, G.N. Chetty Road, T. Nagar Madras 600 017, India

                  E-mail: madhavan@ssf.ernet.in

Abstract

Labelled transition systems can be extended to faithfully model concurrency by permitting transitions between states to be labelled by a collection of actions, denoting a concurrent step. We can characterize a subclass of these step transition systems, called PN-transition systems, which describe the behaviour of Petri nets. This correspondence is formally described in terms of a coreflection between a category of PN-transition systems and a category of Petri nets.

In this paper, we show that we can define subcategories of PN-transition systems whose objects are safe PN-transition systems and elementary PN-transition systems such that there is a coreflection between these subcategories and subcategories of our category of Petri nets corresponding to safe nets and elementary net systems.

We also prove that our category of elementary PN-transition systems is equivalent to the category of (sequential) elementary transition systems defined by Nielsen, Rozenberg and Thiagarajan, thereby establishing that the concurrent behaviour of an elementary net system can be completely recovered from a description of its sequential behaviour.

Finally, we establish a coreflection between our category of safe PN-transition systems and a subcategory of asynchronous transition systems which has been shown by Winskel and Nielsen to be closely linked to safe nets.

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

This report is also published as DAIMI-PB-399, Computer Science Department, Aarhus University, Aarhus, Denmark.

1 Introduction

Labelled transition systems provide a simple and convenient framework for abstractly describing the behaviour of computing systems. Their main shortcoming from the point of view of describing concurrent systems is that they are inherently sequential in nature.

We can overcome this limitation by adding some structure to transition systems. One way of doing this is to permit transitions to be labelled by steps, consisting of more than one action [5, 9]. This step transition relation is intended to be read as describing how the system evolves from one state to another by performing (multi)sets of concurrent actions.

In [9], we have shown a close correspondence between a class of step transition systems, called PN-transition systems, and Petri nets [14]. The relationship is described in terms of a coreflection between a category of PN-transition systems, called PNts, and a category of Petri nets, called PNet, where the morphisms in the two categories correspond to a notion of one system simulating another. This coreflection shows that we can regard PNtransition systems as a model which captures precisely the class of concurrent behaviours described by Petri nets, while abstracting away from the structural information associated with nets.

In this paper, we define subcategories of PNts which correspond to some interesting classes of behaviours and relate these subclasses of PN-transition systems to other models of concurrent systems. In particular, we show that we can identify natural subclasses of PN-transition systems which correspond to two widely studied classes of nets, safe nets and elementary net systems.

The first observation we make in this paper is that the choice of using sequential or step transition systems to describe Petri nets depends on how detailed a description one wants of system behaviour. It turns out that we can characterize in a precise way the sequential transition systems correponding to Petri nets in terms of a coreflection between the full subcategory of PNts whose objects are sequential PN-transition systems and the category PNet of Petri nets.

Next, we turn to the question of representing the behaviour of safe nets in terms of step transition systems. Petri nets are a very general model for describing concurrent systems. To obtain a tractable theory of their behaviour, one often looks at a restricted class of nets called safe nets. Safe nets are very “well-behaved” and have given rise to a rich theory. In particular, we note that there are strong connections between the theory of safe nets, trace languages [7] and event structures [11, 17].

To identify a subcategory of PNts corresponding to safe nets, we further refine the concept of a region. Regions play a key role in establishing the coreflection between PNts and PNet. They were originally defined in the context of sequential transition systems by Ehrenfeucht and Rozenberg [3] as a transition system counterpart of the notion of a condition in an elementary net system. Using regions, they characterized the class of sequential transition systems which represent the behaviour of elementary net systems. To define PN-transition systems, the notion of a region is generalized in [9] to capture the transition system counterpart of a place of a Petri net. Here, we show that we can “tune” the notion of a region to identify a full subcategory SPNts of safe PN-transition systems so that there is a coreflection between SPNts the full subcategory SNet of PNet whose objects are safe nets.

We then turn our attention to elementary net systems. In [12], Nielsen, Rozenberg and Thiagarajan exploit the regions defined in [3] to establish a coreflection between a class of sequential transition systems called elementary transition systems and elementary net systems. Here we show how to describe a full subcategory of elementary PN-transition systems which is equivalent to the category of elementary transition systems defined in [12]. This equivalence provides an alternative proof of the result, established by Hoogeboom and Rozenberg [4], that for elementary net systems, no information about concurrency is lost by restricting one’s attention to sequential transition systems.

Enriching the transition relation to include steps as labels is not the only way of introducing additional structure into transition systems to faithfully describe concurrency. Another possibility is to retain a sequential transition relation, and add a relation which explicitly specifies which underlying events in the system are independent of each other. This is the approach taken in defining asynchronous transition systems [1, 15].

In [19], Winskel and Nielsen establish a coreflection between a category Ats_{0} of asynchronous transition systems and a category of safe nets. From this, it would appear that safe PN-transition systems are closely related to asynchronous transition systems. In fact, we establish a coreflection between our category of safe PN-transition systems and the subcategory Ats_{0} of asynchronous transition systems defined in [19].

The reason this correspondence is a coreflection and not an equivalence is to do with the role played by the independence relation in an asynchronous transition system. It turns out that this relation also incorporates some “structural” information about the system, in addition to information about concurrency. So, in a sense, asynchronous transition systems are a more abstract model than nets but a more concrete model than safe PN-transition systems.

Another point concerning this correspondence between safe PN-transition systems and asynchronous transition systems is that the category of safe nets that we work with is slightly different from the category of safe nets that Winskel and Nielsen work with. However, it turns out that we can establish an adjunction between these two categories of safe nets. This correspondence can be strengthened when we restrict our attention to saturated nets, which are those nets constructed out of transition systems using regions.

The main results of this paper are summarized in Figures 1 and 2. In the diagrams, a double arrow ⇒ represents a coreflection. The arrow indicates the direction of the left adjoint.

The first diagram describes the correspondence between subclasses of PN-transition systems and subclasses of nets. The vertical arrows represent inclusions. For each pair of categories connected by a vertical arrow, the lower category is a full subcategory of the category immediately above. In the bottom row, we have indicated that the category of elementary PN-transition systems is equivalent to both the subcategory of sequential elementary PN-transition systems and to the category of elementary transition systems defined in [12].

In the second diagram, we show the correspondence between safe PN-transition systems and asynchronous transition systems. We also show the adjunction between our category of safe nets and the category of safe nets described in [19], where the right adjoint is the inclusion functor.

The paper is organized as follows. In the next two sections we briefly review some terminology and basic results concerning the categories PNet (of Petri nets) and PNts (of PN-transition systems) defined in [9]. In Section 4 we describe the coreflection between PNts and PNet. In the next section, we characterize the sequential behaviours of Petri nets. Section 6 describes the subcategory of PNts corresponding to safe nets. In Section 7 Sequential PN-transition

systems

⇒

PN-transition systems

⇒

Petri nets

↑  ↑  ↑

Sequential

safe PN-transition

systems

⇒

Safe PN-transition systems

⇒

Safe nets

↑  ↑

Elementary transition systems ≅ Sequential elementary PN-transition

systems

≅

Elementary PN-transition systems

⇒

Elementary net systems

Figure 1: Subclasses of PN-transition systems

Safe  Asynchronous
PN-transition ⇒  transition
systems  systems
⇓  ⇓
Safe  →  Safe nets
nets  ↩^{⊥} (Winskel and Nielsen)

Figure 2: The connection to asynchronous transition systems we describe a subcategory of PNts which is equivalent to the category of elementary transition systems defined in [12]. We relate our category of safe PN-transition systems to Winskel and Nielsen’s category of asynchronous transition systems in Section 8. The next section describes the correspondence between the two different categories of safe nets defined here and in [19]. We conclude with a discussion of the results presented here.

A word about notation—the definition of PN-transition systems uses multisets quite extensively. We describe the notation and terminology we use for multisets in the Appendix.

2 Petri nets

We begin with 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 [14].

Definition 2.1 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 such that ∀t ∈ T. ∃s ∈ S. W (s, t) > 0.

• 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}. For x ∈ S ∪ T, let •x^{•} = ^{•}x ∪ x^{•}. Notice that we have insisted that ^{•}t be nonempty for each t ∈ T.

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

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

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))

If ^{•}t = ∅, it is clear that unboundedly large steps consisting of copies of t will be enabled at any reachable marking. This is a fairly undesirable phenomenon and prompts the restriction we have made that every transition have an input place. This restriction was not present in the nets considered in [9]. We shall say more on this in Section 4.

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

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

Using ⇒_{P N}, we can associate with P N an obvious transition system T S_{P N} whose states are the reachable markings of P N and whose transition relation is labelled by multisets. We shall formally define such step transition systems in the next section.

Here, we proceed by constructing a category of Petri nets. To do so, we have to define a suitable notion of morphism.

Definition 2.2 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).

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

Let PNet be the category whose objects are Petri nets and whose arrows are net morphisms as defined above.

We conclude this section with a result showing that net morphisms preserve concurrent behaviour in a strong way. The proof of this result is given in [9].

Lemma 2.3 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}}.

3 PN-transition systems

A labelled 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. We can then 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”.

Definition 3.1 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 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 three basic restrictions on transition systems. First, we 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. Finally, we insist that there be no unbounded autoconcurrency in the system. Formally, we have the following basic axioms.

(A1) ∀q, q′ ∈ Q. q \underrightarrow{O_{E}} q′ iff q = q′ (where O_{E} is the empty multiset over E).

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

(A3) ∀q ∈ Q. ∀e ∈ E. ∃k ∈ N_{0}. (q, u, q′) ∈ → implies u(e) < k.

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

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

q →^{u} q.

(A3) corresponds to the restriction we have placed on nets that each transition have an input place. Notice that no global bound is placed on autoconcurrency—all (A3) says is that autoconcurrency is locally bounded at each state in the transition system.

To describe PN-transition systems, we need to introduce the notion of a region. Regions were originally defined in the context of elementary transition systems in [3] and exploited to define a coreflection between elementary transition systems and elementary net systems in [12]. Here we generalize the regions of [3, 12] to describe the transition system counterpart of a place of a Petri net.

Definition 3.2 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} 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′) ∈ → . r_{Q}(q) ≥ ∑_{e∈E} u(e) ·^{r}e andr_{Q}(q′) = r_{Q}(q) + ∑_{e∈E} u(e) · (e^{r} −^{r}e).

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). If ^{r}e > 0, we say that r is a preregion of e and if e^{r} > 0, we say that r is a postregion of 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, we can associate an “obvious” transition system T S_{P N}, with states corresponding to the reachable markings of P N, events to the transitions of P N and the step transition relation defined by ⇒_{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 3.3 Let T S = (Q, E, →, q_{in}) be a step transition system. A region r is nontrivial 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):

(A4) Let q, q′ ∈ Q. q ≠ q′ ⇒ ∃r ∈ R_{T S}. r(q) ≠ r(q′). (Separation)

(A5) ∀q ∈ Q. ∀u ∈ MS_{fin}(E). If there does not exist q′ ∈ Q such that q →^{u} q′, then

∃r ∈ R_{T S}. r(q) < ∑_{e∈E} u(e) ·^{r}e. (Enabling)

Axiom (A4) says that any pair of distinct states in Q will be distinguished by at least one (non-trivial) region. Axiom (A5) captures the fundamental idea underlying the dynamic behaviour of a Petri net. It says that 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. In other words, 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.

Definition 3.4 A PN-transition system is a step transition system T S = (Q, E, →, q_{in}) which satisfies axioms (A4) and (A5) (in addition to the basic axioms (A1) to (A3)).

We now state a couple of useful properties of PN-transition systems which are formally established in [9].

The first 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 3.5 Every PN-transition system is deterministic.

The second observation is that every step in a PN-transition system can be broken up into substeps in a consistent way. This shows that steps do indeed reflect concurrency in a natural way.

Proposition 3.6 Let T S = (Q, E, →, q_{in}) be a PN-transition system and let q →^{u} q′ in T S. Then

∀v ⊆_{MS} u. ∃q_{v} ∈ Q. q →^{v} q_{v} and q_{v} ⟶^{u−v} q′.

To construct a category of PN-transition systems, we now define morphisms between PN-transition systems. These are standard transition system morphisms as defined, say, in [12, 19], extended to respect steps.

Definition 3.7 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′).

PN-transition systems with transition system morphisms form a category, which we shall call PNts.

4 Relating Petri nets and PN-transition systems

There is a natural way to define a functor NT from PNet to PNts.

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

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

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

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 ϕ be a net morphism from P N_{1} to P N_{2}. Then, NT(ϕ) = f^{ϕ} is defined as follows.

• ∀t ∈ T_{1}. f^{ϕ}(t) = ϕ(t).

• ∀M ∈ [M_{in}^{1}⟩. f^{ϕ}(M) = M_{ϕ} (where M_{ϕ} is the map defined in Lemma 2.3).

The main result established in [9] is the existence of a left adjoint to this functor.

Theorem 4.1 There exists a functor TN : PNts → PNet such that TN is left adjoint to NT.

The unit of the adjunction in fact turns out to be a natural isomorphism, so there is actually a coreflection between this pair of functors.

We shall not describe TN in any detail. The main idea is that a PN-transition system can be transformed into a Petri net by regarding events as the transitions of the net and regions as the places of the net.

A remark is in order at this point about the categories PNts and PNet and the coreflection that we have defined here. In the original formulation of the coreflection between PN-transition systems and Petri nets in [9], no assumption was made about transitions in a net having input places. Correspondingly, the axiom (A3) that we have introduced for PN-transition systems was not present.

It is quite clear that for any net PN = (S, T, W, M_{in}), if every t ∈ T has an input place, then T S_{P N} will satisfy axiom (A3). It is not difficult to prove the converse—if T S = (Q, E, →, q_{in}) satisfies (A3), then for every e ∈ E there exists an r ∈ R_{T S} such that re > 0 and so TN(T S) will have an input place for each transition.

The coreflection that is established in [9] continues to hold when we restrict TN and NT to the categories we have defined here. The reason we have chosen to work in this more restrictive framework is that here we will be dealing mainly with special classes of nets, like safe nets, which do not exhibit any autoconcurrency under “normal circumstances”. So, for these classes of nets, it is reasonable to demand that we abolish the unbounded autoconcurrency generated by transitions with no input places.

5 Sequential PN-transition systems

PN-transition systems faithfully record the concurrent behaviour of Petri nets by means of transitions labelled with multisets of events.

However, it turns out that we can also characterize the transition systems corresponding to the purely sequential behaviour of Petri nets.

For convenience, we shall define sequential transition systems as special cases of step transition systems.

Definition 5.1 Let T S = (Q, E, →, q_{in}) be a step transition system. T S is sequential iff T S satisfies axioms (A1) to (A3) and, further,

∀(q, u, q′) ∈ → . |u| ≤ 1.

In other words, a sequential transition system can have steps labelled either by single events, or by O_{E}, corresponding to the idling transition at each state.

Definition 5.2 Let T S = (Q, E, →, q_{in}) be a transition system. T S is a sequential PNtransition system if it is sequential and, further, it satisfies the two axioms (A4) and (A5) for PN-transition systems.

It is clear that any sequential PN-transition system is also a (normal) PN-transition system. In fact, we can define a full subcategory SeqPNts whose objects are sequential PN-transition systems and whose arrows are transition system morphisms.

It is not difficult to prove the following.

Theorem 5.3 SeqPNts is a coreflective subcategory of PNts.

Proof To establish this, we have to show that the inclusion functor from SeqPNts to PNts has a right adjoint. The right adjoint is the functor which forgets concurrency.

More formally, define U : PNts → SeqPNts to be the functor which maps a PNtransition system T S = (Q, E, →, q_{in}) to a sequential PN-transition system T S′ = (Q, E, →′, q_{in}), where

→′= {(q, u, q′) | q →^{u} q′ and |u| ≤ 1}.

For each transition system morphism f : T S_{1} → T S_{2} in PNts, U(f) : U(T S_{1}) → U(T S_{2}) is the map such that U(f)_{Q} = f_{Q} and U(f)_{E} = f_{E}.

It is straightforward to verify that U is in fact right adjoint to the inclusion functor. We omit the details. □

So, by composing the inclusion functor with the functor TN : PNts → PNet we obtain a functor which is left adjoint to the functor U∘NT taking nets to their sequential marking diagrams.

We can also characterize sequential PN-transition systems directly in terms of regions.

Proposition 5.4 Let T S = (Q, E, →, q_{in}) be a PN-transition system. T S is sequential iff r_{seq} ∈ R_{T S}, where r_{seq} is defined as follows:

∀q ∈ Q. r_{seq}(q) = 1.

∀e ∈ E. r_{seq}(e) = (1, 1).

Proof It is easy to see that if T S is sequential, r_{seq} is in fact a region. Conversely, if r_{seq} is a region in R_{T S}, clearly for each transition q →^{u} q′ in T S, |u| ≤ 1 and so T S is sequential. □

In the net TN(T S) corresponding to the sequential PN-transition system T S, r_{seq} will be a place marked at the initial marking and connected to all transitions by self-loops, ensuring that the net exhibits no concurrency in its behaviour.

6 Safe nets

Petri nets can exhibit very complex behaviours which are difficult to characterize globally. To obtain a mathematically tractable theory, one often looks at restricted classes of nets.

In this regard, one very important subclass of nets is the class of safe nets. In general, a Petri net PN = (S, T, W, M_{in}) is said to be k-safe if M(s) ≤ k for every reachable marking M ∈ [M_{in}⟩. Call P N a safe net if it is 1-safe.

Thus, in a safe net, every reachable marking is a set, rather than a multiset of places. Let PN = (S, T, W, M_{in}) be a safe net. For any transition t ∈ T, if there is a place s ∈ ^{•}t such that W (s, t) > 1, then t will never be enabled. Similarly, if there is a place s ∈ t^{•} such that W (t, s) > 0, t can never occur because after t occurs, s would be unsafe. So, it makes sense to restrict W to values from {0, 1} instead of the entire range N_{0}.

With this in mind, we define safe nets in terms of our general definition of Petri nets as follows.

Definition 6.1 Let PN = (S, T, W, M_{in}) be a Petri net. Then P N is a safe net provided

(i) ∀s ∈ S. ∀t ∈ T. W (s, t) ≤ 1 and W (t, s) ≤ 1.

(ii) ∀M ∈ [M_{in}⟩. ∀s ∈ S. M(s) ≤ 1.

Let SNet be the full subcategory of PNet whose objects are safe nets. We can restrict the functor NT to a functor SNT : SNet → PNts.

We now want to identify a subcategory SPNts of PNts such that there is a coreflection between STN : SPNts → SNet and SNT : SNet → SPNts.

For this, we define 0/1-regions.

Definition 6.2 Let T S = (Q, E, →, q_{in}) be a step transition system. Then r = (r_{Q}, r_{E}) is a 0/1-region of T S if r is a region and

∀q ∈ Q. r_{Q}(q) ≤ 1.

∀e ∈ E. ^{r}e ≤ 1 and e^{r} ≤ 1.

Let R_{T S}^{0/1} = {r ∈ R_{T S} | r is a 0/1-region }.

We can then modify the regional axioms (A4) and (A5) to refer only to 0/1-regions.

(A4’) Let q, q′ ∈ Q. q ≠ q′ ⇒ ∃r ∈ R_{T S}^{0/1}. r(q) ≠ r(q′). (Separation)

(A5’) ∀q ∈ Q. ∀u ∈ MS_{fin}(E). If there does not exist q′ ∈ Q such that q →^{u} q′, then

∃r ∈ R_{T S}^{0/1}. r(q) < ∑_{e∈E} u(e) ·^{r}e. (Enabling)

Definition 6.3 A safe PN-transtion system is a step transition system T S = (Q, E, →, q_{in}) which satisfies axioms (A4’) and (A5’) (in addition to the basic axioms (A1) to (A3)).

Let SPNts be the full subcategory of PNts whose objects are safe PN-transition systems.

As we had mentioned in Section 2, in general we need to consider steps labelled by multisets rather than sets in order to deal with autoconcurrency. Clearly, a safe net cannot exhibit autoconcurrency. So, since safe PN-transition systems are supposed to describe the behaviour of safe nets, it is not surprising that we have the following.

Proposition 6.4 Let T S = (Q, E, →, q_{in}) be a safe PN-transition system. Then for every transition q →^{u} q′ in T S, u is a set.

Proof Let e ∈ u. It suffices to show that there is a 0/1-region r such that ^{r}e = 1.

By (A3) we know that autoconcurrency is bounded. In other words, at each state q, there is some k ∈ N_{0} such that the step consisting of k occurrences of e is not enabled. By (A5’) there is a 0/1-region r such that r(q) < k ·^{r}e. It is clear that ^{r}e must be 1, and so we are done. □

We now establish that the transition system T S_{P N} associated with a safe net P N is in fact a safe PN-transition system.

Lemma 6.5 Let PN = (S, T, W, M_{in}) be a safe net. Then T S_{P N} = ([M_{in}⟩, T, ⇒_{P N}, M_{in}) is a safe PN-transition system.

Proof It is straightforward to show that T S_{P N} satisfies the three basic axioms (A1) to (A3) for step transition systems. So, what we have to show is that axioms (A4’) and (A5’) are true as well.

For each s ∈ S, we can define a region r_{s} in T S_{P N} as follows.

∀M ∈ [M_{in}⟩. r_{s}(M) = M(s).

∀t ∈ T. r_{s}(t) = (W (s, t), W (t, s)). It is not difficult to establish that r_{s} is a region, and, in fact is a 0/1-region. r_{s} will be non-trivial provided s is not isolated in P N (i.e. there is some t ∈ T such that s ∈ ^{•}t or s ∈ t^{•}.)

It then immediately follows that T S_{P N} satisfies (A4’). Given any 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 0/1-region of T S_{P N} separating M from M′.

Next consider (A5’). Suppose M ∈ [M_{in}⟩ and u ∈ MS_{fin}(T), and there is no M′ such that M →^{u} M′. Then, at the marking M ∈ [M_{in}⟩, u is not enabled. By the firing rule for Petri nets, this implies that there is some s ∈ S such that M(s) < ∑_{t∈u} W (s, t). Clearly, r_{s} is then a non-trivial 0/1-region such that r_{s}(M) < ∑_{t∈u} ^{r_{s}}t and we are done. □

Given a pair of safe nets PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, and a net morphism ϕ : P N_{1} → P N_{2}, for each M ∈ [M_{in}^{1}⟩ we can define a marking M_{ϕ} ∈ [M_{in}^{2}⟩ as in Lemma 2.3. That is

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

We can then define SNT : SNet → SPNts as follows:

• Let PN = (S, T, W, M_{in}) be a safe net. Then SNT(P N) = ([M_{in}⟩, T, ⇒_{P N}, M_{in}).

• Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be a pair of safe nets and ϕ : P N_{1} → P N_{2} a net morphism. Then SNT(ϕ) : SNT(P N_{1}) → SNT(P N_{2}) is given by:

– ∀t ∈ T_{1}. SNT(ϕ)(t) = ϕ(t).

– ∀M ∈ [M_{in}^{1}⟩. SNT(ϕ)(M) = M_{ϕ}.

It is easy to check the following.

Proposition 6.6 SNT : SNet → SPNts is a functor.

We can construct a functor STN : SPNts → SNet which is left adjoint to SNT. We first define STN_{0}, a map on objects from SPNts to SNet.

Let T S = (Q, E, →, q_{in}) be a safe PN-transition system. Then

STN_{0}(T S) = (R_{T S}^{0/1}, 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}^{0/1} and e ∈ E, and M_{in}^{T S}(r) = r(q_{in}) for each r ∈ R_{T S}^{0/1}.

Theorem 6.7 STN_{0} extends to a functor STN : SPNts → SNet such that STN is left adjoint to SNT and the unit of the adjunction is a natural isomorphism.

Proof We just sketch the main ideas. The details are similar to those used to establish the coreflection between TN and NT and can be filled in from [9].

We can first establish that for each safe PN-transition system T S, there is a transition system isomorphism η_{T S} : T S → SNT ∘ STN_{0}(T S). This map will serve as the unit of the adjunction.

Suppose that T S ∈ SPNts and P N ∈ SNet such that there is a transition system morphism f : T S → SNT(P N). Then, we can establish that there is a unique morphism ϕ : STN_{0}(T S) → P N such that f = SNT(ϕ) ∘ η_{T S}.

Given this, if follows (according to [6]), that STN_{0} can be extended uniquely to a functor STN : SPNts → SNet which is left adjoint to SNT. □

7 Elementary transition systems

Next, we look at one of the basic models of net theory, elementary net systems. In [12], Nielsen, Rozenberg and Thiagarajan establish a coreflection between a class of transition systems called elementary transition systems and elementary net systems.

In many ways, that result is the starting point of the work reported here. In this section, we define a subcategory of PNts whose objects are elementary PN-transition systems, which corresponds to the category of elementary transition systems of [12]— that is, there is an equivalence between these two categories.

We begin by describing elementary net systems. This will motivate the axioms we need to put on PN-transition systems to define elementary PN-transition systems.

Rather than try and define elementary net systems in terms of general Petri nets, we start from scratch and provide the standard definition (see, for instance, [16]).

We begin with the definition of a net.

Definition 7.1 A net is a triple N = (S, T, F) where:

(i) S is a set of S-elements and T is a set of T -elements, such that S ∩ T = ∅.

(ii) F ⊆ (S ×T)∪(T ×S) is the flow relation such that ∀x ∈ S ∪T. ∃y ∈ S ∪T. [(x, y) ∈ F ∨ (y, x) ∈ F].

Thus a net specifies the underlying structure of a system. The flow relation F corresponds to the {0, 1}-valued weight function we defined for safe nets. We use ^{•}x, x^{•} and •x^{•} to denote the neighbourhood of x ∈ S ∪ T, as usual.

Normally, the S-elements are called conditions and denoted by B and the T -elements are called events and denoted by E. Here, we shall stick to S and T to remain consistent with the notation for nets used so far.

Definition 7.2 An elementary net system is a quadruple ENS = (S, T, F, c_{in}) where

(i) (S, T, F) is a net, called the underlying net of ENS.

(ii) c_{in} ⊆ S is the initial case.

Thus, the initial case corresponds to an initial marking in a safe net. The essential difference between an elementary net system and a safe net is in the firing rule. Let c, c′ ⊆ S be cases of an elementary net system and t ∈ T be an event. Then

c →^{t} c′ =^{def} c − c′ = ^{•}t ∧ c′ − c = t^{•}

Thus, in an elementary net system, an event cannot occur at a case where its postconditions are not empty. This means that an event which is connected to a condition by a self-loop will be permanently disabled.

Given the transition relation defined above, we can define [c_{in}⟩, the set of cases reachable from c_{in}, in the same way that we defined [M_{in}⟩ for Petri nets. We can then associate a sequential transition relation →_{ENS} with an elementary net system ENS = (S, T, F, c_{in}) in the obvious way:

→_{ENS}= {(c, t, c′) | c, c′ ∈ [c_{in}⟩ and c →^{t} c′}

We can extend this sequential transition relation to a step transition relation between cases. As in a safe net, a set of transitions is concurrently enabled at a case provided each individual transition is enabled and the neighbourhoods of the transitions are pairwise disjoint.

⇒_{ENS}= \{c, u, c′ | \begin{matrix}c, c′ ∈ [c_{in}⟩, u = \{t_{1}, t_{2}, …, t_{n}\}, \\ ∃c_{1}, c_{2}, …, c_{n}. ∀i ∈ \{1, 2, …, n\}. c →^{t_{i}} c_{i}, and \\ ∀i, j ∈ \{1, 2, …, n\}. i ≠ j implies ^{•}t_{i}^{•} ∩^{•}t_{j}^{•} = ∅\} \end{matrix}

So, given an elementary net system ENS = (S, T, F, c_{in}), we can associate with it a sequential transition system ST S_{ENS} = ([c_{in}⟩, T, →_{ENS}, c_{in}) and a step transition system T S_{ENS} = ([c_{in}⟩, T, ⇒_{ENS}, c_{in}).

In [3], Ehrenfeucht and Rozenberg gave a characterization of the sequential transition systems arising from elementary net systems. In [12], this characterization was extended to a coreflection between these elementary transition systems and elementary net systems.

Here we shall show how to characterize the step transition systems corresponding to elementary net systems as a suitable subclass of PN-transition systems. We shall then establish a categorical equivalence between our elementary PN-transition systems and elementary transition systems.

We begin by defining elementary regions.

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

∀q ∈ Q. r(q) ≤ 1.

∀e ∈ E. r(e) ∈ {(0, 1), (1, 0), (0, 0)}.

Let R_{T S}^{E} denote the set of all non-trivial elementary regions of T S.

Thus an elementary region is a 0/1-region with the constraint that r(e) ≠ (1, 1) for any event e. As before, we modify the regional axioms (A4) and (A5) to refer only to elementary regions. We also explicitly add the condition that every e ∈ E have an occurrence.

(A4”) Let q, q′ ∈ Q. q ≠ q′ ⇒ ∃r ∈ R_{T S}^{E}. r(q) ≠ r(q′). (Separation)

(A5”) ∀q ∈ Q. ∀u ∈ MS_{fin}(E). If there does not exist q′ ∈ Q such that q →^{u} q′, then

∃r ∈ R_{T S}^{E}. r(q) < ∑_{e∈E} u(e) ·^{r}e. (Enabling)

(A6”) ∀e ∈ E. ∃q →^{u} q′. e ∈ u.

Definition 7.4 An elementary PN-transition system is a step transition system T S = (Q, E, →, q_{in}) which satisfies axioms (A4”) to (A6”) in addition to the basic axioms (A1) to (A3).

Let EPNts be the full subcategory of PNts whose objects are elementary PN-transition systems. As with safe PN-transition systems, it is easy to show that all steps in an elementary transition system consist of sets of events rather than multisets.

We want to establish a categorical equivalence between the subcategory EPNts and the category of elementary transition systems defined in [12]. In order to do this, we first have to describe elementary transition systems.

Elementary transition systems are defined as a subclass of “conventional” sequential transition systems (as opposed to the sequential versions of step transition systems which we defined Definition 5.1).

Definition 7.5 A transition system is a quadruple ST S = (Q, E, →, q_{in}) where

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

• E is a set of events.

• → ⊆ Q × E × Q is the transition relation.

The next thing to do is to define regions on these transition systems.

Definition 7.6 Let ST S = (Q, E, →, q_{in}) be a transition system. A simple region is a subset ρ ⊆ Q such that:

(i) q →^{t} q′ ∧ q ∈ ρ ∧ q′ ∉ ρ ⇒ ∀q_{1} →^{t} q′_{1} in ST S. [q_{1} ∈ ρ ∧ q′_{1} ∉ ρ]

(ii) q →^{t} q′ ∧ q ∉ ρ ∧ q′ ∈ ρ ⇒ ∀q_{1} →^{t} q′_{1} in ST S. [q_{1} ∉ ρ ∧ q′_{1} ∈ ρ]

ρ is non-trivial if it is not equal to Q or to ∅. Let R_{ST S} denote the set of non-trivial simple regions of ST S.

For e ∈ E, define ρ ∈ ^{•}e if there is a transition q →^{e} q′ in ST S such that q ∈ ρ and q′ ∉ ρ. Similarly, ρ ∈ e^{•} if there is a transition q →^{e} q′ in ST S such that q ∉ ρ and q′ ∈ ρ. As usual, ^{•}e = {ρ ∈ R_{ST S} | ρ ∈ ^{•}e}, e^{•} = {ρ ∈ R_{ST S} | ρ ∈ e^{•}} and ^{•}e^{•} = ^{•}e ∪ e^{•}.

The class of elementary transition systems is then given by the following axioms.

(EA1) ∀q →^{e} q′. q ≠ q′.

(EA2) ∀e ∈ E. ∃q →^{e} q′.

(EA3) ∀q ∈ Q. ∃σ ∈ E^{∗}. (q_{in}, σ, q) ∈ →^{∗}.

(EA4) ∀q, q′ ∈ Q. q ≠ q′ ⇒ ∃ρ ∈ R_{ST S}. q ∈ ρ ⇔ q′ ∉ ρ.

(EA5) ∀q ∈ Q. ∀e ∈ E. If there does not exist q′ such that q →^{e} q′ then ∃ρ ∈ ^{•}e. q ∉ ρ.

The first axiom rules out self loops in the transition system. The other axioms correspond to restrictions we have encountered before. In the formulation of elementary transition systems presented in [12], there is an additional axiom preventing two different transitions between the same pair of states. This amounts to requiring simplicity of the nets one is considering. In [9] we have pointed out that the coreflection between elementary transition systems and elementary net systems holds even without this restriction, so we avoid this additional axiom here.

A morphism between elementary transition systems is, as usual, a total function on the states and a partial function on the events that preserves the transition relation. The only complication is that we do not have idling transitions, so we have to be a bit careful in defining the simulation condition. Once again, the definition we present here is slightly different from the one presented in [12], but is equivalent to their formulation.

Definition 7.7 Let ST S_{i} = (S_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be a pair of transition systems. A morphism f from ST S_{1} to ST S_{2} is pair of maps 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) ∀q →^{e}_{1} q′. If f_{E}(e) is defined, then f_{Q}(q) ⟶^{f_{E}(e)}_{2} f_{Q}(q′). Otherwise, f_{Q}(q) = f_{Q}(q′).

Let ETS denote the category whose objects are elementary transition systems and whose arrows are transition system morphisms as defined above.

In an elementary transition system, every “diamond” represents concurrency. This is stated in a little more generality in the following proposition.

Proposition 7.8 Let ST S = (Q, E, →, q_{in}) be an elementary transition system and {e_{1}, e_{2}, …, e_{n}} ⊆ E, n ≥ 2, be a subset of events in E. Then the following statements are equivalent.

(i) For each i, j ∈ {1, 2, …, n}, i ≠ j implies ^{•}e_{i}^{•} ∩^{•}e_{j}^{•} = ∅

(ii) ∀q ∈ Q. If ∃q_{0}, q_{1}, …, q_{n}. q = q_{0} and q_{i−1} ⟶^{e_{i}} q_{i}, 1 ≤ i ≤ n, then for each permu-

tation π : {1, 2, …, n} → {1, 2, …, n}. ∃q′_{0}, q′_{1}, …, q′_{n} ∈ Q, where q_{0} = q′_{0}, q_{n} = q′_{n}

and q′_{i−1} ⟶^{e_{π(i)}} q′_{i}, 1 ≤ i ≤ n.

Proof ((i) ⇒ (ii)) If the n events have pairwise disjoint neighbourhoods, then they can occur independently. The result is then straightforward, by appealing to axiom (EA5). The proof proceeds by induction on n, the number of pairwise independent events and we omit the details.

((ii) ⇒ (i)) Again, the proof is straightforward, by induction on n.

The base case is when n = 2. So, we have q, q_{1}, q_{2}, q′ ∈ Q and e_{1}, e_{2} ∈ E, such that

q →^{e_{1}} q_{1} →^{e_{2}} q′ and q →^{e_{2}} q_{2} →^{e_{1}} q′.

Consider any ρ ∈ R_{ST S}. Suppose ρ ∈ ^{•}e_{1}. Then, q ∈ ρ and q_{1} ∉ ρ, so, by definition, ρ ∉ ^{•}e_{2}. Similarly, we must have q_{2} ∈ ρ and q′ ∉ ρ, so ρ ∉ e_{2}^{•} either. By a similar argument, if ρ ∈ e_{1}^{•}, ρ ∉ ^{•}e_{2}^{•}.

A symmetric argument shows that ρ ∈ ^{•}e_{2}^{•} implies ρ ∉ ^{•}e_{1}^{•}.

The case n > 2 follows in a straightforward way from the induction hypothesis. We omit the details. □

We now prove some useful properties of elementary PN-transition systems. The first observation is that elementary regions are completely characterized by their value on states.

Proposition 7.9 Let T S = (Q, E, →, q_{in}) be an elementary PN-transition system and r, r′ ∈ R_{T S}^{E}. Then r_{Q} = r′_{Q} implies r = r′.

Proof Consider any e ∈ E. Then, by axiom (A6”) and Proposition 3.6, we know there is some transition q →^{{e}} q′ in T S. From the definition of an elementary region, it is easy to establish that

r(e) = r′(e) = \{ \begin{matrix}(1, 0) & if r(q) = 1 and r(q′) = 0 \\ (0, 1) & if r(q) = 0 and r(q′) = 1 \\ (0, 0) & otherwise \end{matrix}

□

Next, we show that an elementary PN-transition system is free of self-loops labelled by singleton steps.

Proposition 7.10 Let T S = (Q, E, →, q_{in}) be an elementary PN-transition system. Then, there does not exist a transition of the form q ⟶^{{e}} q for any q ∈ Q and e ∈ E.

Proof By appealing to axiom (A3) which locally bounds autoconcurrency, we can deduce that for every e ∈ E, there is an elementary region r such that ^{r}e = 1. It then follows that e^{r} = 0, by the definition of elementary regions. So r(q) cannot be defined consistently for any q such that q →^{{e}} q, and so no such transition can exist in the system. □

We can now define functors Eseq : EPNts → ETS and Estep : ETS → EPNts.

First, we describe Eseq.

• Let T S = (Q, E, →, q_{in}) be an elementary PN-transition system. Then Eseq(T S) =

(Q, E, →′, q_{in}) where

→′= {(q, e, q′) | q →^{{e}} q′}.

• Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be a pair of elementary PN-transition systems and f : T S_{1} → T S_{2} a morphism in EPNts. Then Eseq(f) = f̂ : Eseq(T S_{1}) → Eseq(T S_{2}) is given by:

– ∀q ∈ Q. f̂(q) = f(q).

– ∀e ∈ E. f̂(e) = f(e).

Definition 7.11 Let r ∈ R_{T S}^{E} be a non-trivial elementary region of an elementary PNtransition system T S = (Q, E, →, q_{in}). Then ρ_{r} =^{def} {q ∈ Q | r(q) = 1}.

Proposition 7.12 Let T S = (Q, E, →, q_{in}) be an elementary PN-transition system. Then

(i) ∀r ∈ R_{T S}^{E}. ρ_{r} is an simple region of Eseq(T S).

(ii) ρ_{r} = ρ_{r′} implies r = r′.

Proof Part (ii) follows from Proposition 7.9. The proof of part (i) is straightforward and we omit the details. □

Proposition 7.13 Eseq is a functor.

Proof Given an elementary PN-transition system T S = (Q, E, →, q_{in}), we have to check that Eseq(T S) is an elementary transition system. Axiom (EA1) holds because of Proposition 7.10. (EA2) and (EA3) are satisfied because T S satisfies (A6”) and (A2) respectively. Finally, we come to the regional axioms (EA4) and (EA5). We know that we can find regions in T S satisfying axioms (A4’) and (A5’). By Proposition 7.12, these regions correspond uniquely to regions in Eseq(T S) which would enforce the regional axioms (EA4) and (EA5) in Eseq(T S).

It is then trivial to check that the image of a morphism in EPNts is in fact a morphism in ETS, and we are done. □

To define the functor going the other way, from ETS to EPNts, we implicitly use the result proved in Proposition 7.8.

Let Estep : ETS → EPNts be defined as follows:

• Let ST S = (Q, E, →, q_{in}) be an elementary transition system. Then Estep(ST S) = (Q, E, →′, c_{in}) where

→′ = \{(q, u, q′) | \begin{matrix}u = \{e_{1}, e_{2}, …, e_{n}\} ⊆ E \\ and ∃q_{0}, q_{1}, …, q_{n} ∈ Q. q = q_{0}, q′ = q_{n} \\ such that ∀i ∈ \{1, 2, …, n\}. q_{i−1} →^{e_{i}} q_{i}, \\ where ∀i, j ∈ \{1, 2, …, n\}. i ≠ j ⇒ \\ ^{•}e_{i}^{•} ∩^{•}e_{j}^{•} = ∅\} \end{matrix}

∪ {(q, O_{E}, q) | q ∈ Q}.

• Let ST S_{i} = (S_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be a pair of elementary transition systems and f : ST S_{1} → ST S_{2} a morphism in ETS. Then Estep(f) = f̂ : Estep(ST S_{1}) → Estep(ST S_{2}) is given by:

– ∀q ∈ Q. f̂(q) = f(q).

– ∀e ∈ E. f̂(e) = f(e).

Definition 7.14 Let ρ ∈ R_{ST S} be a non-trivial simple region of an elementary transition system ST S = (Q, E, →, q_{in}). Then r_{ρ} = (r_{ρ_{Q}}, r_{ρ_{E}}), where r_{ρ_{Q}} : Q → {0, 1} and r_{ρ_{E}} : E → {(0, 1), (1, 0), (1, 1)} is defined as follows.

∀q ∈ Q. r_{ρ_{Q}}(q) = 1 iff q ∈ ρ.

∀e ∈ E. r_{ρ_{E}}(e) = \{ \begin{matrix}(0, 1) & if ρ ∈ e^{•} \\ (1, 0) & if ρ ∈ ^{•}e \\ (0, 0) & otherwise \end{matrix}

Proposition 7.15 Let ST S = (Q, E, →, q_{in}) be an elementary transition system. Then

(i) ∀ρ ∈ R_{ST S}. r_{ρ} is an elementary region of Estep(ST S).

(ii) r_{ρ} = r_{ρ′} implies ρ = ρ′.

Proof The proof is straightforward and we omit the details. The main condition we have to check for part (i) is that r_{ρ} permits all the steps we have introduced, and this follows directly from Proposition 7.8. Part (ii) follows from Proposition 7.9. □

Proposition 7.16 Estep is a functor.

Proof For an elementary transition system ST S = (Q, E, →, q_{in}), we have to check that Estep(ST S) is an elementary PN-transition system. Axioms (A1) follows from the definition of →′. Axiom (A2) follows from the fact that ST S satisfies axiom (EA3). (A3) is trivially satisfied. (A6”) follows from the fact that ST S satisfies (EA2). Finally, every region in ST S corresponds uniquely to a region in Estep(ST S), so we can deduce that Estep(ST S) satisfies (A4’) and (A5’) from the fact that ST S satisfies (EA4) and (EA5).

Once again, it is trivial to check that the image of a morphism in ETS is in fact a morphism in EPNts. □

Theorem 7.17 The functors Eseq and Estep define a categorical equivalence between EPNts and ETS.

Proof We have to show that the functor Estep ∘ Eseq is naturally isomorphic to the identity functor id_{EPNts} and, correspondingly, that Eseq ∘ Estep is naturally isomorphic to id_{ETS}.

In fact, we can prove something much stronger. Using the results we have proved so far, it is easy to show that for all T S ∈ EPNts, Estep ∘ Eseq(T S) = T S and for all ST S ∈ ETS, Eseq ∘ Estep(ST S) = ST S. So, these two categories are not just equivalent, they are in fact isomorphic. □

So, we have established that the category of step transition systems defined by elementary net systems is equivalent to the category of sequential transition systems defined by them. This equivalence provides an alternate proof of the result, established combinatorially by Hoogeboom and Rozenberg in [4], that information about the concurrent behaviour of an elementary net system can always be completely recovered from a description of its sequential behaviour.

8 Asynchronous transition systems

Asynchronous transition systems were introduced by Bednarczyk [1] and Shields [15]. These are sequential transition systems equipped with information about concurrency in terms of an independence relation on the events. These transition systems are closely related to safe nets. In fact, in [19], Winskel and Nielsen establish a coreflection between a special class of asynchronous transition systems and safe nets. We now show that there is a coreflection between our category SPNts of safe PN-transition systems and the category of asynchronous transtion systems defined in [19].

We begin by defining asynchronous transition systems. (The particular definition we use is adapted from [19]).

Definition 8.1 An asynchronous transition system is a structure AT S = (Q, E, ⇒, q_{in}, I) such that

• (Q, E, ⇒, q_{in}) is a sequential transition system (in the sense of Definition 5.1).

• I ⊆ E × E is an irreflexive, symmetric, independence relation satisfying the following four conditions:

(i) e ∈ E implies ∃q, q′ ∈ Q. q ⟹^{{e}} q′.

(ii) q ⇒^{u} q′ and q ⇒^{u} q′′ implies q′ = q′′.

(iii) e_{1}Ie_{2} and q ⟹^{{e_{1}}} q_{1} and q ⟹^{{e_{2}}} q_{2} implies ∃q′. q_{1} ⟹^{{e_{2}}} q′ and q_{2} ⟹^{{e_{1}}} q′.

(iv) e_{1}Ie_{2} and q ⟹^{{e_{1}}} q_{1} and q_{1} ⟹^{{e_{2}}} q′ implies ∃q_{2}. q_{1} ⟹^{{e_{2}}} q_{2} and q_{2} ⟹^{{e_{1}}} q′.

Condition (i) in the definition above specifies that each event in E must be “used” somewhere in the system. The second condition stipulates that the system is deterministic. The third and fourth conditions capture the fact that I specifies pairs of events which are independent of each other and can thus occur concurrently if they are simultaneously enabled. Actually, the independence relation specifies more than just concurrency—for instance, two events may be independent without being enabled simultaneously anywhere in the system. We shall return to this point later.

Since we are dealing with sequential transition systems, for convenience we shall write q ⇒^{e} q′ instead of q ⟹^{{e}} q′, where e ∈ E. We shall typically write q ⇒^{u} q′ to indicate that u could either correspond to {e} for some e ∈ E or to the empty step O_{E}.

Notice that the underlying sequential transition system is a step transition system satisfying axioms (A1) to (A3). So, we have idling transitions at each state and every state is reachable from the initial state. ((A3) is trivially satisfied in a sequential transition system).

Asynchronous transition systems are closely connected to safe nets. In [19], Winskel and Nielsen define a category A (which we shall call Ats) consisting of asynchronous transition systems equipped with transition system morphisms which satisfy the additional requirement that the map on events preserve the independence relation. They then establish a coreflection between a subcategory of asynchronous transition systems, denoted A_{0} (which we shall call Ats_{0}), and a category of safe Petri nets.

To identify the subcategory Ats_{0}, they define a version of regions called conditions, using which they define axioms exactly like the regional axioms we impose on PN-transition systems.

Definition 8.2 Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system. Its conditions are nonempty subsets b ⊆ ⇒ such that

(i) (q, e, q′) ∈ b implies (q, O_{E}, q) ∈ b and (q′, O_{E}, q′) ∈ b.

(ii) (a) (q_{1}, e, q′_{1}) ∈ ^{•}b and (q_{2}, e, q′_{2}) ∈ ⇒ implies (q_{2}, e, q′_{2}) ∈ ^{•}b

(b) (q_{1}, e, q′_{1}) ∈ b^{•} and (q_{2}, e, q′_{2}) ∈ ⇒ implies (q_{2}, e, q′_{2}) ∈ b^{•}

where for (q, e, q′) ∈ ⇒ we define

(q, e, q′) ∈ ^{•}b =^{def} (q, e, q′) ∉ b and (q′, O_{E}, q′) ∈ b,

(q, e, q′) ∈ b^{•} =^{def} (q, O_{E}, q) ∈ b and (q, e, q′) ∉ b and

•b^{•} = ^{•}b ∪ b^{•}.

(iii) (q_{1}, e_{1}, q′_{1}) ∈ ^{•}b^{•} and (q_{2}, e_{2}, q′_{2}) ∈ ^{•}b^{•} implies ¬e_{1}Ie_{2}.

Let B be the set of conditions of AT S. For e ∈ E, define

\begin{aligned}^{•}e & = & \{b ∈ B | ∃q, q′. (q, e, q′) ∈ b^{•}\}, \\ e^{•} & = & \{b ∈ B | ∃q, q′. (q, e, q′) ∈ ^{•}b\}, and \\ ^{•}e^{•} & = & ^{•}e ∪ e^{•}. \end{aligned}

Further, for q ∈ Q, define M(q) = {b ∈ B | (q, O_{E}, q) ∈ b}.

Notice that a condition is really a subset of states and transitions. The information about the states is coded up in terms of the idling transitions.

We shall establish that the notion of a condition is equivalent to a natural notion of a region for this class of transition systems, defined as follows.

Definition 8.3 Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system. A region of AT S is a pair of functions r = (r_{Q}, r_{E}) where

r_{Q} : Q → {0, 1} and

r_{E} : E → ({0, 1} × {0, 1}) such that

(i) ∀q ⇒^{e} q′. ^{r}e = 1 implies r_{Q}(q) = 1 and r_{Q}(q′) = r_{Q}(q) + (e^{r} −^{r}e).

(ii) ∀e, e′ ∈ E. If eIe′ then (^{r}e = 1 or e^{r} = 1) implies ^{r}e′ = e′^{r} = 0.

So, regions for asynchronous transition systems are very similar to the 0/1-regions we define for safe PN-transition systems. The only additional requirement is that independent events have disjoint sets of pre and postregions. This reflects the intuition that two transitions in a safe net are independent provided their neighbourhoods are disjoint.

Definition 8.4 Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system. Let B denote the set of conditions of AT S and let R denote the set of regions of AT S. We define two functions, r̂: B → R and b̂: R → B.

First, let r̂: B → R be defined as follows.

∀b ∈ B. ∀q ∈ Q. r̂(b)(q) = \{ \begin{matrix}1 & if (q, O_{E}, q) ∈ b \\ 0 & otherwise \end{matrix}

∀b ∈ B. ∀e ∈ E. r̂(b)(e) = \{ \begin{matrix}(1, 0) & if b ∈ ^{•}e \ e^{•} \\ (0, 1) & if b ∈ e^{•} \^{•}e \\ (1, 1) & if b ∈ ^{•}e^{•} \\ (0, 0) & otherwise \end{matrix}

Next, let b̂: R → B be defined as follows.

∀r ∈ R. b̂(r) = \{(q, u, q′) | \begin{matrix}u = O_{E}, q = q′ and r(q) = 1, or \\ u = \{e\}, r(e) = (0, 0) and r(q) = r(q′) = 1\} \end{matrix}

It is not hard to show the following result.

Proposition 8.5 Let AT S be an asynchronous transition system, with B as its set of conditions and R as its set of regions.

(i) ∀b ∈ B. b̂(r̂(b)) = b.

(ii) ∀r ∈ R. r̂(b̂(r)) = r.

We can now describe the subcategory Ats_{0} defined in [19]. Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system. Then AT S ∈ Ats_{0} if it satisfies the following two axioms, stated in terms of its set of conditions B:

Axiom ATS1 M(q) = M(q′) implies q = q′.

Axiom ATS2 ^{•}e ⊆ M(q) implies ∃q′. q ⇒^{e} q′, for all q ∈ Q, e ∈ E.

Clearly M(q) is equivalent to the set of regions {r ∈ R | r(q) = 1}. And, ^{•}e ⊆ M(q) is equivalent to saying r(q) ≥ ^{r}e for all r ∈ R. So we can reformulate these two axioms in terms of regions and observe that they correspond to the axioms of separation and enabling for PN-transition systems (stated in the contrapositive form).

Axiom ATS1’ (∀r ∈ R. r(q) = r(q′)) implies q = q′.

Axiom ATS2’ (∀r ∈ R. r(q) ≥ ^{r}e) implies ∃q′. q ⇒^{e} q′, for all q ∈ Q, e ∈ E.

Actually, when defining the category Ats of all asynchronous transition systems in [19], Winskel and Nielsen do not assume that every state is reachable (as we have done here by requiring the underlying sequential transition system to satisfy axiom (A2)). The axiom for reachability is then introduced in [19] as a third axiom that an asynchronous transition system must satisfy to be in the subcategory Ats_{0}. Since we are only interested in the subcategory Ats_{0} here, our presentation is equivalent to the one in [19].

The morphisms in Ats_{0} are transition system morphisms that preserve the independence relation. In other words, given two asynchronous transition systems AT S_{i} = (Q_{i}, E_{i}, ⇒_{i}, q_{in}^{i}, I_{i}), i = 1, 2, a morphism f : AT S_{1} → AT S_{2} is a pair (f_{Q}, f_{E}) where:

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

• f_{E} : E_{1} ⇀ E_{2} is a partial function.

• q ⇒^{e}_{1} q′ implies f_{Q}(q) ⟹^{f_{E}(e)}_{2} f_{Q}(q′).

• If e_{1}I_{1}e′_{1} and f_{E}(e_{1}), f_{E}(e′_{1}) are both defined, then f_{E}(e_{1})I_{2}f_{E}(e′_{1}), for all e_{1}, e′_{1} ∈ E_{1}.

We want to establish a relationship between our category of safe PN-transition systems SPNts and the category Ats_{0}. Actually, to describe the result we are after we have to make a slight restriction to our notion of a safe PN-transition system. Henceforth, we assume that if T S = (Q, E, →, q_{in}) is a safe transition system, for every event e ∈ E there is some transition q →^{u} q′ in T S with e ∈ u—that is, every event has an occurrence. We shall discuss the need for this restriction at the end of this section.

We first prove a standard result which describes how the independence relation I in an asynchronous transition system specifies concurrency. It says that a sequence of actions which are pairwise independent corresponds to a concurrent step consisting of those actions. So, if such a sequence is enabled at a state in the system, all permutations of that sequence must also be enabled at that system and, furthermore, they should all lead to the same state as the original sequence.

Lemma 8.6 Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system and {e_{1}, e_{2}, …, e_{n}} ⊆ E, n ≥ 2, be a pairwise independent subset of events in E—in other words, e_{i}Ie_{j} for all 1 ≤ i, j ≤ n, i ≠ j.

If q ⇒^{e_{1}} q_{1} ⇒^{e_{2}} … ⟹^{e_{n−1}} q_{n−1} ⇒^{e_{n}} q′′ then for all permutations π : {1, 2, …, n} →

{1, 2, …, n}, there exist states {q′_{1}, q′_{2}, …, q′_{n−1}} such that q ⟹^{e_{π(1)}} q′_{1} ⟹^{e_{π(2)}} … ⟹^{e_{π(n−1)}} q′_{n−1} ⟹^{e_{π(n)}}

q′′.

Proof The proof is straightforward, by induction on n, the number of pairwise independent events. The base case n = 2 corresponds to condition (iv) in the definition of an asynchronous transition system. We omit the details. □

We can now describe a functor AS : Ats_{0} → SPNts. Given an asynchronous transition system AT S = (Q, E, ⇒, q_{in}, I), AS(AT S) = (Q, E, →, q_{in}), where

→ = \{(q, u, q′) | \begin{matrix}u = \{e_{1}, e_{2}, …, e_{n}\} ⊆ E, such that \\ e_{i}Ie_{j} for all 1 ≤ i, j ≤ n, i ≠ j and \\ ∃q_{1}, q_{2}, …, q_{n−1}. q ⇒^{e_{1}} q_{1} ⇒^{e_{2}} … ⟹^{e_{n−1}} q_{n−1} ⇒^{e_{n}} q′ in AT S\} \end{matrix}

Let AT S_{i} = (Q_{i}, E_{i}, ⇒_{i}, q_{in}^{i}, I_{i}), i = 1, 2, be a pair of asynchronous transition systems and let f : AT S_{1} → AT S_{2} be a morphism in Ats_{0}. Then the corresponding morphism AS(f) : AS(AT S_{1}) → AS(AT S_{2}) is given by AS(f)_{Q} = f_{Q} and AS(f)_{E} = f_{E}.

Lemma 8.7 AS is a functor.

Proof Let AT S = (Q, E, ⇒, q_{in}, I) be an asynchronous transition system in Ats_{0}. To check that AS(AT S) is a safe PN-transition system, we just observe that every region of AT S is also a 0/1-region of AS(AT S). It then follows that AS(AT S) must satisfy the regional axioms (A4’) and (A5’) because AT S satisfies Axioms ATS1’ and ATS2’.

Given a morphism f : AT S_{1} → AT S_{2}, where AT S_{i} = (Q_{i}, E_{i}, ⇒_{i}, q_{in}^{i}, I_{i}), i = 1, 2, and AS(AT S_{i}) = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, we have to check that f̂ = AS(f) satisfies condition (iii) in Definition 3.7.

In other words, if q →^{u}_{1} q′, we have to ensure that f̂(q) ⟶^{f̂(u)}_{2} f̂(q′). Let u = {e_{1}, e_{2}, …, e_{n}}. By the definition of →_{1}, there must exist a sequence of actions q ⇒^{e_{1}}_{1} q_{1} ⇒^{e_{2}}_{1} … ⟹^{e_{n−1}}_{1} q_{n_{1}} ⇒^{e_{n}}_{1} q′. Since f is a transition system morphism, it then follows that the f-image of this sequence exists in AT S_{2}. That is there is a sequence

f(q) ⟹^{f(e_{1})}_{2} f(q_{1}) ⟹^{f(e_{2})}_{2} … ⟹^{f(e_{n−1})}_{2} f(q_{n−1}) ⟹^{f(e_{n})}_{2} f(q′). Since we know that the events in u

are pairwise independent and f preserves independence, the events in f(u) must be pairwise independent as well. It then follows, by the definition of →_{2}, that f(q) ⟶^{f(u)}_{2} f(q′).

□

We now construct a functor SA which is left adjoint to the functor AS. Let T S = (Q, E, →, q_{in}) be a safe PN-transition system. Define SA(T S) = (Q, E, ⇒, q_{in}, I) where

• ⇒= {(q, u, q′) | q →^{u} q′ and |u| ≤ 1}

• I = {(e_{1}, e_{2}), (e_{2}, e_{1}) | ∃q ∈ Q. q ⟶^{{e_{1},e_{2}}} q′}

Let T S_{i} = (Q_{i}, E_{i}, →_{i}, q_{in}^{i}), i = 1, 2, be a pair of safe PN-transition systems and f : T S_{1} → T S_{2} be a morphism in SPNts. Then SA(f) : SA(T S_{1}) → SA(T S_{2}) is given by SA(f)_{Q} = f_{Q} and SA(f)_{E} = f_{E}.

Before proving that SA is a functor, it will be useful to prove a small result about 0/1-regions.

Proposition 8.8 Let T S = (Q, E, →, q_{in}) be a safe PN-transition system. Suppose that e_{1}, e_{2} ∈ E such that there exists a step q ⟶^{{e_{1},e_{2}}} q′ in T S. Then, for all r ∈ R_{T S}^{0/1}, if ^{r}e_{1} = 1 or e_{1}^{r} = 1 then ^{r}e_{2} = e_{2}^{r} = 0.

Proof Suppose that r ∈ R_{T S}^{0/1} such that ^{r}e_{1} = 1. Then, since r(q) ≤ 1, ^{r}e_{2} must be 0, otherwise the step {e_{1}, e_{2}} would not be enabled at q. e_{2}^{r} must be 0 as well. For, consider the state q_{2} reached by the transition q ⟶^{{e_{2}}} q_{2}. (Such a transition must exist by Proposition 3.6). We have r(q_{2}) = r(q) + (e_{2}^{r} −^{r}e_{2}). But r(q) = 1, since ^{r}e_{1} = 1 and e_{1} is enabled at q. We also know that ^{r}e_{2} = 0. So, if e_{2}^{r} were 1, we would have r(q_{2}) = 2, which is not possible.

On the other hand, if e_{1}^{r} = 1, we must have r(q) = 0. Then, we cannot have ^{r}e_{2} = 1, or e_{2} would not be enabled at q. We cannot have e_{2}^{r} = 1 either because then r(q′) = 2, which is not possible. □

Lemma 8.9 SA is a functor.

Proof Let T S = (Q, E, →, q_{in}) be a safe PN-transition system. We have to first check that SA(T S) is an asynchronous transition system. We basically have to check that conditions (i) to (iv) of Definition 8.1 hold.

Condition (i) holds because we have restricted the objects in SPNts appropriately. Condition (ii) follows from Proposition 3.5 which says that PN-transition systems are deterministic.

Conditions (iii) and (iv) pertain to the independence relation. Condition (iii) says

that e_{1}Ie_{2} and q ⟹^{e_{1}} q_{1} and q ⟹^{e_{2}} q_{2} implies ∃q′. q_{1} ⟹^{e_{2}} q′ and q_{2} ⟹^{e_{1}} q′. Since e_{1}Ie_{2},

we know that q′′ ⟶^{{e_{1},e_{2}}} q′′′ somewhere in T S. By the previous proposition, the pre and postregions of e_{1} and e_{2} are disjoint, so if both e_{1} and e_{2} are enabled at a state q, then (by axiom (A5’)) the step {e_{1}, e_{2}} must be enabled as well. The result then follows from Proposition 3.6, which asserts that all steps in a PN-transition system can be broken up into substeps in a consistent way.

Condition (iv) follows by a similar argument.

To verify that SA(T S) satisfies axioms ATS1’ and ATS2’, notice that by the previous proposition, any region r ∈ R_{T S}^{0/1} would correspond to a region in SA(T S). Since T S satisfies axioms (A4’) and (A5’) with respect to regions in R_{T S}^{0/1}, it follows that the corresponding regions in SA(T S) are sufficient to satisfy axioms ATS1’ and ATS2’.

We then have to verify that for any morphism f : T S_{1} → T S_{2}, i = 1, 2, SA(f) = f̂ is a morphism from SA(T S_{1}) to SA(T S_{2}), where SA(T S_{i}) = (Q_{i}, E_{i}, ⇒_{i}, q_{in}^{i}, I_{i}), i = 1, 2. We basically have to verify that if e_{1}I_{1}e_{2} and both f̂(e_{1}) and f̂(e_{2}) are defined, then f̂(e_{1})I_{2}f̂(e_{2}), where f̂(e_{1}) = f(e_{1}) and f̂(e_{2}) = f(e_{2}). If e_{1}I_{1}e_{2}, then, by the definition of I_{1}, we know that q ⟶_{1}^{{e_{1},e_{2}}} q′ somewhere in T S_{1}. This implies that f(q) ⟶_{2}^{{f(e_{1}),f(e_{2})}} f(q′) in T S_{2}. So, if f(e_{1}) and f(e_{2}) are both defined, then, by the definition of I_{2}, we have f(e_{1})I_{2}f(e_{2}) and we are done. □

Theorem 8.10 The functor SA is left adjoint to the functor AS. The unit of the adjunction is a natural isomorphism.

Proof Let T S ∈ SPNts and AT S ∈ Ats_{0}. Suppose that f : T S → AS(AT S) is a morphism. Then, since T S and SA(T S) have the same underlying sets of states and events and AS(AT S) and AT S have the same underlying sets of states and events, it is fairly straightforward to see that f̂: SA(T S) → AT S is also a morphism, where f̂_{Q} = f_{Q} and f̂_{E} = f_{E}. Conversely, if g : SA(T S) → AT S is a morphism, we can show that \overline{g} : T S → AS(AT S) is also a morphism, where \overline{g}_{Q} = g_{Q} and \overline{g}_{E} = g_{E}. Further, \overline{f̂} = f and ˆ \overline{g} = g for all morphisms f ∈ SPNts and g ∈ Ats_{0}. This establishes a bijection between Hom(T S, AS(AT S)) and Hom(SA(T S), AT S). It is not difficult to show that this bijection is natural in both SPNts and Ats_{0}, thereby establishing the adjunction.

It is also not difficult to show that the unit η_{T S} : T S → AS∘SA(T S) is an isomorphism for all T S ∈ SPNts. □

So we have established a coreflection between our category of safe PN-transition systems and the category of asynchronous transition systems Ats_{0} defined by Winskel and Nielsen in [19].

The reason that this correspondence is a coreflection and not a categorical equivalence has to do with the nature of the independence relation. In an asynchronous transition system two events can be independent without ever being enabled simultaneously to give rise to a concurent step. When representing an asynchronous transition system as a safe PN-transition system, we lose information about these “unused” independences. These “unused” independences can be regarded as providing some “structural” information about the system which may not be directly detectable in its concurrent behaviour. For example, two events being independent of each other could denote the fact that they occur at different locations and do not interfere with each other. Under such an interpretation, one comes across very natural examples of asynchronous transition systems in which independent events are never simultaneously enabled (see, for instance, [10]).

It is not difficult to show that our category of safe PN-transition systems is equivalent to a subcategory of Ats_{0} whose objects satisfy the additional constraint that for every pair (e_{1}, e_{2}) ∈ I, there is a state q where both e_{1} and e_{2} are enabled.

We also pointed out a mismatch between the definition of safe PN-transition systems we use in this section and the one we proposed in the Section 6. The additional assumption we have made here is that every event in E have an occurrence. This is required because asynchronous transition systems in the category Ats_{0} satisfy this restriction.

However, this restriction on asynchronous transition systems is a consequence of how conditions are defined. For an asynchronous transtition system AT S = (Q, E, ⇒, q_{in}, I), it is easy to see that one cannot define a condition b ∈ ^{•}e for any e ∈ E which does not occur in AT S. This is because conditions are defined as subsets of transitions which are present in the system. Since we cannot find any b ∈ ^{•}e for an event e which does not occur, Axiom ATS2 would then require e to be enabled at every state in the system, which is a contradiction. So, for asynchronous transition systems in Ats_{0}, condition (i) in Definition 8.1 is implied by Axiom ATS2.

However, in the generalized set up of regions, it is possible to define “disabling regions” which take the value 0 at all states but which are the preregion of some event e, thereby ensuring that e is never enabled. The regional version of the second axiom, Axiom ATS2’, would clearly permit such permanently disabled events to be part of the specification of the system.

It is not difficult to generalize Definition 8.1 by dropping condition (i) and building a slightly larger category Ats′_{0} satisfying Axioms ATS1’ and ATS2’. It then turns out that the coreflection we have described here goes through between the category SPNts as originally defined in the previous section and the more generous category Ats′_{0}.

9 Safe nets revisited

We showed in Section 6 that there is a coreflection between SPNts, the category of safe PN-transition systems and SNet, our category of safe nets. Then, we showed that there is also a coreflection between SPNts and Ats_{0}, where Ats_{0} is a subcategory of the Ats, the category of asynchronous transition systems. In [19], Winskel and Nielsen have established a coreflection between Ats_{0} and a category of safe nets which we shall call WNet.

Unfortunately, the category WNet is not the same as the category SNet we have defined here. However, we show now that there is an adjunction between these two categories. Further, we can establish a coreflection between the subcategories of SNet and WNet consisting of only saturated nets, where saturated nets are those nets which arise out of the regional construction in going from transition systems to nets.

The only difference between WNet and SNet is that the morphisms of WNet are slightly stricter than those of SNet.

Let us briefly recall the definition of the category SNet. The objects of SNet are safe nets, as given by Definition 6.1. Morphisms between safe nets are the same as those between general nets, as given in Definition 2.2. However, since the definition of a morphism becomes slightly simpler when restricted to safe nets, we pause to spell it out in detail.

Let PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2, be a pair of safe nets. An SNet-morphism ϕ : P N_{1} → P N_{2} is a pair ϕ = (ϕ_{S}, ϕ_{T}) where:

(i) ϕ_{S} : S_{2} ⇀ S_{1} is a partial function.

(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}^{•}.

The category WNet also has as its objects safe nets, like SNet. However, the morphisms are slightly stricter than those of SNet. ϕ : P N_{1} → P N_{2} is a morphism in WNet if ϕ is an SNet-morphism, and, in addition, ϕ_{S}^{−1}(M_{in}^{1}) = M_{in}^{2} (where, abusing notation, M_{in}^{i}, i = 1, 2 denote the subsets of S_{1} and S_{2} which are marked initially in P N_{1} and P N_{2} respectively).

So, the essential difference between a WNet-morphism and an SNet-morphism is that in a WNet-morphism ϕ_{S} is a total function when restricted to those places marked initially in the second net.

Clearly, every WNet-morphism is also an SNet-morphism. So WNet is a subcategory of SNet, though not a full subcategory.

It turns out that we can construct a left adjoint to the inclusion functor from WNet to SNet (though this will not constitute a reflection because WNet is not a full subcategory of SNet [6]).

In going from SNet to WNet, we have, in general, to make an SNet-morphism into a WNet-morphism. In other words, we have to convert the map on the initial marking from a partial function to a total function. A standard way to convert a partial function to a total function is to augment the range of the function with a special “undefined” value. Similarly, here we augment the net that is the source of the morphism with an isolated marked place.

Formally, define a functor SNWN : SNet → WNet as follows.

• For PN = (S, T, W, M_{in}) ∈ SNet, SNWN(P N) = (S ⊎ {s̆}, T, W′, M_{in}′), where:

– s̆ ∉ S (we use ⊎ to denote disjoint union).

– ∀s ∈ S ⊎ \{s̆\}. ∀t ∈ T. W′(s, t) = \{ \begin{matrix}W (s, t) & if s ∈ S \\ 0 & otherwise \end{matrix}

– ∀s ∈ S ⊎ \{s̆\}. ∀t ∈ T. W′(t, s) = \{ \begin{matrix}W (t, s) & if s ∈ S \\ 0 & otherwise \end{matrix}

– M_{in}′(s̆) = 1 and ∀s ∈ S. M_{in}′(s) = M_{in}(s).

• Let ϕ : P N_{1} → P N_{2} be a morphism between P N_{1} and P N_{2}, where PN_{i} = (S_{i}, T_{i}, W_{i}, M_{in}^{i}), i = 1, 2. Then, SNWN(ϕ) = ϕ′ : SNWN(P N_{1}) → SNWN(P N_{2}) is given as follows, where SNWN(P N_{i}) = (S_{i} ⊎ {s̆_{i}}, T_{i}, W′_{i}, M_{in}^{i}′), i = 1, 2.

– ∀t ∈ T_{1}. ϕ′(t) = ϕ(t).

– ∀s ∈ S_{2} ⊎ \{s̆_{2}\}. ϕ′(s) = \{ \begin{matrix}s̆_{1} & if (s = s̆_{2}) or \\ (s ∈ S_{2}, M_{in}^{2}′(s) = 1 and \\ ϕ(s) is undefined) \\ ϕ(s) & otherwise \end{matrix}

Theorem 9.1 SNWN : SNet → WNet is left adjoint to the inclusion functor.

Proof Let PN_{1} = (S_{1}, T_{1}, W_{1}, M_{in}^{1}) and PN_{2} = (S_{2}, T_{2}, W_{2}, M_{in}^{2}) be two safe nets. We shall establish a bijection between Hom(P N_{1}, P N_{2}) and Hom(SNWN(P N_{1}), P N_{2}), where SNWN(P N_{1}) = (S_{1} ⊎ s̆_{1}, T_{1}, W′_{1}, M_{in}^{1}′).

We first define a map λ : Hom(P N_{1}, P N_{2}) → Hom(SNWN(P N_{1}), P N_{2}). Suppose that ϕ : P N_{1} → P N_{2} ∈ Hom(P N_{1}, P N_{2}). Define λ(ϕ) : SNWN(P N_{1}) → P N_{2} as follows.

• ∀t ∈ T_{1}. λ(ϕ)(t) = ϕ(t).

• ∀s ∈ S_{2}. λ(ϕ)(s) = \{ \begin{matrix}s̆_{1} & if M_{in}^{2}(s) = 1 and ϕ(s) undefined \\ ϕ(s) & otherwise \end{matrix}

Next we define a map μ : Hom(SNWN(P N_{1}), P N_{2}) → Hom(P N_{1}, P N_{2}). Let ψ : SNWN(P N_{1}) → P N_{2}. Then μ(ψ) : P N_{1} → P N_{2} is given as follows.

• ∀t ∈ T_{1}. μ(ψ)(t) = ψ(t).

• ∀s ∈ S_{2}. μ(ψ)(s) = \{ \begin{matrix}undefined & if ψ(s) = s̆_{1} \\ ψ(s) & otherwise \end{matrix}

It is straightforward to show that μ(λ(ϕ)) = ϕ and λ(μ(ψ)) for all ϕ ∈ Hom(P N_{1}, P N_{2}) and ψ ∈ Hom(SNWN(P N_{1}), P N_{2}). It is not difficult to show that this bijection is natural in SNet and WNet, and we are done.

□

As we mentioned at the beginning of this section, we can establish a slightly stronger result when we look at the safe nets actually arising out of the regional construction from transition systems.

In Section 6, we have described a functor STN which associates a net STN(T S) with each safe PN-transition system T S. Following [12], we can call such a net saturated, because it contains all possible places which are consistent with the behaviour described by T S. A crucial feature of the construction is that these saturated nets have no isolated places because we only use non-trivial regions in the construction of the saturated net.

In [19], Winskel and Nielsen describe a similar functor, which we can call AWN, going from Ats_{0} to WNet. Once again, given an asynchronous transition system AT S, AWN(AT S) will be a saturated net. Here, saturation is with respect to the underlying sequential behaviour of AT S as well as the independence relation I specified by AT S. An important difference between the construction described in [19] and the construction we describe in Section 6 is that the construction in [19] adds trivial regions as well.

The reason why the construction in [19] also includes trivial regions is to do with the stricter notion of a net morphism in the category WNet. Notice that it is always possible to define a trivial morphism between two transition systems in which the map on events is empty. Corresponding to this, in the category SNet it is always possible to define a trivial morphism between two nets where the map on places and the map on transitions are both empty. However, in the category WNet, such trivial maps do not always exist, because of the strong condition on how the initial markings have to be related. If the net that is the source of a morphism has an isolated marked place, however, such a trivial map can also be defined in WNet. Hence, to transport the trivial maps between asynchronous transition systems in Ats_{0} faithfully to trivial maps between the associated nets in WNet, it is essential that the functor AWN create isolated places.

Let SatSNet be the subcategory of SNet where for every net P N ∈ SatSNet, there is a safe PN-transition system T S ∈ SPNts such that P N is isomorphic to STN(T S). Similarly, let SatWNet be the subcategory of WNet such that for every net P N ∈ SatWNet, there is an asynchronous transition system AT S ∈ Ats_{0} such that P N is isomorphic to AWN(AT S).

The functor SNWN : SPNts → WNet restricts to a functor from SatSNet to SatWNet, which we shall again call SNWN, for convenience.

Going in the opposite direction, starting with a net P N ∈ SatWNet, we can first apply the functor WNA, which is the right adjoint of AWN, to obtain an asynchronous

[figure: q_{in}; q_{1}; q_{2}; q_{3}; e_{1}; e_{2}; e_{3}]

Figure 3:

transition system corresponding to P N. Then by applying AS and STN we obtain a net in SatSNet.

Theorem 9.2 The functor SNWN : SatSNet → SatWNet is left adjoint to the functor STN ∘ AS ∘ WNA : SatWNet → SatSNet. The unit of the adjunction is a natural isomorphism.

Proof The proof is tedious but straightforward, based on several results we have proved already, so we omit the details. □

So, even at the level of saturated nets, we only get a coreflection and not a categorical equivalence between SatSNet and SatWNet. This is because a safe net that is saturated with respect its description as an asynchronous transition system need not be saturated with respect to its description as a safe PN-transition system. So, the “obvious” functor from SatWNet to SatSNet which just removes the isolated places will not, in general, yield a net in SatSNet at all.

Consider, for example, the simple transition system T S in Figure 3. If we view this as a safe PN-transition system, the corresponding saturated net STN(T S) would have a place s such that s ∈ e_{1}^{•} and s ∈ ^{•}e_{3}.

However, we can make T S into an asynchronous transition system in more than one way. The obvious asynchronous transition system version of T S has the empty independence relation. But, we can also specify that e_{1} and e_{3} are independent. This would mean that in the net AWN(T S), the neighbourhoods of e_{1} and e_{3} would be disjoint, hence ruling out the place s connecting e_{1} to e_{3} which is present in STN(T S).

Another way of comparing the categories SNet and WNet is to examine subcategories of SNet and WNet where we saturate the nets in both subcategories with respect to the same class of transition systems.

First, we can relate SPNts and WNet by functors STWN : SPNts → WNet and SWNT : WNet → SPNts in much the same way as we related SPNts and SNet by STN and SNT, except that STWN constructs places corresponding to both trivial and nontrivial regions. It is then easy to establish a coreflection between STWN and SWNT. We can then look at the category SatWNet′, consisting of safe nets which are isomorphic to STWN(T S) for some T S ∈ SPNts. It is not difficult to show that SatSNet and SatWNet′ are categorically equivalent, where the functor from SatSNet to SatWNet′ is SNWN as before and the functor in the opposite direction is the one which strips off isolated places from a net.

In a similar way, we can define a coreflection between Ats_{0} and SNet in terms of functors AN : Ats_{0} → SNet and NA : SNet → Ats_{0}, where AN constructs places corresponding to only non-trivial regions. We can then look at the category SatSNet′ consisting of safe nets which are isomorphic to AN(AT S) for some AT S ∈ Ats_{0}. It turns out that SatSNet′ and SatWNet are categorically equivalent.

So, provided we use the same notion of saturation in both SNet and WNet, we end up with equivalent subcategories of saturated nets.

10 Discussion

In this paper we have shown how to define subcategories of PN-transition systems which describe the behaviour of safe nets and elementary net systems. This is achieved by “tuning” the notion of a region appropriately. It then turns out that the coreflection established between the categories PNts and PNet in [9] can be restricted to coreflections between the corresponding subcategories of these two categories.

We have examined the relationship between sequential and step transition systems in the setting of PN-transition systems. In general, there is a coreflection between sequential PN-transition systems and “normal” PN-transition systems with steps. However, when we restrict our attention to transition systems describing the behaviour of elementary net systems, the subcategories of sequential and step transition systems are equivalent. This shows that for elementary net systems, all information about concurrency can be recovered by examining the sequential behaviour of the system.

We have also established a coreflection between safe PN-transition system and asynchronous transition systems. This result shows that asynchronous transition systems are, in a sense, a more concrete model of behaviour than step transition systems because the independence relation can provide “structural” information about a system which cannot be inferred directly from an examination of its behaviour.

A brief remark is in order about the way we have described the correspondence between step transition systems and Petri nets. We have chosen to present the relationship between step transition systems and different classes of Petri nets directly in terms of coreflections, by identifying special categories of step transition systems corresponding to each class of nets. Instead, we could have followed the approach adopted by Winskel and Nielsen in [19] and first established the existence of left adjoints for the natural functors from nets to step transition systems and then “cut down” the adjunctions to coreflections by restricting the class of step transition systems under consideration.

In a sense, it would have been more uniform to follow the approach of [19], because the right adjoints in all the coreflections we establish between transition systems and nets correspond to the same functor—the one taking a net to its “step” marking diagram. We have chosen to directly present the results in terms of coreflections because these coreflections denote, in our opinion, stronger and more relevant relationships between the two classes of models than those represented by simple adjunctions. An adjunction between step transition systems and a particular class of nets describes the minimal way of “massaging” a given step transition system so that it represents the behaviour of some net from the class of nets under consideration. On the other hand, if we have a coreflection between a class of step transition systems and a class of nets, we are guaranteed that the class of transition systems we are considering captures precisely the behaviours describable by the class of nets we are interested in.

It is natural to ask what we achieve by establishing these formal relationships between different models of concurrency. One motivation for establishing such relationships is that they provide a basis for translating results from one model to another. This gives us the freedom to work within whichever framework is most convenient and “automatically” obtain connections to other approaches.

For instance, to obtain a non-interleaved model for a process calculus such as CCS [8], 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 [2, 13] or event structures [18]. Thus, using a very simple extension of the standard operational semantics for CCS, we can provide a non-interleaved semantics for a rich subclass of the language in terms of asynchronous transtition systems from the subcategory Ats_{0} [10]. This implies, by the results connecting Ats_{0} and WNet, that we automatically obtain a net semantics for this language.

The other natural question that one may ask is why we work within the framework of category theory. One reason is that it provides a convenient mathematical language to phrase the kinds of correspondences we would like to describe. For instance, coreflections succintly capture the idea of one model being embedded in another.

The other 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 [19], 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.

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 [19], 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 [19] without too much difficulty.

Acknowledgment We thank Mogens Nielsen for helpful comments.

A Appendix

We fix some terminology and notation regarding multisets.

Definition A.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.

• Let u, v ∈ MS(A). Then u is a submultiset of v, written u ⊆_{MS} v, in case u(a) ≤ v(a) for all a ∈ 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.

References

[1] M.A. Bednarczyk: Categories of asynchronous systems, PhD Thesis, Report 1/88, Computer Science, University of Sussex (1988).

[2] P. Degano, R. de Nicola, U. Montanari: A distributed operational semantics for CCS based on condition/event systems, Acta Informatica, 26, 59–91 (1988).

[3] A. Ehrenfeucht, G. Rozenberg: Partial 2-structures; Part II: State spaces of concurrent systems, Acta Informatica, 27, 348–368 (1990).

[4] H.J. Hoogeboom, G. Rozenberg: Diamond properties of elementary net systems, Fundamenta Informaticae, XIV, 287–300 (1991).

[5] K. Lodaya, R. Ramanujam, P.S. Thiagarajan: A logic for distributed transition systems, Springer Lecture Notes in Computer Science, 354, 508–522 (1989).

[6] S. Mac Lane: Categories for the working mathematician, Springer-Verlag, New York/Berlin (1971).

[7] A. Mazurkiewicz: Basic notions of trace theory, Springer Lecture Notes in Computer Science, 354, 285–363 (1989)

[8] R. Milner: Communication and Concurrency, Prentice-Hall, London (1989).

[9] M. Mukund: A transition system characterization of Petri nets, Report TCS-91-2, School of Mathematics, SPIC Science Foundation, Madras, India (1991).

[10] M. Mukund, M. Nielsen: CCS, locations and asynchronous transition systems, Report DAIMI-PB-395, Computer Science Department, Aarhus Univeristy, Aarhus, Denmark (1992).

[11] M. Nielsen, G. Plotkin, G. Winskel: Petri nets, event structures and domains, part I, Theoretical Computer Science, 13, 45–57 (1981).

[12] M. Nielsen, G. Rozenberg, P.S. Thiagarajan: Elementary transition systems, Theoretical Computer Science, 96, 1, 3-33 (1992).

[13] E.-R. Olderog: Nets, Terms and Formulas, Cambridge University Press, Cambridge (1991).

[14] W. Reisig: Petri nets, Springer-Verlag, Berlin (1985).

[15] M.W. Shields: Concurrent machines, Computer Journal, 28, 449–465 (1985).

[16] P.S. Thiagarajan: Elementary nets systems, Springer Lecture Notes in Computer Science, 254, 60–94 (1987).

[17] G. Winskel: Event structures, Springer Lecture Notes in Computer Science, 255, 325–392 (1987).

[18] G. Winskel: Event structure semantics of CCS and related languages, Springer Lecture Notes in Computer Science, 140, 561–577 (1982).

[19] 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).