A Branching Time Model of CSP

Rob van Glabbeek^{1,2}

1 Data61, CSIRO, Sydney, Australia

2 Comput. Sci. and Engineering, University of New South Wales, Sydney, Australia

Abstract. I present a branching time model of CSP that is finer than all other models of CSP proposed thus far. It is obtained by taking a semantic equivalence from the linear time – branching time spectrum, namely divergence-preserving coupled similarity, and showing that it is a congruence for the operators of CSP. This equivalence belongs to the bisimulation family of semantic equivalences, in the sense that on transition systems without internal actions it coincides with strong bisimilarity. Nevertheless, enough of the equational laws of CSP remain to obtain a complete axiomatisation for closed, recursion-free terms.

1 Introduction

The process algebra CSP—Communicating Sequential Processes—was presented in Brookes, Hoare & Roscoe [4]. It is sometimes called theoretical CSP, to distinguish it from the earlier language CSP of Hoare [10]. It is equipped with a denotational semantics, mapping each CSP process to an element of the failuresdivergences model [4,5]. The same semantics can also be presented operationally, by mapping CSP processes to states in a labelled transition system (LTS), and then mapping LTSs to the failures-divergences model. Olderog & Hoare [13] shows that this yields the same result. Hence, the failures-divergences model of CSP can alternatively be seen as a semantic equivalence on LTSs, namely by calling two states in an LTS equivalent iff they map to the same element of the failures-divergences model.

Several other models of CSP are presented in the literature, and each can be cast as a semantic equivalence on LTSs, which is a congruence for the operators of CSP. One such model is called finer than another if its associated equivalence relation is finer, i.e., included in the other one, or more discriminating. The resulting hierarchy of models of CSP has two pillars: the divergence-strict models, most of which refine the standard failures-divergences model, and the stable models, such as the model based on stable failures equivalence from Bergstra, Klop & Olderog [2], or the stable revivals model of Roscoe [16].

Here I present a new model, which can be seen as the first branching time model of CSP, and the first that refines all earlier models, i.e. both pillars mentioned above. It is based on the notion of coupled similarity from Parrow & Sjödin [14]. What makes it an interesting model of CSP—as opposed to, say, strong or divergence-preserving weak bisimilarity—is that it allows a complete equational axiomatisation for closed recursion-free CSP processes that fits within the existing syntax of that language.

2 CSP

CSP [4,5,11] is parametrised with a set Σ of communications. In this paper I use the subset of CSP given by the following grammar.

P, Q ::= \begin{matrix}STOP | div | a → P | P ⊓ Q | P □ Q | P ▷ Q | \\ P ∥_{A}Q | P \A | f(P) | P △ Q | P Θ_{A} Q | p | μp.P \end{matrix}

Here P and Q are CSP expressions, a ∈ Σ, A ⊆ Σ and f : Σ → Σ. Furthermore, p ranges over a set of process identifiers. A CSP process is a CSP expression in which each occurrence of a process identifier p lays within a recursion construct μp.P. The operators in the above grammar are inaction, divergence, action prefixing, internal, external and sliding choice, parallel composition, concealment, renaming, interrupt and throw. Compared to [15,17], this leaves out

– successful termination (SKIP) and sequential composition (;),

– infinitary guarded choice,

– prefixing operators with name binding, conditional choice,

– relational renaming, and

– the version of internal choice that takes a possibly infinite set of arguments. The operators STOP, a →, ⊓, □, \A, f( ) and recursion stem from [4], and div and ∥_{A} from [13], whereas ▷, △ and Θ_{A} were added to CSP by Roscoe [15,17].

\begin{matrix}div ⟶^{τ} div & (a → P) ⟶^{a} P & P ⊓ Q ⟶^{τ} P & P ⊓ Q ⟶^{τ} Q \\ \frac{P ⟶^{a} P′}{P □ Q ⟶^{a} P′} & \frac{P ⟶^{τ} P′}{P □ Q ⟶^{τ} P′ □ Q} & \frac{Q ⟶^{a} Q′}{P □ Q ⟶^{a} Q′} & \frac{Q ⟶^{τ} Q′}{P □ Q ⟶^{τ} P □ Q′} \\ \frac{P ⟶^{a} P′}{P ▷ Q ⟶^{a} P′} & \frac{P ⟶^{τ} P′}{P ▷ Q ⟶^{τ} P′ ▷ Q} & P ▷ Q ⟶^{τ} Q & \frac{P ⟶^{α} P′}{f(P) ⟶^{f(α)} f(P′)} \\ \frac{P ⟶^{α} P′ (α∉A)}{P ∥_{A}Q ⟶^{α} P′∥_{A}Q} & \frac{P ⟶^{a} P′ Q ⟶^{a} Q′ (a∈A)}{P ∥_{A}Q ⟶^{a} P′∥_{A}Q′} & \frac{Q ⟶^{α} Q′ (α∉A)}{P ∥_{A}Q ⟶^{α} P ∥_{A}Q′} \\ \frac{P ⟶^{α} P′ (α∉A)}{P \A ⟶^{α} P′\A} & \frac{P ⟶^{a} P′ (a∈A)}{P \A ⟶^{τ} P′\A} & \frac{P ⟶^{α} P′ (α∉A)}{P Θ_{A} Q ⟶^{a} P′ Θ_{A} Q} & \frac{P ⟶^{a} P′ (a∈A)}{P Θ_{A} Q ⟶^{a} Q} \\ \frac{P ⟶^{α} P′}{P △Q ⟶^{α} P′△Q} & \frac{Q ⟶^{τ} Q′}{P △Q ⟶^{τ} P′△Q′} & \frac{Q ⟶^{a} Q′}{P △Q ⟶^{a} Q′} & μp.P ⟶^{τ} P [μp.P/p] \end{matrix}

Table 1. Structural operational semantics of CSP

The operational semantics of of CSP is given by the binary transition relations ⟶^{α} between CSP processes. The transitions P ⟶^{α} Q are derived by the rules in Table 1. Here a, b range over Σ and α, β over Σ ._{∪} {τ}, and relabelling operators f are extended to Σ ._{∪} {τ} by f(τ) = τ. The transition labels α are called actions, and τ is the internal action.

3 The Failures-Divergences Model of CSP

The process algebra CSP stems from Brookes, Hoare & Roscoe [4]. It is also called theoretical CSP, to distinguish it from the language CSP of Hoare [10]. Its semantics [5] associates to each CSP process a pair ⟨F, D⟩ of failures F ⊆ Σ^{∗} × P(Σ) and divergences D ⊆ Σ^{∗}, subject to the conditions:

(ε, ∅) ∈ F  (N1)
(st, ∅) ∈ F ⇒ (s, ∅) ∈ F  (N2)
(s, X) ∈ F ∧ Y ⊆ X ⇒ (s, Y) ∈ F  (N3)
(s, X) ∈ F ∧ ∀ c ∈ Y. (sc, ∅) ∉ F ⇒ (s, X ∪ Y) ∈ F  (N4)
∀ Y ∈ P_{fin}(X). (s, Y) ∈ F ⇒ (s, X) ∈ F  (N5)
s ∈ D ⇒ st ∈ D  (D1)
s ∈ D ⇒ (st, X).  (D2)

Here ε ∈ Σ^{∗} is the empty sequence of communications and st denotes the concatenation of sequences s and t ∈ Σ^{∗}. If ⟨F, D⟩ is the semantics of a process P, (s, ∅) ∈ F, with s ∉ D, tells that P can perform the sequence of communications s, possibly interspersed with internal actions. Such a sequence is called a trace of P, and Conditions N1 and N2 say that the set of traces of any processes is non-empty and prefix-closed. A failure (s, X) ∈ F, with s ∉ D, says that after performing the trace s, P may reach a state in which it can perform none of the actions in X, nor the internal action. A communication x ∈ Σ is thought to occur in cooperation between a process and its environment. Thus (s, X) ∈ F indicates that deadlock can occur if after performing s the process runs in an environment that allows the execution of actions in X only. From this perspective, Conditions N3 and N4 are obvious.

A divergence s ∈ D is a trace after which an infinite sequence of internal actions is possible. In the failures-divergences model of CSP divergence is regarded catastrophic: all further information about the process’ behaviour past a divergence trace is erased. This is accomplished by flooding: all conceivable failures (st, X) and divergences st that have s as a prefix are added to the model (regardless whether P actually has a trace st).

A CSP process P from the syntax of Section 2 has the property that for any trace s of P, with s ∉ D, the set next(s) of actions c such that sc is also a trace of P is finite. By (N3–4), (s, X) ∈ F iff (s, X ∩ next(s)) ∈ F. It follows that if (s, X) ∉ F, then there is a finite subset Y of X, namely X ∩ next(s), such that (s, Y) ∉ F. This explains Condition (N5).

In Brookes & Roscoe [5] the semantics of CSP is defined denotationally: for each n-ary CSP operator Op, a function is defined that extracts the failures and divergences of Op(P_{1}, …, P_{n}) out of the failures and divergences of the argument processes P_{1}, …, P_{n}. The meaning of a recursively defined CSP process μp.P is obtained by means of fixed-point theory. Alternatively, the failures and divergences of a CSP process can be extracted from its operational semantics:

Definition 1. Write P ⟹ Q if there are processes P_{0}, …, P_{n}, with n ≥ 0, such that P = P_{0}, P_{i} ⟶^{τ} P_{i+1} for all 0 ≤ i < n, and P_{n} = Q.

