Internal Report  TCS-92-2

November, 1992

CCS, Locations and Asynchronous Transition Systems

Madhavan Mukund ^{1} and Mogens Nielsen^{2}

Abstract

Our aim is to provide a simple non-interleaved operational semantics for CCS in terms of a model that is easy to understand—asynchronous transition systems. Our approach is guided by the requirement that the semantics should identify the concurrency present in the system in a natural way, in terms of events occurring at independent locations in the system.

We extend the standard interleaving transition system for CCS by introducing labels on the transitions with information about the locations of events. We then show that the resulting transition system is an asynchronous transition system which has the additional property of being elementary, which means that it can also be represented by a 1-safe net.

We establish a close correspondence between our semantics and other approaches in terms of foldings.

We also introduce a notion of bisimulation on asynchronous transition systems which preserves independence. We conjecture that the induced equivalence on CCS processes coincides with the notion of location equivalence proposed by Boudol et al.

1School of Mathematics, SPIC Science Foundation, 92, G.N. Chetty Road, T. Nagar, Madras 600 017, India. E-mail: madhavan@ssf.ernet.in.

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.

2Computer Science Department, Aarhus University, Ny Munkegade, DK-8000 Aarhus C, Denmark.

E-mail: mn@daimi.aau.dk This report is also published as DAIMI-PB-395, Computer Science Department, Aarhus University, Aarhus, Denmark.

1 Introduction

Process algebras like CCS [9] are a well established formalism for specifying concurrent systems. However, the traditional semantics for these languages is given in terms of labelled transition systems in which parallel composition is interpreted as non-deterministic interleaving.

Several attempts have been made to provide a non-interleaved semantics for CCSlike languages, in which the concurrency implicit in a process expression P is explicitly represented in the semantics of P.

One approach is to incorporate information about concurrency into the conventional sequential transition system describing the behaviour of P by introducting an algebra of transitions. This can be done implicitly, by decorating each transition with a “proof of its derivation” [3], or explicitly, as in [8].

Another approach is to interpret process expressions in terms of a richer model— typically Petri nets [3, 6, 11]. This involves decomposing a process into local “components” and then constructing a net from these components.

Both these approaches have the drawback that they are complicated. When one introduces an algebra over the transitions, one has to go through a second level of reasoning about the transition system in order to identify the underlying events in the system (where we use the term event in the sense of Petri nets).

On the other hand, translating a term directly into a Petri net suffers from the usual problems associated with explicitly manufacturing one particular net which gives rise to the required behaviour—a lot of effort has to be put into to creating the places and hooking them up correctly to the transitions and then proving that the net one has constructed does in fact exhibit the required behaviour.

Our aim is to provide a simple non-interleaved operational semantics for CCS in terms of a model that is easy to understand. The criteria we have in mind are the following.

• The semantics should be as close to the original (interleaving) transition system as possible.

• The semantics should identify the concurrency present in the system in a natural way, in terms of events occurring at independent locations in the system.

• The structure representing the behaviour should be finite, whenever possible—this means that we should treat recursion carefully and unfold the system only if necessary.

• There should be a way to formally relate our semantics to other existing approaches.

• The semantics should be simple!

With this in mind, we choose to interpret CCS over the class of asynchronous transition systems [2, 12, 13]. An asynchronous transition system is a normal transition system where the labels are viewed as events. The transition system comes equipped with a binary relation on the events which specifies when two events in the system are independent of each other.

Asynchronous transition systems and Petri nets are closely related to each other. In [13], it is shown that one can define a subclass of “elementary” asynchronous transition systems which are, in a precise sense, equivalent to 1-safe Petri nets.

To interpret CCS in terms of asynchronous transition systems, we restrict the language slightly. Instead of the normal operator + expressing non-deterministic choice, we use guarded choice. In other words, we restrict terms with + to be of the form aP + bQ, where a and b could be the invisible action τ—we do not permit general expressions of the form P + Q. The rest of the language is the same as in standard CCS. We claim that this language is still a very powerful and useful language for specifying concurrent systems. For instance, all the examples in [9] conform to our syntactic restriction.

To obtain an asynchronous transition system from a CCS expression, we decorate transitions with labels which indicate the location where the action occurs. While this is in the same spirit as decorating transitions with their proofs, it turns out that our labelling directly gives us the underlying events of the system. In other words, we do not need to impose an algebra on our labels to identify events—two transitions correspond to the occurrence of the same event iff they carry the same label. The independence relation we define on events reflects a natural notion of independence on locations.

We then prove that the asynchronous transition system LT S(P) we associate with a process expression P is in fact elementary. This means that we obtain “for free” a Petri net semantics for our language, by appealing to the results of [13].

We express the connection between our semantics and some other approaches in terms of foldings. These are special types of bisimulations in which the target of the folding is, in general, a smaller, more compact representation of the behaviour described by the first system. We show that the normal interleaved transition system for our language, as defined in [9], can be folded onto the asynchronous transition system we define. On the other hand, in [13], a denotational semantics for CCS is presented in terms of asynchronous transition systems. We show that the denotational transition system associated with a term P can also be folded onto the transition system we associate operationally with P.

Finally, we define a notion of bisimulation on asynchronous transition systems which preserves independence. When applied to the asynchronous transition systems we use to describe the behaviour of CCS processes, this gives rise to an equivalence on process terms which we conjecture is equivalent to the notion of location equivalence defined in [5].

The paper is organized as follows. We begin with a brief introduction to asynchronous transition systems. The next section introduces the process language and its operational semantics. Section 4 establishes that the asynchronous transition system we define for a process P is elementary. In Section 5, we show how to relate our semantics with other standard approaches. The next section describes bisimulations on asynchronous transition systems. We conclude in Section 7 with a discussion of how our work relates to other approaches and suggestions for further study.

2 Asynchronous transition systems

We begin by recalling the standard notion of a (labelled sequential) transition system.

Definition 2.1 (Transition system) A transition system is a quadruple T S = (S, i, E, Tran) where • S is a set of states, with initial state i.

• E is a set of events.

• Tran ⊆ S × E × S is the transition relation.

Asynchronous transition systems were introduced independently by Bednarczyk [2] and Shields [12]. These transition systems incorporate information about concurrency explicitly, in terms of a binary relation which specifies which pairs of events are independent of each other. The particular definition we adopt here is from [13].

Definition 2.2 (Asynchronous transition systems) An asynchronous transition system is a structure AT S = (S, i, E, I, Tran) such that

• (S, i, E, Tran) is a transition system.

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

(i) e ∈ E ⇒ ∃s, s′ ∈ S. (s, e, s′) ∈ Tran.

(ii) (s, e, s′) ∈ Tran and (s, e, s′′) ∈ Tran ⇒ s′ = s′′. (iii) e_{1}Ie_{2} and (s, e_{1}, s_{1}) ∈ Tran and (s, e_{2}, s_{2}) ∈ Tran

⇒ ∃u. (s_{1}, e_{2}, u) ∈ Tran and (s_{2}, e_{1}, u) ∈ Tran.

(iv) e_{1}Ie_{2} and (s, e_{1}, s_{1}) ∈ Tran and (s_{1}, e_{2}, u) ∈ Tran

⇒ ∃s_{2}. (s, e_{2}, s_{2}) ∈ Tran and (s_{2}, e_{1}, u) ∈ Tran.

Condition (i) stipulates that every event in E must appear as the label of some transition in the system. The second condition guarantees that the system is deterministic. The third and fourth conditions express properties of independence: condition (iii) says that if two independent events are enabled at a state, then they should be able to occur “together” and reach a common state; condition (iv) says that if two independent events occur immediately after one another in the system, it should also be possible for them to occur with their order interchanged.

Asynchronous transition systems can be equipped with a natural notion of morphism to form a category [13]. In [13], Winskel and Nielsen establish a coreflection between a subcategory of asynchronous transition systems, which we shall call elementary asynchronous transition systems, and a category of 1-safe Petri nets.

Here, we shall restrict our attention to the correspondence between these two categories at the level of objects. At this level, what the coreflection establishes is that given an elementary asynchronous transition system, we can construct a 1-safe Petri net whose case graph is isomorphic to the transition system we started with.

The extra axioms characterizing elementary asynchronous transition systems are phrased in terms of generalized regions.

Definition 2.3 (Regions) Let AT S = (S, i, E, I, Tran) be an asynchronous transition system. A region of AT S is a pair of functions r = (r_{S}, r_{E}) where

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

r_{E} : E → ({0, 1} × {0, 1}) such that (i) ∀(s, e, s′) ∈ Tran. (r_{E}(e) = (1, 0) or r_{E}(e) = (1, 1)) ⇒ r_{S}(s) = 1.

(ii) ∀(s, e, s′) ∈ Tran. r_{S}(s′) = r_{S}(s) + x_{2} − x_{1}, where r_{E}(e) = (x_{1}, x_{2}).

(iii) Let e_{1}, e′_{1} ∈ E and r_{E}(e_{1}) = (x_{1}, x_{2}) and r_{E}(e′_{1}) = (x′_{1}, x′_{2}).

If e_{1}Ie′_{1} then ((x_{1} = 1) or (x_{2} = 1)) ⇒ x′_{1} = x′_{2} = 0.

For convenience, we shall refer to both components, r_{S} and r_{E}, of a region r simply as r.

Regions correspond to the places of the 1-safe net that one would like to associate with an elementary asynchronous transition system AT S. Intuitively, we want to associate with AT S a 1-safe Petri net N such that AT S represents the case graph of N. Thus, the states of AT S should correspond to the reachable markings of N and the events of AT S should correspond to the transitions of N. Let r be a region in AT S. We specify whether or not the “place” r is marked at the “marking” s by r(s). For each “transition” e, r(e) says how r is “connected” to e in the associated net. Conditions (i) and (ii) in the definition of a region then correspond to the firing rule for Petri nets. Condition (iii) reflects the intuition that two transitions in a net are independent provided their neighbourhoods are disjoint.

