A Branching Time Model of CSP
Rob van Glabbeek







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


A Branching Time Model of CSP
    
Rob van Glabbeek 1,2

    December 30, 2023
=============================




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.




§ INTRODUCTION


The process algebra CSP—Communicating Sequential Processes—was presented in
Brookes, Hoare & Roscoe <cit.>.  It is sometimes called theoretical CSP,
to distinguish it from the earlier language CSP of Hoare <cit.>.
It is equipped with a denotational semantics, mapping each CSP process to an element of the
failures-divergences model <cit.>. 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 <cit.> 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 <cit.>, or the
stable revivals model of Roscoe <cit.>.

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



§ CSP


CSP <cit.> is parametrised with a set Σ of communications.
In this paper I use the subset of CSP given by the following grammar.

    P,Q ::=
    [          |÷| a→ P | P  Q | P  Q | P  Q |; P _A Q | P \ A | f(P) | P Q | P  Q
    ||μ.P ]

Here P and Q are CSP expressions,
a∈Σ, A⊆Σ and f:Σ→Σ.
Furthermore,  ranges over a set of process identifiers.
A CSP process is a CSP expression in which each occurrence of a process identifier 
lays within a recursion construct μ.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 <cit.>, this leaves out





  
  * successful termination () 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 , a→, , , A, f(_) and recursion
stem from <cit.>, and ÷ and _A from <cit.>, whereas ,
 and  were added to CSP by Roscoe <cit.>.



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



§ THE FAILURES-DIVERGENCES MODEL OF CSP


The process algebra CSP stems from Brookes, Hoare & Roscoe <cit.>.  It is also called
theoretical CSP, to distinguish it from the language CSP of Hoare <cit.>.  Its semantics
<cit.> associates to each CSP process a pair ⟨ F, D⟩ of failures
F ⊆Σ^* ×(Σ) 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 ∈_ 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 CSP 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 <cit.> 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 is obtained by means of fixed-point theory.
Alternatively, the failures and divergences of a CSP process can be extracted from its operational
semantics:


  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_1a_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 (P):={st| s  P}.

  A stable failure of a process P is a pair s,X∈Σ^*×(Σ) such
  that P s Q for some Q with I(Q)∩ (X∪{τ}) = ∅.
  The failure set of a process P is
  (p) = {s,X| s ∈(P) s,X P}.

  The semantics P_ of a CSP process P is the pair ⟨(P), (P) ⟩.

  Processes P and Q are failures-divergences equivalent, notation P ≡_FD Q,
  iff P_=Q_.
  Process P is a failures-divergences refinement of Q, notation P ⊒_FD Q,
  iff (P) ⊆(Q) ∧(P) ⊆(Q).

The operational semantics of CSP (then without the operators ,  and
) appears, for instance, in <cit.>, and was created after the denotational semantics.
In Olderog & Hoare <cit.> it is shown that the semantics P of a CSP process defined operationally
through FPoperational equals the denotational semantics given in <cit.>.
The argument extends smoothly to the new operators ,  and  <cit.>.
This can be seen as a justification of the operational semantics of CSP.

In Brookes, Hoare & Roscoe <cit.> 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.[2] So the semantics of ÷ or μ X.X is simply the
set of all failure pairs.  As observed in De Nicola <cit.>, this approach invalidates a
number of intuitively valid laws, such as P ÷ = ÷. The improved semantics of
<cit.> solves this problem.

In Hoare <cit.> 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 <cit.>, 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.



§ A COMPLETE AXIOMATISATION



































































In <cit.> 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 ≡_FD Q,
resp. P ⊑_FD Q.
If  is a collection of equational laws P=Q then ⊢ R=S denotes that the equation
R=S is derivable from the equations in  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  is a collection of inequational laws
P⊑ Q then ⊢ R⊑ S denotes that the inequation R⊑ S is
derivable from the inequations in  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). 

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  is a set of (in)equational laws that are valid for ∼ (resp. ≼) then any (in)equation
R=S with ⊢ R=S (resp. R⊑ S with ⊢ R⊑ S) is valid for ∼ (resp. ≼).