Write P ⟹^{α} Q if there are processes P′, Q′ with P ⟹ P′ ⟶^{α} Q′ ⟹ Q. Write P ⟹^{α̂} Q if either α ∈ Σ and P ⟹^{α} Q, or α = τ and P ⟹ Q. Write P ⟹^{s} Q, for s = a_{1}a_{2} … a_{n} ∈ Σ^{∗} with n ≥ 0, if there are processes

P_{0}, …, P_{n} such that P = P_{0}, P_{i} ⟹^{a_{i}} P_{i+1} for all 0 ≤ i < n, and P_{n} = Q.

Let I(P) = {α ∈ Σ ∪ {τ} | ∃ Q. P ⟶^{α} Q}.

Write P ⇑ if there are processes P_{i} for all i ≥ 0 with P ⟹^{s} P_{0} ⟶^{τ} P_{1} ⟶^{τ} . . .. s ∈ Σ^{∗} is a divergence trace of a process P if there is a Q with P ⟹^{s} Q⇑. The divergence set of P is D(P) := {st | s is a divergence trace of P }. A stable failure of a process P is a pair (s, X) ∈ Σ^{∗} × P(Σ) such that

P ⟹^{s} Q for some Q with I(Q) ∩ (X ∪ {τ}) = ∅. The failure set of a process P is F (p) = {(s, X) | s ∈ D(P) or (s, X) is a stable failure of P }.

The semantics [[ P ]]_{F D} of a CSP process P is the pair ⟨F (P), D(P)⟩.

Processes P and Q are failures-divergences equivalent, notation P ≡_{F D} Q, iff [[ P ]]_{F D} = [[ Q]]_{F D} . Process P is a failures-divergences refinement of Q, notation P ⊒_{F D} Q, iff F (P) ⊆ F (Q) ∧ D(P) ⊆ D(Q).

The operational semantics of Section 2 (then without the operators ▷, △ and Θ_{A}) appears, for instance, in [13], and was created after the denotational semantics. In Olderog & Hoare [13] it is shown that the semantics [[ P ]] of a CSP process defined operationally through Def. 1 equals the denotational semantics given in [5]. The argument extends smoothly to the new operators ▷, △ and Θ_{A} [17]. This can be seen as a justification of the operational semantics of Section 2.

In Brookes, Hoare & Roscoe [4] a denotational semantics of CSP was given involving failures only. Divergences were included only implicitly, namely by thinking of a trace s as a divergence of a process P iff P has all failures (st, X). So the semantics of div or μX.X is simply the set of all failure pairs. As observed in De Nicola [6], this approach invalidates a number of intuitively valid laws, such as P □ div = div. The improved semantics of [5] solves this problem.

In Hoare [11] a slightly different semantics of CSP is given, in which a process is determined by its failures, divergences, as well as its alphabet. The latter is a superset of the set of communications the process can ever perform. Rather than a parallel composition ∥_{A} for each set of synchronising actions A ⊆ Σ, this approach has an operator ∥ where the set of synchronising actions is taken to be the intersection of the alphabets of its arguments. Additionally, there is an operator |||, corresponding to ∥_{∅}. This approach is equally expressive as the one of [5], in the sense that there are semantics preserving translations in both directions. The work reported in this paper could just as well have been carried out in this typed version of CSP.

4 A Complete Axiomatisation

In [4,5,6,11,15,17] many algebraic laws P = Q, resp. P ⊑ Q, are stated that are valid w.r.t. the failures-divergences semantics of CSP, meaning that P ≡_{F D} Q, resp. P ⊑_{F D} Q. If Th is a collection of equational laws P = Q then Th ⊢ R = S denotes that the equation R = S is derivable from the equations in Th using reflexivity, symmetry, transitivity and the rule of congruence, saying that if Op is an n-ary CSP operator and P_{i} = Q_{i} for i = 1, …, n then Op(P_{1}, …, P_{n}) = Op(Q_{1}, …, Q_{n}). Likewise, if Th is a collection of inequational laws P ⊑ Q then Th ⊢ R ⊑ S denotes that the inequation R ⊑ S is derivable from the inequations in Th using reflexivity, transitivity and the rule saying that if Op is an n-ary CSP operator and P_{i} ⊑ Q_{i} for i = 1, …, n then Op(P_{1}, …, P_{n}) ⊑ Op(Q_{1}, …, Q_{n}).

Definition 2. An equivalence ∼ on process expressions is called a congruence for an n-ary operator Op if P_{i} ∼ Q_{i} for i = 1, …, n implies Op(P_{1}, …, P_{n}) ∼ Op(Q_{1}, …, Q_{n}). A preorder ⪯ is a precongruence for Op, or Op is monotone for ⪯, if P_{i} ⪯ Q_{i} for i = 1, …, n implies Op(P_{1}, …, P_{n}) ⪯ Op(Q_{1}, …, Q_{n}).

If ∼ is a congruence for all operators of CSP (resp. ⪯ is a precongruence for all operators of CSP) and Th is a set of (in)equational laws that are valid for ∼ (resp. ⪯) then any (in)equation R = S with Th ⊢ R = S (resp. R ⊑ S with Th ⊢ R ⊑ S) is valid for ∼ (resp. ⪯).

≡_{F D} is a congruence for all operators of CSP. This follows immediately from the existence of the denotational failures-divergences semantics. Likewise, ⊑_{F D} is a precongruence for all operators of CSP [4,5,6,11,13,15,17].

Definition 3. A set Th of (in)equational laws—an axiomatisation—is sound and complete for an equivalence ∼ (or a preorder ⪯) if Th ⊢ R = S iff R ∼ S (resp. Th ⊢ R ⊑ S iff R ⪯ S). Here “⇒” is soundness and “⇐” completeness.

In De Nicola [6] a sound and complete axiomatisation of ⊑_{F D} for recursion-free CSP, and no process identifiers or variables, is presented. It is quoted in Table 2. As this axiomatisation consist of a mix of equations and inequations, formally it is an inequational axiomatisation, where an equation P = Q is understood as the conjunction of P ⊑ Q and Q ⊑ P. This mixed use is justified because ≡_{F D} is the kernel of ⊑_{F D}: one has P ≡_{F D} Q iff P ⊑_{F D} Q ∧ Q ⊑_{F D} P.

In [6], following [4,5], two parallel composition operators ∥ and ||| were considered, instead of the parametrised operator ∥_{A}. Here ∥ = ∥_{Σ} and |||= ∥_{∅}. In Table 2 the axioms for these two operators are unified into an axiomatisation of ∥_{A}. Additionally, I added axioms for sliding choice, renaming, interrupt and throw—these operators were not considered in [6]. The associativity of parallel composition (Axiom P0) is not included in [6] and is not needed for completeness. I added it anyway, because of its importance in equational reasoning.

The soundness of the axiomatisation of Table 2 follows from ⊑_{F D} being a precongruence, and the validity of the axioms—a fairly easy inspection using the denotational characterisation of [[ ]]. To obtain completeness, write □_{i∈I} P_{i}, with I ={i_{1}, …, i_{n}} any finite index set, for P_{i_{1}} □P_{i_{2}} □…□P_{i_{n}}, where □_{i∈∅} P_{i} represents STOP. This notation is justified by Axioms E2–4. Furthermore, ⊓_{j∈J} P_{j}, with J = {j_{1}, .., j_{m}} any finite, nonempty index set, denotes P_{j_{1}} ⊓ P_{j_{2}} ⊓ … ⊓ P_{j_{m}}. This notation is justified by Axioms I2 and I3. Now a normal form is a defined as a CSP expression of the form div or ⊓_{j∈J} R_{j}, with R_{j} = (□_{k∈K_{j}}(a_{kj} → R_{kj}))

⊥  div ⊑ P
I1  P ⊓ P = P
I2  P ⊓ Q = Q ⊓ P
I3  P ⊓ (Q ⊓ R) = (P ⊓ Q) ⊓ R
I4  P ⊓ Q ⊑ P
E1  P □ P = P
E2  P □ Q = Q □ P
E3  P □ (Q □ R) = (P □ Q) □ R
E4  P □ STOP = P
E5  P □ div = div
D1  P □ (Q ⊓ R) = (P □ Q) ⊓ (P □ R)
D2  P ⊓ (Q □ R) = (P ⊓ Q) □ (P ⊓ R)
D3 (a → P) □ (a → Q) = a → (P ⊓ Q)
D4 (a → P) ⊓ (a → Q) = a → (P ⊓ Q)
SC  P ▷ Q = (P □ Q) ⊓ Q
P0  P ∥_{A}(Q∥_{A}R) = (P ∥_{A}Q)∥_{A}R
P1  P ∥_{A}Q = Q∥_{A}P
P2  (P ⊓ Q)∥_{A}R = (P ∥_{A}R) ⊓ (Q∥_{A}R)
P3  P ∥_{A}div = div
P4 If P = □_{i∈I}(a_{i} → P_{i}) and Q = □_{j∈J}(b_{j} → Q_{j}) then :
P ∥Q = □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))□
□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□
□_{b_{j} ∉A}(b_{j} → (P ∥_{A}Q_{j}))
H1  (P ⊓ Q)\A = (P \A) ⊓ (Q\A)
H2  (P □ a → Q)\A = ((P □ Q)\A) ⊓ (Q\A)
H3 (□_{i∈I}(b_{i} → P_{i}))\A = (□_{i∈I}(b_{i} → (P_{i}\A)))  if ∀ i ∈ I. b_{i} ∉ A
H4  div\A = div
R1  f(P ⊓ Q) = f(P) ⊓ f(Q)
R2  f(P □ Q) = f(P) □ f(Q)
R3  f(a → P) = f(a) → f(P)
R4  f(STOP) = STOP
R5  f(div) = div
T1  (P ⊓ Q) Θ_{A} R = (P Θ_{A} R) ⊓ (Q Θ_{A} R)
T2  (P □ Q) Θ_{A} R = (P Θ_{A} R) □ (Q Θ_{A} R)
T3  (a → P) Θ_{A} Q = a → (P Θ_{A} Q)  if a ∉ A
T4  (a → P) Θ_{A} Q = a → Q  if a ∈ A
T5  STOP Θ_{A} Q = STOP
T6  div Θ_{A} Q = div
U1  (P ⊓ Q) △ R = (P △ R) ⊓ (Q △ R)
U2  (P □ Q) △ R = (P △ R) □ (Q △ R)
U3  (a → P) △ Q = (a → (P △ Q)) □ Q
U4  STOP △ P = P
U5  div △ P = div

