A Branching Time Model of CSP

Rob van Glabbeek

arXiv:1702.07844·cs.LO·February 28, 2017

A Branching Time Model of CSP

Rob van Glabbeek

PDF

TL;DR

This paper introduces a new, more refined branching time model of CSP based on divergence-preserving coupled similarity, which is a congruence for CSP operators and aligns with strong bisimilarity on certain systems.

Contribution

It presents a novel semantic equivalence for CSP that is finer than previous models and provides a complete axiomatisation for recursion-free terms.

Findings

01

The new model is finer than all previous CSP models.

02

The equivalence is a congruence for CSP operators.

03

A complete axiomatisation is achieved for recursion-free terms.

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.

Tables4

Table 1. Table 2: A complete axiomatisation of ⊑ F D subscript square-image-of-or-equals 𝐹 𝐷 \sqsubseteq_{FD} for recursion-free CSP

\begin{matrix} ⊥ & 𝐝𝐢𝐯 & ⊑ & P \\ 𝐈𝟏 & P ⊓ P & = & P \\ 𝐈𝟐 & P ⊓ Q & = & Q ⊓ P \\ 𝐈𝟑 & P ⊓ (Q ⊓ R) & = & (P ⊓ Q) ⊓ R \\ 𝐈𝟒 & P ⊓ Q & ⊑ & P \\ 𝐄𝟏 & P □ P & = & P \\ 𝐄𝟐 & P □ Q & = & Q □ P \\ 𝐄𝟑 & P □ (Q □ R) & = & (P □ Q) □ R \\ 𝐄𝟒 & P □ 𝑆𝑇𝑂𝑃 & = & P \\ 𝐄𝟓 & P □ 𝐝𝐢𝐯 & = & 𝐝𝐢𝐯 \\ 𝐃𝟏 & P □ (Q ⊓ R) & = & (P □ Q) ⊓ (P □ R) \\ 𝐃𝟐 & P ⊓ (Q □ R) & = & (P ⊓ Q) □ (P ⊓ R) \\ 𝐃𝟑 & (a \to P) □ (a \to Q) & = & a \to (P ⊓ Q) \\ 𝐃𝟒 & (a \to P) ⊓ (a \to Q) & = & a \to (P ⊓ Q) \\ 𝐒𝐂 & P ▷ Q & = & (P □ Q) ⊓ Q \\ 𝐏𝟎 & {P ∥}_{A} ​ ({Q ∥}_{A} ​ R) & = & {({P ∥}_{A} ​ Q) ∥}_{A} ​ R \\ 𝐏𝟏 & {P ∥}_{A} ​ Q & = & {Q ∥}_{A} ​ P \\ 𝐏𝟐 & {(P ⊓ Q) ∥}_{A} ​ R & = & ({P ∥}_{A} ​ R) ⊓ ({Q ∥}_{A} ​ R) \\ 𝐏𝟑 & {P ∥}_{A} ​ 𝐝𝐢𝐯 & = & 𝐝𝐢𝐯 \\ 𝐏𝟒 & If ​ P = □_{i \in I} (a_{i} \to P_{i}) ​ and ​ Q = □_{j \in J} (b_{j} \to Q_{j}) ​ then : \\ P ∥ Q & = & □_{a_{i} \notin A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q)) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ({P ∥}_{A} ​ Q_{j})) \\ 𝐇𝟏 & (P ⊓ Q) \ A & = & (P \ A) ⊓ (Q \ A) \\ 𝐇𝟐 & (P □ a \to Q) \ A & = & ((P □ Q) \ A) ⊓ (Q \ A) \\ 𝐇𝟑 & (□_{i \in I} (b_{i} \to P_{i})) \ A & = & (□_{i \in I} (b_{i} \to (P_{i} \ A))) if ​ \forall i \in I . b_{i} \notin A \\ 𝐇𝟒 & 𝐝𝐢𝐯 \ A & = & 𝐝𝐢𝐯 \\ 𝐑𝟏 & f ​ (P ⊓ Q) & = & f ​ (P) ⊓ f ​ (Q) \\ 𝐑𝟐 & f ​ (P □ Q) & = & f ​ (P) □ f ​ (Q) \\ 𝐑𝟑 & f ​ (a \to P) & = & f ​ (a) \to f ​ (P) \\ 𝐑𝟒 & f ​ (𝑆𝑇𝑂𝑃) & = & 𝑆𝑇𝑂𝑃 \\ 𝐑𝟓 & f ​ (𝐝𝐢𝐯) & = & 𝐝𝐢𝐯 \\ 𝐓𝟏 & (P ⊓ Q) Θ_{A} R & = & (P Θ_{A} R) ⊓ (Q Θ_{A} R) \\ 𝐓𝟐 & (P □ Q) Θ_{A} R & = & (P Θ_{A} R) □ (Q Θ_{A} R) \\ 𝐓𝟑 & (a \to P) Θ_{A} Q & = & a \to (P Θ_{A} Q) ​ if a \notin A \\ 𝐓𝟒 & (a \to P) Θ_{A} Q & = & a \to Q ​ if a \in A \\ 𝐓𝟓 & 𝑆𝑇𝑂𝑃 Θ_{A} Q & = & 𝑆𝑇𝑂𝑃 \\ 𝐓𝟔 & 𝐝𝐢𝐯 Θ_{A} Q & = & 𝐝𝐢𝐯 \\ 𝐔𝟏 & (P ⊓ Q) △ R & = & (P △ R) ⊓ (Q △ R) \\ 𝐔𝟐 & (P □ Q) △ R & = & (P △ R) □ (Q △ R) \\ 𝐔𝟑 & (a \to P) △ Q & = & (a \to (P △ Q)) □ Q \\ 𝐔𝟒 & 𝑆𝑇𝑂𝑃 △ P & = & P \\ 𝐔𝟓 & 𝐝𝐢𝐯 △ P & = & 𝐝𝐢𝐯 \end{matrix}

Table 2. Table 3: A complete axiomatisation of ≡ C S Δ superscript subscript 𝐶 𝑆 Δ \equiv_{CS}^{\Delta} for recursion-free CSP without interrupt

\begin{matrix} 𝐈𝟏 & P ⊓ P & = & P \\ 𝐈𝟐 & P ⊓ Q & = & Q ⊓ P \\ 𝐈𝟑 & P ⊓ (Q ⊓ R) & = & (P ⊓ Q) ⊓ R \\ 𝐄𝟐 & P □ Q & = & Q □ P \\ 𝐄𝟑 & P □ (Q □ R) & = & (P □ Q) □ R \\ 𝐄𝟒 & P □ 𝑆𝑇𝑂𝑃 & = & P \\ 𝐒𝟏 & P ▷ P & = & P \\ 𝐒𝟐 & P ▷ (Q ▷ R) & = & (P ▷ Q) ▷ R \\ 𝐒𝟑 & (P ▷ Q) ▷ R & = & (P □ Q) ▷ R \\ 𝐒𝟒 & (P ⊓ Q) ▷ R & = & (P □ Q) ▷ R \\ 𝐒𝟓 & 𝑆𝑇𝑂𝑃 ▷ P & = & P \\ 𝐒𝟔 & (P ▷ Q) ⊓ (R ▷ S) & = & (P □ R) ▷ (Q ⊓ S) \\ 𝐒𝟕 & (P ▷ Q) □ (R ▷ S) & = & (P □ R) ▷ (Q □ S) \\ 𝐃𝟏 & P □ (Q ⊓ R) & = & (P □ Q) ⊓ (P □ R) \\ 𝐏𝐫𝐮𝐧𝐞 & (a \to P) □ a \to (P ⊓ Q) & = & a \to (P ⊓ Q) \\ 𝐏𝟎 & {P ∥}_{A} ​ ({Q ∥}_{A} ​ R) & = & {({P ∥}_{A} ​ Q) ∥}_{A} ​ R \\ 𝐏𝟏 & {P ∥}_{A} ​ Q & = & {Q ∥}_{A} ​ P \\ P4–P13 & more axioms for parallel composition follow on the next page \\ 𝐇𝟏 & (P ⊓ Q) \ A & = & (P \ A) ⊓ (Q \ A) \\ 𝐇𝟓 & (□_{i \in I} (a_{i} \to P_{i})) \ A & = & (□_{a_{i} \notin A} (a_{i} \to (P_{i} \ A))) \\ ▷ ⊓_{a_{i} \in A} (P_{i} \ A) \\ 𝐇𝟔 & (𝐝𝐢𝐯 □ □_{i \in I} (a_{i} \to P_{i})) \ A & = & (𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} \ A))) \\ ▷ ⊓_{a_{i} \in A} (P_{i} \ A) \\ 𝐇𝟕 & ((□_{i \in I} (a_{i} \to P_{i})) ▷ P^{'}) \ A & = & (□_{a_{i} \notin A} (a_{i} \to (P_{i} \ A))) \\ ▷ (P^{'} \ A ⊓ ⊓_{a_{i} \in A} (P_{i} \ A)) \\ 𝐇𝟖 & ((𝐝𝐢𝐯 □ □_{i \in I} (a_{i} \to P_{i})) ▷ P^{'}) \ A & = & (𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} \ A))) \\ ▷ (P^{'} \ A ⊓ ⊓_{a_{i} \in A} (P_{i} \ A)) \\ 𝐑𝟎 & f ​ (P ▷ Q) & = & f ​ (P) ▷ f ​ (Q) \\ 𝐑𝟏 & f ​ (P ⊓ Q) & = & f ​ (P) ⊓ f ​ (Q) \\ 𝐑𝟐 & f ​ (P □ Q) & = & f ​ (P) □ f ​ (Q) \\ 𝐑𝟑 & f ​ (a \to P) & = & f ​ (a) \to f ​ (P) \\ 𝐑𝟒 & f ​ (𝑆𝑇𝑂𝑃) & = & 𝑆𝑇𝑂𝑃 \\ 𝐑𝟓 & f ​ (𝐝𝐢𝐯) & = & 𝐝𝐢𝐯 \\ 𝐓𝟎 & (P ▷ Q) Θ_{A} R & = & (P Θ_{A} R) ▷ (Q Θ_{A} R) \\ 𝐓𝟏 & (P ⊓ Q) Θ_{A} R & = & (P Θ_{A} R) ⊓ (Q Θ_{A} R) \\ 𝐓𝟐 & (P □ Q) Θ_{A} R & = & (P Θ_{A} R) □ (Q Θ_{A} R) \\ 𝐓𝟑 & (a \to P) Θ_{A} Q & = & a \to (P Θ_{A} Q) ​ if a \notin A \\ 𝐓𝟒 & (a \to P) Θ_{A} Q & = & a \to Q ​ if a \in A \\ 𝐓𝟓 & 𝑆𝑇𝑂𝑃 Θ_{A} Q & = & 𝑆𝑇𝑂𝑃 \\ 𝐓𝟔 & 𝐝𝐢𝐯 Θ_{A} Q & = & 𝐝𝐢𝐯 \end{matrix}

