Process calculus

Definition

A process calculus is given by the following data.

1. A set of actions, usually names $a, b, \dots$, their co-names $\overline{a}, \overline{b}, \dots$, and an internal action $\tau$.
2. A grammar of process terms built from the inactive process $0$ by operators. Typical operators are action prefix $\alpha.P$, choice $P + Q$, parallel composition $P \mid Q$, restriction $(\nu a)P$, and recursion or replication.
3. An operational semantics: a labelled transition relation $P \xrightarrow{\alpha} P'$ on process terms, defined by inference rules for each operator. In it, a parallel composition can perform $\tau$ when one component does $a$ and the other does $\overline{a}$.
4. A behavioural equivalence, an equivalence relation on process terms, such as strong or weak bisimilarity, used to say when two processes behave the same.

The standard example is Milner's calculus of communicating systems (CCS). Its transition rules are the following, together with the symmetric rules for $+$ and $\mid$. Prefix: $\alpha.P \xrightarrow{\alpha} P$. Choice and parallel: if $P \xrightarrow{\alpha} P'$, then $P + Q \xrightarrow{\alpha} P'$ and $P \mid Q \xrightarrow{\alpha} P' \mid Q$. Communication: if $P \xrightarrow{a} P'$ and $Q \xrightarrow{\overline{a}} Q'$, then $P \mid Q \xrightarrow{\tau} P' \mid Q'$. Restriction: if $P \xrightarrow{\alpha} P'$ and $\alpha \notin \set{a, \overline{a}}$, then $(\nu a)P \xrightarrow{\alpha} (\nu a)P'$.