Table 2. A complete axiomatisation of ⊑_{F D} for recursion-free CSP

for j ∈ J, where the subexpressions R_{kj} are again in normal form. Here J and the K_{j} are finite index sets, J nonempty.

Axioms ⊥ and I4 derive P ⊓ div = div. Together with Axioms D1, SC, P1–4, H1–4, R1–5, T1–6 and U1–5 this allows any recursion-free CSP expression to be rewritten into normal form. In [6] it is shown that for any two normal forms P and Q with P ⊑_{F D} Q, Axioms ⊥, I1–4, E1–5 and D1–4 derive ⊢ P = Q. Together, this yields the completeness of the axiomatisation of Table 2.

5 Other Models of CSP

Several alternative models of CSP have been proposed in the literature, including the readiness-divergences model of Olderog & Hoare [13] and the stable revivals model of Roscoe [16]. A hierarchy of such models is surveyed in Roscoe [17]. Each of these models corresponds with a preorder (and associated semantic equivalence) on labelled transition systems. In [7] I presented a survey of semantic equivalences and preorders on labelled transition systems, ordered by inclusion in a lattice. Each model occurring in [17] correspond exactly with with one of the equivalences of [7], or—like the stable revivals model—arises as the meet or join of two such equivalences.

In the other direction, not every semantic equivalence or preorder from [7] yields a sensible model of CSP. First of all, one would want to ensure that it is a (pre)congruence for the operators of CSP. Additionally, one might impose sanity requirements on the treatment of recursion.

The hierarchy of models in [17] roughly consist of two hierarchies: the stable models, and the divergence-strict ones. The failures-divergences model could be seen as the centre piece in the divergence-strict hierarchy, and the stable failures model [15], which outside CSP stems from Bergstra, Klop & Olderog [2], plays the same role in the stable hierarchy. Each of these hierarchies has a maximal (least discriminating) element, called FL^{⇓} and FL in [17]. These correspond to the ready trace models RT^{↓} and RT of [7].

The goal of the present paper is to propose a sensible model of CSP that is strictly finer than all models thus far considered, and thus unites the two hierarchies mentioned above. As all models of CSP considered so far have a distinctly linear time flavour, I here propose a branching time model, thereby showing that the syntax of CSP is not predisposed towards linear time models. My model can be given as an equivalence relation on labelled transition system, provided I show that it is a congruence for the operators of CSP. I aim for an equivalence that allows a complete axiomatisation in the style of Table 2, obtained by replacing axioms that are no longer valid by weaker ones.

One choice could be to base a model on strong bisimulation equivalence [12]. Strong bisimilarity is a congruence for all CSP operators, because their operational semantics fits the tyft/tyxt format of [9]. However, this is an unsuitable equivalence for CSP, because it fails to abstract from internal actions. Even the axiom I1 would not be valid, as the two sides differ by an internal action.

A second proposal could be based on weak bisimilarity [12]. This equivalence abstracts from internal activity, and validates I1. The default incarnation of weak bisimilarity is not finer than failures-divergences equivalence, because it satisfies div = STOP. Therefore, one would take a divergence-preserving variant of this notion: the weak bisimulation with explicit divergence of Bergstra, Klop & Olderog [2]. Yet, some crucial CSP laws are invalidated, such as I3 and D1. This destroys any hope of a complete axiomatisation along the lines of Table 2.

My final choice is divergence-preserving coupled similarity [7], based on coupled similarity for divergence-free processes from Parrow & Sjödin [14]. This is the finest equivalence in [7] that satisfies I3 and D1. In fact, it satisfies all of the axioms of Table 2, except for the ones marked red: ⊥, I4, E1, E5, D2–4, SC, P2, P3, H2, U2, U3 and U5.

Divergence-preserving coupled similarity belongs to the bisimulation family of semantic equivalences, in the sense that on transition systems without internal actions it coincides with strong bisimilarity.

In Section 6 I present divergence-preserving coupled similarity. In Section 7 I prove that it is a congruence for the operators of CSP, and in Section 8 I present a complete axiomatisation for recursion-free CSP processes without interrupts.

6 Divergence-Preserving Coupled Similarity

Definition 4. A coupled simulation is a binary relation R on CSP processes, such that, for all α ∈ Σ ∪ {τ},

– if P R Q and P ⟶^{α} P′ then there exists a Q′ with Q ⟹^{α̂} Q′ and P′ R Q′,

– and if P R Q then there exists a Q′ with Q ⟹ Q′ and Q′ R P. It is divergence-preserving if P R Q and P ⇑ implies Q⇑. Write P ⊒_{CS}^{Δ} Q if there exists a divergence-preserving coupled simulation R with P R Q. Two processes P and Q are divergence-preserving coupled similar, notation P ≡_{CS}^{Δ} Q, if P ⊒_{CS}^{Δ} Q and Q ⊒_{CS}^{Δ} P.

Note that the union of any collection of divergence-preserving coupled simulations is itself a divergence-preserving coupled simulation. In particular, ⊒_{CS}^{Δ} is a divergence-preserving coupled simulation. Also note that in the absence of the internal action τ, coupled simulations are symmetric, and coupled similarity coincides with strong bisimilarity (as defined in [12]).

Intuitively, P ⊒_{CS}^{Δ} Q says that P is “ahead” of a state matching Q, where P′ is ahead of P if P ⟹ P′. The first clause says that if P is ahead of a state matching Q, then any transition performed by P can be matched by Q— possibly after Q “caught up” with P by performing some internal transitions. The second clause says that if P is ahead of Q, then Q can always catch up, so that it is ahead of P. Thus, if P and Q are in stable states—where no internal actions are possible—then P ⊑_{CS}^{Δ} Q implies Q ⊑_{CS}^{Δ} P. In all other situations, P and Q do not need to be matched exactly, but there do exists under- and overapproximations of a match. The result is that the relation behaves like a weak bisimulation w.r.t. visible actions, but is not so pedantic in matching internal actions.

Proposition 1. ⊒_{CS}^{Δ} is reflexive and transitive, and thus a preorder.

Proof. The identity relation Id is a divergence-preserving coupled simulation, and if R, R′ are divergence-preserving coupled simulations, then so is R ; R′ ∪ R′ ; R. Here R ;R′ is defined by P R ; R′ R iff there is a Q with P R Q R′ R.

R ; R′ is divergence-preserving: if P RQR′R and P ⇑, then Q⇑, and thus R⇑. The same holds for R′ ; R, and thus for R ; R′ ∪ R′ ; R.

To check that R ; R′ ∪ R′ ; R satisfies the first clause of Def. 4, note that if Q R′ R and Q ⟹^{α̂} Q′, then, by repeated application of the first clause of Def. 4, there is an R′ with R ⟹^{α̂} R′ and Q′ R′ R′.

Towards the second clause, if P R Q R′ R, then, using the second clause for R, there is a Q′ with Q ⟹ Q′ and Q′ R P. Hence, using the first clause for R′, there is an R′ with R ⟹ R′ and Q′ R′ R′. Thus, using the second clause for R′, there is an R′′ with R′ ⟹ R′′ and R′′ R′ Q′, and hence R′′ R′ ; R P′. ⊓ ⊔

Proposition 2. If P ⟹ Q then P ⊑_{CS}^{Δ} Q.

Proof. I show that Id ∪ {(Q, P)}, with Id the identity relation, is a coupled simulation. Namely if Q ⟶^{α} Q′ then surely P ⟹^{α} Q′. The second clause of Def. 4 is satisfied because P ⟹ Q. Furthermore, if Q⇑ then certainly P ⇑, so the relation is divergence-preserving. ⊓ ⊔

Proposition 3. P ⊒_{CS}^{Δ} Q iff P ⊓ Q ≡_{CS}^{Δ} Q.

Proof. “⇒”: Let R be the smallest relation such that, for any P and Q, P ⊒_{CS}^{Δ} Q implies P R Q, (P ⊓ Q) R Q and Q R (P ⊓ Q). It suffices to show that R is a divergence-preserving coupled simulation.

That R is divergence-preserving is trivial, using that (P ⊓ Q)⇑ iff P ⇑ ∨ Q⇑. Suppose P^{∗} R Q and P^{∗} ⟶^{α} P′. The case that P^{∗} = P with P ⊒_{CS}^{Δ} Q is

