CCS (Calculus of Communicating Systems) is a process calculus, one of the major models of concurrency, intended for modeling communications between two participants

CCS, the Calculus of Communicating Systems, is a model of concurrency that describes interactions between two participants. Its primitives cover synchronization across channels, parallel composition and choice between actions.

Syntax

$$\begin{align*} \alpha ::= &&& \hspace{-1em} \text{action} \\ & a && \text{input on channel \(a\)} \\ & \bar a && \text{output on channel \(a\)} \\ & \tau && \text{internal transition} \\ P ::= &&&\hspace{-1em} \text{process} \\ & M && \text{named process} \\ & 0 && \text{empty process} \\ & \alpha.P_1 && \text{perform action \(\alpha\) then continue as \(P\)} \\ & P_1 + P_2 && \text{non-deterministic choice: perform \(P_1\) or \(P_2\)} \\ & P_1 \mid P_2 && \text{parallel composition: \(P_1\) in parallel with \(P_2\)} \\ & \nu a.P_1 && \text{restriction: the scope of the channel name \(a\) is \(P_1\)} \\ \end{align*}$$

Processes can be defined recursively. Two formalisms exist:

  • Recursive definitions: $M_1 \stackrel{\mathrm{def}}= P_1 \mathrel; \ldots \mathrel; M_n \stackrel{\mathrm{def}}= P_n$
  • Fixpoint combinator: $P ::= \ldots \mid \mu M.P_1$

Semantics

The behavior of a process is described as a labelled transition system. The core rules are:

  • a process $\alpha.P$ can trigger the action $\alpha$;
  • when two processes emit corresponding input and output actions in parallel, their composition performs an internal transition.

$$ \alpha.P \stackrel{\alpha}\longrightarrow P \hspace{4em} \dfrac{P \stackrel{a}\longrightarrow P' \quad Q \stackrel{\bar a}\longrightarrow Q'} {P \mid \bar Q \stackrel{\tau}\longrightarrow P' \mid Q'} \\ $$

The semantic equivalence of two processes is defined through bisimilarity.

References

history | excerpt history