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

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:

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

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):

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

The trace merge operator \bowtie is defined as follows:

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

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.