trivial. Now let Q be Q^{∗} ⊓ P^{∗}. Since P^{∗} ⟶^{α} P′, surely Q ⟹^{α} P′, and P′ R P′. Finally, let P^{∗} = (P ⊓ Q) with P ⊒_{CS}^{Δ} Q. Then α = τ and P′ is either P or Q. Both cases are trivial, taking Q′ = Q.

Towards the second clause of Def. 4, suppose P^{∗} R Q. The case P^{∗} = P with P ⊒_{CS}^{Δ} Q is trivial. Now let Q be Q^{∗} ⊓ P^{∗}. Then Q ⟹ P^{∗} and P^{∗} R P^{∗}. Finally, let P^{∗} = (P ⊓ Q) with P ⊒_{CS}^{Δ} Q. Then Q ⟹ Q and Q R (P ⊓ Q).

“⇐”: Suppose P ⊓ Q ⊒_{CS}^{Δ} Q. Since P ⊓ Q ⟶^{τ} P there exists a Q′ with Q ⟹ Q′ and P ⊒_{CS}^{Δ} Q′. By Prop. 2 Q′ ⊒_{CS}^{Δ} Q and by Prop. 1 P ⊒_{CS}^{Δ} Q. ⊓ ⊔

7 Congruence Properties

Proposition 4. ≡_{CS}^{Δ} is a congruence for action prefixing.

Proof. I have to show that P ≡_{CS}^{Δ} Q implies (a → P) ≡_{CS}^{Δ} (a → Q).

Let R be the smallest relation such that, for any P and Q, P ⊑_{CS}^{Δ} Q implies P R Q, and P ≡_{CS}^{Δ} Q implies (a → P) R (a → Q). It suffices to show that R is a divergence-preserving coupled simulation.

Checking the conditions of Def. 4 for the case P R Q with P ⊑_{CS}^{Δ} Q is trivial. So I examine the case (a → P) R (a → Q) with P ≡_{CS}^{Δ} Q.

Suppose (a → P) ⟶^{α} P′. Then α = a and P′ = P. Now (a → Q) ⟶^{α} Q and P R Q, so the first condition of Def. 4 is satisfied.

For the second condition, (a → Q) ⟹ (a → Q), and, since Q ≡_{CS}^{Δ} P, (a → Q) R (a → P). Thus, R is a coupled simulation.

As a → P does not diverge, R moreover is divergence-preserving. ⊓ ⊔

Since STOP ⊒_{CS}^{Δ} (a → ST OP) ▷ STOP but STOP ⋢_{CS}^{Δ} (a → ST OP) ▷ STOP, and thus b → STOP ⋣_{CS}^{Δ} b → ((a → ST OP) ▷ STOP), the relation ⊒_{CS}^{Δ} is not a precongruence for action prefixing.

It is possible to express action prefixing in terms of the throw operator: a → P is strongly bisimilar with (a → STOP) Θ_{{a}} P. Consequently, ⊒_{CS}^{Δ} is not a precongruence for the throw operator.

Proposition 5. ≡_{CS}^{Δ} is a congruence for the throw operator.

Proof. Let A ⊆ Σ. Let R be the smallest relation such that, for any P_{1}, P_{2}, Q_{1}, Q_{2}, P_{1} ⊒_{CS}^{Δ} Q_{1} and P_{2} ≡_{CS}^{Δ} Q_{2} implies P_{1} R Q_{1} and (P_{1} Θ_{A} P_{2}) R (Q_{1} Θ_{A} Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{1} ⊒_{CS}^{Δ} Q_{1}, P_{2} ≡_{CS}^{Δ} Q_{2} and (P_{1} Θ_{A} P_{2}) ⟶^{α} P′. Then P_{1} ⟶^{α} P′_{1}

for some P′_{2}, and either α ∉ A and P′ = P′_{1} Θ_{A} P_{2}, or α ∈ A and P′ = P_{2}. So there is a Q′_{1} with Q_{1} ⟹^{α̂} Q′_{1} and P′_{1} ⊒_{CS}^{Δ} Q′_{1}. If α ∉ A it follows that

(Q_{1} Θ_{A} Q_{2}) ⟹^{α̂} (Q′_{1} Θ_{A} Q_{2}) and (P′_{1} Θ_{A} P_{2}) R (Q′_{1} Θ_{A} Q_{2}). If α ∈ A it follows

that (Q_{1} Θ_{A} Q_{2}) ⟹^{α} Q_{2} and P_{2} R Q_{2}.

Now let P_{1} ⊒_{CS}^{Δ} Q_{1} and P_{2} ≡_{CS}^{Δ} Q_{2}. Then there is a Q′_{1} with Q_{1} ⟹ Q′_{1} and Q′_{1} ⊒_{CS}^{Δ} P_{1}. Hence Q_{1} Θ_{A} Q_{2} ⟹ Q′_{1} Θ_{A} Q_{2} and (Q′_{1} Θ_{A} Q_{2}) R (P_{1} Θ_{A} P_{2}).

The same two conditions for the case P R Q because P ⊒_{CS}^{Δ} Q are trivial. Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1} Θ_{A} P_{2}⇑ iff P_{1}⇑. ⊓ ⊔

I proceed to show that ⊒_{CS}^{Δ} is a precongruence for all the other operators of CSP. This implies that ≡_{CS}^{Δ} is a congruence for all the operators of CSP.

Proposition 6. ⊒_{CS}^{Δ} is a precongruence for internal choice.

Proof. Let R be the smallest relation such that, for any P_{i} and Q_{i}, P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 implies P_{i} R Q_{i} (i = 1, 2) and (P_{1} ⊓ P_{2}) R (Q_{1} ⊓ Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 and (P_{1} ⊓ P_{2}) ⟶^{α} P′. Then α = τ and P′ = P_{i} for i = 1 or 2. Now Q_{1} ⊓ Q_{2} ⟹ Q_{i} and P_{i} R Q_{i}.

Now let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2. Then there is a Q′_{1} with Q_{1} ⟹ Q′_{1} and Q′_{1} ⊒_{CS}^{Δ} P_{1}. By Prop. 2 P_{1} ⊒_{CS}^{Δ} P_{1} ⊓ P_{2} and by Prop. 1 Q′_{1} ⊒_{CS}^{Δ} P_{1} ⊓ P_{2}.

The same two conditions for the case P R Q because P ⊒_{CS}^{Δ} Q are trivial. Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1} ⊓ P_{2}⇑ iff P_{1}⇑ ∨ P_{2}⇑. ⊓ ⊔ Proposition 7. ⊒_{CS}^{Δ} is a precongruence for external choice.

Proof. Let R be the smallest relation such that, for any P_{i} and Q_{i}, P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 implies P_{i} R Q_{i} (i = 1, 2) and (P_{1} □ P_{2}) R (Q_{1} □ Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 and (P_{1} □ P_{2}) ⟶^{α} P′. If α ∈ Σ then P_{i} ⟶^{α} P′

for i = 1 or 2, and there exists a Q′ with Q_{i} ⟹^{α} Q′ and P′ ⊒_{CS}^{Δ} Q′. Hence Q_{1} □ Q_{2} ⟹^{α} Q′ and P′ R Q′. If α = τ then either P_{1} ⟶^{τ} P′_{1} for some P′_{1} with P′ = P′_{1} □ P_{2}, or P_{2} ⟶^{τ} P′_{2} for some P′_{2} with P′ = P_{1} □ P′_{2}. I pursue only the first case, as the other follows by symmetry. Here Q_{1} ⟹ Q′_{1} for some Q′_{1} with P′_{1} ⊒_{CS}^{Δ} Q′_{1}. Thus Q_{1} □ Q_{2} ⟹ Q′_{1} □ Q_{2} and (P′_{1} □ P_{2}) R (Q′_{1} □ Q_{2}).

Now let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2. Then, for i = 1, 2, there is a Q′_{i} with Q_{i} ⟹ Q′_{i} and Q′_{i} ⊒_{CS}^{Δ} P_{i}. Hence Q_{1} □ Q_{2} ⟹ Q′_{1} □ Q′_{2} and (Q′_{1} □ Q′_{2}) R (P_{1} □ P_{2}).

Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1} □ P_{2}⇑ iff P_{1}⇑ ∨ P_{2}⇑. ⊓ ⊔

Proposition 8. ⊒_{CS}^{Δ} is a precongruence for sliding choice.

Proof. Let R be the smallest relation such that, for any P_{i} and Q_{i}, P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 implies P_{i} R Q_{i} (i = 1, 2) and (P_{1} ▷ P_{2}) R (Q_{1} ▷ Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 and (P_{1} ▷ P_{2}) ⟶^{α} P′. If α ∈ Σ then P_{1} ⟶^{α} P′,

and there exists a Q′ with Q_{1} ⟹^{α} Q′ and P′ ⊒_{CS}^{Δ} Q′. Hence Q_{1} ▷ Q_{2} ⟹^{α} Q′ and P′ R Q′. If α=τ then either P′ =P_{2} or P_{1} ⟶^{τ} P′_{1} for some P′_{1} with P′ =P′_{1} ▷P_{2}. In the former case Q_{1} ▷ Q_{2} ⟹ Q_{2} and P_{2} R Q_{2}. In the latter case Q_{1} ⟹ Q′_{1} for some Q′_{1} with P′_{1} ⊒_{CS}^{Δ} Q′_{1}. Thus Q_{1} ▷ Q_{2} ⟹ Q′_{1} ▷ Q_{2} and (P′_{1} ▷ P_{2}) R (Q′_{1} ▷ Q_{2}).

Now let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2. Then there is a Q′_{2} with Q_{2} ⟹ Q′_{2} and Q′_{2} ⊒_{CS}^{Δ} P_{2}. By Prop. 2 P_{2} ⊒_{CS}^{Δ} P_{1} ▷ P_{2} and by Prop. 1 Q′_{2} ⊒_{CS}^{Δ} P_{1} ▷ P_{2}.

Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1} ▷ P_{2}⇑ iff P_{1}⇑ ∨ P_{2}⇑. ⊓ ⊔