\begin{matrix} (𝐏𝟒) & {P ∥}_{A} ​ Q & = & □_{a_{i} \notin A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q)) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ({P ∥}_{A} ​ Q_{j})) \\ (𝐏𝟓) & {(𝐝𝐢𝐯 □ P) ∥}_{A} ​ Q & = & 𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q)) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ({(𝐝𝐢𝐯 □ P) ∥}_{A} ​ Q_{j})) \\ (𝐏𝟔) & {(𝐝𝐢𝐯 □ P) ∥}_{A} ​ (𝐝𝐢𝐯 □ Q) & = & 𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to ({P_{i} ∥}_{A} ​ (𝐝𝐢𝐯 □ Q))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ({(𝐝𝐢𝐯 □ P) ∥}_{A} ​ Q_{j})) \\ (𝐏𝟕) & {(P ▷ P^{'}) ∥}_{A} ​ Q & = & (□_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} Q)) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ((P ▷ P^{'}) ∥_{A} Q_{j}))) ▷ P^{'} ∥_{A} Q \\ (𝐏𝟖) & {((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥}_{A} ​ Q & = & (𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} Q)) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to (((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥_{A} Q_{j}))) \\ {▷ P^{'} ∥}_{A} ​ Q \\ (𝐏𝟗) & {(P ▷ P^{'}) ∥}_{A} ​ (𝐝𝐢𝐯 □ Q) & = & ((𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} (𝐝𝐢𝐯 □ Q))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ((P ▷ P^{'}) ∥_{A} Q_{j}))) \\ {▷ P^{'} ∥}_{A} ​ (𝐝𝐢𝐯 □ Q) \\ (𝐏𝟏𝟎) & {((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥}_{A} ​ (𝐝𝐢𝐯 □ Q) & = & (𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} (𝐝𝐢𝐯 □ Q))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to (((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥_{A} Q_{j}))) \\ {▷ P^{'} ∥}_{A} ​ (𝐝𝐢𝐯 □ Q) \\ (𝐏𝟏𝟏) & {(P ▷ P^{'}) ∥}_{A} ​ (Q ▷ Q^{'}) & = & (□_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} (Q ▷ Q^{'}))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to ((P ▷ P^{'}) ∥_{A} Q_{j}))) \\ ▷ ({{P^{'} ∥}_{A} ​ (Q ▷ Q^{'}) ⊓ (P ▷ P^{'}) ∥}_{A} ​ Q^{'}) \\ (𝐏𝟏𝟐) & {((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥}_{A} ​ (Q ▷ Q^{'}) & = & (𝐝𝐢𝐯 □ □_{a_{i} \notin A} (a_{i} \to (P_{i} ∥_{A} (Q ▷ Q^{'}))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to (((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥_{A} Q_{j}))) \\ ▷ ({{P^{'} ∥}_{A} ​ (Q ▷ Q^{'}) ⊓ ((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥}_{A} ​ Q^{'}) \end{matrix}

\begin{matrix} (𝐏𝟏𝟑) & ((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥_{A} ((𝐝𝐢𝐯 □ Q) ▷ Q^{'}) = (𝐝𝐢𝐯 □ \\ □_{a_{i} \notin A} (a_{i} \to ({P_{i} ∥}_{A} ​ ((𝐝𝐢𝐯 □ Q) ▷ Q^{'}))) □ \\ □_{a_{j} = b_{j} \in A} (a_{i} \to ({P_{i} ∥}_{A} ​ Q_{j})) □ \\ □_{b_{j} \notin A} (b_{j} \to (((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥_{A} Q_{j}))) \\ ▷ ({{P^{'} ∥}_{A} ​ ((𝐝𝐢𝐯 □ Q) ▷ Q^{'}) ⊓ ((𝐝𝐢𝐯 □ P) ▷ P^{'}) ∥}_{A} ​ Q^{'}) \end{matrix}

Equations16

P,Q::=\begin{array}[t]{@{}l@{}}\mathord{{\it STOP}}\mid\mathord{{\bf div}}\mid a\rightarrow P\mid P\mathbin{\mathchar 629\relax}Q\mid P\mathbin{{\Box}}Q\mid P\mathbin{\mathchar 302\relax}Q\mid\\ P\|_{A}Q\mid P\backslash A\mid f(P)\mid P\mathbin{\mathchar 564\relax}Q\mid P\mathbin{\Theta\!_{A}}Q\mid p\mid\mu p.P\end{array}

P,Q::=\begin{array}[t]{@{}l@{}}\mathord{{\it STOP}}\mid\mathord{{\bf div}}\mid a\rightarrow P\mid P\mathbin{\mathchar 629\relax}Q\mid P\mathbin{{\Box}}Q\mid P\mathbin{\mathchar 302\relax}Q\mid\\ P\|_{A}Q\mid P\backslash A\mid f(P)\mid P\mathbin{\mathchar 564\relax}Q\mid P\mathbin{\Theta\!_{A}}Q\mid p\mid\mu p.P\end{array}

(ε, \emptyset) \in F

(ε, \emptyset) \in F

(s t, \emptyset) \in F \Rightarrow (s, \emptyset) \in F

(s, X) \in F \land Y \subseteq X \Rightarrow (s, Y) \in F

(s, X) \in F \land (\forall c \in Y . (sc, \emptyset) \in / F \Rightarrow (s, X \cup Y) \in F

(\forall Y \in \Pow_{fin} (X) . (s, Y) \in F \Rightarrow (s, X) \in F

s \in D \Rightarrow s t \in D

s \in D \Rightarrow (s t, X) .

\begin{array}[]{l}N\rightarrow D\mid D\mathbin{\mathchar 302\relax}I\\ I\rightarrow D\mid I\mathbin{\mathchar 629\relax}I\\ D\rightarrow\mathord{{\it STOP}}\mid\mathord{{\bf div}}\mid E\mid\mathord{{\bf div}}\mathbin{{\Box}}E\\ E\rightarrow(a\rightarrow N)\mid(a\rightarrow N)\mathbin{{\Box}}E\;.\vspace{-2ex}\end{array}

\begin{array}[]{l}N\rightarrow D\mid D\mathbin{\mathchar 302\relax}I\\ I\rightarrow D\mid I\mathbin{\mathchar 629\relax}I\\ D\rightarrow\mathord{{\it STOP}}\mid\mathord{{\bf div}}\mid E\mid\mathord{{\bf div}}\mathbin{{\Box}}E\\ E\rightarrow(a\rightarrow N)\mid(a\rightarrow N)\mathbin{{\Box}}E\;.\vspace{-2ex}\end{array}

\begin{array}[]{@{}l@{\quad}rcl@{}}\mathbf{(P14)}&P\|_{A}Q&=&\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{{\Box}}$}}}\nolimits}\nolimits_{a_{i}\notin A}(a_{i}\rightarrow(P_{i}\|_{A}Q))\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}(P\|_{A}Q_{j}))\\ \mathbf{(P15)}&(\mathord{{\bf div}}\mathbin{{\Box}}P)\|_{A}Q&=&\big{(}\mathord{{\bf div}}\mathbin{{\Box}}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{{\Box}}$}}}\nolimits}\nolimits_{a_{i}\notin A}(a_{i}\rightarrow(P_{i}\|_{A}Q))\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}((\mathord{{\bf div}}\mathbin{{\Box}}P)\|_{A}Q_{j}))\\ \end{array}

\begin{array}[]{@{}l@{\quad}rcl@{}}\mathbf{(P14)}&P\|_{A}Q&=&\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{{\Box}}$}}}\nolimits}\nolimits_{a_{i}\notin A}(a_{i}\rightarrow(P_{i}\|_{A}Q))\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}(P\|_{A}Q_{j}))\\ \mathbf{(P15)}&(\mathord{{\bf div}}\mathbin{{\Box}}P)\|_{A}Q&=&\big{(}\mathord{{\bf div}}\mathbin{{\Box}}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{{\Box}}$}}}\nolimits}\nolimits_{a_{i}\notin A}(a_{i}\rightarrow(P_{i}\|_{A}Q))\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}((\mathord{{\bf div}}\mathbin{{\Box}}P)\|_{A}Q_{j}))\\ \end{array}

\begin{array}[]{@{}l@{\qquad\qquad\qquad\qquad\quad}rcl@{\qquad\qquad\qquad}}\mathbf{(P16)}&P\|_{A}Q&=&\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{a_{i}\notin A}(P_{i}\|_{A}Q)\mathbin{\mathchar 629\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}(P\|_{A}Q_{j}))\\ \end{array}

\begin{array}[]{@{}l@{\qquad\qquad\qquad\qquad\quad}rcl@{\qquad\qquad\qquad}}\mathbf{(P16)}&P\|_{A}Q&=&\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{a_{i}\notin A}(P_{i}\|_{A}Q)\mathbin{\mathchar 629\relax}\mathop{\mathop{\vbox{\hbox{\Large$\mathstrut{\mathchar 629\relax}$}}}\nolimits}\nolimits_{j\in J}(P\|_{A}Q_{j}))\\ \end{array}

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Full text

11institutetext: Data61, CSIRO, Sydney, Australia 22institutetext: Comput. Sci. and Engineering, University of New South Wales, Sydney, Australia

A Branching Time Model of CSP

Rob van Glabbeek 1122

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 [5]. It is sometimes called theoretical CSP, to distinguish it from the earlier language CSP of Hoare [11]. It is equipped with a denotational semantics, mapping each CSP process to an element of the failures-divergences model [5, 6]. 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 [14] 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 [3], or the stable revivals model of Roscoe [17].

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 [15]. 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 [5, 6, 12] is parametrised with a set $\Sigma$ of communications. In this paper I use the subset of CSP given by the following grammar.

[TABLE]

Here $P$ and $Q$ are CSP expressions, $a\in\Sigma$ , $A\subseteq\Sigma$ and $f:\Sigma\rightarrow\Sigma$ . 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 $\mu 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 [16, 18], this leaves out

•

successful termination ( $\mathord{{\it 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 $\mathord{{\it STOP}}$ , $a\rightarrow$ , $\mathbin{\mathchar 629\relax}$ , $\mathbin{{\Box}}$ , $\backslash A$ , $f(\leavevmode\vbox{\hrule width=5.0pt})$ and recursion stem from [5], and $\mathord{{\bf div}}$ and $\|_{A}$ from [14], whereas $\mathbin{\mathchar 302\relax}$ , $\mathbin{\mathchar 564\relax}$ and $\mathbin{\Theta\!_{A}}$ were added to CSP by Roscoe [16, 18].

The operational semantics of of CSP is given by the binary transition relations $\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}$ between CSP processes. The transitions $P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q$ are derived by the rules in Table 1. Here $a$ , $b$ range over $\Sigma$ and $\alpha$ , $\beta$ over $\Sigma\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\{\tau\}$ , and relabelling operators $f$ are extended to $\Sigma\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\{\tau\}$ by $f(\tau)=\tau$ . The transition labels $\alpha$ are called actions, and $\tau$ is the internal action.

3 The Failures-Divergences Model of CSP

The process algebra CSP stems from Brookes, Hoare & Roscoe [5]. It is also called theoretical CSP, to distinguish it from the language CSP of Hoare [11]. Its semantics [6] associates to each CSP process a pair $\langle F,D\rangle$ of failures $F\subseteq\Sigma^{*}\times\Pow(\Sigma)$ and divergences $D\subseteq\Sigma^{*}$ , subject to the conditions:

[TABLE]

Here $\varepsilon\in\Sigma^{*}$ is the empty sequence of communications and $st$ denotes the concatenation of sequences $s$ and $t\in\Sigma^{*}$ . If $\langle F,D\rangle$ is the semantics of a process $P$ , $(s,\emptyset)\in F$ , with $s\not\in 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)\in F$ , with $s\notin 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\in\Sigma$ is thought to occur in cooperation between a process and its environment. Thus $(s,X)\in 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\in 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\notin D$ , the set ${\it next}(s)$ of actions $c$ such that $sc$ is also a trace of $P$ is finite. By (N3–4), $(s,X)\in F$ iff $(s,X\cap{\it next}(s))\in F$ . It follows that if $(s,X)\notin F$ , then there is a finite subset $Y$ of $X$ , namely $X\cap{\it next}(s)$ , such that $(s,Y)\notin F$ . This explains Condition (N5).

In Brookes & Roscoe [6] 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},\dots,P_{n})$ out of the failures and divergences of the argument processes $P_{1},\dots,P_{n}$ . The meaning of a recursively defined CSP process $\mu 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\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ if there are processes $P_{0},\dots,P_{n}$ , with $n\geq 0$ , such that $P=P_{0}$ , $P_{i}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{i+1}$ for all $0\leq i<n$ , and $P_{n}=Q$ .