≡_FD is a congruence for all operators of CSP. This follows
immediately from the existence of the denotational failures-divergences semantics.
Likewise, ⊑_FD is a precongruence for all operators of CSP <cit.>.

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

In De Nicola <cit.> a sound and complete axiomatisation of ⊑_FD for recursion-free CSP,
and no process identifiers or variables, is presented.
It is quoted in axsFD.
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 ≡_FD is the kernel of ⊑_FD:
one has P ≡_FD Q iff P ⊑_FD Q ∧ Q ⊑_FD P.



In <cit.>, following <cit.>, two parallel composition operators  and  were considered,
instead of the parametrised operator _A. Here =_Σ and = _∅.
In axsFD 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 <cit.>. The associativity of parallel composition (Axiom ) is not included
in <cit.> and is not needed for completeness. I added it anyway, because of its
importance in equational reasoning.

The soundness of the axiomatisation of axsFD follows from ⊑_FD being a
precongruence, and the validity of the axioms—a fairly easy inspection using the denotational
characterisation of _. To obtain completeness,
write _i∈ IP_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 . This notation is justified by Axioms E2–4.
Furthermore,
  _j∈ JP_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  and .
Now a normal form is a defined as a CSP expression of the form ÷ or _j∈ JR_j,
with R_j=(_k∈ K_j(a_kj→ R_kj))
 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  derive P ÷ =÷. Together with
Axioms , , , H1–4, R1–5, T1–6 and U1–5
this allows any recursion-free CSP expression to be rewritten into normal form.
In <cit.> it is shown that for any two normal forms P and Q with P ⊑_FD Q,
Axioms , I1–4,  and  derive ⊢ P=Q.
Together, this yields the completeness of the axiomatisation of axsFD.



§ OTHER MODELS OF CSP


Several alternative models of CSP have been proposed in the literature, including the
readiness-divergences model of Olderog & Hoare <cit.> and the stable revivals model of
Roscoe <cit.>.
A hierarchy of such models is surveyed in Roscoe <cit.>.
Each of these models corresponds with a preorder (and associated semantic equivalence) on labelled
transition systems. In <cit.> I presented a survey of semantic equivalences and preorders on
labelled transition systems, ordered by inclusion in a lattice. Each model occurring in <cit.>
correspond exactly with with one of the equivalences of <cit.>, 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 <cit.> 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 <cit.> 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 <cit.>, which outside CSP stems
from Bergstra, Klop & Olderog <cit.>, plays the same role in the stable hierarchy.
Each of these hierarchies has a maximal (least discriminating) element, called FL^⇓
and FL in <cit.>. These correspond to the ready trace models RT^↓ and
RT of <cit.>.

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 axsFD, obtained by replacing axioms that are no longer valid by
weaker ones.

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

A second proposal could be based on weak bisimilarity <cit.>. This equivalence abstracts
from internal activity, and validates .


The default incarnation of weak bisimilarity is not finer than failures-divergences equivalence,
because it satisfies ÷=. Therefore, one would take a divergence-preserving variant of this
notion: the weak bisimulation with explicit divergence of Bergstra, Klop & Olderog <cit.>.
Yet, some crucial CSP laws are invalidated, such as  and . This destroys any hope of
a complete axiomatisation along the lines of axsFD.

My final choice is divergence-preserving coupled similarity <cit.>, based on coupled
similarity for divergence-free processes from Parrow & Sjödin <cit.>. This is the finest equivalence in
<cit.> that satisfies  and . In fact, it satisfies all of the axioms of axsFD,
except for the ones marked red: , , , , ,
, , , , ,  and .

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 coupled I present divergence-preserving coupled similarity.
In congruence I prove that it is a congruence for the operators of CSP,
and in complete I present a complete axiomatisation for recursion-free CSP processes without interrupts.