Proposition 9. ⊒_{CS}^{Δ} is a precongruence for parallel composition.

Proof. Let A ⊆ Σ. Let R be the smallest relation such that, for any P_{i} and Q_{i}, P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 implies (P_{1}∥_{A}P_{2}) R (Q_{1}∥_{A}Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 and (P_{1}∥_{A}P_{2}) ⟶^{α} P′. If α ∉ A then P_{i} ⟶^{α} P′_{i}

for i = 1 or 2, and P′ = P′_{1}∥_{A}P′_{2}, where P′_{3−i} := P_{3−i}. Hence there exists a Q′_{i}

with Q_{i} ⟹^{α̂} Q′_{i} and P′_{i} ⊒_{CS}^{Δ} Q′_{i}. Let Q′_{3−i} := Q_{3−i}. Then Q_{1}∥_{A}Q_{2} ⟹^{α̂} Q′_{1}∥Q′_{2}

and (P′_{1}∥P′_{2}) R (Q′_{1}∥Q′_{2}). If α ∈ A then P_{i} ⟶^{α} P′_{i} for i = 1 and 2. Hence, for

i = 1, 2, Q_{i} ⟹^{α} Q′_{i} for some Q′_{i} with P′_{i} ⊒_{CS}^{Δ} Q′_{i}. Thus Q_{1}∥_{A}Q_{2} ⟹^{α} Q′_{1}∥_{A}Q′_{2} and

(P′_{1}∥_{A}P′_{2}) R (Q′_{1}∥_{A}Q′_{2}).

Now let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2. Then, for i = 1, 2, there is a Q′_{i} with Q_{i} ⟹ Q′_{i} and Q′_{i} ⊒_{CS}^{Δ} P_{i}. Hence Q_{1}∥_{A}Q_{2} ⟹ Q′_{1}∥_{A}Q′_{2} and (Q′_{1}∥_{A}Q′_{2}) R (P_{1}∥_{A}P_{2}).

Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1}∥_{A}P_{2}⇑ iff P_{1}⇑ ∨ P_{2}⇑. ⊓ ⊔ Proposition 10. ⊒_{CS}^{Δ} is a precongruence for concealment.

Proof. Let A ⊆ Σ. Let R be the smallest relation such that, for any P and Q, P ⊑_{CS}^{Δ} Q implies (P \A) R (Q\A). It suffices to show that R is a divergencepreserving coupled simulation.

So let P ⊑_{CS}^{Δ} Q and P \A ⟶^{α} P^{∗}. Then P^{∗} = P′\A for some P′ with P ⟶^{β} P′, and either β ∈ A and α = τ, or β = α ∉ A. Hence Q ⟶^{β} Q′ for some

Q′ with P′ ⊑_{CS}^{Δ} Q′. Therefore Q\A ⟶^{α} Q′\A and (P′\A) R (Q′\A).

Now let P ⊑_{CS}^{Δ} Q. Then there is a Q′ with Q ⟹ Q′ and Q′ ⊒_{CS}^{Δ} P. Hence Q\A ⟹ Q′\A and (Q′\A) R (P \A).

To check that R is divergence-preserving, suppose (P \A)⇑. Then there are

P_{i} and α_{i} ∈ A ∪ {τ} for all i > 0 such that P ⟶^{α_{1}} P_{1} ⟶^{α_{2}} P_{2} ⟶^{α_{3}} . . .. By the

first condition of Def. 4, there are Q_{i} for all i > 0 such that P_{i} R Q_{i} and

Q ⟹^{α̂_{1}} Q_{1} ⟹^{α̂_{2}} Q_{2} ⟹^{α̂_{3}} . . .. This implies Q\A ⟹ Q_{1}\A ⟹ Q_{2}\A ⟹ . . ..

In case α_{i} ∈ Σ for infinitely many i, then for infinitely many i one has Q_{i−1} ⟹^{α_{i}} Q_{i} and thus Q_{i−1}\A ⟹^{τ} Q_{i}\A. This implies that (Q\A)⇑.

Otherwise there is an n > 0 such that α_{i} = τ for all i ≥ n. In that case P_{n}⇑ and thus Q_{n}⇑. Hence (Q_{n}\A)⇑ and thus (Q\A)⇑. ⊓ ⊔

Proposition 11. ⊒_{CS}^{Δ} is a precongruence for renaming.

Proof. Let f : Σ → Σ. Let R be the smallest relation such that, for any P and Q, P ⊑_{CS}^{Δ} Q implies f(P) R f(Q). It suffices to show that R is a divergencepreserving coupled simulation.

So let P ⊑_{CS}^{Δ} Q and f(P) ⟶^{α} P^{∗}. Then P^{∗} = f(P′) for some P′ with P ⟶^{β} P′ and f(β) = α. Hence Q ⟶^{β} Q′ for some Q′ with P′ ⊑_{CS}^{Δ} Q′. Therefore

f(Q) ⟶^{α} f(Q′) and f(P′) R f(Q′).

Now let P ⊑_{CS}^{Δ} Q. Then there is a Q′ with Q ⟹ Q′ and Q′ ⊒_{CS}^{Δ} P. Hence f(Q) ⟹ f(Q′) and f(Q′) R f(P).

To check that R is divergence-preserving, suppose f(P)⇑. Then P ⇑, so Q⇑ and f(Q)⇑. ⊓ ⊔

Proposition 12. ⊒_{CS}^{Δ} is a precongruence for the interrupt operator.

Proof. Let R be the smallest relation such that, for any P_{i} and Q_{i}, P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 implies P_{2} R Q_{2} and (P_{1} △ P_{2}) R (Q_{1} △ Q_{2}). It suffices to show that R is a divergence-preserving coupled simulation.

So let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2 and (P_{1} △P_{2}) ⟶^{α} P′. Then either P′ = P′_{1} △P_{2} for some P′_{1} with P_{1} ⟶^{α} P′_{1}, or α = τ and P′ = P_{1} △ P′_{2} for some P′_{2} with

P_{2} ⟶^{τ} P′_{2}, or α ∈ Σ and P_{2} ⟶^{α} P′.

In the first case there is a Q′_{1} with Q_{1} ⟹^{α̂} Q′_{1} and P′_{1} ⊒_{CS}^{Δ} Q′_{1}. It follows that

(Q_{1} △ Q_{2}) ⟹^{α̂} (Q′_{1} △ Q_{2}) and (P′_{1} △ P_{2}) R (Q′_{1} △ Q_{2}).

In the second case there is a Q′_{2} with Q_{2} ⟹ Q′_{2} and P′_{2} ⊒_{CS}^{Δ} Q′_{2}. It follows that (Q_{1} △ Q_{2}) ⟹ (Q_{1} △ Q′_{2}) and (P_{1} △ P′_{2}) R (Q_{1} △ Q′_{2}).

In the last case there is a Q′_{2} with Q_{2} ⟹^{α} Q′_{2} and P′_{2} ⊒_{CS}^{Δ} Q′_{2}. It follows that

(Q_{1} △ Q_{2}) ⟹^{α} Q′_{2} and P′_{2} R Q′_{2}.

Now let P_{i} ⊒_{CS}^{Δ} Q_{i} for i = 1, 2. Then, for i = 1, 2, there is a Q′_{i} with Q_{i} ⟹ Q′_{i} and Q′_{i} ⊒_{CS}^{Δ} P_{i}. Hence Q_{1} △ Q_{2} ⟹ Q′_{1} △ Q′_{2} and (Q′_{1} △ Q′_{2}) R (P_{1} △ P_{2}).

Thus R is a coupled simulation. That R is divergence-preserving follows because P_{1} △ P_{2}⇑ iff P_{1}⇑ ∨ P_{2}⇑. ⊓ ⊔

8 A Complete Axiomatisation of ≡_{CS}^{Δ}

A set of equational laws valid for ≡_{CS}^{Δ} is presented in Table 3. It includes the laws from Table 2 that are still valid for ≡_{CS}^{Δ}. I will show that this axiomatisation is sound and complete for ≡_{CS}^{Δ} for recursion-free CSP without the interrupt operator. The axioms U2 and U3, which are not valid for ≡_{CS}^{Δ}, played a crucial rôle in reducing CSP expressions with interrupt into normal form. It is not trivial to find valid replacements, and due to lack of space and time I do not tackle this problem here.

The axiom H5 replaces the fallen axiom H2, and is due to [17]. Here the result of hiding actions results in a process that cannot be expressed as a normal form built up from a →, ⊓ and □. For this reason, one needs a richer normal form, involving the sliding choice operator. It is given by the context-free grammar