Write $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q$ if there are processes $P^{\prime},Q^{\prime}$ with $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q^{\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ .

Write $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q$ if either $\alpha\in\Sigma$ and $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q$ , or $\alpha=\tau$ and $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ .

Write $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ s $}$ \hskip 2.5pt}\hfil}} $}}}Q$ , for $s=a_{1}a_{2}\dots a_{n}\in\Sigma^{*}$ with $n\geq 0$ , if there are processes $P_{0},\dots,P_{n}$ such that $P=P_{0}$ , $P_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ a_{i} $}$ \hskip 2.5pt}\hfil}} $}}}P_{i+1}$ for all $0\leq i<n$ , and $P_{n}=Q$ .

Let $I(P)=\{\alpha\in\Sigma\cup\{\tau\}\mid\mathop{\mathstrut{\exists}}\nolimits Q.\,P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q\}$ .

Write $P{\Uparrow}$ if there are processes $P_{i}$ for all $i\mathbin{\geq}0$ with $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ s $}$ \hskip 2.5pt}\hfil}} $}}}P_{0}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{1}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\dots$ .

$s\in\Sigma^{*}$ is a divergence trace of a process $P$ if there is a $Q$ with $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ s $}$ \hskip 2.5pt}\hfil}} $}}}Q{\Uparrow}$ .

The divergence set of $P$ is $\D(P):=\{st\mid s\mbox{\penalty 10000\ is a divergence trace of\penalty 10000\ }P\}$ .

A stable failure of a process $P$ is a pair $(s,X)\in\Sigma^{*}\times\Pow(\Sigma)$ such that $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ s $}$ \hskip 2.5pt}\hfil}} $}}}Q$ for some $Q$ with $I(Q)\cap(X\cup\{\tau\})=\emptyset$ . The failure set of a process $P$ is $\F(p)=\{(s,X)\mid s\in\D(P)\mbox{\penalty 10000\ or\penalty 10000\ }(s,X)\mbox{\penalty 10000\ is a stable failure of\penalty 10000\ }P\}$ .

The semantics $\mbox{$ [[ $}\,P\,\mbox{$ ]] $}_{\F\D}$ of a CSP process $P$ is the pair $\langle\F(P),\D(P)\rangle$ .

Processes $P$ and $Q$ are failures-divergences equivalent, notation $P\equiv_{FD}Q$ , iff $\mbox{$ [[ $}\,P\,\mbox{$ ]] $}_{\F\D}=\mbox{$ [[ $}\,Q\,\mbox{$ ]] $}_{\F\D}$ . Process $P$ is a failures-divergences refinement of $Q$ , notation $P\sqsupseteq_{FD}Q$ , iff $\F(P)\subseteq\F(Q)\wedge\D(P)\subseteq\D(Q)$ .

The operational semantics of Section 2 (then without the operators $\mathbin{\mathchar 302\relax}$ , $\mathbin{\mathchar 564\relax}$ and $\mathbin{\Theta\!_{A}}$ ) appears, for instance, in [14], and was created after the denotational semantics. In Olderog & Hoare [14] it is shown that the semantics $\mbox{$ [[ $}\,P\,\mbox{$ ]] $}$ of a CSP process defined operationally through Def. 1 equals the denotational semantics given in [6]. The argument extends smoothly to the new operators $\mathbin{\mathchar 302\relax}$ , $\mathbin{\mathchar 564\relax}$ and $\mathbin{\Theta\!_{A}}$ [18]. This can be seen as a justification of the operational semantics of Section 2.

In Brookes, Hoare & Roscoe [5] 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 $\mathord{{\bf div}}$ or $\mu X.X$ is simply the set of all failure pairs. As observed in De Nicola [7], this approach invalidates a number of intuitively valid laws, such as $P\mathbin{{\Box}}\mathord{{\bf div}}=\mathord{{\bf div}}$ . The improved semantics of [6] solves this problem.

In Hoare [12] 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\subseteq\Sigma$ , 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 $\mathrel{\mathchar 618\relax\mathchar 618\relax\mathchar 618\relax}$ , corresponding to $\|_{\emptyset}$ . This approach is equally expressive as the one of [6], 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 [5, 6, 7, 12, 16, 18] many algebraic laws $P=Q$ , resp. $P\sqsubseteq Q$ , are stated that are valid w.r.t. the failures-divergences semantics of CSP, meaning that $P\equiv_{FD}Q$ , resp. $P\sqsubseteq_{FD}Q$ . If ${\it Th}$ is a collection of equational laws $P=Q$ then ${\it Th}\vdash R=S$ denotes that the equation $R=S$ is derivable from the equations in ${\it 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,\dots,n$ then $Op(P_{1},\dots,P_{n})=Op(Q_{1},\dots,Q_{n})$ . Likewise, if ${\it Th}$ is a collection of inequational laws $P\sqsubseteq Q$ then ${\it Th}\vdash R\sqsubseteq S$ denotes that the inequation $R\sqsubseteq S$ is derivable from the inequations in ${\it Th}$ using reflexivity, transitivity and the rule saying that if $Op$ is an $n$ -ary CSP operator and $P_{i}\sqsubseteq Q_{i}$ for $i=1,\dots,n$ then $Op(P_{1},\dots,P_{n})\sqsubseteq Op(Q_{1},\dots,Q_{n})$ .

Definition 2

An equivalence $\sim$ on process expressions is called a congruence for an $n$ -ary operator $Op$ if $P_{i}\sim Q_{i}$ for $i=1,\dots,n$ implies $Op(P_{1},\dots,P_{n})\sim Op(Q_{1},\dots,Q_{n})$ . A preorder $\preceq$ is a precongruence for $Op$ , or $Op$ is monotone for $\preceq$ , if $P_{i}\preceq Q_{i}$ for $i=1,\dots,n$ implies $Op(P_{1},\dots,P_{n})\preceq Op(Q_{1},\dots,Q_{n})$ .

If $\sim$ is a congruence for all operators of CSP (resp. $\preceq$ is a precongruence for all operators of CSP) and ${\it Th}$ is a set of (in)equational laws that are valid for $\sim$ (resp. $\preceq$ ) then any (in)equation $R=S$ with ${\it Th}\vdash R=S$ (resp. $R\sqsubseteq S$ with ${\it Th}\vdash R\sqsubseteq S$ ) is valid for $\sim$ (resp. $\preceq$ ).

$\equiv_{FD}$ is a congruence for all operators of CSP. This follows immediately from the existence of the denotational failures-divergences semantics. Likewise, $\sqsubseteq_{FD}$ is a precongruence for all operators of CSP [5, 6, 7, 12, 14, 16, 18].

Definition 3

A set ${\it Th}$ of (in)equational laws—an axiomatisation—is sound and complete for an equivalence $\sim$ (or a preorder $\preceq$ ) if ${\it Th}\vdash R=S$ iff $R\sim S$ (resp. ${\it Th}\vdash R\sqsubseteq S$ iff $R\preceq S$ ). Here “ $\Rightarrow$ ” is soundness and “ $\Leftarrow$ ” completeness.

In De Nicola [7] a sound and complete axiomatisation of $\sqsubseteq_{FD}$ 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\sqsubseteq Q$ and $Q\sqsubseteq P$ . This mixed use is justified because $\equiv_{FD}$ is the kernel of $\sqsubseteq_{FD}$ : one has $P\equiv_{FD}Q$ iff $P\sqsubseteq_{FD}Q\wedge Q\sqsubseteq_{FD}P$ .

In [7], following [5, 6], two parallel composition operators $\|$ and $\mathrel{\mathchar 618\relax\mathchar 618\relax\mathchar 618\relax}$ were considered, instead of the parametrised operator $\|_{A}$ . Here $\|=\|_{\Sigma}$ and $\mathrel{\mathchar 618\relax\mathchar 618\relax\mathchar 618\relax}=\|_{\emptyset}$ . 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 [7]. The associativity of parallel composition (Axiom $\mathbf{P0}$ ) is not included in [7] 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 $\sqsubseteq_{FD}$ being a precongruence, and the validity of the axioms—a fairly easy inspection using the denotational characterisation of $[[$

$]]$ . To obtain completeness, write $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in I}P_{i}$ , with $I\mathbin{=}\{i_{1},\ldots,i_{n}\}$ any finite index set, for $P_{i_{1}}\mathbin{\mathbin{{\Box}}}P_{i_{2}}\mathbin{\mathbin{{\Box}}}\dots\mathbin{\mathbin{{\Box}}}P_{i_{n}}$ , where $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in\emptyset}P_{i}$ represents $\mathord{{\it STOP}}$ . This notation is justified by Axioms E2–4. Furthermore, $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{j\in J}P_{j}$ , with $J\mathbin{=}\{j_{1},..,j_{m}\}$ any finite, nonempty index set, denotes $P_{j_{1}}\mathbin{\mathbin{\mathchar 629\relax}}P_{j_{2}}\mathbin{\mathbin{\mathchar 629\relax}}\dots\mathbin{\mathbin{\mathchar 629\relax}}P_{j_{m}}$ . This notation is justified by Axioms $\mathbf{I2}$ and $\mathbf{I3}$ . Now a normal form is a defined as a CSP expression of the form $\mathord{{\bf div}}$ or $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{j\in J}R_{j}$ , with $R_{j}=\big{(}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{k\in K_{j}}(a_{kj}\rightarrow R_{kj})\big{)}$ for $j\in J$ , where the subexpressions $R_{kj}$ are again in normal form. Here $J$ and the $K_{j}$ are finite index sets, $J$ nonempty.