In [13], regions (or conditions, as they are called there) are described slightly differently, in terms of subsets of states and transitions. Our formulation is equivalent to the one in [13]. Our regions are generalizations of those originally used to describe the connection between elementary net systems and elementary transition systems [7, 10].

We introduce some notational conventions for regions, borrowed from net theory. Given a region r and an event e, we say that r ∈ ^{•}e if r(e) = (1, 0) or r(e) = (1, 1). Similarly, we say that r ∈ e^{•} if r(e) = (0, 1) or r(e) = (1, 1). We say that e ∈ ^{•}r if r ∈ e^{•} and e ∈ r^{•} if r ∈ ^{•}e. Finally, for s ∈ S, we sometimes say that s ∈ r, or that r holds at s, to indicate that r(s) = 1.

We can now characterize elementary asynchronous transition systems.

Definition 2.4 (Elementary asynchronous transition systems) Let AT S = (S, i, E, I, Tran) be an asynchronous transition system. AT S is said to be elementary if it satisfies the following three conditions.

(i) Every state in S is reachable by a finite sequence of transitions from the initial state i. (Reachability)

(ii) ∀s, s′ ∈ S. s ≠ s′ ⇒ ∃ a region r. r(s) ≠ r(s′). (Separation)

(iii) ∀s ∈ S. ∀e ∈ E. If there does not exist s′ such that (s, e, s′) ∈ Tran, then there exists an r ∈ ^{•}e such that r(s) = 0. (Enabling)

Call a region r non-trivial iff there exists some e ∈ E such that r ∈ ^{•}e or r ∈ e^{•}. Clearly, for a trivial region r, r(s) = r(s′) for all s, s′ ∈ S. So, it follows that conditions (ii) and (iii) in the definition of elementary asynchronous transition systems actually require the existence of a non-trivial region satisfying the required properties.

As we have mentioned before, given an elementary asynchronous transition system AT S, we can construct a 1-safe net N_{AT S} whose case graph is isomorphic to AT S. The transitions of N_{AT S} are given by the events of AT S and the places of N_{AT S} are given by the regions of AT S. We shall not go into the details of the construction of N_{AT S}. The interested reader is referred to [13]. (A similar construction is described for going from elementary transition systems to elementary net systems in [10]).

A final point that should be emphasized is that so far we have been working with unlabelled asynchronous transition systems. Thus, the “labels” on the transitions correspond to the events of the system and are analogous to the “names” of the transitions of a Petri net. To relate asynchronous transition systems to, say, process algebras like CCS, we have to add an extra layer of labelling by means of a labelling function as follows.

Definition 2.5 (Labelled asynchronous transition systems) Let Σ be an alphabet. A Σ-labelled asynchronous transition system is a pair (AT S, l) where AT S = (S, i, E, I, Tran) is an asynchronous transition system, and l : E → Σ is a labelling function.

Thus, for the CCS term a nil∥a nil, we would associate an asynchronous transition system with two events e_{1} and e_{2} which are independent of each other, both labelled a.

Given a labelled elementary asynchronous transition system, we can easily transport the labelling to the corresponding net that we construct since we keep track of the underlying events. In fact, in [13] it is shown that the coreflection between unlabelled elementary asynchronous transition systems and 1-safe Petri nets can be lifted in a natural way to a coreflection between the corresponding categories of labelled systems. We shall not go into the details here.

3 The language and its operational semantics

The process language we consider is a subset of CCS where choice is always guarded.

We fix a set of actions Act = Λ ∪ \overline{Λ}, where Λ is a set of names ranged over by α, β, … and \overline{Λ} is the corresponding set of co-names \{\overline{α} | α ∈ Λ\}. As usual, we assume that ^{−} is a bijection such that \overline{\overline{α}} = α for all α ∈ Λ. The symbol τ ∉ Act denotes the invisible action. We use a, b, c … to range over Act and μ, ν … to range over Act_{τ} = Act ∪ {τ}. We also assume a set V of process variables and let x, y, … range over V.

The set of process expressions Proc is given by the following grammar.

P ::= ∑_{i∈I} μ_{i}P_{i} | P ∥P | P \α | x | rec x.P

where μ_{i} ∈ Act_{τ}, α ∈ Λ and x ∈ V.

Thus, the guarded sum ∑_{i∈I} μ_{i}P_{i} represents the process which can execute any one of the actions μ_{i} (which could be τ) and evolve into the corresponding process E_{i}. The indexing set I could, in general, be infinite. We abbreviate by nil the process consisting of a guarded sum indexed by the empty set. The normal CCS prefixing operator aP is represented by a guarded sum over a singleton index set.

The other constructs are standard. P_{1}∥P_{2} denotes the parallel composition of P_{1} and P_{2}—i.e. the process consisting of P_{1} and P_{2} executing independently, with the possibility of synchronization. P \α denotes the restriction of P with respect to α—P \α is the process that behaves like P but is not permitted to perform visible actions α or \overline{α}. rec x.P is the process satisfying the recursive definition x = P. We assume that each occurrence of x in P is guarded by an action μ ∈ Act_{τ}—in other words, each x in P appears within a subterm of the form ∑_{i∈I} μ_{i}P_{i}. We do not consider the relabelling operator, though it could be incorporated without too much difficulty into our setup.

We enrich the standard operational semantics of CCS by adding some information on the labels of the transitions which will permit us to directly extract the underlying events of the transition system representing the behaviour of a CCS term.

We have to depart slightly from the traditional transition system for CCS, where states are given directly by process expressions. We will need to identify recursive processes with their one-step unfoldings. So, define ≡ to be the least congruence with respect to the operators ∥ and \α such that

rec x.P ≡ P [rec x.P/x]

where, as usual, P [rec x.P/x] denotes the term obtained by substituting rec x.P for x in P. For P ∈ Proc, let [P] denote the set of process expressions equivalent to P. The states of our transition system will effectively be equivalence classes of process expressions.

Our operational semantics is defined as follows (henceforth we assume that {0, 1}∩Λ = ∅):

P = ∑_{i∈I}μ_{i}P_{i}− →^{\frac{μ_{i}}{[P][P_{i}]}}P_{i}  (Sum)
P_{0}⟶^{\frac{μ}{u}}P′_{0}  implies P_{0}∥P_{1}−→^{\frac{μ}{0u}}P′_{0}∥P_{1}  (Par)

P_{1}∥P_{0}−→^{\frac{μ}{1u}}P_{1}∥P′_{0}

P_{0}⟶^{\frac{a}{u}}P′_{0}, P_{1}⟶^{\frac{\overline{a}}{v}}P′_{1}  implies P_{0}∥P_{1}− →^{\frac{τ}{⟨0u,1v⟩}}P′_{0}∥P′_{1} (Com)
P ⟶^{\frac{μ}{u}}P′  implies P \α−→^{\frac{μ}{αu}}P′\α,  (Res)

μ ∉ \{α, \overline{α}\}

P ⟶^{\frac{μ}{u}}P′, P ≡ P_{1} and P′ ≡ P′_{1} implies P_{1}⟶^{\frac{μ}{u}}P′_{1}  (Struct)

So, for a basic action performed by a process of the form ∑_{i∈I} μ_{i}P_{i}, we tag the transition with the source and target process expressions. We extend the tag with 0’s and 1’s on the left as we lift the transition through the left and right branches of a parallel composition. With each communication, we keep track of the tags corresponding to the two components participating in the communication. By extending the tag to the left with α for each restriction \α, we keep track of the nesting of restrictions with respect to the overall structure of the process. This will be crucial in order to be able to determine whether or not a communication is possible even though the visible actions which make up the communication are restricted away. Finally, (Struct) ensures that processes from the same equivalence class are capable of making exactly the same moves.

The string of 0’s and 1’s which we use to tag a transition when we move down the left and right branches of a parallel composition essentially pins down the location where the transition occurs. Locations will provide us with a natural way of identifying independence between transitions. Our notion of location is closely related to the static approach advocated by Aceto [1] for dealing with the idea of locations introduced by Boudol et al [4, 5]. We have more to say on the connection between our approach and the approach of [1, 4, 5] in Section 6.

[figure: a∥b; nil∥b; a∥nil; nil∥nil; a; 0[a][nil]; b; 1[b][nil]; b; 1[b][nil]; a; 0[a][nil]; ab + ba; b; a; nil; a; [ab+ba][b]; b; [ab+ba][a]; b; [b][nil]; a; [a][nil]]

Figure 1: Concurrency versus non-deterministic interleaving

It is not difficult to establish that the states of the transition system defined by our operational semantics are in fact equivalence classes of process expressions. Formally, we have the following proposition.

Proposition 3.1

∀P, P′. ∀μ. ∀u. ( P ⟶^{\frac{μ}{u}}P′ iff ∀P_{1} ≡ P. ∀P′_{1} ≡ P′. P_{1}⟶^{\frac{μ}{u}}P′_{1} ).

We conclude this section with a couple of examples. The first example illustrates how our semantics distinguishes concurrency from non-deterministic interleaving. Figure 1 shows the behaviour of the processes a∥b and ab + ba. Notice that the transition system for a∥b has four transitions, but only two distinct labels on the transitions. This captures the fact that there are only two underlying (independent) events, one labelled a and the other labelled b. In contrast, the process ab + ba has four distinct events.