N → D | D ▷ I
I → D | I ⊓ I
D → STOP | div | E | div □ E
E → (a → N) | (a → N) □ E .

Definition 5. A CSP expression is in head normal form if it is of the form ([div □] □_{i∈I}(a_{i} → R_{i})) ▷ ⊓_{j∈J} R_{j}, with R_{j} = ([div □] □_{k∈K_{j}}(a_{kj} → R_{kj})) for j ∈ J. Here I, J and the K_{j} are finite index sets, and the parts between square brackets are optional. Here, although ⊓_{i∈∅} P_{i} is undefined, I use P ▷ ⊓_{i∈∅} P_{i} to represent P. An expression is in normal form if it has this form and also the subexpressions R_{i} and R_{kj} are in normal form.

A head normal form is saturated if the div-summand on the left is present whenever any of the R_{j} has a div-summand, and for any j ∈ J and any k ∈ K_{j} there is an i ∈ I with a_{i} = a_{kj} and R_{i} = R_{kj}.

My proof strategy is to ensure that there are enough axioms to transform any CSP process without recursion and interrupt operators into normal form, and to make these forms saturated; then to equate saturated normal forms that are divergence-preserving coupled simulation equivalent.

Due to the optional presence in head normal forms of a div-summand and a sliding choice, I need four variants of the axiom H5; so far I have not seen a way around this. Likewise, there are 4 × 4 variants of the axiom P4 from Table 2, of which 6 could be suppressed by symmetry (P4–P13). There are also 3 axioms replacing P2 (P14–P16).

I1  P ⊓ P = P
I2  P ⊓ Q = Q ⊓ P
I3  P ⊓ (Q ⊓ R) = (P ⊓ Q) ⊓ R
E2  P □ Q = Q □ P
E3  P □ (Q □ R) = (P □ Q) □ R
E4  P □ STOP = P
S1  P ▷ P = P
S2  P ▷ (Q ▷ R) = (P ▷ Q) ▷ R
S3  (P ▷ Q) ▷ R = (P □ Q) ▷ R
S4  (P ⊓ Q) ▷ R = (P □ Q) ▷ R
S5  STOP ▷ P = P
S6  (P ▷ Q) ⊓ (R ▷ S) = (P □ R) ▷ (Q ⊓ S)
S7  (P ▷ Q) □ (R ▷ S) = (P □ R) ▷ (Q □ S)
D1  P □ (Q ⊓ R) = (P □ Q) ⊓ (P □ R)
Prune  (a → P) □ a → (P ⊓ Q) = a → (P ⊓ Q)
P0  P ∥_{A}(Q∥_{A}R) = (P ∥_{A}Q)∥_{A}R
P1  P ∥_{A}Q = Q∥_{A}P
P4–P13 more axioms for parallel composition follow on the next page
H1  (P ⊓ Q)\A = (P \A) ⊓ (Q\A)
H5  (□_{i∈I}(a_{i} → P_{i}))\A = (□_{a_{i}∉A}(a_{i} → (P_{i}\A)))
▷ ⊓_{a_{i}∈A}(P_{i}\A)
H6  (div □ □_{i∈I}(a_{i} → P_{i}))\A = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}\A)))
▷ ⊓_{a_{i}∈A}(P_{i}\A)
H7  ((□_{i∈I}(a_{i} → P_{i})) ▷ P′) \A = (□_{a_{i}∉A}(a_{i} → (P_{i}\A)))
▷ (P′\A ⊓ ⊓_{a_{i}∈A}(P_{i}\A))
H8  ((div □ □_{i∈I}(a_{i} → P_{i})) ▷ P′)\A = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}\A)))
▷ (P′\A ⊓ ⊓_{a_{i}∈A}(P_{i}\A))
R0  f(P ▷ Q) = f(P) ▷ f(Q)
R1  f(P ⊓ Q) = f(P) ⊓ f(Q)
R2  f(P □ Q) = f(P) □ f(Q)
R3  f(a → P) = f(a) → f(P)
R4  f(STOP) = STOP
R5  f(div) = div
T0  (P ▷ Q) Θ_{A} R = (P Θ_{A} R) ▷ (Q Θ_{A} R)
T1  (P ⊓ Q) Θ_{A} R = (P Θ_{A} R) ⊓ (Q Θ_{A} R)
T2  (P □ Q) Θ_{A} R = (P Θ_{A} R) □ (Q Θ_{A} R)
T3  (a → P) Θ_{A} Q = a → (P Θ_{A} Q)  if a ∉ A
T4  (a → P) Θ_{A} Q = a → Q  if a ∈ A
T5  STOP Θ_{A} Q = STOP
T6  div Θ_{A} Q = div

Table 3. A complete axiomatisation of ≡_{CS}^{Δ} for recursion-free CSP without interrupt Below P = □_{i∈I}(a_{i} → P_{i}) and Q = □_{j∈J}(b_{j} → Q_{j}).

(P4)  P ∥_{A}Q = □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → (P ∥_{A}Q_{j}))

(P5)  (div □ P)∥_{A}Q = div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → ((div □ P)∥_{A}Q_{j}))

(P6)  (div □ P)∥_{A}(div □ Q) = div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}(div □ Q)))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → ((div □ P)∥_{A}Q_{j}))

(P7)  (P ▷ P′)∥_{A}Q = (□_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → ((P ▷ P′)∥_{A}Q_{j}))) ▷ P′∥_{A}Q

(P8)  ((div □ P) ▷ P′)∥_{A}Q = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → (((div □ P) ▷ P′)∥_{A}Q_{j})))

▷ P′∥_{A}Q

(P9)  (P ▷ P′)∥_{A}(div □ Q) = ((div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}(div □ Q)))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → ((P ▷ P′)∥_{A}Q_{j})))

▷ P′∥_{A}(div □ Q)

(P10) ((div □ P) ▷ P′)∥_{A}(div □ Q) = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}(div □ Q)))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → (((div □ P) ▷ P′)∥_{A}Q_{j})))

▷ P′∥_{A}(div □ Q)

(P11)  (P ▷ P′)∥_{A}(Q ▷ Q′) = (□_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}(Q ▷ Q′)))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → ((P ▷ P′)∥_{A}Q_{j})))

▷ (P′∥_{A}(Q ▷ Q′) ⊓ (P ▷ P′)∥_{A}Q′)

(P12) ((div □ P) ▷ P′)∥_{A}(Q ▷ Q′) = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}(Q ▷ Q′)))□

□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□

□_{b_{j} ∉A}(b_{j} → (((div □ P) ▷ P′)∥_{A}Q_{j})))

▷ (P′∥_{A}(Q ▷ Q′) ⊓ ((div □ P) ▷ P′)∥_{A}Q′)

Table 3. A complete axiomatisation of ≡_{CS}^{Δ} for recursion-free CSP (continued)

(P13)  ((div □ P) ▷ P′)∥_{A}((div □ Q) ▷ Q′) = (div□
□_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}((div □ Q) ▷ Q′)))□
□_{a_{j} =b_{j} ∈A}(a_{i} → (P_{i}∥_{A}Q_{j}))□
□_{b_{j} ∉A}(b_{j} → (((div □ P) ▷ P′)∥_{A}Q_{j})))

▷ (P′∥_{A}((div □ Q) ▷ Q′) ⊓ ((div □ P) ▷ P′)∥_{A}Q′)

Below P = □_{i∈I}(a_{i} → P_{i}) and Q = ⊓_{j∈J} Q_{j}.

(P14)  P ∥_{A}Q = □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q)) ▷ ⊓_{j∈J}(P ∥_{A}Q_{j}))
(P15) (div □ P)∥_{A}Q = (div □ □_{a_{i}∉A}(a_{i} → (P_{i}∥_{A}Q))) ▷ ⊓_{j∈J}((div □ P)∥_{A}Q_{j}))

Below P = ⊓_{i∈I} P_{i} and Q = ⊓_{j∈J} Q_{j}.

(P16)  P ∥_{A}Q = ⊓_{a_{i}∉A}(P_{i}∥_{A}Q) ⊓ ⊓_{j∈J}(P ∥_{A}Q_{j}))

Table 3. A complete axiomatisation of ≡_{CS}^{Δ} for recursion-free CSP (continued)

9 Soundness

Since divergence-preserving coupled similarity is a congruence for all CSP operators, to establish the soundness of the axiomatisation of Table 3 it suffices to show the validity w.r.t. ≡_{CS}^{Δ} of all axioms. When possible, I show validity w.r.t. strong bisimilarity, which is a strictly finer equivalence.

Definition 6. Two processes are strongly bisimilar [12] if they are related by a binary relation R on processes such that, for all α ∈ Σ ∪ {τ},

– if P R Q and P ⟶^{α} P′ then there exists a Q′ with Q ⟶^{α} Q′ and P′ R Q′,

– if P R Q and Q ⟶^{α} Q′ then there exists a P′ with P ⟶^{α} P′ and P′ R Q′.

Proposition 13. Axiom I1 is valid for ≡_{CS}^{Δ}.

Proof. {(P ⊓ P, P), (P, P ⊓ P) | P a process} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔

Proposition 14. Axiom I2 is valid even for strong bisimilarity.

Proof. {(P ⊓ Q, Q ⊓ P) | P, Q processes} ∪ Id is a strong bisimulation. ⊓ ⊔

Proposition 15. Axiom I3 is valid for ≡_{CS}^{Δ}.