Axioms $\mathbf{\bot}$ and $\mathbf{I4}$ derive $P\mathbin{\mathchar 629\relax}\mathord{{\bf div}}=\mathord{{\bf div}}$ . Together with Axioms $\mathbf{D1}$ , $\mathbf{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 [7] it is shown that for any two normal forms $P$ and $Q$ with $P\sqsubseteq_{FD}Q$ , Axioms $\mathbf{\bot}$ , I1–4, E1–5 and D1–4 derive $\vdash 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 [14] and the stable revivals model of Roscoe [17]. A hierarchy of such models is surveyed in Roscoe [18]. Each of these models corresponds with a preorder (and associated semantic equivalence) on labelled transition systems. In [8] I presented a survey of semantic equivalences and preorders on labelled transition systems, ordered by inclusion in a lattice. Each model occurring in [18] correspond exactly with with one of the equivalences of [8], 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 [8] 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 [18] 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 [16], which outside CSP stems from Bergstra, Klop & Olderog [3], plays the same role in the stable hierarchy. Each of these hierarchies has a maximal (least discriminating) element, called $\cal{FL}^{\Downarrow}$ and $\cal{FL}$ in [18]. These correspond to the ready trace models ${\it RT}^{\downarrow}$ and ${\it RT}$ of [8].

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 [13]. Strong bisimilarity is a congruence for all CSP operators, because their operational semantics fits the tyft/tyxt format of [10]. However, this is an unsuitable equivalence for CSP, because it fails to abstract from internal actions. Even the axiom $\mathbf{I1}$ would not be valid, as the two sides differ by an internal action.

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

My final choice is divergence-preserving coupled similarity [8], based on coupled similarity for divergence-free processes from Parrow & Sjödin [15]. This is the finest equivalence in [8] that satisfies $\mathbf{I3}$ and $\mathbf{D1}$ . In fact, it satisfies all of the axioms of Table 2, except for the ones marked red: $\mathbf{\bot}$ , $\mathbf{I4}$ , $\mathbf{E1}$ , $\mathbf{E5}$ , D2–4, $\mathbf{SC}$ , $\mathbf{P2}$ , $\mathbf{P3}$ , $\mathbf{H2}$ , $\mathbf{U2}$ , $\mathbf{U3}$ and $\mathbf{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 $\alpha\in\Sigma\cup\{\tau\}$ ,

•

if $P\R Q$ and $P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ then there exists a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P^{\prime}\R Q^{\prime}$ ,

•

and if $P\R Q$ then there exists a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $Q^{\prime}\R P$ .

It is divergence-preserving if $P\R Q$ and $P{\Uparrow}$ implies $Q{\Uparrow}$ . Write $P\sqsupseteq_{CS}^{\Delta}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\equiv_{CS}^{\Delta}Q$ , if $P\sqsupseteq_{CS}^{\Delta}Q$ and $Q\sqsupseteq_{CS}^{\Delta}P$ .

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

Intuitively, $P\sqsupseteq_{CS}^{\Delta}Q$ says that $P$ is “ahead” of a state matching $Q$ , where $P^{\prime}$ is ahead of $P$ if $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime}$ . 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\sqsubseteq_{CS}^{\Delta}Q$ implies $Q\sqsubseteq_{CS}^{\Delta}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

$\sqsupseteq_{CS}^{\Delta}$ * is reflexive and transitive, and thus a preorder.*

Proof

The identity relation ${\it Id}$ is a divergence-preserving coupled simulation, and if $\R$ , $\R^{\prime}$ are divergence-preserving coupled simulations, then so is $\R\mathbin{\mathchar 24635\relax}\R^{\prime}\cup\R^{\prime}\mathbin{\mathchar 24635\relax}\R$ . Here ${\R}\mathbin{\mathchar 24635\relax}{\R^{\prime}}$ is defined by $P\mathrel{{\R}\mathbin{\mathchar 24635\relax}{\R^{\prime}}}R$ iff there is a $Q$ with $P\R Q\R^{\prime}R$ .

$\R{\mathbin{\mathchar 24635\relax}}\R^{\prime}$ is divergence-preserving: if $P{\R}Q{\R^{\prime}}R$ and $P{\Uparrow}$ , then $Q{\Uparrow}$ , and thus $R{\Uparrow}\!$ . The same holds for $\R^{\prime}\mathbin{\mathchar 24635\relax}\R$ , and thus for $\R\mathbin{\mathchar 24635\relax}\R^{\prime}\cup\R^{\prime}\mathbin{\mathchar 24635\relax}\R$ .

To check that $\R\mathbin{\mathchar 24635\relax}\R^{\prime}\cup\R^{\prime}\mathbin{\mathchar 24635\relax}\R$ satisfies the first clause of Def. 4, note that if $Q\R^{\prime}R$ and $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ , then, by repeated application of the first clause of Def. 4, there is an $R^{\prime}$ with $R\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime}$ and $Q^{\prime}\R^{\prime}R^{\prime}$ .

Towards the second clause, if $P\R Q\R^{\prime}R$ , then, using the second clause for $\R$ , there is a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $Q^{\prime}\R P$ . Hence, using the first clause for $\R^{\prime}$ , there is an $R^{\prime}$ with $R\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime}$ and $Q^{\prime}\R^{\prime}R^{\prime}$ . Thus, using the second clause for $\R^{\prime}$ , there is an $R^{\prime\prime}$ with $R^{\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime\prime}$ and $R^{\prime\prime}\R^{\prime}Q^{\prime}$ , and hence $R^{\prime\prime}\mathrel{{\R^{\prime}}\mathbin{\mathchar 24635\relax}{\R}}P^{\prime}$ . ∎

Proposition 2

If $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ then $P\sqsubseteq_{CS}^{\Delta}Q$ .

Proof

I show that ${\it Id}\cup\{(Q,P)\}$ , with ${\it Id}$ the identity relation, is a coupled simulation. Namely if $Q\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q^{\prime}$ then surely $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ . The second clause of Def. 4 is satisfied because $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ . Furthermore, if $Q{\Uparrow}$ then certainly $P{\Uparrow}$ , so the relation is divergence-preserving. ∎

Proposition 3

$P\sqsupseteq_{CS}^{\Delta}Q$ * iff $P\mathbin{\mathchar 629\relax}Q\equiv_{CS}^{\Delta}Q$ .*

Proof

“ $\Rightarrow$ ”: Let $\R$ be the smallest relation such that, for any $P$ and $Q$ , $P\sqsupseteq_{CS}^{\Delta}Q$ implies $P\R Q$ , $(P\mathbin{\mathchar 629\relax}Q)\R Q$ and $Q\R(P\mathbin{\mathchar 629\relax}Q)$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

That $\R$ is divergence-preserving is trivial, using that $(P\mathbin{\mathchar 629\relax}Q){\Uparrow}$ iff $P{\Uparrow}\vee Q{\Uparrow}$ .

Suppose $P^{*}\R Q$ and $P^{*}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . The case that $P^{*}=P$ with $P\sqsupseteq_{CS}^{\Delta}Q$ is trivial. Now let $Q$ be $Q^{*}\mathbin{\mathchar 629\relax}P^{*}$ . Since $P^{*}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ , surely $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime}$ , and $P^{\prime}\R P^{\prime}$ . Finally, let $P^{*}=(P\mathbin{\mathchar 629\relax}Q)$ with $P\sqsupseteq_{CS}^{\Delta}Q$ . Then $\alpha=\tau$ and $P^{\prime}$ is either $P$ or $Q$ . Both cases are trivial, taking $Q^{\prime}=Q$ .

Towards the second clause of Def. 4, suppose $P^{*}\R Q$ . The case $P^{*}=P$ with $P\sqsupseteq_{CS}^{\Delta}Q$ is trivial. Now let $Q$ be $Q^{*}\mathbin{\mathchar 629\relax}P^{*}$ . Then $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{*}$ and $P^{*}\R P^{*}$ . Finally, let $P^{*}=(P\mathbin{\mathchar 629\relax}Q)$ with $P\sqsupseteq_{CS}^{\Delta}Q$ . Then $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q$ and $Q\R(P\mathbin{\mathchar 629\relax}Q)$ .

“ $\Leftarrow$ ”: Suppose $P\mathbin{\mathchar 629\relax}Q\sqsupseteq_{CS}^{\Delta}Q$ . Since $P\mathbin{\mathchar 629\relax}Q\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P$ there exists a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P\sqsupseteq_{CS}^{\Delta}Q^{\prime}$ . By Prop. 2 $Q^{\prime}\sqsupseteq_{CS}^{\Delta}Q$ and by Prop. 1 $P\sqsupseteq_{CS}^{\Delta}Q$ . ∎

7 Congruence Properties

Proposition 4

$\equiv_{CS}^{\Delta}$ * is a congruence for action prefixing.*

Proof

I have to show that $P\equiv_{CS}^{\Delta}Q$ implies $(a\rightarrow P)\equiv_{CS}^{\Delta}(a\rightarrow Q)$ .

Let $\R$ be the smallest relation such that, for any $P$ and $Q$ , $P\sqsubseteq_{CS}^{\Delta}Q$ implies $P\R Q$ , and $P\equiv_{CS}^{\Delta}Q$ implies $(a\rightarrow P)\R(a\rightarrow 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\sqsubseteq_{CS}^{\Delta}Q$ is trivial. So I examine the case $(a\rightarrow P)\R(a\rightarrow Q)$ with $P\equiv_{CS}^{\Delta}Q$ .

Suppose $(a\rightarrow P)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . Then $\alpha=a$ and $P^{\prime}=P$ . Now $(a\rightarrow Q)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q$ and $P\R Q$ , so the first condition of Def. 4 is satisfied.

For the second condition, $(a\rightarrow Q)\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}(a\rightarrow Q)$ , and, since $Q\equiv_{CS}^{\Delta}P$ , $(a\rightarrow Q)\R(a\rightarrow P)$ . Thus, $\R$ is a coupled simulation.

As $a\rightarrow P$ does not diverge, $\R$ moreover is divergence-preserving. ∎

Since $\mathord{{\it STOP}}\sqsupseteq_{CS}^{\Delta}(a\mathbin{\rightarrow}STOP)\mathbin{\mathchar 302\relax}\mathord{{\it STOP}}$ but $\mathord{{\it STOP}}\not\sqsubseteq_{CS}^{\Delta}(a\mathbin{\rightarrow}STOP)\mathbin{\mathchar 302\relax}\mathord{{\it STOP}}$ ,and thus $b\rightarrow\mathord{{\it STOP}}\not\sqsupseteq_{CS}^{\Delta}b\rightarrow\big{(}(a\rightarrow STOP)\mathbin{\mathchar 302\relax}\mathord{{\it STOP}}\big{)}$ , the relation $\sqsupseteq_{CS}^{\Delta}$ is not a precongruence for action prefixing.

It is possible to express action prefixing in terms of the throw operator: $a\rightarrow P$ is strongly bisimilar with $(a\rightarrow\mathord{{\it STOP}})\mathbin{\Theta_{\{a\}}}P$ . Consequently, $\sqsupseteq_{CS}^{\Delta}$ is not a precongruence for the throw operator.

Proposition 5

$\equiv_{CS}^{\Delta}$ * is a congruence for the throw operator.*

Proof