The next example illustrates how our semantics deals with recursion. Consider the two processes rec x.ax∥rec x.ax and rec x.(ax∥ax). The transition systems corresponding to these processes are shown in Figure 2.

The standard interleaved transition system for the first process would consist of a single state with a single a-labelled transition looping back to that state. On the other

[figure: rec x.ax∥rec x.ax; a; 1[rec x.ax][rec x.ax]; a; 0[rec x.ax][rec x.ax]; P = rec x(ax∥ax); P ∥aP; aP ∥P; (P ∥aP)∥aP; …; (P ∥P); …; aP ∥(aP ∥P); …; …; …; …; …; a; 0[aP][P]; a; 1[aP][P]; a; 1[aP][P]; a; 0[aP][P]; a; 00[aP][P]; a; 11[aP][P]]

Figure 2: Recursion hand, our semantics generates two a-labelled transitions, because, intuitively, the a could occur at two different locations in the process. However, notice that our semantics still yields a finite transition system for this term.

The standard interleaved transition system for rec x.(ax∥ax) is infinite, because unfolding the term creates more and more components in parallel. Our semantics also assigns an infinite transition system in such a case. Notice though, that it still keeps track of the underlying events in a consistent manner. Thus, the two top level a-transtions (labelled − →^{\frac{a}{0[aP][P]}} and − →^{\frac{a}{1[aP][P]}}) correspond to events which are distinct from the a-transitions

arising in the new components generated by the unfolding (for example, the transition

labelled − →^{\frac{a}{00[aP][P]}}).

The two examples in Figure 2 illustrate a general point about our semantics—our semantics will assign a finite transition system to a process P whenever the standard interleaving semantics would do so. This connection is made more precise in Section 5.

4 From CCS to asynchronous transition systems

We would like to establish that the transition system describing the behaviour of a process P ∈ Proc is in fact a (labelled) elementary asynchronous transition system.

To do this, we first show that the extra information that we have introduced into the labels of the transitions when defining the operational semantics of our process language is sufficient to distinguish the events of the underlying transition system and define a natural notion of independence between events.

We then prove that we have “enough” regions around to ensure that the transition system we are considering satisfies the two regional separation properties which are required for it to be elementary.

We begin by establishing a simple fact about the nature of the labels in the transition system defined by our operational semantics.

Proposition 4.1 (Syntax of labels)

For any transition P̂⟶^{\frac{μ}{u}}P̂′, u is of the form

(i) s[P][P′], where s ∈ ({0, 1} ∪ Λ)^{∗}, and μ ∈ Act.

(ii) s[P][P′], where s ∈ ({0, 1} ∪ Λ)^{∗}, and μ = τ.

(iii) s⟨s_{0}[P_{0}][P′_{0}], s_{1}[P_{1}][P′_{1}]⟩, where s, s_{0}, s_{1} ∈ ({0, 1} ∪ Λ)^{∗}, and μ = τ.

Proof By induction on the length of the derivation of the transition P̂⟶^{\frac{μ}{u}}P̂′. □

Henceforth, for convenience, we shall omit the brackets around the process expressions in the event labels and simply write sP P′ instead of s[P][P′] and s⟨s_{0}P_{0}P′_{0}, s_{1}P_{1}P′_{1}⟩ instead of s⟨s_{0}[P_{0}][P′_{0}], s_{1}[P_{1}][P′_{1}]⟩.

Each distinct label in our transition system will correspond to an event, as follows.

Definition 4.2 (Events) Define the set of events Ev as follows:

Ev = \{(μ, u) | ∃P, P′ ∈ Proc. P ⟶^{\frac{μ}{u}}P′\}

For e ∈ Ev, we can identify Loc(e) ⊆ {0, 1}^{∗}, the location(s) where e occurs, as follows:

