Pi-calculus
Encyclopedia
In theoretical computer science
, the π-calculus (or 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 π-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.
, 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
The process constructs available in the calculus are the following (a precise definition is given in the following section):
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, truth values, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public-key cryptography. The applied due to Abadi and Fournet http://citeseer.ist.psu.edu/rd/0%2C573109%2C1%2C0.25%2CDownload/http%3AqSqqSqwww.cse.ucsc.eduqSq%7EabadiqSqPapersqSqisss02.pdf put these various extensions on a formal footing by extending the with arbitrary datatypes.
is only known by the first two components.
The first two components are able to communicate on the channel
, and the name 
becomes bound to 
. The next step in the process is therefore
Note that the remaining
is not affected because it is defined in an inner scope.
The second and third parallel components can now communicate on the channel name
, and the name 
becomes bound to 
. The next step in the process is now
Note that since the local name
has been output, the scope of 
is extended to cover the third component as well. Finally, the channel 
can be used for sending the name 
.
for the π-calculus is built from the following BNF grammar (where x and y are any names from Χ):
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.
More precisely, structural congruence is defined as the least equivalence relation preserved by the process constructs and satisfying:
Alpha-conversion:
Axioms for parallel composition:
Axioms for restriction:
Axiom for replication:
Axiom relating restriction and parallel:
This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how a bound name
may be extruded by an output action, causing the scope of 
to be extended. In cases where 
is a free name of 
, alpha-conversion may be used to allow extension to proceed.
if 
can perform a computation step, following which it is now 
.
This reduction relation
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:
There are three additional rules:
The latter rule states that processes that are structurally congruent have the same reductions.
Applying the definition of the reduction semantics, we get the reduction
Note how, applying the reduction substitution axiom, occurrences of
are now labeled as 
.
Next, we get the reduction
Note that since the local name
has been output, the scope of 
is extended to cover the third component as well. This was captured using the scope extension axiom.
). Transitions in this semantics are of the form:
This notation
signifies that
after the action 
becomes 
. 
can be an input action 
, an output action 
, or a tau-action 
corresponding to an internal communication.
A standard result about the labelled semantics is that it agrees with the reduction semantics in the sense that
if and only if 
for some action
.
A nondeterministic choice operator
can be added to the syntax.
A test for name equality
can be added to the syntax. This match operator can proceed as 
if and only if 
and 
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 continuation, i.e. output atoms of the form
, 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.
The polyadic π-calculus allows communicating more than one name in a single action:
(polyadic output) and 
(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
is encoded as 
is encoded as 
All other process constructs are left unchanged by the encoding.
In the above,
denotes the encoding of all prefixes in the continuation 
in the same way.
The full power of replication
is not needed. Often, one only considers replicated input 
, whose structural congruence axiom is 
.
Replicated input process such as
can be understood as servers, waiting on channel
to be invoked by clients. Invocation of a server spawns a new copy of
the process
, 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
Here,
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 π-calculus: passing a process P can be
simulated by just passing a name that points to P instead.
Vol. 2, pp. 119–141, 1992), 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, "
is bound to term 
" – as replicating agents that respond to requests for their bindings by sending back a connection to the term 
.
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 (Mads Dam: On the Decidability of Process Equivalences for the pi-Calculus. Theoretical Computer Science 183, 1997, pp. 215–228.)
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
and 
denote processes and 
denote binary relations over processes.
A binary relation
over processes is an early bisimulation if for every pair of processes 
,
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, the π-calculus (or pi-calculus) is a process calculus
Process calculus
In computer science, the process calculi are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes...
originally developed by Robin Milner
Robin Milner
Arthur John Robin Gorell Milner FRS FRSE was a prominent British computer scientist.-Life, education and career:...
, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems
Calculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
). 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
Game semantics
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
. 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 λ-calculusLambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda 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
, where 
and 
are two processes or threads executed concurrently. - communication, where
- input prefixing
is a process waiting for a message that was sent on a communication channel named 
before proceeding as binding the name received to the name Typically, this models either a process expecting a communication from the network or a label cusable only once by agoto coperation. - output prefixing
describes that the name 
is emitted on channel 
before proceeding as Typically, this models either sending a message on the network or a goto coperation.
- input prefixing
- replication, written
, which may be seen as a process which can always create a new copy of Typically, this models either a network service or a label cwaiting for any number ofgoto coperations. - creation of a new name, written
, which may be seen as a process allocating a new constant 
within The constants of 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, truth values, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public-key cryptography. The applied due to Abadi and Fournet http://citeseer.ist.psu.edu/rd/0%2C573109%2C1%2C0.25%2CDownload/http%3AqSqqSqwww.cse.ucsc.eduqSq%7EabadiqSqPapersqSqisss02.pdf put these various extensions on a formal footing by extending the with arbitrary datatypes.
A small example
Below is a tiny example of a process which consists of three parallel components. The channel name is only known by the first two components.The first two components are able to communicate on the channel
, and the name becomes bound to . The next step in the process is thereforeNote that the remaining
is not affected because it is defined in an inner scope.The second and third parallel components can now communicate on the channel name
, and the name becomes bound to . The next step in the process is nowNote that since the local name
has been output, the scope of is extended to cover the third component as well. Finally, the channel can be used for sending the name .Syntax
Let Χ be a set of objects called names. The abstract syntaxAbstract syntax
The abstract syntax of data is its structure described as a data type , independent of any particular representation or encoding....
for the π-calculus is built from the following BNF grammar (where x and y are any names from Χ):
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
process has no free names and no bound names.
- The free names of
are 
, 
, and the free names of 
. The bound names of 
are the bound names of 
.
- The free names of
are 
and the free names of 
, except for 
. The bound names of 
are 
and the bound names of 
.
- The free names of
are those of 
together with those of 
. The bound names of 
are those of 
together with those of 
.
- The free names of
are those of 
, except for 
. The bound names of 
are 
and the bound names of 
.
- The free names of
are those of 
. The bound names of 
are those of 
.
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:
-
if 
can be obtained from 
by renaming one or more bound names in 
.
Axioms for parallel composition:
Axioms for restriction:
Axiom for replication:
Axiom relating restriction and parallel:
-
if 
is not a free name of 
.
This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how a bound name
may be extruded by an output action, causing the scope of to be extended. In cases where is a free name of , alpha-conversion may be used to allow extension to proceed.Reduction semantics
We write if can perform a computation step, following which it is now .This reduction relation
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:
- where
denotes the process 
in which the free name 
has been substituted for the free occurrences of 
. If a free occurrence of 
occurs in a location where 
would not be free, alpha-conversion may be required.
There are three additional rules:
- If
then also 
.
- This rule says that parallel composition does not inhibit computation.
- If
, then also 
.
- If
- This rule ensures that computation can proceed underneath a restriction.
- If
and 
where 
, then also 
.
- If
The latter rule states that processes that are structurally congruent have the same reductions.
The example revisited
Consider again the processApplying the definition of the reduction semantics, we get the reduction
Note how, applying the reduction substitution axiom, occurrences of
are now labeled as .Next, we get the reduction
Note that since the local name
has been output, the scope of 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 SystemsCalculus of Communicating Systems
The Calculus of Communicating Systems is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing parallel...
). Transitions in this semantics are of the form:
This notation
State transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
signifies that
after the action becomes . can be an input action , an output action , or a tau-action corresponding to an internal communication.A standard result about the labelled semantics is that it agrees with the reduction semantics in the sense that
if and only if for some action
.Extensions and variants
The syntax given above is a minimal one. However, the syntax may be modified in various ways.A nondeterministic choice operator
can be added to the syntax.A test for name equality
can be added to the syntax. This match operator can proceed as if and only if and 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 continuation, i.e. output atoms of the form
, 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.The polyadic π-calculus allows communicating more than one name in a single action:
(polyadic output) and (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 is encoded as is encoded as All other process constructs are left unchanged by the encoding.
In the above,
denotes the encoding of all prefixes in the continuation in the same way.The full power of replication
is not needed. Often, one only considers replicated input , whose structural congruence axiom is .Replicated input process such as
can be understood as servers, waiting on channel to be invoked by clients. Invocation of a server spawns a new copy ofthe process
, where a is the name passed by the client to theserver, 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
Here,
denotes a process variable which can be instantiated by a process term. Sangiorgiestablished the surprising result 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.
Turing completeness
The π-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 π-calculus. One encoding simulates the eager (call-by-value) evaluation strategy
Evaluation strategy
In computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
, 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, "
is bound to term " – as replicating agents that respond to requests for their bindings by sending back a connection to the term .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
Turing
Alan Turing was a British mathematician, logician, cryptanalyst, and computer scientist.Turing may also refer to:*Turing machine, a basic, abstract symbol-manipulating device...
-powerful. This can be seen by the fact that bisimulation
Bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
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 (Mads Dam: On the Decidability of Process Equivalences for the pi-Calculus. Theoretical Computer Science 183, 1997, pp. 215–228.)
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
and denote processes and 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.A binary relation
over processes is an early bisimulation if for every pair of processes ,
- whenever
then for every name 
there exists some 
such that 
and 
;
- for any non-input action
, if 
then there exists some 
such that 
and 
;
- and symmetric requirements with
and 
interchanged.
Processes
and 
are said to be early bisimilar, written 
if the pair 
for some early bisimulation 
.
In late bisimilarity, the transition match must be independent of the name being transmitted.
A binary relation
over processes is a late bisimulation if for every pair of processes 
,
- whenever
then for some 
it holds that 
and 
for every name y;
- for any non-input action
, if 
implies that there exists some 
such that 
and 
;
- and symmetric requirements with
and 
interchanged.
Processes
and 
are said to be late bisimilar, written 
if the pair 
for some late bisimulation 
.
Both
and 
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 
and 
such that 
but 
. One may remedy this problem by considering the maximal congruence relations included in 
and 
, 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.
A binary relation
over processes is an open bisimulation if for every pair of elements 
and for every name substitution 
and every action 
, whenever 
then there exists some 
such that 
and 
.
Processes
and 
are said to be open bisimilar, written 
if the pair 
for some open bisimulation 
.
Early, late and open bisimilarity are in fact all distinct. The containments are proper, so
.
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
if process 
immediately allows an input or an output on name 
.
A binary relation
over processes is a barbed bisimulation if it is a symmetric relation which satisfies that for every pair of elements 
we have that
if and only if 
for every name 
and
for every reduction
there exists a reduction 
such that
.
We say that
and 
are barbed bisimilar if there exists a barbed bisimulation 
where 
.
Defining a context as a π term with a hole [] we say that two processes P and Q are barbed congruent, written
if for every context 
we have that 
. 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, Martin AbadiMartín AbadiMartín Abadi is an argentinian computer scientist, currently working at the University of California, Santa Cruz and Microsoft Research. He earned his Ph.D...
and Andrew Gordon proposed an extension of the π-calculus, the Spi-calculus, as a formal notation for describing and reasoning about cryptographic protocols. The spi-calculus extends the π-calculus with primitives for encryption and decryption. In 2001, Martin AbadiMartín AbadiMartín Abadi is an argentinian computer scientist, currently working at the University of California, Santa Cruz and Microsoft Research. He earned his Ph.D...
and Cedric Fournet generalised the handling of cryptographic protocols to produce the applied π calculus. There is now a large body of work devoted to variants of the applied π calculus, including a number of experimental verification tools. One example is the tool ProVerifProVerifProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet....
http://www.proverif.ens.fr/ due to Bruno Blanchet, based on a translation of the applied π-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 π-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 LanguageBusiness Process Modeling LanguageBusiness Process Modeling Language is a meta-language for the modeling of business processes, just as XML is a meta-language for the modeling of business data. BPML was a proposed language, but now the BPMI has dropped support for this in favor of BPEL4WS...
(BPML), and of Microsoft's XLANG.
The π-calculus has also attracted interest in molecular biology. In 1999, Aviv RegevAviv RegevAviv Regev is a computational biologist at the Broad Institute of MIT and Harvard, an assistant professor in the department of biology at Massachusetts Institute of Technology and an Early Career Scientist at Howard Hughes Medical Institute....
and Ehud ShapiroEhud ShapiroEhud Shapiro is an Israeli computer scientist at the Weizmann Institute of Science. He received his Ph.D from Yale for his dissertation entitled "Algorithmic Program Debugging" which was an ACM distinguished dissertation for 1982. He has been an exponent of the Prolog computer language and logic...
showed that one can describe a cellular signaling pathway (the so-called RTKReceptor tyrosine kinaseReceptor tyrosine kinases s are the high-affinity cell surface receptors for many polypeptide growth factors, cytokines, and hormones. Of the 90 unique tyrosine kinase genes identified in the human genome, 58 encode receptor tyrosine kinase proteins....
/MAPK cascade) and in particular the molecular "lego" which implements these tasks of communication in an extension of the π-calculus.
Implementations
The following programming languages are implementations either of the π-calculus or of its variants:
- Acute
- Business Process Modeling LanguageBusiness Process Modeling LanguageBusiness Process Modeling Language is a meta-language for the modeling of business processes, just as XML is a meta-language for the modeling of business data. BPML was a proposed language, but now the BPMI has dropped support for this in favor of BPEL4WS...
(BPML) - Nomadic Pict
- jumel : a compiler for a dialect of ML augmented with pi-calculus primitives for message-passing
- occam-π
- PictPict programming languagePict is a statically typed programming language, one of the very few based on the Π-calculus. Work on the language began at the University of Edinburgh in 1992. The language is still at an experimental stage.-Sources:*-External links:...
- JoCamlJoCamlJoCaml is an experimental functional programming language derived from OCaml. It integrates the primitives of the join-calculus to enable flexible, type-checked concurrent and distributed programming.- External links :* *...
(based on the Join-calculusJoin-calculusThe join-calculus is a process calculus developed at INRIA. The join-calculus was developed to provide a formal basis for the design of distributed programming languages, and therefore intentionally avoids communications constructs found in other process calculi, such as rendezvous communications,...
) - Funnel (A JRE-compatible join calculus implementation)
- The CubeVM (a stackless implementation)
- The SpiCO language: a stochastic pi-calulus for concurrent objects
- BioSPI and SPiM: simulators for the stochastic pi-calculus
- Ateji PX: a Java language extension with parallel primitives inspired from π-calculus
External links
- PiCalculus on the C2 wiki
- Calculi for Mobile Processes
- FAQ on π-Calculus by Jeannette M. Wing
- and symmetric requirements with
- for any non-input action
- and symmetric requirements with
- for any non-input action