Let $A\subseteq\Sigma$ . Let $\R$ be the smallest relation such that, for any $P_{1},P_{2},Q_{1}$ , $Q_{2}$ , $P_{1}\sqsupseteq_{CS}^{\Delta}Q_{1}$ and $P_{2}\equiv_{CS}^{\Delta}Q_{2}$ implies $P_{1}\R Q_{1}$ and $(P_{1}\mathbin{\Theta\!_{A}}P_{2})\R(Q_{1}\mathbin{\Theta\!_{A}}Q_{2})$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P_{1}\sqsupseteq_{CS}^{\Delta}Q_{1}$ , $P_{2}\equiv_{CS}^{\Delta}Q_{2}$ and $(P_{1}\mathbin{\Theta\!_{A}}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . Then $P_{1}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P_{1}^{\prime}$ for some $P_{2}^{\prime}$ , and either $\alpha\notin A$ and $P^{\prime}=P_{1}^{\prime}\mathbin{\Theta\!_{A}}P_{2}$ , or $\alpha\in A$ and $P^{\prime}=P_{2}$ . So there is a $Q_{1}^{\prime}$ with $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ and $P_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{1}^{\prime}$ . If $\alpha\notin A$ it follows that $(Q_{1}\mathbin{\Theta\!_{A}}Q_{2})\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}(Q_{1}^{\prime}\mathbin{\Theta\!_{A}}Q_{2})$ and $(P^{\prime}_{1}\mathbin{\Theta\!_{A}}P_{2})\R(Q^{\prime}_{1}\mathbin{\Theta\!_{A}}Q_{2})$ . If $\alpha\in A$ it follows that $(Q_{1}\mathbin{\Theta\!_{A}}Q_{2})\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}$ and $P_{2}\R Q_{2}$ .

Now let $P_{1}\sqsupseteq_{CS}^{\Delta}Q_{1}$ and $P_{2}\equiv_{CS}^{\Delta}Q_{2}$ . Then there is a $Q_{1}^{\prime}$ with $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ and $Q_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{1}$ . Hence $Q_{1}\mathbin{\Theta\!_{A}}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\mathbin{\Theta\!_{A}}Q_{2}$ and $(Q_{1}^{\prime}\mathbin{\Theta\!_{A}}Q_{2})\R(P_{1}\mathbin{\Theta\!_{A}}P_{2})$ .

The same two conditions for the case $P\R Q$ because $P\sqsupseteq_{CS}^{\Delta}Q$ are trivial. Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\mathbin{\Theta\!_{A}}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}$ . ∎

I proceed to show that $\sqsupseteq_{CS}^{\Delta}$ is a precongruence for all the other operators of CSP. This implies that $\equiv_{CS}^{\Delta}$ is a congruence for all the operators of CSP.

Proposition 6

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for internal choice.*

Proof

Let $\R$ be the smallest relation such that, for any $P_{i}$ and $Q_{i}$ , $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ implies $P_{i}\R Q_{i}$ ( $i=1,2$ ) and $(P_{1}\mathbin{\mathchar 629\relax}P_{2})\R(Q_{1}\mathbin{\mathchar 629\relax}Q_{2})$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ and $(P_{1}\mathbin{\mathchar 629\relax}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . Then $\alpha=\tau$ and $P^{\prime}=P_{i}$ for $i=1$ or $2$ . Now $Q_{1}\mathbin{\mathchar 629\relax}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}$ and $P_{i}\R Q_{i}$ .

Now let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ . Then there is a $Q_{1}^{\prime}$ with $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ and $Q_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{1}$ . By Prop. 2 $P_{1}\sqsupseteq_{CS}^{\Delta}P_{1}\mathbin{\mathchar 629\relax}P_{2}$ and by Prop. 1 $Q_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{1}\mathbin{\mathchar 629\relax}P_{2}$ .

The same two conditions for the case $P\R Q$ because $P\sqsupseteq_{CS}^{\Delta}Q$ are trivial. Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\mathbin{\mathchar 629\relax}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}\vee P_{2}{\Uparrow}$ . ∎

Proposition 7

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for external choice.*

Proof

Let $\R$ be the smallest relation such that, for any $P_{i}$ and $Q_{i}$ , $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ implies $P_{i}\R Q_{i}$ ( $i=1,2$ ) and $(P_{1}\mathbin{{\Box}}P_{2})\R(Q_{1}\mathbin{{\Box}}Q_{2})$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ and $(P_{1}\mathbin{{\Box}}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . If $\alpha\in\Sigma$ then $P_{i}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ for $i=1$ or $2$ , and there exists a $Q^{\prime}$ with $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P^{\prime}\sqsupseteq_{CS}^{\Delta}Q^{\prime}$ . Hence $Q_{1}\mathbin{{\Box}}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P^{\prime}\R Q^{\prime}$ . If $\alpha=\tau$ then either $P_{1}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{1}^{\prime}$ for some $P_{1}^{\prime}$ with $P^{\prime}=P_{1}^{\prime}\mathbin{{\Box}}P_{2}$ , or $P_{2}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{2}^{\prime}$ for some $P_{2}^{\prime}$ with $P^{\prime}=P_{1}\mathbin{{\Box}}P_{2}^{\prime}$ . I pursue only the first case, as the other follows by symmetry. Here $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ for some $Q_{1}^{\prime}$ with $P_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{1}^{\prime}$ . Thus $Q_{1}\mathbin{{\Box}}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\mathbin{{\Box}}Q_{2}$ and $(P_{1}^{\prime}\mathbin{{\Box}}P_{2})\R(Q_{1}^{\prime}\mathbin{{\Box}}Q_{2})$ .

Now let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ . Then, for $i=1,2$ , there is a $Q_{i}^{\prime}$ with $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}^{\prime}$ and $Q_{i}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{i}$ . Hence $Q_{1}\mathbin{{\Box}}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\mathbin{{\Box}}Q_{2}^{\prime}$ and $(Q_{1}^{\prime}\mathbin{{\Box}}Q_{2}^{\prime})\R(P_{1}\mathbin{{\Box}}P_{2})$ .

Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\mathbin{{\Box}}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}\vee P_{2}{\Uparrow}$ . ∎

Proposition 8

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for sliding choice.*

Proof

Let $\R$ be the smallest relation such that, for any $P_{i}$ and $Q_{i}$ , $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ implies $P_{i}\R Q_{i}$ ( $i=1,2$ ) and $(P_{1}\mathbin{\mathchar 302\relax}P_{2})\R(Q_{1}\mathbin{\mathchar 302\relax}Q_{2})$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ and $(P_{1}\mathbin{\mathchar 302\relax}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . If $\alpha\in\Sigma$ then $P_{1}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ , and there exists a $Q^{\prime}$ with $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P^{\prime}\sqsupseteq_{CS}^{\Delta}Q^{\prime}$ . Hence $Q_{1}\mathbin{\mathchar 302\relax}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $P^{\prime}\R Q^{\prime}$ . If $\alpha\mathbin{=}\tau$ then either $P^{\prime}\mathbin{=}P_{2}$ or $P_{1}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{1}^{\prime}$ for some $P_{1}^{\prime}$ with $P^{\prime}\mathbin{=}P_{1}^{\prime}\mathbin{\mathchar 302\relax}P_{2}$ . In the former case $Q_{1}\mathbin{\mathchar 302\relax}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}$ and $P_{2}\R Q_{2}$ . In the latter case $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ for some $Q_{1}^{\prime}$ with $P_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{1}^{\prime}$ . Thus $Q_{1}\mathbin{\mathchar 302\relax}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\mathbin{\mathchar 302\relax}Q_{2}$ and $(P_{1}^{\prime}\mathbin{\mathchar 302\relax}P_{2})\R(Q_{1}^{\prime}\mathbin{\mathchar 302\relax}Q_{2})$ .

Now let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ . Then there is a $Q_{2}^{\prime}$ with $Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}^{\prime}$ and $Q_{2}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{2}$ . By Prop. 2 $P_{2}\sqsupseteq_{CS}^{\Delta}P_{1}\mathbin{\mathchar 302\relax}P_{2}$ and by Prop. 1 $Q_{2}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{1}\mathbin{\mathchar 302\relax}P_{2}$ .

Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\mathbin{\mathchar 302\relax}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}\vee P_{2}{\Uparrow}$ . ∎

Proposition 9

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for parallel composition.*

Proof

Let $A\subseteq\Sigma$ . Let $\R$ be the smallest relation such that, for any $P_{i}$ and $Q_{i}$ , $P_{i}\sqsupseteq_{CS}^{\Delta}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}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ and $(P_{1}\|_{A}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . If $\alpha\notin A$ then $P_{i}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P_{i}^{\prime}$ for $i=1$ or $2$ , and $P^{\prime}=P_{1}^{\prime}\|_{A}P_{2}^{\prime}$ , where $P_{3-i}^{\prime}:=P_{3-i}$ . Hence there exists a $Q_{i}^{\prime}$ with $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}^{\prime}$ and $P_{i}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{i}^{\prime}$ . Let $Q_{3-i}^{\prime}:=Q_{3-i}$ . Then $Q_{1}\|_{A}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\|Q^{\prime}_{2}$ and $(P_{1}^{\prime}\|P^{\prime}_{2})\R(Q_{1}^{\prime}\|Q^{\prime}_{2})$ . If $\alpha\in A$ then $P_{i}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P_{i}^{\prime}$ for $i=1$ and $2$ . Hence, for $i=1,2$ , $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}^{\prime}$ for some $Q_{i}^{\prime}$ with $P_{i}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{i}^{\prime}$ . Thus $Q_{1}\|_{A}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\|_{A}Q_{2}^{\prime}$ and $(P_{1}^{\prime}\|_{A}P^{\prime}_{2})\R(Q_{1}^{\prime}\|_{A}Q^{\prime}_{2})$ .

Now let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ . Then, for $i=1,2$ , there is a $Q_{i}^{\prime}$ with $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}^{\prime}$ and $Q_{i}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{i}$ . Hence $Q_{1}\|_{A}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\|_{A}Q_{2}^{\prime}$ and $(Q_{1}^{\prime}\|_{A}Q_{2}^{\prime})\R(P_{1}\|_{A}P_{2})$ .

Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\|_{A}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}\vee P_{2}{\Uparrow}$ . ∎

Proposition 10

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for concealment.*

Proof

Let $A\subseteq\Sigma$ . Let $\R$ be the smallest relation such that, for any $P$ and $Q$ , $P\sqsubseteq_{CS}^{\Delta}Q$ implies $(P\backslash A)\R(Q\backslash A)$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P\sqsubseteq_{CS}^{\Delta}Q$ and $P\backslash A\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{*}$ . Then $P^{*}=P^{\prime}\backslash A$ for some $P^{\prime}$ with $P\stackrel{{\scriptstyle\beta}}{{\longrightarrow}}P^{\prime}$ , and either $\beta\in A$ and $\alpha=\tau$ , or $\beta=\alpha\notin A$ . Hence $Q\stackrel{{\scriptstyle\beta}}{{\longrightarrow}}Q^{\prime}$ for some $Q^{\prime}$ with $P^{\prime}\sqsubseteq_{CS}^{\Delta}Q^{\prime}$ . Therefore $Q\backslash A\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q^{\prime}\backslash A$ and $(P^{\prime}\backslash A)\R(Q^{\prime}\backslash A)$ .

