Foundations of Software Technology and Theoretical Computer Science, 12th Conference, Proceedings, R. Shyamasundar (Ed.), Lecture Notes in Computer Science 652, Springer-Verlag (1992) 328–341.

CCS, Locations and Asynchronous Transition Systems

Madhavan Mukund^{⋆} and Mogens Nielsen^{⋆⋆}

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

Abstract. We provide a simple non-interleaved operational semantics for CCS in terms of asynchronous transition systems. We 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 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.

1 Introduction

Process algebras like CCS [9] are a well established formalism for specifying concurrent systems. Several attempts have been made to provide a non-interleaved semantics for CCS-like 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 introducing 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, 13].

Both these approaches have some drawbacks. 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

⋆ Permanent address: School of Mathematics, SPIC Science Foundation, 92, G.N. Chetty Road, T. Nagar, Madras 600 017, India. Email: madhavan@ssf.ernet.in. The author’s stay in Denmark was supported by a grant from the Aarhus University Research Foundation.

⋆⋆ Email: mn@daimi.aau.dk

gives rise to the required behaviour—a lot of effort has to be put into 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.

All existing attempts at defining a non-interleaved semantics for CCS result in transition systems whose state spaces are considerably larger than those of the transition systems generated by the traditional interleaving semantics. In fact, Olderog conjectures in [13] that “It is impossible to find an operational Petri net semantics which represents all the intended concurrency of process terms and for which the reachable markings are in 1-1 correspondence with the global states of the standard operational interleaving semantics.”

In this paper, we provide a simple non-interleaved operational semantics for a slightly restricted version of CCS satisfying the properties of Olderog’s conjecture.

The restriction we make on CCS syntax is as follows. 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 major examples in [9] conform to our syntactic restriction.

We interpret CCS over the class of asynchronous transition systems [2, 14, 15]. An asynchronous transition system is a labelled 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 [15], 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 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. 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 [15].

We go on to define a notion of bisimulation on asynchronous transition systems which preserves independence. When applied to the transition systems we use to describe 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 and discusses the connection between our semantics and the traditional interleaved semantics for CCS. The next section describes bisimulations on asynchronous transition systems. We conclude in Section 6 with a discussion of how our work relates to other approaches and suggestions for further study.

2 Asynchronous transition systems

Asynchronous transition systems were introduced independently by Bednarczyk [2] and Shields [14]. 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 [15].

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

– (S, i, E, Tran) is a transition system, where S is a set of states (with initial state i), E is a set of events and Tran ⊆ S × E × S is the transition relation.

– 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 [15]. In [15], 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. At the level of objects, 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 [7, 10, 12].

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

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

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

3 The language and its operational semantics

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

332

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. 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 all free occurrences of 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′\α, μ ∉ \{α, \overline{α}\} (Res)
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 is 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 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 5.

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.

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, labelled a and b. In contrast, the process ab + ba has four distinct events.

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

Fig. 1. Concurrency versus non-deterministic interleaving

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

[figure: rec x.ax∥rec x.ax; a; a; 1[rec x.ax][rec x.ax]; 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; a; 0[aP][P]; 0[aP][P]; a; a; 1[aP][P]; 1[aP][P]; a; a; 00[aP][P]; 11[aP][P]]

Fig. 2. Recursion

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.

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.

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.

Due to space constraints, we restrict ourselves to an informal account of the proof. Full details can be found in [11].

We first look at the labels associated with transitions by our operational semantics. We can show that for any transition P̂⟶^{\frac{μ}{u}}P̂′, u is either of the form s[P][P′],

where s ∈ ({0, 1} ∪ Λ)^{∗} and μ ∈ Act_{τ}, or of the form s⟨s_{0}[P_{0}][P′_{0}], s_{1}[P_{1}][P′_{1}]⟩, where s, s_{0}, s_{1} ∈ ({0, 1} ∪ Λ)^{∗} and μ = τ. The first kind of label is associated with an “independent” action performed by an individual component of a process, while the second kind of label arises out of a synchronization. Henceforth, we shall often write P instead of [P], for convenience.

Each distinct label in our transition system corresponds to an event. We can define the set of events Ev as follows:

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

Using the information present in the labels, for each event 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. First, let I_{l} ⊆ {0, 1}^{∗} × {0, 1}^{∗} be given by:

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

where ⪯ is the prefix relation on strings.

Now, 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}.

To analyze the behaviour of a process term P, we need to decompose it into its basic components. Components are identified by a (partial) function Comp : ({0, 1} ∪ Λ)^{∗} × Proc ⇀ Proc which, given a process term P and a location s, returns the subprocess of P located at s. Comp is 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])

Notice that a process expression given by a guarded sum cannot be broken down further into components. Such expressions can be regarded as sequential components.

Using the labels on the transitions, we can “project” each move of P down to the sequential component where it occurs. For instance, given a transition of the form P − →^{\frac{μ}{sP_{1}P′_{1}}}P′, we can assert that this event occurs in the sequential component P_{1} ≡