§ DIVERGENCE-PRESERVING COUPLED SIMILARITY



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


  * if P  Q and P α P' then there exists a Q' with Q α̂ Q' and P'  Q',

  * and if P  Q then there exists a Q' with Q  Q' and Q'  P.

It is divergence-preserving if P  Q and P ⇑ implies Q ⇑.
Write P ⊒_CS^Δ Q if there exists a divergence-preserving coupled simulation  with P  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 <cit.>).

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.


⊒_CS^Δ is reflexive and transitive, and thus a preorder.


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

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

To check that ;' ∪'; satisfies the first clause of coupled,
note that if Q ' R and Q α̂ Q', then,
by repeated application of the first clause of coupled, there is an R' with R α̂ R' and Q' ' R'.

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



If P  Q then P ⊑_CS^Δ Q.


I show that ∪{(Q,P)}, with  the identity relation, is a coupled simulation.
Namely if Q αQ' then surely P α Q'.
The second clause of coupled is satisfied because P  Q.
Furthermore, if Q ⇑ then certainly P ⇑, so the relation is divergence-preserving.



P ⊒_CS^Δ Q iff P Q ≡_CS^Δ Q.


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

That  is divergence-preserving is trivial, using that (P  Q)⇑ iff
P⇑∨ Q⇑.

Suppose P^*  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'  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 coupled, suppose P^*  Q.
The case P^*=P with P ⊒_CS^Δ Q is trivial.
Now let Q be Q^*  P^*. Then Q P^* and P^*  P^*.
Finally, let P^*=(P Q) with P ⊒_CS^Δ Q.
Then Q  Q and Q  (P Q).

“⇐”:
Suppose P  Q ⊒_CS^Δ Q.
Since P  Q τ P there exists a Q' with Q  Q' and P ⊒_CS^Δ Q'.
By tau Q' ⊒_CS^Δ Q and by preorder P ⊒_CS^Δ Q.




§ CONGRUENCE PROPERTIES



≡_CS^Δ is a congruence for action prefixing.


I have to show that P ≡_CS^Δ Q implies (a→ P) ≡_CS^Δ (a→ Q).

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

Checking the conditions of coupled for the case P  Q with P ⊑_CS^Δ Q is trivial.
So I examine the case (a→ P)  (a→ Q) with P ≡_CS^Δ Q.

Suppose (a→ P) α P'. Then α=a and P'=P.
Now (a→ Q)α Q and P  Q, so the first condition of coupled is
satisfied.

For the second condition, (a→ Q) (a→ Q), and, since Q ≡_CS^Δ P,
(a→ Q)  (a→ P).
Thus,  is a coupled simulation.

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

