Person. Matthew Hennessy [mhennessy]

Research Professor
Trinity College, Dublin
https://www.scss.tcd.ie/Matthew.Hennessy

Backlinks

CCS with Termination [loc-0051]

July 25, 2026
Liam O'Connor

As part of Xin Lu's project we needed to come up with a version of CCS that supports explicit termination in the style of ACP. There is a paper by Luca Aceto and Matthew Hennessy which introduces a termination predicate, but they require that a nondeterministic choice $P + Q$ is judged terminating (written $P + Q \checkmark$ ) only when both $P \checkmark$ and $Q \checkmark$ . In other words, a process is only terminating if it has no choice but to terminate.

In our case, we want a judgement for possible termination, not guaranteed termination. So we had to come up with our own notions. We've formalised this in Isabelle, but what follows is the same but presented as Forester notes. Eventually, these notes may become part of another research notebook or even lecture notes.

Definition. Syntax of (non-recursive) CCS [pa-0001]

Liam O'Connor

The Calculus of Communicating Systems (CCS) is a process algebra with the following basic syntax.

\begin {array}{lcll} \alpha & & & \text {(names)}\\ a & ::= & \alpha \mid \overline {\alpha } \mid \tau & \text {(actions, co-actions, and internal moves)}\\ P & ::= & \textbf {0} & \\ & \mid & a.P & \text {(action prefixing)} \\ & \mid & \sum _{i \in I} P_i & \text {(nondeterministic choice)} \\ & \mid & P | Q & \text {(parallel composition)} \\ & \mid & P \setminus \alpha & \text {(restriction)} \\ & \mid & P [ f ] & \text {(renaming)} \end {array}

In the above, $f$ denotes a valid renaming function that satisfies the side-condition $\forall a.\; f(\overline {a}) = \overline {f(a)}$ . Here we have naturally extended the co-action notation ( $\overline {\alpha }$ ) to an operation on actions $a$ , where $\overline {\overline {a}} = a$ and $\overline {\tau } = \tau$ .

We allow for infinite sums in nondeterministic choice. To recover finite choice, we use a two element index set like $\mathbb {B} = \{\top ,\bot \}$ , as follows:

P + Q \equiv \sum _{i \in \mathbb {B}} R_i\; \text {where}\ R_\top = P\ \text {and}\ R_\bot = Q

Definition. Operational semantics for (non-recursive) CCS [pa-0002]

Liam O'Connor

We assign an operational semantics to CCS by describing a series of transition rules $P \xrightarrow {a} Q$ inductively as follows:

\begin {gather*} \dfrac { }{a.P \xrightarrow {a} P} \quad \dfrac {P_k \xrightarrow {a} P'}{\sum _{i \in I} P_i \xrightarrow {a} P'} \\[2em] \dfrac { P \xrightarrow {a} P'}{P|Q \xrightarrow {a} P'|Q} \quad \dfrac { Q \xrightarrow {a} Q'}{P|Q \xrightarrow {a} P|Q'} \dfrac { P \xrightarrow {a} P' \quad Q \xrightarrow {\overline {a}} Q'}{P|Q \xrightarrow {\tau } P'|Q'} \\[2em] \dfrac { P \xrightarrow {a} P' \quad a \notin \{\alpha , \overline {\alpha }\}}{ P\setminus \alpha \xrightarrow {a} P' \setminus \alpha } \quad \dfrac { P \xrightarrow {a} P'}{ P [ f ] \xrightarrow {f(a)} P' [ f ]} \end {gather*}

Let the relation $P \xrightarrow {\sigma }^\ast Q$ denote the reflexive, transitive closure of the above step relation, where $\sigma$ denotes a finite trace (a finite sequence of actions):

\dfrac { }{P \xrightarrow {\varepsilon }^\ast P} \quad \dfrac {P \xrightarrow {a} P' \quad P' \xrightarrow {\sigma }^\ast Q}{P \xrightarrow {a\sigma }^\ast Q}

Definition. Partial trace semantics for (non-recursive) CCS [pa-0003]

Liam O'Connor

A simple denotational semantics for CCS is in terms of partial traces: finite sequences of actions.

