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

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