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.