\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {PT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {PT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \cup \{ \varepsilon \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {PT} & = & \{ \varepsilon \} \cup \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {PT} \\ \llbracket P|Q \rrbracket _\text {PT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {PT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {PT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {PT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {PT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {PT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {PT} \} \end {array}

The trace merge operator $\bowtie$ is defined as follows:

\begin {array}{lcl} \sigma \bowtie \varepsilon &=& \{\sigma \} \\ \varepsilon \bowtie \sigma &=& \{\sigma \} \\ a\sigma \bowtie b\rho &=& \{ a\varsigma \mid \varsigma \in \sigma \bowtie b\rho \} \\ &\cup & \{ b\varsigma \mid \varsigma \in a\sigma \bowtie \rho \} \\ &\cup & \{ \tau \varsigma \mid \varsigma \in \sigma \bowtie \rho \land a = \overline {b} \} \\ \end {array}

Theorem. Soundness and adequacy of partial trace semantics for (non-recursive) CCS [pa-0004]

Liam O'Connor

The finite partial trace denotational semantics of CCS gives exactly those finite partial traces reachable via the operational semantics.

\llbracket P \rrbracket _\text {PT} = \{ \sigma \mid \exists Q.\ P \xrightarrow {\sigma }^\ast Q \}

Proof.

Liam O'Connor

Proved by induction on $P$ .

Explicit termination for (non-recursive) CCS [pa-0005]

Liam O'Connor

We add to syntax of CCS an additional process constant, $\textbf {1}$ , which, like $\mathbf {0}$ , has no rules in the operational semantics, and whose finite partial traces are just $\llbracket \textbf {1} \rrbracket _\text {PT} = \{\varepsilon \}$ .

The difference between $\textbf {0}$ and $\textbf {1}$ only comes in once we introduce a notion of possible successful termination. Intuitively, we want the ability to denote when it is OK for a process to stop.

Definition. Possible termination predicate for CCS with $\textbf {1}$ [pa-0006]

Liam O'Connor

We define an inductive judgement $P \checkmark$ , where $P$ is a process in CCS augmented with an additional process constant $\textbf {1}$ :

\begin {gather*} \dfrac { }{ \textbf {1} \checkmark } \quad \dfrac {P_k \checkmark }{\sum _{i \in I} P_i \checkmark } \\[2em] \dfrac { P \checkmark \quad Q \checkmark }{P|Q \checkmark } \dfrac { P \checkmark }{ P\setminus \alpha \checkmark } \quad \dfrac { P \checkmark }{ P [ f ] \checkmark } \end {gather*}

Definition. Finite completed trace semantics for CCS with $\textbf {1}$ [pa-0007]

Liam O'Connor

We offer a denotational semantics for CCS augmented with a $\textbf {1}$ constant, denoting successful termination. Unlike our partial trace semantics, this semantics only includes finite completed traces — traces where the process has terminated.

\begin {array}{lcl} \llbracket \textbf {0} \rrbracket _\text {CT} & = & \emptyset \\ \llbracket \textbf {1} \rrbracket _\text {CT} & = & \{ \varepsilon \} \\ \llbracket a.P \rrbracket _\text {CT} & = & \{ a\sigma \mid \sigma \in \llbracket P \rrbracket _\text {CT} \}\\ \llbracket \sum _{i \in I} P_i \rrbracket _\text {CT} & = & \bigcup _{i \in I} \llbracket P_i \rrbracket _\text {CT} \\ \llbracket P|Q \rrbracket _\text {CT} & = & \bigcup _{\sigma \in \llbracket P \rrbracket _\text {CT}} \bigcup _{\rho \in \llbracket Q \rrbracket _\text {CT}} \sigma \bowtie \rho \\ \llbracket P \setminus \alpha \rrbracket _\text {CT} & = & \{ \sigma \in \llbracket P \rrbracket _\text {CT} \mid \alpha \notin \sigma \land \overline {\alpha } \notin \sigma \} \\ \llbracket P [ f ] \rrbracket _\text {CT} & = & \{ \hat {f}(\sigma ) \mid \sigma \in \llbracket P \rrbracket _\text {CT} \} \end {array}

The trace merge operator $\bowtie$ is defined exactly as in the partial trace semantics.

Theorem. Soundness and adequacy of finite completed trace semantics for CCS [pa-0008]

Liam O'Connor

The finite completed trace semantics of CCS gives exactly those finite partial traces reachable via the operational semantics that end in a terminating state.

\llbracket P \rrbracket _\text {CT} = \{ \sigma \mid \exists Q.\ P \xrightarrow {\sigma }^\ast Q \land Q \checkmark \}

Proof.

Liam O'Connor

Proved by induction on $P$ .

Definition. A translation to turn partial traces into completed traces [pa-0009]

Liam O'Connor

Define a syntactic transformation on CCS terms (augmented with $\textbf {1}$ ) $\Upsilon$ as follows:

\begin {array}{lcl} \Upsilon (\textbf {0}) &=& \textbf {1} \\ \Upsilon (\textbf {1}) &=& \textbf {1} \\ \Upsilon (a.P) &=& \textbf {1} + a.\Upsilon (P) \\ \Upsilon (\sum _{i \in I} P_i) &=& \textbf {1} + \sum _{i \in I} \Upsilon (P_i) \\ \Upsilon (P | Q) &=& \Upsilon (P) | \Upsilon (Q)\\ \Upsilon (P \setminus \alpha ) &=& \Upsilon (P) \setminus \alpha \\ \Upsilon (P [ f ]) &=& \Upsilon (P) [ f ] \end {array}

Theorem. Correctness of the $\Upsilon$ translation [pa-000A]

Liam O'Connor

Our syntactic transformation $\Upsilon$ gives a process whose completed traces are the same as the partial traces of the original process.

\llbracket P \rrbracket _\text {PT} = \llbracket \Upsilon (P) \rrbracket _\text {CT}

Proof.

Liam O'Connor

A very straightforward structural induction on $P$ , where each case follows from the definitions.

The Plotkin powerdomain [dt-0067]

Liam O'Connor

As before, let $X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A))$ be finite, non-empty sets of compact elements of a Scott domain $A$ . The Plotkin powerdomain construction is based on the following preorder, simply combining the orderings from the Hoare and Smyth constructions: $X \preceq _P Y\quad \text {iff}\quad X \preceq _H Y \land X \preceq _S Y$ This ordering is also called the Egli-Milner ordering. On a flat domain, it simplifies to: $A\sqsubseteq B\quad \text {iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot \})\subseteq B)$ Note that this is antisymmetric in the case of a flat domain, and the lub of a chain of sets can be found by taking the union of all elements of the chain if all elements contain $\bot$ If not, then the element without $\bot$ will be the least upper bound.

The failures of antisymmetry can only be observed in domains of height higher than one. Consider a set $\{x,y\}$ containing two elements. According to the induced equivalence from this preorder $\approx _P$ , this set would be considered equal to the set that contains those two elements plus any elements that lie between them on the information ordering: $\{x,y\} \approx _P \{ z \mid x \sqsubseteq z \sqsubseteq y \}$ The Plotkin powerdomain is sometimes called the convex powerdomain, due to the similarity of this to the geometric definition of convexity. Thus, we use the ideal completion trick (as with the Hoare and Smyth constructions) here to arrive at a definition of powerdomain that distinguishes between all three programs outlined in Remark [dt-0063].

Aside.

Liam O'Connor

There is a beautiful algebraic characterisation of Plotkin powerdomains in Matthew Hennessy Gordon Plotkin's paper, Full abstraction for a simple parallel programming language.

Related

Institution. Trinity College, Dublin [tcd]

Dublin, Ireland
https://www.tcd.ie

Contributions

Reference. Adding Action Refinement to a Finite Process Algebra [aceto-hennessy-1994]

December 1994
Luca Aceto, Matthew Hennessy
Information and Computation, Volume 115, Issue 2
10.1006/inco.1994.1096

Reference. Full abstraction for a simple parallel programming language [hennessy-plotkin-1979]

September 7, 1979
Matthew Hennessy, Gordon Plotkin
MFCS '79: Mathematical Foundations of Computer Science 1979
10.1007/3-540-09526-8_8