In theoretical computer science, the π-calculus (or pi-calculus) is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker in 1992, based on ideas by Uffe Engberg and Mogens Nielsen. It can be seen as a continuation of Milner's work on the process calculus CCS (Calculus of Communicating Systems). The π-calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation.
The π-calculus is elegantly simple yet very expressive. Functional programs can be encoded into the π-calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics. Extensions of the π-calculus, such as the spi calculus and applied π, have been successful in reasoning about cryptographic protocols. Beside the original use in describing concurrent systems, the π-calculus has also been used to reason about business processes and molecular biology.
Informal definition
The π-calculus belongs to the family of process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the π-calculus, like the λ-calculus, is so minimal that it does not contain primitives such as numbers, booleans, data structures, variables, functions, or even the usual flow control statements (such as if-then-else
, while
).
Process constructs
Central to the π-calculus is the notion of name. The simplicity of the calculus lies in the dual role that names play as communication channels and variables.
The process constructs available in the calculus are the following (a precise definition is given in the following section):
- concurrency, written $P\; \backslash mid\; Q$, where $P$ and $Q$ are two processes or threads executed concurrently.
- communication, where
- input prefixing $c\backslash left(x\backslash right).P$ is a process waiting for a message that was sent on a communication channel named $c$ before proceeding as $P$, binding the name received to the name $x$. Typically, this models either a process expecting a communication from the network or a label
c
usable only once by a goto c
operation.
- output prefixing $\backslash overline\{c\}\; \backslash langle\; y\; \backslash rangle.P$ describes that the name $y$ is emitted on channel $c$ before proceeding as $P$. Typically, this models either sending a message on the network or a
goto c
operation.
- replication, written $!\backslash ,P$, which may be seen as a process which can always create a new copy of $P$. Typically, this models either a network service or a label
c
waiting for any number of goto c
operations.
- creation of a new name, written $\backslash left(\backslash nu\; x\backslash right)P$, which may be seen as a process allocating a new constant $x$ within $P$. The constants of π-calculus are defined by their names only and are always communication channels. Creation of a new name in a process is also called restriction.
- the nil process, written 0, is a process whose execution is complete and has stopped.
Although the minimalism of the π-calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first-order functions, [2] put these various extensions on a formal footing by extending the π-calculus with arbitrary datatypes.
A small example
Below is a tiny example of a process which consists of three parallel components. The channel name $x$ is only known by the first two components.
- $$
\begin{align}
& \begin{align}
(\nu x) \; & ( \; \overline{x} \langle z \rangle . \; 0 \\
& | \; x(y). \; \overline{y}\langle x \rangle . \; x(y). \; 0 \; )
\end{align} \\
| \; & z(v) . \; \overline{v}\langle v \rangle . 0
\end{align}
The first two components are able to communicate on the channel $x$, and the name $y$ becomes bound to $z$. The next step in the process is therefore
- $$
\begin{align}
& \begin{align}
( \nu x) \; ( \; & 0 \\
| \; & \overline{z} \langle x \rangle . \; x(y). \; 0 \; )
\end{align}
\\
| \; & z(v). \; \overline{v}\langle v \rangle . \; 0
\end{align}
Note that the remaining $y$ is not affected because it is defined in an inner scope.
The second and third parallel components can now communicate on the channel name $z$, and the name $v$ becomes bound to $x$. The next step in the process is now
- $$
\begin{align}
(\nu x) ( \; & 0 \\
| \; & x(y). \; 0 \\
| \; & \overline{x}\langle x \rangle . \; 0 \; )
\end{align}
Note that since the local name $x$ has been output, the scope of $x$ is extended to cover the third component as well. Finally, the channel $x$ can be used for sending the name $x$. After that all concurrently executing processes have stopped
- $$
\begin{align}
(\nu x) ( \; & 0 \\
| \; 0 \\
| \; 0 \; )
\end{align}
Formal definition
Syntax
Let Χ be a set of objects called names. The abstract syntax for the π-calculus is built from the following BNF grammar (where x and y are any names from Χ):^{[1]}
- $$
\begin{align}
P ::= \, & x(y).P \,\,\, \\
|\,\,\, & \overline{x} \langle y \rangle.P \,\,\, \\
|\,\,\, & P|P \,\,\, \\
|\,\,\, & (\nu x)P \,\,\, \\
|\,\,\, & !P \,\,\, \\
|\,\,\, & 0
\end{align}
In the concrete syntax below, the prefixes bind more tightly than the parallel composition (|), and parentheses are used to disambiguate.
Names are bound by the restriction and input prefix constructs. Formally, the sets of free and bound names of a process in π–calculus are defined inductively as follows.
- The $0$ process has no free names and no bound names.
- The free names of $\backslash overline\{a\}\; \backslash langle\; x\; \backslash rangle.P$ are $a$, $x$, and the free names of $P$. The bound names of $\backslash overline\{a\}\; \backslash langle\; x\; \backslash rangle.P$ are the bound names of $P$.
- The free names of $a(x).P$ are $a$ and the free names of $P$, except for $x$. The bound names of $a(x).P$ are $x$ and the bound names of $P$.
- The free names of $P|Q$ are those of $P$ together with those of $Q$. The bound names of $P|Q$ are those of $P$ together with those of $Q$.
- The free names of $(\backslash nu\; x).P$ are those of $P$, except for $x$. The bound names of $(\backslash nu\; x).P$ are $x$ and the bound names of $P$.
- The free names of $!P$ are those of $P$. The bound names of $!P$ are those of $P$.
Structural congruence
Central to both the reduction semantics and the labelled transition semantics is the notion of structural congruence. Two processes are structurally congruent, if they are identical up to structure. In particular, parallel composition is commutative and associative.
More precisely, structural congruence is defined as the least equivalence relation preserved by the process constructs and satisfying:
Alpha-conversion:
- $P\; \backslash equiv\; Q$ if $Q$ can be obtained from $P$ by renaming one or more bound names in $P$.
Axioms for parallel composition:
- $P|Q\; \backslash equiv\; Q|P$
- $(P|Q)|R\; \backslash equiv\; P|(Q|R)$
- $P\; |\; 0\; \backslash equiv\; P$
Axioms for restriction:
- $(\backslash nu\; x)(\backslash nu\; y)P\; \backslash equiv\; (\backslash nu\; y)(\backslash nu\; x)P$
- $(\backslash nu\; x)0\; \backslash equiv\; 0$
Axiom for replication:
- $!P\; \backslash equiv\; P|!P$
Axiom relating restriction and parallel:
- $(\backslash nu\; x)(P\; |\; Q)\; \backslash equiv\; (\backslash nu\; x)P\; |\; Q$ if $x$ is not a free name of $Q$.
This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how a bound name $x$ may be extruded by an output action, causing the scope of $x$ to be extended. In cases where $x$ is a free name of $Q$, alpha-conversion may be used to allow extension to proceed.
Reduction semantics
We write $P\; \backslash rightarrow\; P\text{'}$ if $P$ can perform a computation step, following which it is now $P\text{'}$.
This reduction relation $\backslash rightarrow$ is defined as the least relation closed under a set of reduction rules.
The main reduction rule which captures the ability of processes to communicate through channels is the following:
- $\backslash overline\{x\}\backslash langle\; z\; \backslash rangle.P\; |\; x(y).Q\; \backslash rightarrow\; P\; |\; Q[z/y]$
- where $Q[z/y]$ denotes the process $Q$ in which the free name $z$ has been substituted for the free occurrences of $y$. If a free occurrence of $y$ occurs in a location where $z$ would not be free, alpha-conversion may be required.
There are three additional rules:
- If $P\; \backslash rightarrow\; Q$ then also $P|R\; \backslash rightarrow\; Q|R$.
- This rule says that parallel composition does not inhibit computation.
- If $P\; \backslash rightarrow\; Q$, then also $(\backslash nu\; x)P\; \backslash rightarrow\; (\backslash nu\; x)Q$.
- This rule ensures that computation can proceed underneath a restriction.
- If $P\; \backslash equiv\; P\text{'}$ and $P\text{'}\; \backslash rightarrow\; Q\text{'}$ where $Q\text{'}\; \backslash equiv\; Q$, then also $P\; \backslash rightarrow\; Q$.
The latter rule states that processes that are structurally congruent have the same reductions.
The example revisited
Consider again the process
- $(\backslash nu\; x)(\backslash overline\{x\}\; \backslash langle\; z\; \backslash rangle.0\; |\; x(y).\; \backslash overline\{y\}\backslash langle\; x\; \backslash rangle\; .\; x(y).0\; )\; |\; z(v)\; .\; \backslash overline\{v\}\backslash langle\; v\; \backslash rangle.\; 0$
Applying the definition of the reduction semantics, we get the reduction
- $(\backslash nu\; x)(\backslash overline\{x\}\; \backslash langle\; z\; \backslash rangle.0\; |\; x(y).\; \backslash overline\{y\}\backslash langle\; x\; \backslash rangle\; .\; x(y).0\; )\; |\; z(v)\; .\; \backslash overline\{v\}\backslash langle\; v\; \backslash rangle.\; 0\; \backslash rightarrow\; (\backslash nu\; x)(0|\; \backslash overline\{z\}\backslash langle\; x\; \backslash rangle\; .\; x(y).\; 0\; )\; |\; z(v).\; \backslash overline\{v\}\backslash langle\; v\; \backslash rangle\; .0$
Note how, applying the reduction substitution axiom, occurrences of $y$ are now labeled as $z$.
Next, we get the reduction
- $(\backslash nu\; x)(0|\; \backslash overline\{z\}\backslash langle\; x\; \backslash rangle\; .\; x(y).\; 0\; )\; |\; z(v).\; \backslash overline\{v\}\backslash langle\; v\; \backslash rangle\; .0\; \backslash rightarrow\; (\backslash nu\; x)(0|\; x(y).\; 0\; |\; \backslash overline\{x\}\backslash langle\; x\; \backslash rangle\; .0)$
Note that since the local name $x$ has been output, the scope of $x$ is extended to cover the third component as well. This was captured using the scope extension axiom.
Labelled semantics
Alternatively, one may give the pi-calculus a labelled transition semantics (as has been done with the Calculus of Communicating Systems). Transitions in this semantics are of the form:
- $P\backslash ,\backslash xrightarrow\backslash alpha\backslash ,P\text{'}$
This notation signifies that $P$ after the action $\backslash alpha$ becomes $P\text{'}$. $\backslash alpha$ can be an input action $a(x)$, an output action $\backslash overline\{a\}\backslash langle\; x\; \backslash rangle$, or a tau-action $\backslash tau$ corresponding to an internal communication.
A standard result about the labelled semantics is that it agrees with the reduction semantics in the sense that $P\; \backslash rightarrow\; P\text{'}$ if and only if $P\backslash ,\backslash xrightarrow\backslash tau\backslash ,P\text{'}$
for some action $\backslash tau$.
Extensions and variants
The syntax given above is a minimal one. However, the syntax may be modified in various ways.
A nondeterministic choice operator $P\; +\; Q$ can be added to the syntax.
A test for name equality $[x=y]P$ can be added to the syntax. This match operator can proceed as $P$ if and only if $x$ and $y$ are the same name.
Similarly, one may add a mismatch operator for name inequality. Practical programs which can pass names (URLs or pointers) often use such functionality: for directly modelling such functionality inside the calculus, this and related extensions are often useful.
The asynchronous π-calculus allows only outputs with no suffix, i.e. output atoms of the form $\backslash overline\{x\}\backslash langle\; y\; \backslash rangle$, yielding a smaller calculus. However, any process in the original calculus can be represented by the smaller asynchronous π-calculus using an extra channel to simulate explicit acknowledgement from the receiving process. Since a continuation-free output can model a message-in-transit, this fragment shows that the original π-calculus, which is intuitively based on synchronous communication, has an expressive asynchronous communication model inside its syntax. However, the nondeterministic choice operator defined above cannot be expressed in this way, as an unguarded choice would be converted into a guarded one; this fact has been used to demonstrate that the asynchronous calculus is strictly less expressive than the synchronous one (with the choice operator).^{[2]}
The polyadic π-calculus allows communicating more than one name in a single action: $\backslash overline\{x\}\backslash langle\; z\_1,...z\_n\backslash rangle.P$ (polyadic output) and $x(z\_1,...z\_n)$ (polyadic input). This polyadic extension, which is useful especially when studying types for name passing processes, can be encoded in the monadic calculus by passing the name of a private channel through which the multiple arguments are then passed in sequence. The encoding is defined recursively by the clauses
$\backslash overline\{x\}\backslash langle\; y\_1,\backslash cdots,y\_n\backslash rangle.P$ is encoded as $(\backslash nu\; w)\; \backslash overline\{x\}\backslash langle\; w\; \backslash rangle.\backslash overline\{w\}\backslash langle\; y\_1\backslash rangle.\backslash cdots.\backslash overline\{w\}\backslash langle\; y\_n\backslash rangle.[P]$
$x(y\_1,\backslash cdots,y\_n).P$ is encoded as $x(w).w(y\_1).\backslash cdots.w(y\_n).[P]$
All other process constructs are left unchanged by the encoding.
In the above, $[P]$ denotes the encoding of all prefixes in the continuation $P$ in the same way.
The full power of replication $!P$ is not needed. Often, one only considers replicated input $!\; x(y).P$, whose structural congruence axiom is $!\; x(y).P\; \backslash equiv\; x(y).P\; |!x(y).P$.
Replicated input process such as $!x(y).P$ can be understood as servers, waiting on channel
$x$ to be invoked by clients. Invocation of a server spawns a new copy of
the process $P[a/y]$, where a is the name passed by the client to the
server, during the latter's invocation.
A higher order π-calculus can be defined where not only names but processes are sent through channels.
The key reduction rule for the higher order case is
$\backslash overline\{x\}\backslash langle\; R\; \backslash rangle.P\; |\; x(Y).Q\; \backslash rightarrow\; P\; |\; Q[R/Y]$
Here, $Y$ denotes a process variable which can be instantiated by a process term. Sangiorgi
established that the ability to pass processes does not
increase the expressivity of the π-calculus: passing a process P can be
simulated by just passing a name that points to P instead.
Properties
Turing completeness
The π-calculus is a universal model of computation. This was first observed by Milner in his paper "Functions as Processes",^{[3]} in which he presents two encodings of the lambda-calculus in the π-calculus. One encoding simulates the eager (call-by-value) evaluation strategy, the other encoding simulates the normal-order (call-by-name) strategy. In both of these, the crucial insight is the modeling of environment bindings – for instance, "$x$ is bound to term $M$" – as replicating agents that respond to requests for their bindings by sending back a connection to the term $M$.
The features of the π-calculus that make these encodings possible are name-passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the π-calculus ceases to be Turing-powerful. This can be seen by the fact that bisimulation equivalence becomes decidable for the recursion-free calculus and even for the finite-control π-calculus where the number of parallel components in any process is bounded by a constant.^{[4]}
Bisimulations in the π-calculus
As for process calculi, the π-calculus allows for a definition of bisimulation equivalence. In the π-calculus, the definition of bisimulation equivalence (also known as bisimilarity) may be based on either the reduction semantics or on the labelled transition semantics.
There are (at least) three different ways of defining labelled bisimulation equivalence in the π-calculus: Early, late and open bisimilarity. This stems from the fact that the π-calculus is a value-passing process calculus.
In the remainder of this section, we let $p$ and $q$ denote processes and $R$ denote binary relations over processes.
Early and late bisimilarity
Early and late bisimilarity were both discovered by Milner, Parrow and Walker in their original paper on the π-calculus.^{[5]}
A binary relation $R$ over processes is an early bisimulation if for every pair of processes $(p,\; q)\; \backslash in\; R$,
p \,\xrightarrow{a(x)}\,p'
then for every name $y$ there exists some $q\text{'}$ such that $q\; \backslash ,\backslash xrightarrow\{a(x)\}\backslash ,q\text{'}$ and $(p\text{'}[y/x],q\text{'}[y/x])\; \backslash in\; R$;
- for any non-input action $\backslash alpha$, if $$
p \xrightarrow\alpha p'
then there exists some $q\text{'}$ such that $$
q \xrightarrow\alpha q'
and $(p\text{'},q\text{'})\; \backslash in\; R$;
- and symmetric requirements with $p$ and $q$ interchanged.
Processes $p$ and $q$ are said to be early bisimilar, written $p\; \backslash sim\_e\; q$ if the pair $(p,q)\; \backslash in\; R$ for some early bisimulation $R$.
In late bisimilarity, the transition match must be independent of the name being transmitted.
A binary relation $R$ over processes is a late bisimulation if for every pair of processes $(p,\; q)\; \backslash in\; R$,
p \xrightarrow{a(x)} p'
then for some $q\text{'}$ it holds that $q\; \backslash xrightarrow\{a(x)\}\; q\text{'}$ and $(p\text{'}[y/x],q\text{'}[y/x])\; \backslash in\; R$ for every name y;
- for any non-input action $\backslash alpha$, if $$
p \xrightarrow\alpha p'
implies that there exists some $q\text{'}$ such that $$
q \xrightarrow\alpha q'
and $(p\text{'},q\text{'})\; \backslash in\; R$;
- and symmetric requirements with $p$ and $q$ interchanged.
Processes $p$ and $q$ are said to be late bisimilar, written $p\; \backslash sim\_l\; q$ if the pair $(p,q)\; \backslash in\; R$ for some late bisimulation $R$.
Both $\backslash sim\_e$ and $\backslash sim\_l$ suffer from the problem that they are not congruence relations in the sense that they are not preserved by all process constructs. More precisely, there exist processes $p$ and $q$ such that $p\; \backslash sim\_e\; q$ but $a(x).p\; \backslash not\; \backslash sim\_e\; a(x).q$. One may remedy this problem by considering the maximal congruence relations included in $\backslash sim\_e$ and $\backslash sim\_l$, known as early congruence and late congruence, respectively.
Open bisimilarity
Fortunately, a third definition is possible, which avoids this problem, namely that of open bisimilarity, due to Sangiorgi.^{[6]}
A binary relation $R$ over processes is an open bisimulation if for every pair of elements $(p,\; q)\; \backslash in\; R$ and for every name substitution $\backslash sigma$ and every action $\backslash alpha$, whenever $p\backslash sigma\; \backslash xrightarrow\backslash alpha\; p\text{'}$ then there exists some $q\text{'}$ such that $q\backslash sigma\; \backslash xrightarrow\backslash alpha\; q\text{'}$
and $(p\text{'},q\text{'})\; \backslash in\; R$.
Processes $p$ and $q$ are said to be open bisimilar, written $p\; \backslash sim\_o\; q$ if the pair $(p,q)\; \backslash in\; R$ for some open bisimulation $R$.
Early, late and open bisimilarity are distinct
Early, late and open bisimilarity are distinct. The containments are proper, so $\backslash sim\_o\; \backslash subsetneq\; \backslash sim\_l\; \backslash subsetneq\; \backslash sim\_e$.
In certain subcalculi such as the asynchronous pi-calculus, late, early and open bisimilarity are known to coincide. However, in this setting a more appropriate notion is that of asynchronous bisimilarity.
The reader should note that, in the literature, the term open bisimulation usually refers to a more sophisticated notion, where processes and relations are indexed by distinction relations; details are in Sangiorgi's paper cited above.
Barbed equivalence
Alternatively, one may define bisimulation equivalence directly from the reduction semantics. We write $p\; \backslash Downarrow\; a$ if process $p$ immediately allows an input or an output on name $a$.
A binary relation $R$ over processes is a barbed bisimulation if it is a symmetric relation which satisfies that for every pair of elements $(p,\; q)\; \backslash in\; R$ we have that
- (1) $p\; \backslash Downarrow\; a$ if and only if $q\; \backslash Downarrow\; a$ for every name $a$
and
- (2) for every reduction $p\; \backslash rightarrow\; p\text{'}$ there exists a reduction $q\; \backslash rightarrow\; q\text{'}$
such that $(p\text{'},q\text{'})\; \backslash in\; R$.
We say that $p$ and $q$ are barbed bisimilar if there exists a barbed bisimulation $R$ where $(p,q)\; \backslash in\; R$.
Defining a context as a π term with a hole [] we say that two processes P and Q are barbed congruent, written $P\; \backslash sim\_b\; Q\backslash ,\backslash !$, if for every context $C[]$ we have that $C[P]$ and $C[Q]$ are barbed bisimilar. It turns out that barbed congruence coincides with the congruence induced by early bisimilarity.
Applications
The π-calculus has been used to describe many different kinds of concurrent systems. In fact, some of the most recent applications lie outside the realm of computer science.
In 1997, [4], due to Andrew Gordon and Alan Jeffrey, which uses Woo and Lam's method of correspondence assertions as the basis for type systems that can check for authentication properties of cryptographic protocols.
Around 2002, Howard Smith and Peter Fingar became interested in using the π-calculus as a description tool for modelling business processes. As of July 2006, there is discussion in the community as to how useful this will be. Most recently, the π-calculus has been used as the theoretical basis of Business Process Modeling Language (BPML), and of Microsoft's XLANG.^{[7]}
The π-calculus has also attracted interest in molecular biology. In 1999, Aviv Regev and Ehud Shapiro showed that one can describe a cellular signaling pathway (the so-called RTK/MAPK cascade) and in particular the molecular "lego" which implements these tasks of communication in an extension of the π-calculus.^{[8]} Following this seminal paper, other authors described the whole metabolic network of a minimal cell.^{[9]}
Implementations
The following programming languages are implementations either of the π-calculus or of its variants:
- Acute
- Business Process Modeling Language (BPML)
- Nomadic Pict
- jumel : a compiler for a dialect of ML augmented with pi-calculus primitives for message-passing
- occam-π
- Pict
- JoCaml (based on the Join-calculus)
- Funnel (A JRE-compatible join calculus implementation)
- The CubeVM (a stackless implementation)
- The SpiCO language: a stochastic pi-calulus for concurrent objects
- SPiM: simulators for the stochastic pi-calculus
- Ateji PX: a Java language extension with parallel primitives inspired from π-calculus
- The Masterkube Platform: a web based system completely created having pi-calculus as the base. Also listed as one of the top innovation of 2011 conducted by FICCI, Directorate of Sciences India, Lockheed and Martin
Notes
References
External links
- PiCalculus on the C2 wiki
- Jeannette M. Wing
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.