Pi-calculus

In theoretical computer science, the pi-calculus is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems). The aim of the pi-calculus is to be able to describe concurrent computations whose configuration may change during the computation.

Informal definition

The pi-calculus belongs to the family of process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the pi-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 pi-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 mid Q, where P and Q are two processes or threads executed concurrently.
* "communication", where
** "input prefixing" cleft(x ight).P is a process waiting for a message that was sent on a communication channel named c before proceeding as nowrap|P, binding the name received to the name nowrap|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" overline{c} langle y angle.P describes that the name y is emitted on channel c before proceeding as nowrap|P. Typically, this models either sending a message on the network or a goto c operation.
* "replication", written !,P, which may be seen as a process which can always create a new copy of nowrap|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 left( u x ight)P, which may be seen as a process allocating a new constant x within nowrap|P. As opposed to functional programming's let x=... in... operation, the constants of nowrap|pi-calculus are defined by their name only and are always communication channels.
* the nil process, written "0", is a process whose execution is complete and has stopped.

Although the minimality of the pi-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, truth values, lists and integers. Moreover, extensions of the nowrap|pi-calculus have been proposed which take into account distribution or public-key cryptography. The "applied nowrap|pi-calculus" due to Abadi and Fournet [http://citeseer.ist.psu.edu/rd/0%2C573109%2C1%2C0.25%2CDownload/http%3AqSqqSqwww.cse.ucsc.eduqSq%7EabadiqSqPapersqSqisss02.pdf] puts these various extensions on a formal footing by extending the nowrap|pi-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.

: ( u x)(overline{x} langle z angle.0 | x(y). overline{y}langle x angle . x(y).0 ) | z(v) . overline{v}langle v angle. 0

The first two components are able to communicate on the channel x, and the name z becomes bound to y. The continuation of the process is therefore

: ( u x)(0| overline{z}langle x angle . x(y). 0 ) | z(v). overline{v}langle v angle .0

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 x is bound to v. The continuation of the process is now

: ( u x)(0| x(y). 0 | overline{x}langle x angle .0)

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.

Formal definition

Syntax

Let Χ be a set of objects called "names". The "processes" of pi-calculus are built from names by the syntax (where "x" and "y" are any names from Χ)

:egin{matrix}P ::= & x(y).P\
& overline{x} langle y angle.P \
& P;|;P \
& ( u x)P \
& !P \
& 0end{matrix}

Names can be bound by the restriction and input prefix constructs. The sets of free and bound names of a process in pi–calculus are defined inductively as follows.

* The 0 process has no free names and no bound names.

* The free names of overline{a} langle x angle.P are a, x, and the free names of P. The bound names of overline{a} langle x angle.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 ( u x).P are those of P, except for x. The bound names of ( u 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 equiv Q if Q can be obtained from P by renaming one or more bound names in P.

"Axioms for parallel composition":

:* P|Q equiv Q|P :* (P|Q)|R equiv P|(Q|R):*P | 0 equiv P

"Axioms for restriction":

:* ( u x)( u y)P equiv ( u y)( u x)P:* ( u x)0 equiv 0

"Axiom for replication":

:* !P equiv P|!P

"Axiom relating restriction and parallel":

:* ( u x)(P | Q) equiv ( u 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.

Reduction semantics

We write P ightarrow P' if P can perform a computation step, following which it is now P'.This "reduction relation" ightarrow 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:
* overline{x}langle z angle.P | x(y).Q ightarrow P | Q [z/y] : where Q [z/y] denotes the process Q in which the free name z has been "substituted" for the free name y. Note that this substitution may involve alpha-conversion to avoid name clashes.

There are three additional rules:
* If P ightarrow Q then also P|R ightarrow Q|R.: This rule says that parallel composition does not inhibit computation.
* If P ightarrow Q, then also ( u x)P ightarrow ( u x)Q.: This rule ensures that computation can proceed underneath a restriction.
* If P equiv P' and P' ightarrow Q' where Q' equiv Q, then also P ightarrow Q.

The latter rule states that processes that are structurally congruent have the same reductions.

The example revisited

Consider again the process

: ( u x)(overline{x} langle z angle.0 | x(y). overline{y}langle x angle . x(y).0 ) | z(v) . overline{v}langle v angle. 0

Applying the definition of the reduction semantics, we get the reduction

: ( u x)(overline{x} langle z angle.0 | x(y). overline{y}langle x angle . x(y).0 ) | z(v) . overline{v}langle v angle. 0 ightarrow ( u x)(0| overline{z}langle x angle . x(y). 0 ) | z(v). overline{v}langle v angle .0

Next, we get the reduction

: ( u x)(0| overline{z}langle x angle . x(y). 0 ) | z(v). overline{v}langle v angle .0 ightarrow ( u x)(0| x(y). 0 | overline{x}langle x angle .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,xrightarrowalpha,P'

This notation signifies that P after the action alpha becomes P'. alpha can be an "input action" a(x), an "output action" "alangle x angle", or a tau-action au 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 ightarrow P' if and only if P,xrightarrow au,P'for some action au.

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 pi-calculus" allows only outputs with no continuation, i.e. output atoms of the form overline{x}langle y angle, yielding a smaller calculus. However, any process in the original calculus can be represented by the smaller asynchronous pi-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 pi-calculus, which is intuitively based on synchronous communication, has an expressive asynchronous communication model inside its syntax.

The "polyadic pi-calculus" allows communicating more than one name in a single action: overline{x}.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

overline{x}langle y_1,cdots,y_n angle.P is encoded as ( u w) overline{x}langle w angle.overline{w}langle y_1 angle.cdots.overline{w}langle y_n angle. [P]

x(y_1,cdots,y_n).P is encoded as x(w).w(y_1).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 equiv x(y).P | !x(y).P.

Replicated input process such as !x(y).P can be understood as servers, waiting on channelx to be invoked by clients. Invocation of a server spawns a new copy ofthe process P [a/y] , where a is the name passed by the client to the server, during the latter's invocation.

A "higher order pi-calculus" can be defined where not only names but processes are sent through channels.The key reduction rule for the higher order case is

overline{x}langle R angle.P | x(Y).Q ightarrow P | Q [R/Y]

Here, Y denotes a "process variable" which can be instantiated by a process term. Sangiorgi established the surprising result that the ability to pass processes does not increase the expressivity of the pi-calculus: passing a process "P" can be simulated by just passing a name that points to "P" instead.

Properties

Turing completeness

The pi-calculus is a universal model of computation. This was first observed by Milner in his paper "Functions as Processes" (Mathematical Structures in Computer Science,Vol. 2, pp. 119-141, 1992), in which he presents two encodings of the lambda-calculus in the pi-calculus. One encoding simulates the call-by-value reduction strategy, the other encoding simulates the lazy (call-by-name) strategy.

The features of the pi-calculus that make these encodings possible are name-passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the pi-calculus ceases to be Turing-powerful. This can be seen by the fact the bisimulation equivalence becomes decidable for the recursion-free calculus and even for the finite-control pi-calculus where the number of parallel components in any process is bounded by a constant (Mads Dam: On the Decidability of Process Equivalences for the pi-Calculus. Theoretical Computer Science 183, 1997, pp. 215-228.)

Bisimulations in the pi-calculus

As for process calculi, the pi-calculus allows for a definition of bisimulation equivalence. In the pi-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 pi-calculus: Early, late and open bisimilarity. This stems from the fact that the pi-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 pi-calculus. [cite journal|last=Milner|first=R.|coauthors=J. Parrow and D. Walker|title=A calculus of mobile processes|journal=Information and Computation|issue=100|pages=1--40|year=1992|doi=10.1016/0890-5401(92)90008-4|volume=100]

A binary relation R over processes is an "early bisimulation" if for every pair of processes (p, q) in R,
* whenever p ,xrightarrow{a(x)},p' then for every name y there exists some q' such that q ,xrightarrow{a(x)},q' and (p' [y/x] ,q' [y/x] ) in R;
* for any non-input action alpha, if p xrightarrowalpha p' then there exists some q' such that q xrightarrowalpha q' and (p',q') in R;
* and symmetric requirements with p and q interchanged.

Processes p and q are said to be early bisimilar, written p sim_e q if the pair (p,q) in R for some early bisimulation R. sim_e

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) in R,
* whenever p xrightarrow{a(x)} p' then for some q' it holds that q xrightarrow{a(x)} q' and (p' [y/x] ,q' [y/x] ) in R "for every name y";
*for any non-input action alpha, if p xrightarrowalpha p' implies that there exists some q' such that q xrightarrowalpha q' and (p',q') in R;
* and symmetric requirements with p and q interchanged.Processes p and q are said to be late bisimilar, written p sim_l q if the pair (p,q) in R for some late bisimulation R.

Both sim_e and 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 sim_e q but a(x)p ot sim_e a(x).q. One may remedy this problem by considering the maximal congruence relations included in sim_e and 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 [cite journal|last=Sangiorgi|first=D.|title=A theory of bisimulation for the pi-calculus|journal=Acta Informatica|volume=33|pages=69–97|year=1996|doi=10.1007/s002360050036] .

A binary relation R over processes is an "open bisimulation" if for every pair of elements (p, q) in R and for every name substitution sigma and every action alpha, whenever psigma xrightarrowalpha p' then there exists some q' such that qsigma xrightarrowalpha q' and (p',q') in R.

Processes p and q are said to be open bisimilar, written p sim_o q if the pair (p,q) in R for some open bisimulation R. sim_o

Early, late and open bisimilarity are in fact all distinct. The containments are proper, so sim_o subsetneq sim_l subsetneq 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 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) in R we have that

:(1) p Downarrow a if and only if q Downarrow a for every name a

and

:(2) for every reduction p ightarrow p' there exists a reduction q ightarrow q'

such that (p',q') in R.

We say that p and q are "barbed bisimilar" if there exists a barbed bisimulation R where (p,q) in R.

Definying a context as a π term with a hole [] we say that two processes P and Q are "barbed congruent", written P sim_b Q,! if for every context C [] we have that C [P] sim_b C [Q] ,!. It turns out that barbed congruence coincides with the congruence induced by early bisimilarity.

Applications

The pi-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, Martin Abadi and Andrew Gordon proposed an extension of the pi-calculus, the Spi-calculus, as a formal notation for describing and reasoning about cryptographic protocols. The spi-calculus extends the pi-calculus with primitives for encryption and decryption. There is now a large body of work devoted to variants of the spi-calculus, including a number of experimental verification tools. One example is the tool ProVerif [http://www.di.ens.fr/~blanchet/crypto-eng.html] due to Bruno Blanchet, based on a translation of the applied pi-calculus into Blanchet's logic programming framework. Another example is Cryptyc [http://www.cryptyc.org] , 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 pi-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 pi-calculus has been used as the theoretical basis of Business Process Modeling Language (BPML), and of Microsoft's XLANG. ["BPML | BPEL4WS: A Convergence Path toward a Standard BPM Stack." BPMI.org Position Paper. August 15, 2002. [http://www.bpmi.org/downloads/BPML-BPEL4WS.pdf] ]

The pi-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 pi-calculus. [cite journal|first=Aviv|last=Regev|authorlink=Aviv Regev|coauthors=William Silverman and Ehud Y. Shapiro|title=Representation and Simulation of Biochemical Processes Using the pi-Calculus Process Algebra|journal=Pacific Symposium on Biocomputing 2001|pages=459–470]

Implementations

The following programming languages are implementations either of the pi-calculus or of its variants:

* Acute
* Business Process Modeling Language (BPML)
* Nomadic Pict
* occam-π
* Pict
* JoCaml (based on the Join-calculus a variant of pi-calculus)
* Funnel (A JRE-compatible join calculus implementation)
* The [http://www-poleia.lip6.fr/~pesch/cube/about.html CubeVM] (a stackless implementation)
* The [http://spico.gforge.inria.fr/ SpiCO] language: a stochastic pi-calulus for concurrent objects

Notes

References

* Robin Milner: "Communicating and Mobile Systems: the Pi-Calculus", Cambridge Univ. Press, 1999, ISBN 0-521-65869-1

* Robin Milner: [http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ "The Polyadic pi-Calculus: A Tutorial"] . Logic and Algebra of Specification, 1993.

* Davide Sangiorgi and David Walker: "The Pi-calculus: A Theory of Mobile Processes", Cambridge University Press, ISBN 0-521-78177-9

External links

* [http://c2.com/cgi/wiki?PiCalculus PiCalculus] on the C2 wiki
* [http://move.to/mobility Calculi for Mobile Processes]
* [http://www.eecs.harvard.edu/~nr/cs257/archive/jeannette-wing/pi.pdf FAQ on Pi-Calculus] by Jeannette M. Wing


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Calculus (disambiguation) — Calculus is Latin for pebble, and has a number of meanings in English: In mathematics and computer science Calculus , in its most general sense, is any method or system of calculation. To modern theoreticians the answer to the question what is a… …   Wikipedia

  • Calculus of variations — is a field of mathematics that deals with extremizing functionals, as opposed to ordinary calculus which deals with functions. A functional is usually a mapping from a set of functions to the real numbers. Functionals are often formed as definite …   Wikipedia

  • Calculus — Cal cu*lus, n.; pl. {Calculi}. [L, calculus. See {Calculate}, and {Calcule}.] 1. (Med.) Any solid concretion, formed in any part of the body, but most frequent in the organs that act as reservoirs, and in the passages connected with them; as,… …   The Collaborative International Dictionary of English

  • Calculus of functions — Calculus Cal cu*lus, n.; pl. {Calculi}. [L, calculus. See {Calculate}, and {Calcule}.] 1. (Med.) Any solid concretion, formed in any part of the body, but most frequent in the organs that act as reservoirs, and in the passages connected with… …   The Collaborative International Dictionary of English

  • Calculus of operations — Calculus Cal cu*lus, n.; pl. {Calculi}. [L, calculus. See {Calculate}, and {Calcule}.] 1. (Med.) Any solid concretion, formed in any part of the body, but most frequent in the organs that act as reservoirs, and in the passages connected with… …   The Collaborative International Dictionary of English

  • Calculus of probabilities — Calculus Cal cu*lus, n.; pl. {Calculi}. [L, calculus. See {Calculate}, and {Calcule}.] 1. (Med.) Any solid concretion, formed in any part of the body, but most frequent in the organs that act as reservoirs, and in the passages connected with… …   The Collaborative International Dictionary of English

  • Calculus of variations — Calculus Cal cu*lus, n.; pl. {Calculi}. [L, calculus. See {Calculate}, and {Calcule}.] 1. (Med.) Any solid concretion, formed in any part of the body, but most frequent in the organs that act as reservoirs, and in the passages connected with… …   The Collaborative International Dictionary of English

  • Calculus (book) — Calculus , by Michael Spivak, is a textbook on calculus. It is not an ordinary calculus textbook mdash; although it introduces calculus from first principles, it may be unsuitable for persons wishing to learn to apply calculus to scientific and… …   Wikipedia

  • Calculus of predispositions — is a basic part of Predispositioning Theory and belongs to the indeterministic procedures. “The key component of any indeterministic procedure is the evaluation of a position. Since it is impossible to devise a deterministic chain linking the… …   Wikipedia

  • Calculus of Broadcasting Systems — (CBS) is a CCS like calculus where processes speak one at a time and each is heard instantaneously by all others. Speech is autonomous, contention between speakers being resolved nondeterministically, but hearing only happens when someone else… …   Wikipedia

  • Calculus bovis — Calculus bovis[1], niu huang or ox bezoars are dried gallstones of cattle used in Chinese herbology, where they are claimed to remove toxins from the body. In Asian countries calculus bovis are harvested when cattle (Bos taurus domesticus Gmelin) …   Wikipedia


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.