Proof. The relation {(P ⊓ (Q ⊓ R), (P ⊓ Q) ⊓ R), ((P ⊓ Q) ⊓ R, P ⊓ (Q ⊓ R)), (Q⊓R, (P ⊓Q)⊓R), (P ⊓Q, P ⊓(Q⊓R)), (R, Q⊓R), (P, P ⊓Q) | P, Q, R processes} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 16. Axioms E2–4 are valid for strong bisimilarity. Proof. The relation {(P □ (Q □ R), (P □ Q) □ R) | P, Q, R processes} ∪ Id is a strong bisimulation. So is {(P □ Q, Q □ P) | P, Q processes} ∪ Id, as well as {(P □ STOP, P) | P a process} ∪ Id. ⊓ ⊔ Proposition 17. Axiom S1 is valid for ≡_{CS}^{Δ}. Proof. {(P′ ▷ P, P), (P, P′ ▷ P) | P′ ⊒_{CS}^{Δ} P } ∪ Id is a divergence-preserving coupled simulation. This follows from Prop. 2. ⊓ ⊔ Proposition 18. Axiom S2 is valid for ≡_{CS}^{Δ}. Proof. {(P ▷(Q▷R), (P ▷Q)▷R), ((P ▷Q)▷R, P ▷(Q▷R)) | P, Q, R processes}∪Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 19. Axiom S3 is valid for ≡_{CS}^{Δ}. Proof. {((P ▷Q)▷R, (P □Q)▷R), ((P □Q′)▷R, (P ▷Q)▷R), (Q▷R, (P □Q)▷R), (R, Q ▷ R) | Q′ ⊒_{CS}^{Δ} Q} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 20. Axiom S4 is valid for ≡_{CS}^{Δ}. Proof. {((P ⊓Q)▷R, (P □Q)▷R), ((P′□Q′)▷R, (P ⊓Q)▷R), (P ▷R, (P □Q)▷R), (Q ▷ R, (P □ Q) ▷ R), (R, Q ▷ R) | P′ ⊒_{CS}^{Δ} P ∧ Q′ ⊒_{CS}^{Δ} Q} ∪ Id is a divergencepreserving coupled simulation. Checking this involves Prop. 2. ⊓ ⊔ Proposition 21. Axiom S5 is valid for ≡_{CS}^{Δ}. Proof. The relation {(STOP ▷ P, P), (P, STOP ▷ P) | P a process} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 22. Axiom S6 is valid for ≡_{CS}^{Δ}. Proof. {((P ▷Q)⊓(R▷S), (P □R)▷(Q⊓S)), ((P′□R′)▷(Q⊓S), (P ▷Q)⊓(R▷S)), (P ▷ Q, (P □ R) ▷ (Q ⊓ S)), (R ▷ S, (P □ R) ▷ (Q ⊓ S)), (Q ⊓ S, (P ▷ Q) ⊓ (R ▷ S)), (S, (P′ □ R′) ▷ (Q ⊓ S)), (S, R ▷ S), (S, Q ⊓ S) | P′ ⊒_{CS}^{Δ} P ∧ R′ ⊒_{CS}^{Δ} R} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 23. Axiom S7 is valid for ≡_{CS}^{Δ}. Proof. {((P ▷Q)□(R▷S), (P □R)▷(Q□S)), ((P □R)▷(Q□S), (P ▷Q)□(R▷S)), (Q′ □ (R ▷ S), (P □ R) ▷ (Q □ S)) , ((P ▷ Q) □ S′, (P □ R) ▷ (Q □ S)), (Q′ □ S′, Q′ □ (R ▷ S)), (Q′ □ S′, (P ▷ Q) □ S′), | Q ⟹ Q′ ∧ S ⟹ S′} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 24. Axiom D1 is valid for ≡_{CS}^{Δ}. Proof. {(P′ □ (Q ⊓ R), (P □ Q) ⊓ (P □ R)), ((P □ Q) ⊓ (P □ R), P □ (Q ⊓ R)), (P′ □ Q, P′ □ (Q ⊓ R)) | P ⟹ P′} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 25. Axiom Prune is valid for ≡_{CS}^{Δ}. Proof. {((a→P) □ a→(P ⊓ Q), a→(P ⊓ Q)), (a→(P ⊓ Q), (a→P) □ a→(P ⊓ Q))} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔ Proposition 26. Axioms P0–1 and P4–10 are valid for strong bisimilarity. Axioms P11–16 are valid for ≡_{CS}^{Δ}.

Proof. Straightforward. ⊓ ⊔

Proposition 27. Axioms U4, H1, R0–5 and T0–6 are valid for strong bisimilarity. Axioms H5–8 are valid for ≡_{CS}^{Δ}.

Proof. Straightforward. ⊓ ⊔

Proposition 28. Axiom U1 is valid for ≡_{CS}^{Δ}.

Proof. {((P ⊓ Q) △ R′, (P △ R) ⊓ (Q △ R)), ((P △ R) ⊓ (Q △ R), (P ⊓ Q) △ R), (P △ R′, (P ⊓ Q) △ R′) | R ⟹ R′} ∪ Id is a divergence-preserving coupled simulation. ⊓ ⊔

10 Completeness

Let Th be the axiomatisation of Table 3.

Proposition 29. For each recursion-free CSP process P without interrupt operators there is a CSP process Q in normal form such that Th ⊢ P = Q.

Proof. By structural induction on P it suffices to show that for each n-ary CSP operator Op, and all CSP processes P_{1}, ..., P_{n} in normal form, also Op(P_{1}, ..., P_{n}) can be converted to normal form. This I do with structural induction on the arguments P_{i}.

– Let P = STOP or div. Then P is already in normal form. Take Q := P.

– Let P = a → P′. By assumption P′ is in normal form; therefore so is P.

– Let P = P_{1} ⊓ P_{2}. By assumption P_{1} and P_{2} are in normal form. So P = (([div □] □_{i∈I}(a_{i} → R_{i})) ▷ ⊓_{j∈J}R_{j})⊓(([div □] □_{l∈L}(a_{l} → R_{l})) ▷ ⊓_{j∈M}R_{j})

with R_{j} = ([div □] □_{k∈K_{j}}(a_{kj} → R_{kj})) for j ∈ J ∪ M. With Axiom S5 I

may assume that J, M ≠ ∅. Now Axiom S6 converts P to normal form.

– Let P = P_{1} □ P_{2}. By assumption P_{1} and P_{2} are in normal form. So P = (([div □] □_{i∈I}(a_{i} → R_{i})) ▷ ⊓_{j∈J}R_{j})□(([div □] □_{l∈L}(a_{l} → R_{l})) ▷ ⊓_{j∈M}R_{j})

with R_{j} = ([div□]□_{k∈K_{j}}(a_{kj} → R_{kj})) for j ∈ J∪M. With S5 I may assume

that J, M ≠ ∅. Now Axioms S7 and D1 convert P to normal form.

– Let P = P_{1} ▷ P_{2}. Axioms S2–4 and D1 convert P to normal form.

– Let P = P_{1}∥_{A}P_{2}. Axioms P1 and P4–16, together with the induction hypothesis, convert P to normal form.

– Let P = P \A. Axioms H1 and H5–8, together with the induction hypothesis, convert P to normal form.

– Let P = f(P). Axioms R0–5, together with the induction hypothesis, convert P to normal form.

– Let P = P_{1} Θ_{A} P_{2}. Axioms T0–6, together with the induction hypothesis, convert P to normal form.

Lemma 1. For any CSP expression P in head normal form there exists a saturated CSP expression Q in head normal form.

Proof. Let P = ([div □] □_{i∈I}(a_{i} → R_{i})) ▷ ⊓_{j∈J}R_{j}. Then P has the form S ▷ R. By Axioms S1–3 Th ⊢ P = (S □ R) ▷ R. By means of Axioms D1 and S4 the subexpression S □ R can be brought in the form [div □] □_{l∈L}(a_{l} → R_{l}). The resulting term is saturated. ⊓ ⊔

Definition 7. A CSP expression (□_{i∈I}(b_{i} → P_{i})) is pruned if, for all i, h ∈ I, b_{i} = b_{h} ∧ P_{i} ⊒_{CS}^{Δ} P_{h} ⇒ i = h.

Theorem 1. Let P and Q be recursion-free CSP processes without interrupt operators. Then P ≡_{CS}^{Δ} Q iff Th ⊢ P = Q.

Proof. “⇐” is an immediate consequence of the soundness of the axioms of Th, and the fact that ≡_{CS}^{Δ} is a congruence for all operators of CSP.

“⇒”: Let depth(P) be the length of the longest trace of P —well-defined for recursion-free processes P. If P ≡_{CS}^{Δ} Q then depth(P) = depth(Q). Given P ≡_{CS}^{Δ} Q, I establish Th ⊢ P = Q with induction on depth(P).

By Prop. 29 I may assume, without loss of generality, that P and Q are in normal form. By Lem. 1 I furthermore assume that P and Q are saturated. Let P =([div□]□_{i∈I}(a_{i} →R_{i}))▷⊓_{j∈J}R_{j} and Q=([div□]□_{l∈L}(a_{l} →R_{l}))▷⊓_{j∈M}R_{j} with R_{j} = ([div □] □_{k∈K_{j}}(a_{kj} → R_{kj})) for j ∈J ∪M, where R_{i}, R_{l} and R_{kj} are again in normal form.