Now let $P\sqsubseteq_{CS}^{\Delta}Q$ . Then there is a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $Q^{\prime}\sqsupseteq_{CS}^{\Delta}P$ . Hence $Q\backslash A\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}\backslash A$ and $(Q^{\prime}\backslash A)\R(P\backslash A)$ .

To check that $\R$ is divergence-preserving, suppose $(P\backslash A){\Uparrow}$ . Then there are $P_{i}$ and $\alpha_{i}\in A\cup\{\tau\}$ for all $i>0$ such that $P\stackrel{{\scriptstyle\alpha_{1}}}{{\longrightarrow}}P_{1}\stackrel{{\scriptstyle\alpha_{2}}}{{\longrightarrow}}P_{2}\stackrel{{\scriptstyle\alpha_{3}}}{{\longrightarrow}}\dots$ . By the first condition of Def. 4, there are $Q_{i}$ for all $i>0$ such that $P_{i}\R Q_{i}$ and $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha}{1} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha}{2} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha}_{3} $}$ \hskip 2.5pt}\hfil}} $}}}\dots$ . This implies $Q\backslash A\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}\backslash A\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}\backslash A\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}\dots$ .

In case $\alpha_{i}\in\Sigma$ for infinitely many $i$ , then for infinitely many $i$ one has $Q_{i-1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha_{i} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}$ and thus $Q_{i-1}\backslash A\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \tau $}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}\backslash A$ . This implies that $(Q\backslash A){\Uparrow}$ .

Otherwise there is an $n>0$ such that $\alpha_{i}=\tau$ for all $i\geq n$ . In that case $P_{n}{\Uparrow}$ and thus $Q_{n}{\Uparrow}$ . Hence $(Q_{n}\backslash A){\Uparrow}$ and thus $(Q\backslash A){\Uparrow}$ . ∎

Proposition 11

$\sqsupseteq_{CS}^{\Delta}$ * is a precongruence for renaming.*

Proof

Let $f:\Sigma\rightarrow\Sigma$ . Let $\R$ be the smallest relation such that, for any $P$ and $Q$ , $P\sqsubseteq_{CS}^{\Delta}Q$ implies $f(P)\R f(Q)$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P\sqsubseteq_{CS}^{\Delta}Q$ and $f(P)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{*}$ . Then $P^{*}=f(P^{\prime})$ for some $P^{\prime}$ with $P\stackrel{{\scriptstyle\beta}}{{\longrightarrow}}P^{\prime}$ and $f(\beta)=\alpha$ . Hence $Q\stackrel{{\scriptstyle\beta}}{{\longrightarrow}}Q^{\prime}$ for some $Q^{\prime}$ with $P^{\prime}\sqsubseteq_{CS}^{\Delta}Q^{\prime}$ . Therefore $f(Q)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}f(Q^{\prime})$ and $f(P^{\prime})\R f(Q^{\prime})$ .

Now let $P\sqsubseteq_{CS}^{\Delta}Q$ . Then there is a $Q^{\prime}$ with $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ and $Q^{\prime}\sqsupseteq_{CS}^{\Delta}P$ . Hence $f(Q)\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}f(Q^{\prime})$ and $f(Q^{\prime})\R f(P)$ .

To check that $\R$ is divergence-preserving, suppose $f(P){\Uparrow}$ . Then $P{\Uparrow}$ , so $Q{\Uparrow}$ and $f(Q){\Uparrow}$ . ∎

Proposition 12

$\sqsupseteq_{CS}^{\Delta}$ * 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}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ implies $P_{2}\R Q_{2}$ and $(P_{1}\mathbin{\mathchar 564\relax}P_{2})\R(Q_{1}\mathbin{\mathchar 564\relax}Q_{2})$ . It suffices to show that $\R$ is a divergence-preserving coupled simulation.

So let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ and $(P_{1}\mathbin{\mathchar 564\relax}P_{2})\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ . Then either $P^{\prime}=P_{1}^{\prime}\mathbin{\mathchar 564\relax}P_{2}$ for some $P_{1}^{\prime}$ with $P_{1}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P_{1}^{\prime}$ , or $\alpha=\tau$ and $P^{\prime}=P_{1}\mathbin{\mathchar 564\relax}P_{2}^{\prime}$ for some $P_{2}^{\prime}$ with $P_{2}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P_{2}^{\prime}$ , or $\alpha\in\Sigma$ and $P_{2}\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ .

In the first case there is a $Q_{1}^{\prime}$ with $Q_{1}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}$ and $P_{1}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{1}^{\prime}$ . It follows that $(Q_{1}\mathbin{\mathchar 564\relax}Q_{2})\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \hat{\alpha} $}$ \hskip 2.5pt}\hfil}} $}}}(Q_{1}^{\prime}\mathbin{\mathchar 564\relax}Q_{2})$ and $(P^{\prime}_{1}\mathbin{\mathchar 564\relax}P_{2})\R(Q^{\prime}_{1}\mathbin{\mathchar 564\relax}Q_{2})$ .

In the second case there is a $Q_{2}^{\prime}$ with $Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}^{\prime}$ and $P_{2}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{2}^{\prime}$ . It follows that $(Q_{1}\mathbin{\mathchar 564\relax}Q_{2})\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}(Q_{1}\mathbin{\mathchar 564\relax}Q_{2}^{\prime})$ and $(P_{1}\mathbin{\mathchar 564\relax}P_{2}^{\prime})\R(Q_{1}\mathbin{\mathchar 564\relax}Q_{2}^{\prime})$ .

In the last case there is a $Q_{2}^{\prime}$ with $Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}^{\prime}$ and $P_{2}^{\prime}\sqsupseteq_{CS}^{\Delta}Q_{2}^{\prime}$ . It follows that $(Q_{1}\mathbin{\mathchar 564\relax}Q_{2})\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \alpha $}$ \hskip 2.5pt}\hfil}} $}}}Q_{2}^{\prime}$ and $P_{2}^{\prime}\R Q_{2}^{\prime}$ .

Now let $P_{i}\sqsupseteq_{CS}^{\Delta}Q_{i}$ for $i=1,2$ . Then, for $i=1,2$ , there is a $Q_{i}^{\prime}$ with $Q_{i}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{i}^{\prime}$ and $Q_{i}^{\prime}\sqsupseteq_{CS}^{\Delta}P_{i}$ . Hence $Q_{1}\mathbin{\mathchar 564\relax}Q_{2}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q_{1}^{\prime}\mathbin{\mathchar 564\relax}Q_{2}^{\prime}$ and $(Q_{1}^{\prime}\mathbin{\mathchar 564\relax}Q_{2}^{\prime})\R(P_{1}\mathbin{\mathchar 564\relax}P_{2})$ .

Thus $\R$ is a coupled simulation. That $\R$ is divergence-preserving follows because $P_{1}\mathbin{\mathchar 564\relax}P_{2}{\Uparrow}$ iff $P_{1}{\Uparrow}\vee P_{2}{\Uparrow}$ . ∎

8 A Complete Axiomatisation of $\equiv_{CS}^{\Delta}$

A set of equational laws valid for $\equiv_{CS}^{\Delta}$ is presented in Table 3. It includes the laws from Table 2 that are still valid for $\equiv_{CS}^{\Delta}$ . I will show that this axiomatisation is sound and complete for $\equiv_{CS}^{\Delta}$ for recursion-free CSP without the interrupt operator. The axioms $\mathbf{U2}$ and $\mathbf{U3}$ , which are not valid for $\equiv_{CS}^{\Delta}$ , 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 $\mathbf{H5}$ replaces the fallen axiom $\mathbf{H2}$ , and is due to [18]. Here the result of hiding actions results in a process that cannot be expressed as a normal form built up from $a\rightarrow$ , $\mathbin{\mathchar 629\relax}$ and $\mathbin{{\Box}}$ . For this reason, one needs a richer normal form, involving the sliding choice operator. It is given by the context-free grammar

[TABLE]

Definition 5

A CSP expression is in head normal form if it is of the form $\big{(}[\mathord{{\bf div}}\mathrel{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in I}(a_{i}\rightarrow R_{i})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{j\in J}R_{j}$ , with $R_{j}=\big{(}[\mathord{{\bf div}}\mathrel{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{k\in K_{j}}(a_{kj}\rightarrow R_{kj})\big{)}$ for $j\in J$ . Here $I$ , $J$ and the $K_{j}$ are finite index sets, and the parts between square brackets are optional. Here, although $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{i\in\emptyset}P_{i}$ is undefined, I use $P\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{i\in\emptyset}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 $\mathord{{\bf div}}$ -summand on the left is present whenever any of the $R_{j}$ has a $\mathord{{\bf div}}$ -summand, and for any $j\mathbin{\in}J$ and any $k\mathbin{\in}K_{j}$ there is an $i\mathbin{\in}I$ with $a_{i}\mathbin{=}a_{kj}$ and $R_{i}\mathbin{=}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 $\mathord{{\bf div}}$ -summand and a sliding choice, I need four variants of the axiom $\mathbf{H5}$ ; so far I have not seen a way around this. Likewise, there are $4\times 4$ variants of the axiom $\mathbf{P4}$ from Table 2, of which 6 could be suppressed by symmetry (P4–P13). There are also 3 axioms replacing $\mathbf{P2}$ (P14–P16).

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. $\equiv_{CS}^{\Delta}$ 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 [13] if they are related by a binary relation $\R$ on processes such that, for all $\alpha\in\Sigma\cup\{\tau\}$ ,

•

if $P\R Q$ and $P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ then there exists a $Q^{\prime}$ with $Q\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q^{\prime}$ and $P^{\prime}\R Q^{\prime}$ ,

•

if $P\R Q$ and $Q\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}Q^{\prime}$ then there exists a $P^{\prime}$ with $P\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}P^{\prime}$ and $P^{\prime}\R Q^{\prime}$ .

Proposition 13

Axiom $\mathbf{I1}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{(P\mathbin{\mathchar 629\relax}P,P),(P,P\mathbin{\mathchar 629\relax}P)\mid P\,\,\mbox{a process}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 14

Axiom $\mathbf{I2}$ is valid even for strong bisimilarity.

Proof

$\{(P\mathbin{\mathchar 629\relax}Q,Q\mathbin{\mathchar 629\relax}P)\mid P,Q\,\,\mbox{processes}\}\cup{\it Id}$ is a strong bisimulation. ∎

Proposition 15

Axiom $\mathbf{I3}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

The relation $\{\big{(}P\mathbin{\mathchar 629\relax}(Q\mathbin{\mathchar 629\relax}R),(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 629\relax}R\big{)},\big{(}(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 629\relax}R,P\mathbin{\mathchar 629\relax}(Q\mathbin{\mathchar 629\relax}R)\big{)},\linebreak[3]\big{(}Q\mathbin{\mathchar 629\relax}R,(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 629\relax}R\big{)},\big{(}P\mathbin{\mathchar 629\relax}Q,P\mathbin{\mathchar 629\relax}(Q\mathbin{\mathchar 629\relax}R)\big{)},\big{(}R,Q\mathbin{\mathchar 629\relax}R\big{)},\big{(}P,P\mathbin{\mathchar 629\relax}Q\big{)}\,|\,P,Q,R\,\,\mbox{processes}\}\linebreak\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 16

Axioms E2–4 are valid for strong bisimilarity.

Proof

The relation $\{\big{(}P\mathbin{{\Box}}(Q\mathbin{{\Box}}R),(P\mathbin{{\Box}}Q)\mathbin{{\Box}}R\big{)}\mid P,Q,R\,\,\mbox{processes}\}\cup{\it Id}$ is a strong bisimulation. So is $\{(P\mathbin{{\Box}}Q,Q\mathbin{{\Box}}P)\mid P,Q\,\,\mbox{processes}\}\cup{\it Id}$ , as well as $\{(P\mathbin{{\Box}}\mathord{{\it STOP}},P)\mid P\,\,\mbox{a process}\}\cup{\it Id}$ . ∎

Proposition 17

Axiom $\mathbf{S1}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{(P^{\prime}\mathbin{\mathchar 302\relax}P,P),(P,P^{\prime}\mathbin{\mathchar 302\relax}P)\mid P^{\prime}\sqsupseteq_{CS}^{\Delta}P\}\cup{\it Id}$ is a divergence-preserving coupled simulation. This follows from Prop. 2. ∎

Proposition 18

Axiom $\mathbf{S2}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}P\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 302\relax}R),(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 302\relax}R,P\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 302\relax}R)\big{)}\mid P,Q,R\,\,\mbox{processes}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 19