Since ⊒_CS^Δ (a→ STOP) but
⋢_CS^Δ (a→ STOP),and thus
b→⋣_CS^Δ b→((a→ 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 →) Θ_{a} P.
Consequently, ⊒_CS^Δ is not a precongruence for the throw operator.


  ≡_CS^Δ is a congruence for the throw operator.


  Let A⊆Σ. Let  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  Q_1 and (P_1 P_2)  (Q_1 Q_2).
  It suffices to show that  is a divergence-preserving coupled simulation.

  So let P_1 ⊒_CS^Δ Q_1, P_2 ≡_CS^Δ Q_2 and (P_1 P_2) α P'.
  Then P_1 α P_1' for some P_2', and
  either α∉ A and P'=P_1'  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 Q_2) α̂ (Q_1' Q_2)
  and (P'_1 P_2)  (Q'_1 Q_2).
  If α∈ A it follows that (Q_1 Q_2) α Q_2 and P_2  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 Q_2  Q_1'  Q_2 and (Q_1' Q_2)  (P_1 P_2).

  The same two conditions for the case P  Q because P ⊒_CS^Δ Q are trivial.
  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1  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.


  ⊒_CS^Δ is a precongruence for internal choice.


  Let  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  Q_i (i=1,2) and (P_1 P_2)  (Q_1 Q_2).
  It suffices to show that  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  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 tau P_1 ⊒_CS^Δ P_1 P_2 and by preorder
  Q_1' ⊒_CS^Δ P_1 P_2.


  The same two conditions for the case P  Q because P ⊒_CS^Δ Q are trivial.
  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1  P_2 ⇑ iff P_1 ⇑∨ P_2 ⇑.
  [2]



  ⊒_CS^Δ is a precongruence for external choice.


  Let  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  Q_i (i=1,2) and (P_1 P_2)  (Q_1 Q_2).
  It suffices to show that  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' 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)  (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')  (P_1 P_2).

  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1  P_2 ⇑ iff P_1 ⇑∨ P_2 ⇑.
  


  ⊒_CS^Δ is a precongruence for sliding choice.


  Let  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  Q_i (i=1,2) and (P_1 P_2)  (Q_1 Q_2).
  It suffices to show that  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' 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  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)  (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 tau P_2 ⊒_CS^Δ P_1 P_2 and by preorder
  Q_2' ⊒_CS^Δ P_1 P_2.

  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1  P_2 ⇑ iff P_1 ⇑∨ P_2 ⇑.
  


  ⊒_CS^Δ is a precongruence for parallel composition.


  Let A⊆Σ.
  Let  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)  (Q_1_A Q_2).
  It suffices to show that  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) (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)  (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')  (P_1_A P_2).

  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1 _A P_2 ⇑ iff P_1 ⇑∨ P_2 ⇑.
  


  ⊒_CS^Δ is a precongruence for concealment.


Let A⊆Σ. Let  be the smallest relation such that, for any P and Q,
P ⊑_CS^Δ Q implies (P A)  (Q  A).
It suffices to show that  is a divergence-preserving 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)  (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)  (P A).

To check that  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 coupled, there are Q_i for all i>0 such that
P_i  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) ⇑.



  ⊒_CS^Δ is a precongruence for renaming.


Let f:Σ→Σ.
Let  be the smallest relation such that, for any P and Q,
P ⊑_CS^Δ Q implies f(P)  f(Q).
It suffices to show that  is a divergence-preserving 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')  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')  f(P).

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



  ⊒_CS^Δ is a precongruence for the interrupt operator.


  Let  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  Q_2 and (P_1 P_2)  (Q_1 Q_2).
  It suffices to show that  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)  (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')  (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'  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')  (P_1 P_2).

  Thus  is a coupled simulation. That  is divergence-preserving follows because
  P_1  P_2 ⇑ iff P_1 ⇑∨ P_2 ⇑.




§ A COMPLETE AXIOMATISATION OF ≡_CS^Δ


A set of equational laws valid for ≡_CS^Δ is presented in axsCS.
It includes the laws from axsFD 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  and , 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  replaces the fallen axiom , and is due to <cit.>.
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 →|÷| E |÷ E; E → (a→ N) | (a→ N) E . ]

