THE PI-CALCULUS AND RELATED PROCESS ALGEBRAS
The
pi-calculus was developed by Robin Milner as a formal language for concurrent
computational processes, such as mobile telephone systems. The pi-calculus
provides a framework for the representation, simulation, analysis and
verification of mobile communication systems.
A typical system in the
pi-calculus consists of multiple concurrent processes. Pairs of processes
interact with each other by sending and receiving messages in a synchronized
way. This communication is done on complementary (input and output) channels.
The content of messages is also channels. As a result of such a communication
event, the recipient process may now use the received channel for further
communication. This feature, called
mobility, allows the network “wiring” to change with interaction. Note, that
the calculus is non-deterministic.
Thus, when several options are available, the actual interaction that
occurs is chosen on a completely random basis.
A concise and simple syntax is all is needed in order to specify a system in
the pi-calculus. Several congruence laws determine
when two syntactically different expressions are in fact equivalent. Four reduction rules specify when and how communication
occurs.
The
pi-calculus belongs to a family of concise languages called mobile calculi
(or: process algebras). Two such calculi, the stochastic pi-calculus and the
ambient calculus are particularly important for our needs. The former, developed by Corrado Priami,
allows us to assign rates to communication actions, and is essential for
accurate modeling of biochemical systems. The latter, developed by Luca Cardelli, facilitates
the specification of process location and movement through domains, and can be
used for the representation of various aspects of molecular localization and
compartmentalization.
A simple description of the
syntax and semantics of the pi calculus can be found in our posters, presentations, and papers.
Complete information on the original pi-calculus and the stochastic variant is
available here.