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

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.

Related

Journal. Information and Computation [inco]

https://www.sciencedirect.com/journal/information-and-computation

Information and Computation welcomes original papers in all areas of theoretical computer science and computational applications of information theory. Survey articles of exceptional quality will also be considered.