∀e = (μ, u). Loc(e) = \{ \begin{matrix}\{s ↓_{\{0,1\}}\} & if u = sP P′ \\ \{ss_{0} ↓_{\{0,1\}}, ss_{1} ↓_{\{0,1\}}\} & if u = s⟨s_{0}P_{0}P′_{0}, s_{1}P_{1}P′_{1}⟩ \end{matrix}

where, for s ∈ ({0, 1} ∪ Λ)^{∗}, s ↓_{{0,1}} denotes the projection of s onto {0, 1}. In other words, s ↓_{{0,1}} is the subsequence of s obtained by erasing all elements not in {0, 1}.

From the way we introduce information about locations into our event labels, it is clear that the location Loc(e) of an event e is a string which identifies the nested component where e occurs. We can identify a natural independence relation on locations and lift it to events as follows.

Definition 4.3 (Independence on events)

Define an independence relation on locations I_{l} ⊆ {0, 1}^{∗} × {0, 1}^{∗} as follows:

∀s, s′ ∈ {0, 1}^{∗}. (s, s′) ∈ I_{l} iff s ⪯̸ s′ and s′ ⪯̸ s

where ⪯ is the prefix relation on strings.

We can extend this to a relation Î_{l} ⊆ ({0, 1} ∪ Λ)^{∗} × ({0, 1} ∪ Λ)^{∗} in the obvious way.

∀ŝ, ŝ′ ∈ ({0, 1} ∪ Λ)^{∗}. (ŝ, ŝ′) ∈ Î_{l} iff (ŝ ↓_{{0,1}}, ŝ′ ↓_{{0,1}}) ∈ I_{l}

For convenience, we shall write both Î_{l} and I_{l} as I_{l}.

Using I_{l} we can define an independence relation on events I ⊆ Ev × Ev as follows:

∀e, e′ ∈ Ev. (e, e′) ∈ I iff ∀s ∈ Loc(e). ∀s′ ∈ Loc(e′). (s, s′) ∈ I_{l}

Having defined the set of events Ev and the independence relation I on events, we have essentially all the data we need to define an asynchronous transition system corresponding to the operational behaviour of a process P. However, we shall hold off defining this transition system for a while and first analyze the behaviour of P as given by the operational semantics in greater detail.

To analyze the behaviour of a process term P, we will need to decompose it into its sequential components.

Definition 4.4 (Component of P at location s)

Comp : ({0, 1} ∪ Λ)^{∗} × Proc ⇀ Proc

is a (partial) function defined inductively as follows.

Comp(ε, P)  = P, provided P ≠ rec x.P_{x}

(where ε is the empty string)

Comp(0s, P_{0}∥P_{1}) = Comp(s, P_{0})
Comp(1s, P_{0}∥P_{1}) = Comp(s, P_{1})
Comp(αs, P \α) = Comp(s, P)
Comp(s, rec x.P) = Comp(s, P [rec x.P/x])

The following observation will prove useful later on.

Proposition 4.5

(i) ∀P ∈ Proc. Comp(ε, P) ≡ P.

(ii) If P ≡ P′ and Comp(s, P) is defined, then Comp(s, P) ≡ Comp(s, P′).

(iii) ∀P ∈ Proc. Comp(s_{1}s_{2}, P) ≡ Comp(s_{2}, Comp(s_{1}, P)).

Proof These follow in a straightforward way from the definition of Comp. □

Having identified the sequential components of a process term P, the next lemma shows that we can use the extra labelling information on each transition to “project” each move of P down to the actual sequential component where it occurs.

Lemma 4.6 (Decomposing transitions)

(i) ∀s. ∀P. If P − →^{\frac{μ}{sP_{1}P′_{1}}}P′ then P_{1} = ∑_{i∈I}μ_{i}P_{i}− →^{\frac{μ_{j}}{P_{1}P′_{1}}}P_{j} = P′_{1}, where j ∈ I, μ_{j} = μ and Comp(s, P) ≡ P_{1}, Comp(s, P′) ≡ P′_{1} and neither μ nor \overline{μ} appears in s.

(ii) ∀s, s_{0}, s_{1}. ∀P. If  P −  →^{\frac{τ}{s⟨s_{0}P_{0}P′_{0},s_{1}P_{1}P′_{1}⟩}}P′ then P_{0}− →^{\frac{a}{P_{0}P′_{0}}}P′_{0}, P_{1}− →^{\frac{\overline{a}}{P_{1}P′_{1}}}P′_{1}, for some a, \overline{a} ∈ Act, Comp(ss_{0}, P) ≡ P_{0}, Comp(ss_{0}, P′) ≡ P′_{0}, Comp(ss_{1}, P) ≡ P_{1}, Comp(ss_{1}, P′) ≡ P′_{1} and s_{0} = 0s′_{0} and s_{1} = 1s′_{1} and neither a nor \overline{a} appears in s_{0} or s_{1}.

Proof

(i) We proceed by induction on n, the length of the derivation of the transition

P − →^{\frac{μ}{sP_{1}P′_{1}}}P′.

n = 1: Then P must be of the form ∑_{i∈I} μ_{i}P_{i} with μ = μ_{j} for some j ∈ I and the required result follows trivially.

n > 1: We have to consider the rule applied at the final step of the derivation of this transition.

In all cases the proof follows in a straightforward manner from the induction hypothesis and we omit the details.

(ii) We proceed by induction on n = |s|.

n = 0: We then know that the last rule applied to derive the transition P − →^{\frac{τ}{⟨s_{0}P_{0}P′_{0},s_{1}P_{1}P′_{1}⟩}}P′

which modified its label was (Com).

By the definition of (Com), it follows that P = P_{l}∥P_{r} and P′ = P′_{l}∥P′_{r}, with P_{l}− →^{\frac{a}{s′_{0}P_{0}P′_{0}}}P′_{l}

and P_{r}− →^{\frac{\overline{a}}{s′_{1}P_{1}P′_{1}}}P′_{r}, where a ∈ Act and s_{0} = 0s′_{0} and s_{1} = 1s′_{1}. The rest of the result then

follows by appealing to (i).

After the last application of (Com), (Struct) may have been applied one or more times to obtain the actual transition. However, in applying (Struct), the label on the transition is left unchanged. Further, the new process expressions which are the source and target of the transition are structurally equivalent to the original ones, so, by Proposition 4.5 the required property continues to hold.

n > 0: We have to consider the cases where s = 0s′, s = 1s′ and s = αs′ for some α ∈ Λ. All three cases follow in a straightforward manner from the induction hypothesis.

□

Just as we can project moves down from a process to its sequential components, we can identify when the moves of the sequential components can be lifted to the whole process. (This is not completely straightforward. The move of the sequential component may be forbidden in the overall process because the component lies within the scope of a restriction. This is where we crucially use the information in the labels about the nesting of restriction symbols with respect to the locations).

Lemma 4.7 (Composing transitions)

(i) ∀s. ∀P. If Comp(s, P) ≡ P_{1} and P_{1} = ∑_{i∈I}μ_{i}P_{i}− →^{\frac{μ_{j}}{P_{1}P′_{1}}}P_{j} = P′_{1}, where j ∈ I and neither μ_{j} nor \overline{μ_{j}} appears in s then P − →^{\frac{μ_{j}}{sP_{1}P′_{1}}}P′, where Comp(s, P′) ≡ P′_{1}

(ii) ∀s, s_{0}, s_{1}. ∀P. If  Comp(ss_{0}, P) ≡ P_{0}, Comp(ss_{1}, P) ≡ P_{1}, with P_{0}− →^{\frac{a}{P_{0}P′_{0}}}P′_{0}, P_{1}− →^{\frac{\overline{a}}{P_{1}P′_{1}}}P′_{1}, for some a, \overline{a} ∈ Act, where s_{0} = 0s′_{0}, s_{1} = 1s′_{1} and neither a nor \overline{a} appears in s_{0} or s_{1}. then P −  →^{\frac{τ}{s⟨s_{0}P_{0}P′_{0},s_{1}P_{1}P′_{1}⟩}}P′ where Comp(ss_{0}, P′) ≡ P′_{0} and Comp(ss_{1}, P′) ≡ P′_{1}.

Proof (i) We proceed by induction on n = |s|, the length of s.

n = 0: Then Comp(ε, P) ≡ P_{1} = ∑_{i∈I} μ_{i}P_{i}. Clearly P − →^{\frac{μ_{j}}{P_{1}P′_{1}}}P′ as required, where

Comp(ε, P′) ≡ P′ ≡ P′_{1}. n > 0: We have three cases to consider—s = 0s′, s = 1s′ and s = αs′, for some α ∈ Λ. Let s = 0s′. Then, since Comp(0s′, P) is defined, P must be equivalent to an ex-

pression of the form P_{l}∥P_{r}. Since Comp(0s′, P) ≡ Comp(s′, P_{l}) ≡ P_{1}, by the induction hypothesis, we know that P_{l}− →^{\frac{μ_{j}}{s′P_{1}P′_{1}}}P′_{l} for some P′_{l} such that Comp(s′, P′_{l}) ≡ P′_{1}. Applying

the rule (Par) (and possibly (Struct)), it then follows that P ≡ P_{l}∥P_{r}− →^{\frac{μ_{j}}{sP_{1}P′_{1}}}P′_{l}∥P_{r} ≡ P′

with Comp(s, P′) ≡ P′_{1} by the definition of Comp.

The case s = 1s′ is symmetric to the case s = 0s′.

The last case is when s = αs′. Then it is clear that P is equivalent to an expression of the form P_{α}\α. Since Comp(αs′, P) ≡ Comp(s′, P_{α}) ≡ P_{1}, by the induction hypothesis P_{α}− →^{\frac{μ_{j}}{s′P_{1}P′_{1}}}P′_{α} with Comp(s′, P_{α}) ≡ P_{1} and Comp(s′, P′_{α}) ≡ P′_{1}. Since we know that neither

μ_{j} nor \overline{μ_{j}} appear in αs′, we can apply (Res) (and possibly (Struct)) to obtain P ≡ P_{α}\α− →^{\frac{μ_{j}}{sP_{1}P′_{1}}}P′_{α}\α ≡ P′ with Comp(s, P′) ≡ P′_{1} by the definition of Comp.

(ii) By induction on n = |s|.

n = 0:

Since s_{0} = 0s′_{0} and s_{1} = 1s′_{1} and both Comp(s_{0}, P) and Comp(s_{1}, P) exist, it must be the case that P is equivalent to an expression of the form P_{l}∥P_{r}.

Then, by appealing to (i) we know that P_{l}− →^{\frac{a}{s′_{0}P_{0}P′_{0}}}P′_{l} and P_{r}− →^{\frac{\overline{a}}{s′_{1}P_{1}P′_{1}}}P′_{r}, where

Comp(s′_{0}, P′_{l}) ≡ P′_{0} and Comp(s′_{1}, P′_{r}) ≡ P′_{1}. Applying (Com) (and possibly (Struct)), it then follows that P ≡ P_{l}∥P_{r}− →^{\frac{τ}{⟨s_{0}P_{0}P′_{0},s_{1}P_{1}P′_{1}⟩}}P′_{l}∥P′_{r} ≡ P′. From the definition of Comp it

is straightforward to check that Comp(s_{0}, P′) ≡ P′_{0} and Comp(s_{1}, P′) ≡ P′_{1} as required.

n > 0:

The result follows in a straightforward manner from the induction hypothesis. The proof is similar to the induction step in part (i) of this lemma and we omit the details.

□

From the way we have described the “local” behaviour of processes, it is natural to expect that the occurrence of an event e should leave sequential components lying at locations independent of Loc(e) untouched. This is expressed by the following lemma.

Lemma 4.8

(i) ∀s, s′. ∀P. P − →^{\frac{μ}{sP_{1}P′_{1}}}P′ and (s, s′) ∈ I_{l} implies that Comp(s′, P) = Comp(s′, P′).

(ii) ∀s, s_{0}, s_{1}, s′. ∀P. P − →^{\frac{τ}{s⟨s_{0}P_{0}P′_{0},s_{1}P_{1}P′_{1}⟩}}P′ and (ss_{0}, s′) ∈ I_{l} and (ss_{1}, s′) ∈ I_{l} implies that

Comp(s′, P) = Comp(s′, P′).

Proof (i) By induction on n = |s|.

n = 0: Then s = ε and so for any s′, (s, s′) ∉ I_{l} and there is nothing to prove.

n > 0: First, consider the case where s = 0s_{1}. Then P must be equivalent to a process of the form P_{l}∥P_{r}.

Then Comp(s, P) = Comp(s_{1}, P_{l}). Since the transition must have come from the left side of a parallel compostion, we have P_{l}− →^{\frac{μ}{s_{1}P_{1}P′_{1}}}P′_{l}. It is also straightforward to argue

that P′ must be equivalent to P′_{l}∥P_{r}.

For Comp(s′, P) to be defined, s′ must either be of the form 0s′_{1} or 1s′_{1}.

Suppose that s′ = 0s′_{1}. Then, we must have (s_{1}, s′_{1}) ∈ I_{l} as well and, by the induction hypothesis, Comp(s′_{1}, P_{l}) = Comp(s′_{1}, P′_{l}). Since Comp(s′, P) = Comp(s′_{1}, P_{l}) and Comp(s′, P′) = Comp(s′_{1}, P′_{l}), the result follows.

On the other hand, if s′ = 1s′_{1}, then we know that Comp(s′, P) = Comp(s′_{1}, P_{r}) = Comp(s′, P′) and we are done.

The case s = 1s_{1} is symmetric to the case s = 0s_{1}.

The final case is where s = αs_{1}. Then P must be equivalent to a process of the form P_{α}\α. It then follows that s′ must also be of the form αs′_{1} in order for Comp(s′, P) to be defined. But then (s_{1}, s′_{1}) ∈ I_{l} and the result follows easily from the induction hypothesis.

(ii) Again by induction on n = |s|.

This time we have to analyze ss_{0} and ss_{1} with respect to s′. The result follows by a straightforward, though tedious argument, similar to the one used to prove part (i) of this lemma.

□

We now have enough results about the operational behaviour of a process to be able to prove the result we are after. Define the obvious transition system T S_{CCS} = (S, i, E, I, Tran) where

• S = {[P] | P ∈ Proc}.

• E = Ev.

• I ⊆ Ev × Ev is given by Definition 4.3.

• Tran ⊆ S × Ev × S = \{([P], (μ, u), [P′]) | P ⟶^{\frac{μ}{u}}P′\}.

The only problem is that this transition system does not have an initial state i. It can be checked, however, that the notion of a region does not depend on the existence of an initial state. So, for convenience, we shall define regions over this (large) transition system without an initial state, and then prove that the axioms for elementariness hold for the reachable part of the transition system for an arbitrary choice of initial state.

In what follows, we shall, for simplicity, denote an element [P] of S simply as P.

Definition 4.9 (Regions)

Let s ∈ ({0, 1} ∪ Λ)^{∗} and P = ∑_{i∈I}μ_{i}P_{i}. Then R(s, P) is a pair of functions

R(s, P)_{S} : S → {0, 1} and

R(s, P)_{E} : E → ({0, 1} × {0, 1}) defined as follows:

∀P′ ∈ S. R(s, P)_{S}(P′) = \{ \begin{matrix}1 & if Comp(s, P′) ≡ P \\ 0 & otherwise \end{matrix}

∀e = (μ, s_{1}P_{1}P′_{1}) ∈ E. R(s, P)_{E}(e) = (x, y), where :

x = \{ \begin{matrix}1 & if s = s_{1} and P ≡ P_{1} \\ 0 & otherwise \end{matrix}
y = \{ \begin{matrix}1 & if ∃s′_{1}. s_{1}s′_{1} = s and Comp(s′_{1}, P′_{1}) ≡ P \\ 0 & otherwise \end{matrix}

∀e = (τ, s′⟨s_{0}P_{0}P′_{0}, s_{1}P_{1}P′_{1}⟩) ∈ E. R(s, P)_{E}(e) = (x, y), where :

x = \{ \begin{matrix}1 & if (s = s′s_{0} and P ≡ P_{0}) \\ & or (s = s′s_{1} and P ≡ P_{1}) \\ 0 & otherwise \end{matrix}

y = \{ \begin{matrix}1 & if ∃s′_{0}. s′s_{0}s′_{0} = s and Comp(s′_{0}, P′_{0}) ≡ P \\ & or ∃s′_{1}. s′s_{1}s′_{1} = s and Comp(s′_{1}, P′_{1}) ≡ P \\ 0 & otherwise \end{matrix}

So, a region R(s, P) holds at a state P′ iff the component of P′ at location s is a sequential component equivalent to P.

For e = (μ, u), R(s, P) ∈ ^{•}e iff e is located at s and e originates from a sequential component equivalent to P.

To decide when R(s, P) ∈ e^{•} is a little more complicated. If e = (μ, s_{1}P_{1}P′_{1}), the naïve expectation is that R(s, P) ∈ e^{•} provided that s = s_{1} and P′_{1} ≡ P. However P′_{1} need not be a sequential term, so we actually have to link e to the sequential components of P′_{1}. In other words, we have to check that Comp(s′_{1}, P′_{1}) ≡ P for some s′_{1}. Since s′_{1} is the “sub-location” of the component with respect to s_{1}, the location where e occurs, it must in fact be the case that s_{1}s′_{1} = s in order that R(s, P) ∈ e^{•}.

Lemma 4.10 ∀s. ∀P = ∑_{i∈I}μ_{i}P_{i}. R(s, P) is a region of the (pseudo)-transition system

T S_{CCS}.

Proof We have to establish three facts:

(i) ∀R(s, P). ∀e, e′ ∈ E. If (e, e′) ∈ I then R(s, P) ∈ (^{•}e ∪ e^{•}) ⇒ R(s, P) ∉ (^{•}e′ ∪ e′^{•}).

(ii) ∀R(s, P). ∀(P_{1}, (μ, u), P′_{1}) ∈ Tran. R(s, P) ∈ ^{•}(μ, u) implies R(s, P)(P_{1}) = 1.

(iii) ∀R(s, P). ∀(P_{1}, (μ, u), P′_{1}) ∈ Tran. R(s, P)(P′_{1}) = R(s, P)(P_{1}) + y − x, where R(s, P)(μ, u) = (x, y).

(i) follows in a straightforward manner from the definition of the independence relation I and the definition of regions.

(ii) follows directly from Lemma 4.6 and the definition of regions.

To establish (iii) we have to consider the various possibilities. First, assume that the event e is of the form (μ, s_{2}P_{2}P′_{2}). In other words, we are looking at a transition (P_{1}, (μ, s_{2}P_{2}P′_{2}), P′_{1}) ∈ Tran. Consider an arbitrary region r = R(s, P).

(a) Suppose that r ∈ ^{•}e and r ∉ e^{•}. Since r ∈ ^{•}e, we know that s = s_{2} and P ≡ P_{2}. Since r ∉ e^{•}, we know that Comp(ε, P′_{2}) ≢ P (since s_{2}ε = s). By Lemma 4.6, we know that Comp(s, P_{1}) = Comp(s_{2}, P_{1}) ≡ P_{2} ≡ P and so R(s, P)(P_{1}) = 1. On the other hand, again by Lemma 4.6, Comp(s_{2}, P′_{1}) ≡ P′_{2}, which implies that Comp(s, P′_{1}) = Comp(s_{2}, P′_{1}) ≢ P. So R(s, P)(P′_{1}) = 0 and we are done.

(b) Next, suppose that r ∉ ^{•}e and r ∈ e^{•}. Since r ∈ e^{•}, we know that there exists s′_{2} such that s_{2}s′_{2} = s and Comp(s′_{2}, P′_{2}) ≡ P. To find out whether Comp(s, P′_{1}) ≡ P, we can rewrite this as Comp(s_{2}s′_{2}, P′_{1}). This is equivalent to Comp(s′_{2}, Comp(s_{2}, P′_{1})). But, by Lemma 4.6, we know that Comp(s_{2}, P′_{1}) ≡ P′_{2} and so we have Comp(s, P′_{1}) ≡ Comp(s′_{2}, P′_{2}) ≡ P. So R(s, P)(P′_{1}) = 1.

On the other hand, since r ∉ ^{•}e, we know that either s ≠ s_{2} or s = s_{2} and P_{2} ≢ P. Suppose s = s_{2}. Then Comp(s, P_{1}) ≡ P_{2} (by Lemma 4.6) and, since P_{2} ≢ P, we have R(s, P)(P_{1}) = 0. On the other hand, if s ≠ s_{2}, we know from the fact that r ∈ e^{•} that s_{2} ⪯ s—i.e. there exists s′_{2} such that s_{2}s′_{2} = s. But we know from Lemma 4.6 that Comp(s_{2}, P_{1}) ≡ P_{2} and, furthermore, P_{2} = ∑_{i} μ_{i}P_{i}. Hence Comp(s, P_{1}) ≡ Comp(s′_{2}, Comp(s_{2}, P_{1})) ≡ Comp(s′_{2}, P_{2}) must be undefined, because s′_{2} ≠ ε. Thus Comp(s, P_{1}) ≢ P and so R(s, P)(P_{1}) = 0.

(c) Next, suppose that r ∈ ^{•}e and r ∈ e^{•}. Then, from arguments similar to the ones used for (a) and (b), it follows that R(s, P)(P_{1}) = R(s, P)(P′_{1}) = 1.

(d) Finally, suppose that r ∉ ^{•}e and r ∉ e^{•}.

If s = s_{2}, by Lemma 4.6, it is easy to see that Comp(s, P_{1}) = Comp(s_{2}, P_{1}) ≡ P_{2}. So R(s, P)(P_{1}) = 1 iff P ≡ P_{2} iff R(s, P) ∈ ^{•}e. So, we must have R(s, P)(P_{1}) = 0. Similarly, we can argue that R(s, P)(P′_{1}) = 0.

Next consider the case when s ≠ s_{2}.

Suppose that (s, s_{2}) ∈ I_{l}. Then, by Lemma 4.8, it follows that R(s, P)(P_{1}) = R(s, P)(P′_{1}) and we are done.

On the other hand, suppose that s ⪯ s_{2}. Then there exists s′ such that ss′ = s_{2}. We know, by Lemma 4.6, that Comp(s_{2}, P_{1}) ≡ P_{2}. So, if Comp(s, P_{1}) ≡ P, where P = ∑_{i} μ_{i}P_{i}, then we would have Comp(s_{2}, P_{1}) ≡ Comp(s′, Comp(s, P_{1})) ≡ Comp(s′, P) which is undefined, since s′ ≠ ε. This is a contradiction, so we cannot have Comp(s, P_{1}) ≡ P and therefore R(s, P)(P_{1}) = 0. By a similar argument, it then follows that R(s, P)(P′_{1}) = 0 as well.

The final situation is when s_{2} ⪯ s. Then there exists s′_{2} such that s_{2}s′_{2} = s. We know that Comp(s, P_{1}) ≡ Comp(s′_{2}, Comp(s_{2}, P_{1})) ≡ Comp(s′_{2}, P_{2}) (by Lemma 4.6.) But, P_{2} = ∑_{i} μ_{i}P_{i}, so Comp(s′_{2}, P_{2}) must be undefined for s′_{2} ≠ ε and hence R(s, P)(P_{1}) = 0. To show that R(s, P)(P′_{1}) = 0, notice that Comp(s′_{2}, P′_{2}) ≢ P because R(s, P) ∉ e^{•}. But Comp(s, P′_{1}) = Comp(s_{2}s′_{2}, P′_{1}) ≡ Comp(s′_{2}, Comp(s_{2}, P′_{1})) ≡ Comp(s′_{2}, P′_{2}), by Lemma 4.6. So Comp(s, P′_{1}) ≢ P and R(s, P)(P′_{1}) = 0.

We have to do a similar analysis in case e corresponds to a synchronization of the form (τ, s′⟨s_{l}P_{l}P′_{l}, s_{r}P_{r}P′_{r}⟩). The details are essentially the same and we omit them.

□

We now define precisely the asynchronous transition system which we wish to prove elementary.

Let P̂ be any process expression. Then LT S(P̂) = ((SP̂, [P̂], EP̂, IP̂, TranP̂), lP̂) where

• SP̂ = {[P′] | P′ ∈ Proc and P′ is reachable from P̂ in T S_{CCS}}. [P̂] is the initial state.

• EP̂ = \{(μ, u) ∈ Ev | ∃[P′], [P′′] ∈ SP̂. P′⟶^{\frac{μ}{u}}P′′\}.

• IP̂ = I ∩ (EP̂ × EP̂), where I is the relation defined in Definition 4.3.

• TranP̂ ⊆ SP̂ × EP̂ × SP̂ = \{([P], (μ, u), [P′]) | P ⟶^{\frac{μ}{u}}P′\}

• lP̂ : EP̂ → Act_{τ} is given by lP̂(μ, u) = μ.

It is straightforward to verify that for each P̂, LT S(P̂) is in fact a labelled asynchronous transition system. What we need to show is that it is elementary.

In what follows, fix a process expression P̂ and the corresponding transition system LT S(P̂). For simplicity, we shall refer to the states [P] of LT S(P̂) simply as P.

We first have the following simple proposition, which we state without a proof.

Proposition 4.11 Let R(s, P) be a region of T S_{CCS} as defined above. Then R(s, P) is a (possibly trivial) region of LT S(P̂).

To establish that the asynchronous transition system LT S(P̂) that we have defined is elementary, we have to establish that the two regional axioms hold with respect to regions which are non-trivial when restricted to LT S(P̂).

Lemma 4.12 (Separation by regions) Let LT S(P̂) = ((SP̂, [P̂], EP̂, IP̂, TranP̂), lP̂). ∀P_{1}, P_{2} ∈ SP̂. P_{1} ≢ P_{2} implies that there exist s and P such that R(s, P) is a non-trivial region of LT S(P̂) and either P_{1} ∈ R(s, P) and P_{2} ∉ R(s, P) or P_{1} ∉ R(s, P) and P_{2} ∈ R(s, P).

Proof It is fairly obvious from our definition of Comp that if P_{1} ≢ P_{2} then there is some s for which Comp(s, P_{1}) ≢ Comp(s, P_{2}). So there is no problem finding a region R(s, P) which separates P_{1} and P_{2}.

What we have to argue is that the region separating P_{1} and P_{2} is non-trivial. However, notice that the previous lemma about regions applies to all regions. Consider any trivial region R(s′, P′). If R(s′, P′) holds somewhere in LT S(P̂), R(s′, P′) can cease to hold only by the occurrence of some event e such that R(s′, P′) ∈ ^{•}e. Similarly, R(s′, P′) could have begun to hold only after the occurrence of some event e such that R(s′, P′) ∈ e^{•}. Since R(s′, P′) was assumed to be trivial, it therefore follows that it either holds for all states in SP̂ or fails to hold for all states in SP̂.

In other words, if Comp(s′, P_{1}) ≡ P′, but R(s′, P′) is a trivial region, we know that Comp(s′, P_{2}) ≡ P′ as well and so this is not the component on which P_{1} and P_{2} differ. Thus, any component on which P_{1} and P_{2} differ must correspond to a non-trivial region, and we are done. □

Lemma 4.13 (Enabling) Let LT S(P̂) = ((SP̂, [P̂], EP̂, IP̂, TranP̂), lP̂). ∀P ∈ SP̂. ∀(μ, u) ∈ EP̂. If there does not exist a P′ such that (P, (μ, u), P′) ∈ TranP̂, then there is some non-trivial region R(s′, P′) ∈ ^{•}(μ, u) such that P ∉ R(s′, P′).

Proof First consider the case where e = (μ, u) is of the form (μ, s_{1}P_{1}P′_{1}). Then, since e must occur somewhere in the transition system, we know that there exists P_{2} and P′_{2} such that P_{2}− →^{\frac{μ}{s_{1}P_{1}P′_{1}}}P′_{2}. So, by the definition of a region, R(s_{1}, P_{1}) ∈ ^{•}e. Further, by

Lemma 4.6, neither μ nor \overline{μ} appears in s_{1}.

Now, if P ∈ R(s_{1}, P_{1}), then, by Lemma 4.7, there must exist a P′ such that P − →^{\frac{μ}{s_{1}P_{1}P′_{1}}}P′.

Since we have assumed that there is no − →^{\frac{μ}{s_{1}P_{1}P′_{1}}} move leading out of P, we can conclude

that P ∉ R(s_{1}, P_{1}) and we are done.

The situation when e is of the form (τ, s⟨s_{0}P_{0}P′_{0}, s_{1}P_{1}P′_{1}⟩) is handled similarly, appealing to part (ii) of Lemmas 4.6 and 4.7.

□

Theorem 4.14 ∀P ∈ Proc. LT S(P) is an elementary asynchronous transition system.

5 Relationships to other approaches

We now show how the operational semantics we have provided for this language relates to two other approaches for providing a semantics for CCS.

The first connection we draw is with respect to the standard interleaving transition system for CCS, as defined by Milner in [9]. We “project” down from the asynchronous transition system LT S(P) we assign to a term P to obtain a corresponding labelled sequential transition system T S(P) by forgetting the extra information about the events. We then exhibit a strong relationship between T S(P) and the transition system for P which would be generated by the semantics in [9].

The other comparison is with respect to the way Winskel and Nielsen define a denotational semantics for a process language in [13]. They provide a semantics in the category of asynchronous transition systems, where the operators of the process language are interpreted as appropriate categorical constructions. We will sketch their approach briefly, without going into too much technical detail, and then describe how the asynchronous transition systems they assign denotationally compare to the asynchronous transition systems we assign operationally.

We begin by relating our semantics to the standard interleaving semantics for CCS. Recall the definition of LT S(P) for a term P. LT S(P) = ((S_{P} , [P], E_{P} , I_{P} , Tran_{P}), l_{P}) where

• S_{P} = {[P′] | P′ ∈ Proc and P′ is reachable from P in T S_{CCS}}. [P] is the initial state.

• E_{P} = \{(μ, u) ∈ Ev | ∃[P′], [P′′] ∈ S_{P} . P′⟶^{\frac{μ}{u}}P′′\}.

• I_{P} = I ∩ (E_{P} × E_{P}), where I is the relation defined in Definition 4.3.

• Tran_{P} ⊆ S_{P} × E_{P} × S_{P} = \{([P], (μ, u), [P′]) | P ⟶^{\frac{μ}{u}}P′\}.

• l_{P} : E_{P} → Act_{τ} is given by l_{P} (μ, u) = μ.

We extract a labelled (sequential) transition system T S(P) from LT S(P) in the obvious way, by forgetting the extra information in the labels of the events.

Definition 5.1 Let LT S(P) = ((S_{P} , [P], E_{P} , I_{P} , Tran_{P}), l_{P}). Then, T S_{P} = (S′_{P} , [P], E′_{P} , Tran′_{P}) where

• S′_{P} = S_{P}, with [P] as the initial state.

• E′_{P} = {μ | (μ, u) ∈ E_{P} }.

• Tran′_{P} ⊆ S′_{P} × E′_{P} × S′_{P} = {([P], μ, [P′]) | ([P], (μ, u), [P′]) ∈ Tran_{P} }.

Let Seq(T) be the standard sequential transition system for a process term P ∈ Proc. Essentially, this is the transition system obtained using our rules (Sum), (Par), (Com) and (Res), ignoring the labels “below the arrow”, and adding in place of (Struct) the following rule.

P [rec x.P/x]⟶^{\underline{μ}}P′ implies rec x.P ⟶^{\underline{μ}}P′ (Rec)

To relate these two approaches formally, we define a folding map on transition systems as follows.

Definition 5.2 (Foldings) Let T S_{k} = (S_{k}, i_{k}, E_{k}, Tran_{k}), k = 1, 2, be two labelled sequential transition systems. Then, a folding from T S_{1} onto T S_{2} a pair of functions f = (f_{S}, f_{E}) where

f_{S} : S_{1} → S_{2} and

f_{E} : E_{1} → E_{2} such that:

(i) f_{S} is onto, with f_{S}(i_{1}) = i_{2}.

(ii) ∀(s_{1}, e_{1}, s′_{1}) ∈ Tran_{1}. (f_{S}(s_{1}), f_{E}(e_{1}), f_{S}(s′_{1})) ∈ Tran_{2}.

(iii) ∀(f_{S}(s_{1}), e_{2}, s′_{2}) ∈ Tran_{2}. ∃(s_{1}, e_{1}, s′_{1}) ∈ Tran_{1} such that f_{E}(e_{1}) = e_{2} and f_{S}(s′_{1}) = s′_{2}.

A similar notion has been defined in [6] where it is called a transition preserving homomorphism.

If f_{E} = id, the identity function, then a folding corresponds to a special type of a bisimulation, where the second system is, in general, a smaller, more compact representation of the behaviour described by the first system.

Theorem 5.3 There is a folding from Seq(P) onto T S(P) whose map on the events is the identity and whose map on states takes a process term P to its equivalence class [P].

Proof The proof follows by induction on the structure of P and we omit the details. □

So, we have shown that the asynchronous transition system we generate is, in some sense, a “practical” transition system. It is finite whenever the normal interleaved transition system is finite and has, in fact, slightly fewer states in general.

However, as we have pointed out in Section 3, the asynchronous transition system we associate with a process P ∈ Proc could have more transitions than the standard interleaved transtion system for P. For instance, we have shown that P = rec x.ax∥rec x.ax would generate two a-labelled transitions in our set up whereas it would have only one a-labelled transition in the standard approach. However, when we project these two a transitions down to T S(P), we only get a single a transition because sequential transition systems are extensional—there cannot be two different transitions with the same label connecting the same pair of states. It is not difficult to see, though, that the set of transitions that we add at any state in going from Seq(P) to LT S(P) is always finite.

This is also a good place to discuss why we identify states in our transition system as equivalence classes [P] rather than just process expressions P. The natural way to work directly with process expressions as states in our framework would be to extend the rule (Rec) with extra labels on the transitions as follows.

P [rec x.P/x]⟶^{\frac{μ}{u}}P′ implies rec x.P ⟶^{\frac{μ}{u}}P′ (Rec′)

However, since the moves of rec x.P are then exactly the same as those of P [rec x.P/x], the asynchronous transition we end up with is no longer elementary, in general. For instance, the transition system corresponding to the term a rec x.ax would have two states, a rec x.ax and rec x.ax. There would be a transition from a rec x.ax to rec x.ax via the event (a, [a rec x.ax][rec x.ax]) and a transition via the same event looping from the state rec x.ax back to itself. It is not difficult to show that this does not correspond to an elementary asynchronous transition system.

Next, we describe, somewhat informally, the approach taken by Winskel and Nielsen in [13] to provide a denotational semantics for CCS-like languages in terms of asynchronous transition systems.

Let the “basic” operators which are used to build up process terms be prefixing (aP), choice (+), parallel composition (∥), restriction (\α) and recursion (rec x.P).

Assuming inductively that we have built up an asynchronous transition system Den(P) denoting a term P, the transition system corresponding to aP is obtained by adjoining a new initial state to Den(P) and adding a new event labelled a which connects the new initial state to the initial state of Den(P).

P_{1}∥P_{2} is modelled by a version the categorical product of Den(P_{1}) and Den(P_{2}). This produces a transition system which is essentially the same as the one our operational semantics produces for P_{1}∥P_{2}.

Restriction is also handled directly in a categorical framework, using cartesian liftings and fibrations, which essentially achieve the same effect as one would expect intuitively.

The first major difference between the denotational approach and our operational appoach arises in the treatment of +. The denotational transition system corresponding to the term P_{1}+P_{2} is obtained by taking the categorical coproduct of Den(P_{1}) and Den(P_{2}). This operation essentially consists of taking disjoint copies of Den(P_{1}) and Den(P_{2}) and fusing together their initial states. This means that the denotation of the term a nil +a nil would be a transition system with two distinct a-labelled transitions leading from the initial state. On the other hand, our operational semantics would generate only a single event for this process. Thus, in general, the denotational treatment of + would give rise to “wider” transition systems than our operational semantics.

The other major difference is in the treatment of recursion. In the denotational approach, a term of the form rec x.P is always completely unfolded. Thus any process of this form gives rise to an infinite transition system. On the other hand, terms of the form rec x.ax would produce finite cyclic transition systems according to our operational semantics.

Thus, the denotation of a term P would, in general, be an “unfolded” version of the transition system that our operational semantics would generate. The “unfolding” would be both “horizontal” (because of the treatment of +) and “vertical” (because of the treatment of recursion).

To relate these two approaches, we extend our definition of a folding to asynchronous transition systems as follows.

Definition 5.4 (Strong foldings) Let (AT S_{1}, l_{1}) and (AT S_{2}, l_{2}) be two Σ-labelled transition systems, where AT S_{k} = (S_{k}, i_{k}, E_{k}, I_{k}, Tran_{k}), k = 1, 2. Then, a strong folding from (AT S_{1}, l_{1}) onto (AT S_{2}, l_{2}) is a pair of functions f = (f_{S}, f_{E}) where

f_{S} : S_{1} → S_{2} and

f_{E} : E_{1} → E_{2} such that:

(i) f is a folding from T S_{1} = (S_{1}, i_{1}, E_{1}, Tran_{1}) onto T S_{2} = (S_{2}, i_{2}, E_{2}, Tran_{2}).

(ii) ∀e_{1} ∈ E_{1}. ∀e_{2} ∈ E_{2}. e_{2} = f_{E}(e_{1}) implies l_{2}(e_{2}) = l_{1}(e_{1}).

(iii) ∀e_{1}, e′_{1} ∈ E_{1}. (e_{1}, e′_{1}) ∈ I_{1} implies (f_{E}(e_{1}), f_{E}(e′_{1})) ∈ I_{2}.

(iv) ∀(f_{S}(s_{1}), e′_{2}, s′_{2}), (f_{S}(s_{1}), e′′_{2}, s′′_{2}) ∈ Tran_{2}. (e′_{2}, e′′_{2}) ∈ I_{2} implies ∃(s_{1}, e′_{1}, s′_{1}), (s_{1}, e′′_{1}, s′′_{1}) ∈ Tran_{1} such that f_{E}(e′_{1}) = e′_{2}, f_{S}(s′_{1}) = s′_{2}, f_{E}(e′′_{1}) = e′′_{2}, f_{S}(s′′_{1}) = s′′_{2} and (e′_{1}, e′′_{1}) ∈ I_{1}.

The extra requirements on a strong folding are that the map on the underlying events preserve labels and the independence relation. The last clause adds the requirement that concurrent steps in the second system be pulled back to concurrent steps in the first system. This is a bit weaker than saying that every pair of independent events in the second system has a pair of independent events in the first system as its pre-image via f_{E}, because we could have “unused” independences in the second system which never actually give rise to a concurrent step. (For instance, in the term a(b∥c)+d(e∥f), the event labelled b and the event labelled f would be independent by our operational semantics, though there is no state where they are simultaneously enabled and, in fact, no run where they both occur).

For P ∈ Proc, let Den(P) be the denotational transition system corresponding to a term (as defined in [13]) and let LT S(P) be the asynchronous transition system corresponding to P defined in the previous section. We then have the following result.

Theorem 5.5 There exists a folding from Den(P) onto LT S(P).

Proof We shall not go into the details, because it will also involve describing the denotational semantics more precisely. The proof is fairly straightforward, by induction on the structure of the term P. □

6 Bisimulations on asynchronous transition systems

We now examine the question of how to define a sensible notion of bisimulation on labelled asynchronous transition systems which respects the independence relation on the underlying events.

As we had mentioned earlier, asynchronous transition systems can be equipped with a natural notion of morphism [13]. These morphisms map states and events in such a way that independence is preserved globally.

Though transition system morphisms preserve behaviour, they appear to be unsatisfactory for defining a natural notion of bisimulation. The main problem is the stipulation that independence must be preserved globally.

Intuitively, a bisimulation describes how systems match each other’s behaviour along individual runs. In the conventional framework, the existence of a bisimulation between two systems ensures that the branching behaviour of each system can be faithfully simulated by the other along each run. When extending this to asynchronous transition systems, it is natural to further require that the independence relation be preserved by the bisimulation along each run, but not necessarily globally.

To illustrate this point, consider the two CCS expressions (b + α∥\overline{α}b)\α and b + τb. In the first process, the two b moves would be considered independent in our set up, because they appear on different sides of the ∥ operator. However, it is easy to see that in any run of the first process, exactly one of the two b moves will occur. So, it seems reasonable to expect that these two processes should be bisimilar, though the second process has no independent events.

Thus one needs a way of relating two systems along each run. Unfortunately, this means that it no longer suffices to present the bisimulation in terms of a relation on states—we have also to “remember” how we reached the state. In particular, we need to remember the independences we have observed so far. This ensures that in extending the run from that state, we can remain consistent with the choices already made while relating events along this run.

One way to formalize this intuition is to follow the approach Aceto uses to characterize a static version of location equivalence [1].

For the next few definitions, fix a pair of labelled asynchronous transition systems (AT S_{1}, l_{1}) and (AT S_{2}, l_{2}), where AT S_{k} = (S_{k}, i_{k}, E_{k}, I_{k}, Tran_{k}), k = 1, 2.

Definition 6.1 A relation φ ⊆ E_{1} × E_{2} is lI-consistent provided

• ∀(e_{1}, e_{2}) ∈ φ. l_{1}(e_{1}) = l_{2}(e_{2}).

• ∀e_{1}, e′_{1} ∈ E_{1}. ∀e_{2}, e′_{2} ∈ E_{2}. (e_{1}, e_{2}) ∈ φ and (e′_{1}, e′_{2}) ∈ φ ⇒ e_{1}I_{1}e′_{1} iff e_{2}I_{2}e′_{2}.

The first condition says that the labels on the related events must match, whereas the second condition says that the independence relation must be preserved by φ in a strong way. In other words, φ is consistent with respect to both l and I.

Let Φ denote the family of all lI-consistent relations φ ⊆ E_{1} × E_{2}.

We now wish to define a notion of equivalence based on these lI-consistent relations between events. The idea is straightforward—as we match events from the two systems along a given run, we have to ensure at each stage that the events we have related constitute an lI-consistent relation. To make this a bisimulation, we have to further ensure that at each stage the choices available to each process can be matched by the other process in such a way that the current lI-consistent relation extends to a larger one.

To achieve this, we associate with each φ ∈ Φ, a relation ∼_{φ} ⊆ S_{1} × S_{2}. s_{1} ∼_{φ} s_{2} is to be read as follows; if we reach s_{1} in T S_{1} and s_{2} in T S_{2} during a simulation along which we have associated events by φ, then it is possible to extend the simulation along all possible choices of transitions at s_{1} and s_{2} in a manner consistent with φ.

Formally, we have the following definition:

Definition 6.2 ∼_{Φ}= {∼_{φ}| φ ∈ Φ} is the largest Φ-indexed family of symmetric relations on S_{1} × S_{2} satisfying:

If s_{1} ∼_{φ} s_{2} then ∀(s_{1}, e_{1}, s′_{1}) ∈ Tran_{1}. ∃(s_{2}, e_{2}, s′_{2}) ∈ Tran_{2} such that φ ∪ {(e_{1}, e_{2})} ∈ Φ and s′_{1} ∼_{φ∪{(e_{1},e_{2})}} s′_{2}.

Two labelled asynchronous transition systems are bisimilar if their initial states are related by the empty relation between events.

Definition 6.3 AT S_{1} ∼ AT S_{2} iff i_{1} ∼_{∅} i_{2}.

It is easy to verify the following.

Proposition 6.4 ∼ is an equivalence relation on labelled asynchronous transition systems.

Example 6.1 Let P_{1} = (b + α∥\overline{α}b)\α and P_{2} = b + τb. Then LT S(P_{1}) ∼ LT S(P_{2}), as shown below.

LT S(P_{1}) has three events, e_{1} = (b, α0[b + α][nil]), e_{2} = (τ, α⟨0[b + α][nil], 1[\overline{α}b][b]⟩), and e_{3} = (b, α1[b][nil]).

LT S(P_{2}) also has three events, e′_{1} = (b, [b + τb][nil]), e′_{2} = (τ, [b + τb][b]), and e′_{3} = (b, [b][nil]).

We can define

• ∼_{∅}= {(P_{1}, P_{2}), (P_{2}, P_{1})}.

• ∼_{\{(e_{1},e′_{1})\}}= \{((nil∥\overline{α}b)\α, nil), (nil, (nil∥\overline{α}b)\α)\}.

• ∼_{{(e_{2},e′_{2})}}= {((nil∥b)\α, b), (b, (nil∥b)\α)}.

• ∼_{{(e_{2},e′_{2}),(e_{3},e′_{3})}}= {((nil∥nil)\α, nil), (nil, (nil∥nil)\α)}.

Example 6.2 Let P_{1} = (aαc∥b\overline{α}d)\α and P_{2} = (aαd∥b\overline{α}c)\α. Then LT S(P_{1}) ≁ LT S(P_{2}).

Both processes are deterministic, so they both have only one possible run. Since each event has a unique label in each process, along this run we will have to relate, for instance, the a and c labelled events in P_{1} to the corresponding a and c events in P_{2}. However, these events are not independent in P_{1} whereas they are independent in P_{2}. So, there exists no lI-consistent relation corresponding to the (unique) maximal run of P_{1} and P_{2}.

The equivalence we have described applies in general to all labelled asynchronous transition systems. When restricted to the transition systems we construct for CCS terms, it amounts to defining a notion of strong bisimulation over terms in Proc. We can extend the definition smoothly to deal with weak bisimulation over CCS terms as follows.

First, given an Act_{τ}-labelled asynchronous transition system (AT S, l), where AT S = (S, i, E, I, Tran), define the weak transistion relation ⇒ ⊆ S × E × S in the obvious way.

⇒ = \{(s, e, s′) | \begin{matrix}∃s_{0}, s_{1}, …, s_{n}. ∃e_{0}, e_{1}, …, e_{n−1}. s = s_{0}, s′ = s_{n} \\ and ∀0 ≤ i < n. (s_{i}, e_{i}, s_{i+1}) \\ such that e = e_{j}, 0 ≤ j < n, where l(e) ≠ τ \\ and ∀0 ≤ i < n. i ≠ j ⇒ l(e_{i}) = τ\} \end{matrix}

We need to extend ⇒ to describe purely internal transitions between states. In this framework, it is convenient to construct a second relation ⇝ ⊆ S × S such that

⇝ = {(s, s′) | s = s′ or ∃s_{0}, s_{1}, …, s_{n}. ∃e_{0}, e_{1}, …, e_{n−1}. s = s_{0}, s′ = s_{n} and ∀0 ≤ i < n. (s_{i}, e_{i}, s_{i+1}), where l(e_{i}) = τ}

Now consider a pair of Act_{τ}-labelled asynchronous transition systems (AT S_{1}, l_{1}) and (AT S_{2}, l_{2}), where AT S_{k} = (S_{k}, i_{k}, E_{k}, I_{k}, Tran_{k}), k = 1, 2, with weak transition relations ⇒_{k} and ⇝_{k}, k = 1, 2 respectively.

We retain the notion of an lI-consistent relation as before. We can now define a weak notion of equivalence ≃ between transition systems. We first begin with the Φ-indexed versions of ≃.

Definition 6.5 ≃_{Φ}= {≃_{φ}| φ ∈ Φ} is the largest Φ-indexed family of symmetric relations on S_{1} × S_{2} satisfying:

If s_{1} ≃_{φ} s_{2} then

• ∀(s_{1}, e_{1}, s′_{1}) ∈ ⇒_{1} . ∃(s_{2}, e_{2}, s′_{2}) ∈ ⇒_{2} such that φ ∪ {(e_{1}, e_{2})} ∈ Φ and s′_{1} ≃_{φ∪{(e_{1},e_{2})}} s′_{2}.

• ∀(s_{1}, s′_{1}) ∈ ⇝_{1} . ∃(s_{2}, s′_{2}) ∈ ⇝_{2} such that s′_{1} ≃_{φ} s′_{2}.

Once again we say that AT S_{1} ≃ AT S_{2} iff i_{1} ≃_{∅} i_{2}. It can be verified that ≃ is an equivalence relation on Act_{τ}-labelled asynchronous transition systems.

The induced weak equivalence ≃ on process terms is closely related to the notion of location equivalence defined by Boudol et al [5]. Aceto [1] has provided an alternative characterization of this equivalence for a sublanguage where processes are viewed as “networks” of sequential components—i.e. parallel composition is restricted to the top level.

It is not hard to see that by restricting our language to a language like the one Aceto considers, our definition of ≃ coincides with his notion of location equivalence, and hence, with the notion of Boudol et al. In fact, we believe that this is true for the entire language we consider. Let ≈_{l} denote the location equivalence of [5].

Conjecture ∀P, P′ ∈ Proc. LT S(P) ≃ LT S(P′) iff P ≈_{l} P′.

7 Discussion

In this paper, we have described how to provide a semantics for CCS in terms of elementary asynchronous transition systems. By appealing to the coreflection between this class of transition systems and 1-safe Petri nets established in [13], we obtain as a corollary a Petri net semantics for the language we consider.

Admittedly, the language we consider is not full CCS. However, as we have already mentioned, we believe that the language studied here is a powerful and useful subset of CCS which is sufficient for specifying most concurrent systems of interest.

As we had pointed out in the Introduction, many other people have provided noninterleaved semantics for CCS [3, 6, 8, 11]. Our claim is that our semantics is simpler and more natural than those described elsewhere. To a large part, this is because all these approaches deal with full CCS, whereas we avoid having to deal with processes of the form P + (Q∥R), which are the main source of complications for these approaches. However, we feel that the benefits that we obtain by restricting the syntax more than justify the choice we have made.

For one, we use a very straightforward extension of the standard operational semantics. To actually read off the events of the transition system and the independence relation on the events from our operational semantics is trivial. Having proved here once and for all that the resulting asynchronous transition system is elementary, we can be sure that we are working with a “nice” object. So, for instance, feeding our operational description of a term into a verification tool should be no more difficult than feeding the standard interleaved description of the term.

In contrast, using “proved transitions” [3] or working with an algebra of transitions [8] always requires a second level of reasoning about the transitions to recover the underlying events of the system.

In the approaches which directly yield a Petri net semantics [3, 6, 11], for every term P one has to first construct a “concrete” implementation of a net describing the behaviour of P and then work back to recover the global states, because one typically needs to reason about the global states of the system. Instead, we directly provide the global states and, through the independence relation, provide a means of recovering the local states if they are required.

Another interesting feature of the semantics we describe here is that the independence relation on events directly reflects the idea of events occurring at independent locations. This seems to be a very natural way to think about independence. We feel that it would be difficult to extend this idea in a straightforward way to deal with the full language.

We also believe that our result establishing that the normal interleaved transition system for a term can be folded onto our asynchronous transition system is quite valuable. This means that our approach yields a tractable system whenever the conventional approach would and, once again, has a bearing on the possibilities of mechanically verifying properties of such systems. (In [6], a similar result is proved, but in the opposite direction—i.e. they show that the non-interleaved transition system they define can be folded into the standard interleaved one).

In this paper, we have also introduced a notion of bisimulation over labelled asynchronous transition systems which preserves independence in a fairly natural way. This permits us to equip our language with a simple notion of equivalence which respects the non-interleaved nature of our semantics and yet abstracts away from the concrete syntax. This is a feature which has been lacking in earlier approaches to providing a non-interleaved semantics for CCS.

It is clear that there is a close connection between the equivalence we define and the location equivalence of [5]. A problem with the equivalence defined in [5] is that it is based on a transition system which is infinitely branching, even for the simplest of process terms. If our conjecture that the two equivalences coincide is true, then our definition would provide an effective way of checking location equivalence for a very large class of CCS processes.

An issue which is yet to be resolved is how best to define bisimulations over asynchronous transition systems. We believe that our approach reflects the right intuition. However, we would be happier with a more “global” definition of how to relate two systems, rather than the incremental definition we have provided here, which makes is rather clumsy to actually present a bisimulation (as in Example 6.1).

Acknowledgment We have benefited greatly from many discussions with P.S. Thiagarajan.

References

[1] L. Aceto: A static view of localities, Report 1483, INRIA, Sophia-Antipolis (1991).

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

[3] G. Boudol, I. Castellani: Three equivalent semantics for CCS, Semantics of Systems of Concurrent Processes, Springer LNCS 469, 96–141 (1990).

[4] G. Boudol, I. Castellani, M. Hennessy, A. Kiehn: Observing localities, Proc. MFCS ’91, Springer LNCS 520, 93–102 (1991) (full version appears as Report 4/91, Computer Science, University of Sussex (1991)).

[5] G. Boudol, I. Castellani, M. Hennessy, A. Kiehn: A theory of processes with localities, Report 1632, INRIA, Sophia-Antipolis (1992) (an earlier version appears as Report 13/91, Computer Science, University of Sussex (1991)).

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

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

[8] G.L. Ferrari, U. Montanari: Towards the unification of models for concurrency, Proc. CAAP ’90, Springer LNCS 431, 162–176 (1990)

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

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

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

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

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