Axiom $\mathbf{S3}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 302\relax}R,(P\mathbin{{\Box}}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}(P\mathbin{{\Box}}Q^{\prime})\mathbin{\mathchar 302\relax}R,(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}Q\mathbin{\mathchar 302\relax}R,(P\mathbin{{\Box}}Q)\mathbin{\mathchar 302\relax}R\big{)},\linebreak[3]\big{(}R,Q\mathbin{\mathchar 302\relax}R\big{)}\mid Q^{\prime}\sqsupseteq_{CS}^{\Delta}Q\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 20

Axiom $\mathbf{S4}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 302\relax}R,(P\mathbin{{\Box}}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}(P^{\prime}\mathbin{{\Box}}Q^{\prime})\mathbin{\mathchar 302\relax}R,(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}P\mathbin{\mathchar 302\relax}R,(P\mathbin{{\Box}}Q)\mathbin{\mathchar 302\relax}R\big{)},\linebreak[3]\big{(}Q\mathbin{\mathchar 302\relax}R,(P\mathbin{{\Box}}Q)\mathbin{\mathchar 302\relax}R\big{)},\big{(}R,Q\mathbin{\mathchar 302\relax}R\big{)}\mid P^{\prime}\sqsupseteq_{CS}^{\Delta}P\wedge Q^{\prime}\sqsupseteq_{CS}^{\Delta}Q\}\cup{\it Id}$ is a divergence-preserving coupled simulation. Checking this involves Prop. 2. ∎

Proposition 21

Axiom $\mathbf{S5}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

The relation $\{(\mathord{{\it STOP}}\mathbin{\mathchar 302\relax}P,P),(P,\mathord{{\it STOP}}\mathbin{\mathchar 302\relax}P)\mid P\,\,\mbox{a process}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 22

Axiom $\mathbf{S6}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 629\relax}(R\mathbin{\mathchar 302\relax}S),(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 629\relax}S)\big{)},\big{(}(P^{\prime}\mathbin{{\Box}}R^{\prime})\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 629\relax}S),(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 629\relax}(R\mathbin{\mathchar 302\relax}S)\big{)},\linebreak\big{(}P\mathbin{\mathchar 302\relax}Q,(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 629\relax}S)\big{)},\big{(}R\mathbin{\mathchar 302\relax}S,(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 629\relax}S)\big{)},\big{(}Q\mathbin{\mathchar 629\relax}S,(P\mathbin{\mathchar 302\relax}Q)\mathbin{\mathchar 629\relax}(R\mathbin{\mathchar 302\relax}S)\big{)},\linebreak\big{(}S,(P^{\prime}\mathbin{{\Box}}R^{\prime})\mathbin{\mathchar 302\relax}(Q\mathbin{\mathchar 629\relax}S)\big{)},\big{(}S,R\mathbin{\mathchar 302\relax}S\big{)},\big{(}S,Q\mathbin{\mathchar 629\relax}S\big{)}\mid P^{\prime}\sqsupseteq_{CS}^{\Delta}P\wedge R^{\prime}\sqsupseteq_{CS}^{\Delta}R\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 23

Axiom $\mathbf{S7}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(P\mathbin{\mathchar 302\relax}Q)\mathbin{{\Box}}(R\mathbin{\mathchar 302\relax}S),(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{{\Box}}S)\big{)},\big{(}(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{{\Box}}S),(P\mathbin{\mathchar 302\relax}Q)\mathbin{{\Box}}(R\mathbin{\mathchar 302\relax}S)\big{)},\linebreak\big{(}Q^{\prime}\mathbin{{\Box}}(R\mathbin{\mathchar 302\relax}S),(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{{\Box}}S)\big{)}\,\,,\,\,\big{(}(P\mathbin{\mathchar 302\relax}Q)\mathbin{{\Box}}S^{\prime},(P\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}(Q\mathbin{{\Box}}S)\big{)},\linebreak\big{(}Q^{\prime}\mathbin{{\Box}}S^{\prime},Q^{\prime}\mathbin{{\Box}}(R\mathbin{\mathchar 302\relax}S)\big{)},\big{(}Q^{\prime}\mathbin{{\Box}}S^{\prime},(P\mathbin{\mathchar 302\relax}Q)\mathbin{{\Box}}S^{\prime}\big{)},\mid Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}\wedge S\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}S^{\prime}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 24

Axiom $\mathbf{D1}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}P^{\prime}\mathbin{{\Box}}(Q\mathbin{\mathchar 629\relax}R),(P\mathbin{{\Box}}Q)\mathbin{\mathchar 629\relax}(P\mathbin{{\Box}}R)\big{)},\big{(}(P\mathbin{{\Box}}Q)\mathbin{\mathchar 629\relax}(P\mathbin{{\Box}}R),P\mathbin{{\Box}}(Q\mathbin{\mathchar 629\relax}R)\big{)},\linebreak\big{(}P^{\prime}\mathbin{{\Box}}Q,P^{\prime}\mathbin{{\Box}}(Q\mathbin{\mathchar 629\relax}R)\big{)}\mid P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

Proposition 25

Axiom $\mathbf{Prune}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(a{\rightarrow}P)\mathbin{{\Box}}a{\rightarrow}(P\mathbin{\mathchar 629\relax}Q),a{\rightarrow}(P\mathbin{\mathchar 629\relax}Q)\big{)},\big{(}a{\rightarrow}(P\mathbin{\mathchar 629\relax}Q),(a{\rightarrow}P)\mathbin{{\Box}}a{\rightarrow}(P\mathbin{\mathchar 629\relax}Q)\big{)}\}\linebreak[3]\cup{\it 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 $\equiv_{CS}^{\Delta}$ .*

Proof

Straightforward. ∎

Proposition 27

Axioms $\mathbf{U4}$ , $\mathbf{H1}$ , R0–5 and T0–6 are valid for strong bisimilarity. Axioms H5–8 are valid for $\equiv_{CS}^{\Delta}$ .

Proof

Straightforward. ∎

Proposition 28

Axiom $\mathbf{U1}$ is valid for $\equiv_{CS}^{\Delta}$ .

Proof

$\{\big{(}(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 564\relax}R^{\prime},(P\mathbin{\mathchar 564\relax}R)\mathbin{\mathchar 629\relax}(Q\mathbin{\mathchar 564\relax}R)\big{)},\big{(}(P\mathbin{\mathchar 564\relax}R)\mathbin{\mathchar 629\relax}(Q\mathbin{\mathchar 564\relax}R),(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 564\relax}R\big{)},\linebreak\big{(}P\mathbin{\mathchar 564\relax}R^{\prime},(P\mathbin{\mathchar 629\relax}Q)\mathbin{\mathchar 564\relax}R^{\prime}\big{)}\mid R\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime}\}\cup{\it Id}$ is a divergence-preserving coupled simulation. ∎

10 Completeness

Let ${\it 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 ${\it Th}\vdash 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=\mathord{{\it STOP}}$ or $\mathord{{\bf div}}$ . Then $P$ is already in normal form. Take $Q:=P$ .

•

Let $P=a\rightarrow P^{\prime}$ . By assumption $P^{\prime}$ is in normal form; therefore so is $P$ .

•

Let $P=P_{1}\mathbin{\mathchar 629\relax}P_{2}$ . By assumption $P_{1}$ and $P_{2}$ are in normal form. So $P\mathbin{=}\left(\!\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in J}\!R_{j}\!\right)\mathbin{\mathchar 629\relax}\left(\!\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L}(a_{l}\mathbin{\rightarrow}R_{l})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in M}\!R_{j}\!\right)$ with $R_{j}=\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{k\in K_{j}}(a_{kj}\rightarrow R_{kj})\big{)}$ for $j\in J\cup M$ . With Axiom $\mathbf{S5}$ I may assume that $J,M\neq\emptyset$ . Now Axiom $\mathbf{S6}$ converts $P$ to normal form.

•

Let $P=P_{1}\mathbin{{\Box}}P_{2}$ . By assumption $P_{1}$ and $P_{2}$ are in normal form. So $P\mathbin{=}\left(\!\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in J}\!R_{j}\!\right)\mathbin{{\Box}}\left(\!\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L}(a_{l}\mathbin{\rightarrow}R_{l})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in M}\!R_{j}\!\right)$ with $R_{j}=\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{k\in K_{j}}(a_{kj}\rightarrow R_{kj})\big{)}$ for $j\in J\cup M$ . With $\mathbf{S5}$ I may assume that $J,M\neq\emptyset$ . Now Axioms $\mathbf{S7}$ and $\mathbf{D1}$ convert $P$ to normal form.

•

Let $P=P_{1}\mathbin{\mathchar 302\relax}P_{2}$ . Axioms S2–4 and $\mathbf{D1}$ convert $P$ to normal form.

•

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

•

Let $P=P\backslash A$ . Axioms $\mathbf{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}\mathbin{\Theta\!_{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=\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in J}\!R_{j}$ . Then $P$ has the form $S\mathbin{\mathchar 302\relax}R$ . By Axioms S1–3 ${\it Th}\vdash P=(S\mathbin{{\Box}}R)\mathbin{\mathchar 302\relax}R$ . By means of Axioms $\mathbf{D1}$ and $\mathbf{S4}$ the subexpression $S\mathbin{{\Box}}R$ can be brought in the form $[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L}(a_{l}\mathbin{\rightarrow}R_{l})$ . The resulting term is saturated. ∎

Definition 7

A CSP expression $\big{(}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in I}(b_{i}\rightarrow P_{i})\big{)}$ is pruned if, for all $i,h\in I$ , $b_{i}\mathbin{=}b_{h}\wedge P_{i}\sqsupseteq_{CS}^{\Delta}P_{h}\Rightarrow i=h$ .

