Tag Info

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.