A CSP expression is in head normal form if  it is of the form
([÷]_i∈ I (a_i→ R_i))_j∈ JR_j,
with R_j=([÷]_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 ÷-summand on the left is present
whenever any of the R_j has a ÷-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 ÷-summand and a sliding choice,
I need four variants of the axiom ; so far I have not seen a way around this.
Likewise, there are 4× 4 variants of the axiom  from axsFD, of which 6 could be
suppressed by symmetry (P4–P13). There are also 3 axioms replacing  (P14–P16).








§ SOUNDNESS


Since divergence-preserving coupled similarity is a congruence for all CSP operators, to establish
the soundness of the axiomatisation of axsCS 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.

Two processes are strongly bisimilar <cit.> if they are related by a binary relation
 on processes such that, for all α∈Σ∪{τ},


  * if P  Q and P α P' then there exists a Q' with Q α Q' and P'  Q',

  * if P  Q and Q α Q' then there exists a P' with P α P' and P'  Q'.




  Axiom  is valid for ≡_CS^Δ.


  {(P P, P), (P, P P) | P   }∪
  is a divergence-preserving coupled simulation.



  Axiom  is valid even for strong bisimilarity.


  {(P Q, Q  P)| P,Q   }∪ is a strong bisimulation.



  Axiom  is valid for ≡_CS^Δ.


  The relation {( P  (Q  R) , (P  Q)  R ),
  ((P  Q)  R , P  (Q  R) ),[3]
  (Q  R , (P  Q)  R ),
  (P  Q, P  (Q  R)), (R,Q  R),
  (P,P Q)  |  P,Q,R   }∪
  is a divergence-preserving coupled simulation.
[3]



  Axioms E2–4 are valid for strong bisimilarity.


  The relation {( P  (Q  R) , (P  Q)  R )
  | P,Q,R   }∪ is a strong bisimulation.
  So is {(P Q, Q  P)| P,Q   }∪,
  as well as {(P, P)| P   }∪.



  Axiom  is valid for ≡_CS^Δ.


  {(P'  P, P),(P,P'  P) | P' ⊒_CS^Δ P}∪
  is a divergence-preserving coupled simulation. This follows from tau.



  Axiom  is valid for ≡_CS^Δ.


  {( P  (Q  R) , (P  Q)  R ),
  ((P  Q)  R , P  (Q  R) ) | P,Q,R   }∪
  is a divergence-preserving coupled simulation.
[2]



  Axiom  is valid for ≡_CS^Δ.


  {( (P  Q)  R , (P  Q)  R ),
  ( (P  Q')  R , (P  Q)  R ),
  ( Q  R , (P  Q)  R ),[3]
  ( R , Q  R )
  |  Q' ⊒_CS^Δ Q}∪
  is a divergence-preserving coupled simulation.



  Axiom  is valid for ≡_CS^Δ.


  {( (P  Q)  R , (P  Q)  R ),
  ( (P'  Q')  R , (P  Q)  R ),
  ( P  R , (P  Q)  R ),[3]
  ( Q  R , (P  Q)  R ),
  ( R , Q  R )
  | P' ⊒_CS^Δ P ∧ Q' ⊒_CS^Δ Q}∪
  is a divergence-preserving coupled simulation. Checking this involves tau.



  Axiom  is valid for ≡_CS^Δ.


  The relation {( P, P), (P,  P) | P   }∪
  is a divergence-preserving coupled simulation.



  Axiom  is valid for ≡_CS^Δ.


  {( (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}∪ is a divergence-preserving coupled simulation.



  Axiom  is valid for ≡_CS^Δ.


  {( (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'}∪ is a divergence-preserving coupled simulation.



  Axiom  is valid for ≡_CS^Δ.


  {( P'  (Q  R) , (P  Q)  (P  R) ),
     ( (P  Q)  (P  R) , P  (Q  R) ),( P'  Q , P'  (Q  R) )
   | P  P'}∪ is a divergence-preserving coupled simulation.



  Axiom  is valid for ≡_CS^Δ.


  {( (a→ P)  a→(P  Q) , a→(P  Q) ),
     ( a→(P  Q) , (a→ P)  a→(P  Q) )}[3]
  ∪ is a divergence-preserving coupled simulation.
[3]



  Axioms P0–1 and P4–10 are valid for strong bisimilarity.

  Axioms P11–16 are valid for ≡_CS^Δ.


   Straightforward.



  Axioms , , R0–5 and T0–6  are valid for strong bisimilarity.
  Axioms H5–8 are valid for ≡_CS^Δ.


   Straightforward.




  Axiom  is valid for ≡_CS^Δ.


  {( (P  Q) R' , (P R)  (Q R) ),
     ( (P R')  (Q R) , (P  Q) R ),( Q R' , (P  Q) R' ),
     ( Q R , (P R')  (Q R))
  | R  R'}∪ is a divergence-preserving coupled simulation.




  Axiom  is valid for ≡_CS^Δ.


  {( (P  Q) R' , (P R)  (Q R) ),
     ( (P R)  (Q R) , (P  Q) R ),( P R' , (P  Q) R' )
  | R  R'}∪ is a divergence-preserving coupled simulation.




  Axiom ' is valid for strong bisimilarity.


   {( P  Q , (_i∈ I (a_i → (P_i Q) ))  Q ),
      ( (_i∈ I (a_i → (P_i Q) ))  Q , P  Q )
   | P = _i ∈ I(a_i→ P_i) ∧ 
        Q = _j ∈ J(b_j→ Q_j)}∪ is a strong bisimulation.





§ COMPLETENESS


Let  be the axiomatisation of axsCS.

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



  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= or ÷. 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=(([÷]_i∈ I (a_i→ R_i))_j∈ JR_j)
  (([÷]_l∈ L (a_l→ R_l))_j∈ MR_j)
  with R_j=([÷]_k∈ K_j(a_kj→ R_kj)) for j∈ J∪ M.
  With Axiom  I may assume that J,M≠∅.
  Now Axiom  converts P to normal form.

  * Let P=P_1  P_2. By assumption P_1 and P_2 are in normal form.
  So P=(([÷]_i∈ I (a_i→ R_i))_j∈ JR_j)
  (([÷]_l∈ L (a_l→ R_l))_j∈ MR_j)
  with R_j=([÷]_k∈ K_j(a_kj→ R_kj)) for j∈ J∪ M.
  With  I may assume that J,M≠∅.
  Now Axioms  and  convert P to normal form.

  * Let P=P_1  P_2.
  Axioms S2–4 and  convert P to normal form.

  * Let P=P_1 _A P_2.
  Axioms  and P4–16, together with the induction hypothesis, convert P to normal form.

  * Let P=P A.
  Axioms  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  P_2.
  Axioms T0–6, together with the induction hypothesis, convert P to normal form.




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


Let P=([÷]_i∈ I (a_i→ R_i))_j∈ JR_j.
Then P has the form S  R. By Axioms S1–3
⊢ P = (S R)  R. By means of Axioms  and  the
subexpression S  R can be brought in the form
[÷]_l∈ L (a_l→ R_l).
The resulting term is saturated.


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.



Let P and Q be recursion-free CSP processes without interrupt operators. Then
P ≡_CS^Δ Q iff ⊢ P = Q.



“⇐” is an immediate consequence of the soundness of the axioms of ,
and the fact that ≡_CS^Δ is a congruence for all operators of CSP.

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

By nf I may assume, without loss of generality, that P and Q are in normal form.
By saturated I furthermore assume that P and Q are saturated.
Let P=([÷]_i∈ I (a_i→ R_i))_j∈ JR_j
and Q=([÷]_l∈ L (a_l→ R_l))_j∈ MR_jwith R_j=([÷]_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 CSpreorder.
Since (R_i  R_h) < (P), the induction hypothesis yields
⊢ R_i  R_h = R_h. Hence
Axiom  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 ÷-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 coupled 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 tau Q' ⊒_CS^Δ R_l and by preorder 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=([÷]_i∈ I (a_i→ R_f(i)))_j∈ MR_j
with R_i ≡_CS^Δ R_f(i) for all i ∈ I.
By induction ⊢ R_i = R_f(i) for all i∈ I.

So in the special case that I=M=∅ I obtain ⊢ 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 ⊢ P = R_j. This holds for all j ∈ J, so by Axiom 
⊢ Q=([÷]_i∈ I (a_i→ R_i)) P.
By Axiom  one obtains ⊢ 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
⊢ R_j =R_h(j) for all j ∈ J.

Let j ∈ J. Since P τ R_j, by coupled 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 coupled R_jR' 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 ⊢ R_j = R_m. Take h(j):=m.

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




§ 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 <cit.>.

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 <cit.>, but a multitude of them is needed due to the optional
presence of divergence-summands 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 <cit.>. Unfortunately, failures-divergences
equivalence fails to be a congruence for the left-merge, and the same problems exists for any other
models of CSP <cit.>. In <cit.> 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  from the axiomatisation of axsFD. 
Unfortunately, the axiom that splits a parallel composition between a left-, right- and communication
merge (Axiom CM1 in <cit.>), 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.




eptcsini