Theorem 10.1

Let $P$ and $Q$ be recursion-free CSP processes without interrupt operators. Then $P\equiv_{CS}^{\Delta}Q$ iff ${\it Th}\vdash P=Q$ .

Proof

“ $\Leftarrow$ ” is an immediate consequence of the soundness of the axioms of ${\it Th}$ , and the fact that $\equiv_{CS}^{\Delta}$ is a congruence for all operators of CSP.

“ $\Rightarrow$ ”: Let $0pt(P)$ be the length of the longest trace of $P$ —well-defined for recursion-free processes $P$ . If $P\equiv_{CS}^{\Delta}Q$ then $0pt(P)=0pt(Q)$ . Given $P\equiv_{CS}^{\Delta}Q$ , I establish ${\it Th}\vdash P=Q$ with induction on $0pt(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\mathbin{=}\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in J}\!R_{j}$ and $Q\mathbin{=}\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L\!}(a_{l}\mathbin{\rightarrow}R_{l})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{\!j\in M}\!R_{j}$ with $R_{j}\mathbin{=}\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{k\in K_{j}}(a_{kj}\rightarrow R_{kj})\big{)}$ for $j\mathbin{\in}J\cup M$ , where $R_{i}$ , $R_{l}$ and $R_{kj}$ are again in normal form.

Suppose that there are $i,h\in I$ with $i\neq h$ , $a_{i}=a_{h}$ and $R_{i}\sqsupseteq_{CS}^{\Delta}R_{h}$ . Then $R_{i}\mathbin{\mathchar 629\relax}R_{h}\equiv_{CS}^{\Delta}R_{h}$ by Prop. 3. Since $0pt(R_{i}\mathbin{\mathchar 629\relax}R_{h})<0pt(P)$ , the induction hypothesis yields ${\it Th}\vdash R_{i}\mathbin{\mathchar 629\relax}R_{h}=R_{h}$ . Hence Axiom $\mathbf{Prune}$ allows me to prune the summand $a_{i}\rightarrow R_{i}$ from $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})$ . Doing this repeatedly makes $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})$ pruned. By the same reasoning I may assume that $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L}(a_{l}\mathbin{\rightarrow}R_{l})$ is pruned.

Since $P{\Uparrow}\Leftrightarrow Q{\Uparrow}$ and $P$ and $Q$ are saturated, $P$ has the $\mathord{{\bf div}}$ -summand iff $Q$ does. I now define a function $f:I\rightarrow L$ such that $a_{f(i)}=a_{i}$ and $R_{i}\sqsupseteq_{CS}^{\Delta}R_{f(i)}$ for all $i\in I$ .

Let $i\in I$ . Since $P\stackrel{{\scriptstyle a_{i}}}{{\longrightarrow}}R_{i}$ , by Def. 4 $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ a_{i} $}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ for some $Q^{\prime}$ with $R_{i}\sqsupseteq_{CS}^{\Delta}Q^{\prime}$ . Hence either there is an $l\in L$ such that $a_{l}=a_{i}$ and $R_{l}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ , or there is a $j\in M$ and $k\in K_{j}$ such that $a_{kj}=a_{i}$ and $R_{kj}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ . Since $P$ is saturated, the first of these alternatives must apply. By Prop. 2 $Q^{\prime}\sqsupseteq_{CS}^{\Delta}R_{l}$ and by Prop. 1 $R_{i}\sqsupseteq_{CS}^{\Delta}R_{l}$ . Take $f(i):=l$ .

By the same reasoning there is a function $g:L\rightarrow I$ such that $a_{g(l)}=a_{l}$ and $R_{l}\sqsupseteq_{CS}^{\Delta}R_{g(l)}$ for all $l\in L$ . Since $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!i\in I}(a_{i}\mathbin{\rightarrow}R_{i})$ and $\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{\!l\in L}(a_{l}\mathbin{\rightarrow}R_{l})$ are pruned, there are no different $i,h\in I$ (or in $L$ ) with $a_{i}=a_{h}$ and $R_{i}\sqsupseteq_{CS}^{\Delta}R_{h}$ . Hence the functions $f$ and $g$ must be inverses of each other. It follows that $Q=\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in I}(a_{i}\rightarrow R_{f(i)})\big{)}\mathbin{\mathchar 302\relax}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{\mathchar 629\relax} $}}}\nolimits}\nolimits_{j\in M}R_{j}$ with $R_{i}\equiv_{CS}^{\Delta}R_{f(i)}$ for all $i\in I$ . By induction ${\it Th}\vdash R_{i}=R_{f(i)}$ for all $i\in I$ .

So in the special case that $I=M=\emptyset$ I obtain ${\it Th}\vdash P=Q$ . (*)

Next consider the case $J=\emptyset$ but $M\neq\emptyset$ . Let $j\in M$ . Since $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R_{j}$ , there is a $P^{\prime}$ with $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime}$ and $R_{j}\sqsupseteq_{CS}^{\Delta}P^{\prime}$ . Moreover, there is a $P^{\prime\prime}$ with $P^{\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}P^{\prime\prime}$ and $P^{\prime\prime}\sqsupseteq_{CS}^{\Delta}R_{j}$ . Since $J=\emptyset$ , $P^{\prime\prime}=P^{\prime}=P$ , so $P\equiv_{CS}^{\Delta}R_{j}$ . By (*) above ${\it Th}\vdash P\mathbin{=}R_{j}$ . This holds for all $j\in J$ , so by Axiom $\mathbf{I1}$ ${\it Th}\vdash Q=\big{(}[\mathord{{\bf div}}\mathbin{\mathbin{{\Box}}]}\mathop{\mathop{\vbox{\hbox{\Large$ \mathstrut{{\Box}} $}}}\nolimits}\nolimits_{i\in I}(a_{i}\rightarrow R_{i})\big{)}\mathbin{\mathchar 302\relax}P$ . By Axiom $\mathbf{S1}$ one obtains ${\it Th}\vdash P=Q$ .

The same reasoning applies when $M\mathbin{=}\emptyset$ but $J\mathbin{\neq}\emptyset$ . So henceforth I assume $J,M\mathbin{\neq}\emptyset$ . I now define a function $h\mathop{:}J\mathbin{\rightarrow}M$ with ${\it Th}\mathbin{\vdash}R_{j}\mathbin{=}R_{h(j)}$ for all $j\mathbin{\in}J$ .

Let $j\in J$ . Since $P\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$ \tau $}$ \hskip 2.5pt}\hfil}} $}}}R_{j}$ , by Def. 4 $Q\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime}$ for some $Q^{\prime}$ with $R_{j}\sqsupseteq_{CS}^{\Delta}Q^{\prime}$ , and $Q^{\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}Q^{\prime\prime}$ for some $Q^{\prime\prime}$ with $Q^{\prime\prime}\sqsupseteq_{CS}^{\Delta}R_{j}$ . There must be an $m\in M$ with $Q^{\prime\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R_{m}$ . By Def. 4 $R_{j}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime}$ for some $R^{\prime}$ with $R_{m}\sqsupseteq_{CS}^{\Delta}R^{\prime}$ , and $R^{\prime}\mathrel{\mathrel{\hbox{$ \mathop{\hbox to15.00002pt{ $\mathord{=}\mkern-6.0mu\cleaders\hbox{$ \mkern-2.0mu\mathord{=}\mkern-2.0mu $}\hfill\mkern-6.0mu\mathord{\Rightarrow}$ }}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt $\scriptstyle\raisebox{0.56001pt}{\scriptsize$$}$ \hskip 2.5pt}\hfil}} $}}}R^{\prime\prime}$ for some $R^{\prime\prime}$ with $R^{\prime\prime}\sqsupseteq_{CS}^{\Delta}R_{m}$ . By the shape of $R_{j}$ one has $R^{\prime\prime}=R^{\prime}=R_{j}$ , so $R_{j}\equiv_{CS}^{\Delta}R_{m}$ . By (*) above ${\it Th}\vdash R_{j}=R_{m}$ . Take $h(j):=m$ .

By the same reasoning there is a function $e\mathop{:}M\rightarrow J$ with ${\it Th}\mathbin{\vdash}R_{m}\mathbin{=}R_{e(m)}$ for all $m\mathbin{\in}M$ . Using Axioms I1–3 one obtains ${\it Th}\vdash 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 $\tau$ -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 [16, 18].

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 [13], 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 [4]. Unfortunately, failures-divergences equivalence fails to be a congruence for the left-merge, and the same problems exists for any other models of CSP [9, Section 3.2.1]. In [2] an alternative left-merge is proposed, for which failures-divergences equivalence, and also $\equiv_{CS}^{\Delta}$ , is a congruence. It might be used to eliminate the expansion law $\mathbf{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 [4]), although valid in the failures-divergences model, is not valid for $\equiv_{CS}^{\Delta}$ . This leaves the question of how to better manage the axiomatisation of parallel composition entirely open.

Bibliography18

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1]
2[2] 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: http://dx.doi.org/10.1007/3-540-54430-5˙82 .
3[3] 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 t h superscript 3 𝑡 ℎ 3^{th} IFIP WG 2.2 working conference, Ebberup 1986, North-Holland, Amsterdam, pp. 77–103.
4[4] J.A. Bergstra & J.W. Klop (1984): Process Algebra for Synchronous Communication . Inform. and Control 60, pp. 109–137, doi: http://dx.doi.org/10.1016/S 0019-9958(84)80025-X .
5[5] 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: http://dx.doi.org/10.1145/828.833 .
6[6] 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: http://dx.doi.org/10.1007/3-540-15670-4˙14 .
7[7] 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: http://dx.doi.org/10.1016/S 0019-9958(85)80048-6 .
8[8] 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. CONCUR’93, LNCS 715, Springer, pp. 66–81, doi: http://dx.doi.org/10.1007/3-540-57208-2 6 .

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

A Branching Time Model of CSP

Abstract

1 Introduction

2 CSP

3 The Failures-Divergences Model of CSP

Definition 1

4 A Complete Axiomatisation

Definition 2

Definition 3

5 Other Models of CSP

6 Divergence-Preserving Coupled Similarity

Definition 4

Proposition 1

Proof

Proposition 2

Proof

Proposition 3

Proof

7 Congruence Properties

Proposition 4

Proof

Proposition 5

Proof

Proposition 6

Proof

Proposition 7

Proof

Proposition 8

Proof

Proposition 9

Proof

Proposition 10

Proof

Proposition 11

Proof

Proposition 12

Proof

8 A Complete Axiomatisation of ≡CSΔ\equiv_{CS}^{\Delta}≡CSΔ​

Definition 5

9 Soundness

Definition 6

Proposition 13

Proof

Proposition 14

Proof

Proposition 15

Proof

Proposition 16

Proof

Proposition 17

Proof

Proposition 18

Proof

Proposition 19

Proof

Proposition 20

Proof

Proposition 21

Proof

Proposition 22

Proof

Proposition 23

Proof

Proposition 24

Proof

Proposition 25

Proof

Proposition 26

Proof

Proposition 27

Proof

Proposition 28

Proof

10 Completeness

8 A Complete Axiomatisation of $\equiv_{CS}^{\Delta}$