Comp(s, P), resulting in the component at s being transformed to the expression P′_{1} ≡ Comp(s, P′).

Conversely, we can identify when the moves of the sequential components can be lifted to the whole process. This is not completely straightforward. The moves of a 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.

Finally, it turns out that the occurrence of an event e leaves sequential components lying at locations independent of Loc(e) untouched. This confirms that our definition of the independence relation on events, based on the locations where they occur, is a natural one.

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_{0}, P_{1}, …, P_{n}. P = P_{0}, P′ = P_{n} and for all i ∈ \{1, 2, …, n\}, there exists a move P_{i−1}−→^{\frac{μ_{i}}{u_{i}}}P_{i}—i.e. P′ is reachable from P̂\}.

[P̂] is the initial state.

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

– IP̂ = I ∩ (EP̂ × EP̂), where I is the independence relation on events defined earlier.

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

To show that it is elementary we have to identify enough regions to satisfy the properties of “separation” and “enabling” given in Definition 2.3.

Given s ∈ ({0, 1} ∪ Λ)^{∗} and P of the form ∑_{i∈I} μ_{i}P_{i}, we can define a region R(s, P), consisting of all process terms whose sequential component at s is given by P.

So, the region R(s, P) holds at a state P′ iff the component of P′ at location s is a sequential component equivalent to P —in other words, Comp(s, P′) ≡ 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^{•}.

We can then show that regions of the form R(s, P) are sufficient to ensure that for every process term P̂, LT S(P̂) satisfies the regional axioms required for it to be elementary. In this way, we achieve what we set out to prove.

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

In [11], we compare our semantics with the traditional interleaved semantics for CCS in terms of foldings. Here we shall just briefly present the main results. Details can be found in [11].

Foldings 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. Foldings have also been defined in [6], where they are called transition-preserving (tp) homomorphisms.

For a process term P in our language, let T S(P) denote the standard transition system associated with P by the interleaved semantics given in [9]. Then, we can show the following.

Theorem 4.2. For each P ∈ Proc, T S(P) can be folded onto LT S(P) (when we “forget” about the independence relation and regard LT S(P) as just a labelled transition system).

This means that our approach yields a tractable system whenever the conventional approach would. This has an important bearing on the possibilities of mechanically verifying properties of such systems.

We can extend the notion of a folding to asynchronous transition systems in such a way that the folding preserves the independence relation. We can then relate our operational semantics to Winskel and Nielsen’s denotational semantics for CCS in terms of asynchronous transition systems [15]. For P ∈ Proc, let Den(P) denote the asynchronous transition system associated with P by the denotational semantics of [15]. Then we have the following.

Theorem 4.3. For each P ∈ Proc, there is an (independence-preserving) folding from Den(P) onto LT S(P).

This provides a formal justification for our choice of the independence relation between events.

5 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 [15]. Though transition system morphisms preserve behaviour, they are unsatisfactory for defining a natural notion of bisimulation because they map states and events in such a way that independence is 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 5.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}.

To define a notion of equivalence based on these lI-consistent relations between events, 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 5.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 5.3. AT S_{1} ∼ AT S_{2} iff i_{1} ∼_{∅} i_{2}.

It is easy to verify the following.

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

Example 5.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 5.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 ∼ 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 5.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′.

6 Discussion

In this paper, we have described how to provide a semantics for CCS in terms of elementary asynchronous transition systems which is close to the standard operational semantics for CCS. By appealing to the coreflection between this class of transition systems and 1-safe Petri nets established in [15], 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. 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.

It may appear that our semantics is but a special case of, say, the proved transition approach of [3]. However, if we derive an asynchronous transition system describing a term P in our language using their semantics, with the independence relation given by their concurrency relation on proofs, the resulting transition system is not necessarily elementary.

In comparison with the approaches of [3, 8], our semantics is simple in the sense that labels on transitions directly yield the underlying events of the system, without resorting to a second level of reasoning about the transitions.

In the approaches which directly yield a Petri net semantics [3, 6, 13], 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.

The fact that the traditional interleaved transition system for a process P can be folded onto the asynchronous transition system LT S(P) assigned by our semantics means that our approach yields a tractable system whenever the conventional approach would.

Another interesting feature of our semantics 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 the full language.

In this paper, we have also introduced a notion of bisimulation over labelled asynchronous transition systems which preserves independence along individual runs. 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]. The equivalence defined in [5] 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 we would have 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 5.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, Springer LNCS 469, 96–141 (1990).

4. G. Boudol, I. Castellani, M. Hennessy, A. Kiehn: Observing localities, Springer LNCS 520, 93–102 (1991).

5. G. Boudol, I. Castellani, M. Hennessy, A. Kiehn: A theory of processes with localities, Report 1632, INRIA, Sophia-Antipolis (1992)

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, Springer LNCS 431, 162-176 (1990).

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

10. M. Mukund: Transition system models for concurrency, Report DAIMI-PB-399, Computer Science Department, Aarhus University, Aarhus, Denmark (1992).

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

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. M.W. Shields: Concurrent machines, Computer Journal, 28, 449–465 (1985).

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