The Azimuth Project
Process calculus (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed


A process calculus is a framework allowing for a high-level description of interactions, communications, and synchronizations between a collection of independent agents or processes. The pi 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. Beside the original use in theoretical computer science, process calculi have also been used to reason about business processes and molecular biology.

For an introduction, see see:

For process calculi in biology, see:

Pi calculus

Perhaps most well-known process calculus is the pi calculus or π calculus. The pi calculus was originally developed by Robin Milner, Joachim Parrow and David Walker, based on ideas by Uffe Engberg and Mogens Nielsen. It can be seen as a continuation of Milner’s Calculus of Communicating Systems.

Stochastic pi calculus

The stochastic pi calculus can be seen as a generalization of the stochastic Petri net or chemical reaction network formalisms:

• Luca Cardelli and Radu Mardare, Stochastic pi-calculus revisited.

• Andrew Phillips and Luca Cardelli, Simulating biological systems in the stochastic pi calculus.

• Microsoft, Stochastic pi machine.

Continuous pi calculus

We introduce the continuous π-calculus, a process algebra for modelling behaviour and variation in molecular systems. Key features of the language are: its expressive succinctness; support for diverse interaction between agents via a flexible network of molecular affinities; and operational semantics for a continuous space of processes. This compositional semantics also gives a modular way to generate conventional differential equations for system behaviour over time. We illustrate these features with a model of an existing biological system, a simple oscillatory pathway in cyanobacteria. We then discuss future research directions, in particular routes to applying the calculus in the study of evolutionary properties of biochemical pathways.

Chris Banks has a tool to model check processes for properties described in a temporal logic. The code is available here.

Performance evaluation process algebra

PEPA or Performance evaluation process algebra is another stochastic process algebra:

Categorical semantics of Markov processes

Prakash Panangaden has written a book on labeled Markov processes which includes categorical semantics. Since a semantics for PEPA models and stochastic pi calculus can be given using labeled markov processes this would seem to be worth considering in this context.

  • Prakash Panangaden, book.