Pi-Calculus

The π-calculus differs from other models of communicating behaviour mainly in its treatment of mobility. The movement of a piece of data inside a computer program is treated exactly the same as the transfer of a message - or indeed an entire computer program - across the internet. One can also describe networks which reconfigure themselves.

The calculus is very simple but powerful. Its most prominent notion is that of a name, and it has two important ingredients: the concept of behavioural (or observational) equivalence, and the use of a new theory of types to classify patterns of interactive behaviour.

(Milner 1999)

Syntax

Prefixes

Processes evolve by performing actions. The capabilities for action are expressed via the prefixes, of which there are four kinds:

\[ \pi ::= \overline{x}y \mid x(z) \mid \tau \mid [x=y]\pi \]

(Sangiorgi and Walker 2003, 11)

Agents

\begin{align*} P ::=\,& 0 \tag{Nil}\\ \,& \alpha.P \tag{Prefix}\\ \,& P + P \tag{Sum}\\ \,& P \mid P \tag{Parallel}\\ \,& \texttt{if } x = y \texttt{ then } P \tag{Match}\\ \,& \texttt{if } x \neq y \texttt{ then } P \tag{Missmatch}\\ \,& (\nu x)P \tag{Restriction}\\ \,& A(y_1 , \ldots, y_n) \tag{Identifier} \end{align*}

References:

Milner, Robin. 1999. Communicating and Mobile Systems: The Pi Calculus. Cambridge university press.

Sangiorgi, Davide, and David Walker. 2003. The Pi-Calculus: A Theory of Mobile Processes. Cambridge university press.