Suppose that there are i, h ∈ I with i ≠ h, a_{i} = a_{h} and R_{i} ⊒_{CS}^{Δ} R_{h}. Then R_{i} ⊓ R_{h} ≡_{CS}^{Δ} R_{h} by Prop. 3. Since depth(R_{i} ⊓ R_{h}) < depth(P), the induction hypothesis yields Th ⊢ R_{i} ⊓ R_{h} = R_{h}. Hence Axiom Prune allows me to prune the summand a_{i} → R_{i} from □_{i∈I}(a_{i} → R_{i}). Doing this repeatedly makes □_{i∈I}(a_{i} →R_{i}) pruned. By the same reasoning I may assume that □_{l∈L}(a_{l} →R_{l}) is pruned.

Since P ⇑ ⇔ Q⇑ and P and Q are saturated, P has the div-summand iff Q does. I now define a function f : I → L such that a_{f(i)} = a_{i} and R_{i} ⊒_{CS}^{Δ} R_{f(i)} for all i ∈ I.

Let i ∈ I. Since P ⟶^{a_{i}} R_{i}, by Def. 4 Q ⟹^{a_{i}} Q′ for some Q′ with R_{i} ⊒_{CS}^{Δ} Q′. Hence either there is an l ∈ L such that a_{l} = a_{i} and R_{l} ⟹ Q′, or there is a j ∈ M and k ∈ K_{j} such that a_{kj} = a_{i} and R_{kj} ⟹ Q′. Since P is saturated, the first of these alternatives must apply. By Prop. 2 Q′ ⊒_{CS}^{Δ} R_{l} and by Prop. 1 R_{i} ⊒_{CS}^{Δ} R_{l}. Take f(i) := l.

By the same reasoning there is a function g : L → I such that a_{g(l)} = a_{l} and R_{l} ⊒_{CS}^{Δ} R_{g(l)} for all l ∈ L. Since □_{i∈I}(a_{i} → R_{i}) and □_{l∈L}(a_{l} → R_{l}) are pruned, there are no different i, h ∈ I (or in L) with a_{i} = a_{h} and R_{i} ⊒_{CS}^{Δ} R_{h}. Hence the functions f and g must be inverses of each other. It follows that Q = ([div □] □_{i∈I}(a_{i} → R_{f(i)})) ▷ ⊓_{j∈M} R_{j} with R_{i} ≡_{CS}^{Δ} R_{f(i)} for all i ∈ I. By induction Th ⊢ R_{i} = R_{f(i)} for all i ∈ I.

So in the special case that I = M = ∅ I obtain Th ⊢ P = Q. (*)

Next consider the case J = ∅ but M ≠ ∅. Let j ∈ M. Since Q ⟹ R_{j}, there is a P′ with P ⟹ P′ and R_{j} ⊒_{CS}^{Δ} P′. Moreover, there is a P′′ with P′ ⟹ P′′ and P′′ ⊒_{CS}^{Δ} R_{j}. Since J = ∅, P′′ = P′ = P, so P ≡_{CS}^{Δ} R_{j}. By (*) above Th ⊢ P =R_{j}. This holds for all j ∈ J, so by Axiom I1 Th ⊢ Q = ([div □] □_{i∈I}(a_{i} → R_{i})) ▷ P. By Axiom S1 one obtains Th ⊢ P = Q.

The same reasoning applies when M = ∅ but J ≠ ∅. So henceforth I assume J, M ≠ ∅. I now define a function h: J → M with Th ⊢ R_{j} = R_{h(j)} for all j ∈ J.

Let j ∈ J. Since P ⟹^{τ} R_{j}, by Def. 4 Q ⟹ Q′ for some Q′ with R_{j} ⊒_{CS}^{Δ} Q′, and Q′ ⟹ Q′′ for some Q′′ with Q′′ ⊒_{CS}^{Δ} R_{j}. There must be an m ∈ M with Q′′ ⟹ R_{m}. By Def. 4 R_{j} ⟹ R′ for some R′ with R_{m} ⊒_{CS}^{Δ} R′, and R′ ⟹ R′′ for some R′′ with R′′ ⊒_{CS}^{Δ} R_{m}. By the shape of R_{j} one has R′′ = R′ = R_{j}, so R_{j} ≡_{CS}^{Δ} R_{m}. By (*) above Th ⊢ R_{j} = R_{m}. Take h(j) := m.

By the same reasoning there is a function e: M → J with Th ⊢ R_{m} = R_{e(m)} for all m ∈ M. Using Axioms I1–3 one obtains Th ⊢ P = Q. ⊓ ⊔

11 Conclusion

This paper contributed a new model of CSP, presented as a semantic equivalence on labelled transition systems that is a congruence for the operators of CSP. It is the finest I could find that allows a complete equational axiomatisation for closed recursion-free CSP processes that fits within the existing syntax of the language. For τ-free system, my model coincides with strong bisimilarity, but in matching internal transitions it is less pedantic than weak bisimilarity.

It is left for future work to show that recursion is treated well in this model, and also to extend my complete axiomatisation with the interrupt operator of Roscoe [15,17].

An annoying feature of my complete axiomatisation is the enormous collections of heavy-duty axioms needed to bring parallel compositions of CSP processes in head normal form. These are based on the expansion law of Milner [12], but a multitude of them is needed due to the optional presence of divergencesummands and sliding choices in head normal forms. In the process algebra ACP the expansion law could be avoided through the addition of two auxiliary operators: the left merge and the communication merge [3]. Unfortunately, failures-divergences equivalence fails to be a congruence for the left-merge, and the same problems exists for any other models of CSP [8, Section 3.2.1]. In [1] an alternative left-merge is proposed, for which failures-divergences equivalence, and also ≡_{CS}^{Δ}, is a congruence. It might be used to eliminate the expansion law P4 from the axiomatisation of Table 2. Unfortunately, the axiom that splits a parallel composition between a left-, right- and communication merge (Axiom CM1 in [3]), although valid in the failures-divergences model, is not valid for ≡_{CS}^{Δ}. This leaves the question of how to better manage the axiomatisation of parallel composition entirely open.

References

1. L. Aceto & A. Ingólfsdóttir (1991): A Theory of Testing for ACP. In J.C.M. Baeten & J.F. Groote, editors: Proc. CONCUR’91, LNCS 527, Springer, pp. 78–95, doi:10.

1007/3-540-54430-5_82.

2. J.A. Bergstra, J.W. Klop & E.-R. Olderog (1987): Failures without chaos: a new process semantics for fair abstraction. In M. Wirsing, editor: Formal Description of Programming Concepts – III, Proceedings of the 3^{th} IFIP WG 2.2 working conference, Ebberup 1986, North-Holland, Amsterdam, pp. 77–103.

3. J.A. Bergstra & J.W. Klop (1984): Process Algebra for Synchronous Communication. Inform. and Control 60, pp. 109–137, doi:10.1016/S0019-9958(84)80025-X.

4. S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journ. of the ACM 31(3), pp. 560–599, doi:10.1145/828.833.

5. S.D. Brookes & A.W. Roscoe (1985): An improved failures model for communicating processes. In S.D. Brookes, A.W. Roscoe & G. Winskel, editors: Seminar on Concurrency, LNCS 197, Springer, pp. 281–305, doi:10.1007/3-540-15670-4_14.

6. R. De Nicola (1985): Two Complete Axiom Systems for a Theory of Communicating Sequential Processes. Information and Control 64(1-3), pp. 136–172, doi:10.1016/

S0019-9958(85)80048-6.

7. R.J. van Glabbeek (1993): The Linear Time – Branching Time Spectrum II; The semantics of sequential systems with silent moves. In E. Best, editor: Proc. CON-CUR’93, LNCS 715, Springer, pp. 66–81, doi:10.1007/3-540-57208-2_6.

8. R.J. van Glabbeek & F.W. Vaandrager (1993): Modular Specification of Process Algebras. Theoretical Computer Science 113(2), pp. 293–348, doi:10.1016/

0304-3975(93)90006-F.

9. J.F. Groote & F.W. Vaandrager (1992): Structured Operational Semantics and Bisimulation as a Congruence. Information and Computation 100(2), pp. 202–

260, doi:10.1016/0890-5401(92)90013-6.

10. C.A.R. Hoare (1978): Communicating sequential processes. Communications of the ACM 21(8), pp. 666–677, doi:10.1145/359576.359585.

11. C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall.

12. R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980.

13. E.-R. Olderog & C.A.R. Hoare (1986): Specification-oriented semantics for communicating processes. Acta Informatica 23, pp. 9–66, doi:10.1007/BF00268075.

14. J. Parrow & P. Sjödin (1992): Multiway Synchronization Verified with Coupled Simulation. In R. Cleaveland, editor: Proc. CONCUR ’92, LNCS 630, Springer,

pp. 518–533, doi:10.1007/BFb0084813.

15. A.W. Roscoe (1997): The Theory and Practice of Concurrency. Prentice-Hall.

http://www.comlab.ox.ac.uk/bill.roscoe/publications/68b.pdf.

16. A.W. Roscoe (2009): Revivals, stuckness and the hierarchy of CSP models. Journal of Logic and Algebraic Programming 78(3), pp. 163–190, doi:10.1016/j.jlap.

2008.10.002.

17. A.W. Roscoe (2010): Understanding Concurrent Systems. Springer, doi:10.1007/

978-1-84882-258-0.