The Azimuth Project
Process calculus


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:

For process calculi in biology, see:

  • D. Prandi, C. Priami and P. Quaglia, Process calculi in a biological context, Bull EATCS 85 (2006), 53–69.

  • C. Priami and M.J. Morine, Analysis of Biological Systems, Imperial College Press, 2015.

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. Corrado Priami introduced the stochastic pi-calculus:

Priami and others have applied the stochastic pi-calculus to biology:

  • C. Priami, A. Regev, E. Shapiro, W. Silverman, Application of a stochastic name-passing calculus to representation and simulation of molecular processes, Information Processing Letters 80 (2001), 25.

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

Also, COSBI developed a set of languages to model biological systems which are related to the pi-calculus (e.g., beta-binders, BlenX, L languages). Most of them are implemented and freely available online here and here. Some relevant papers are here:

  • C. Priami and P. Quaglia, Beta binders for biological interactions. Computational Methods in Systems Biology (2005), 20–33.

  • L. Dematte, C. Priami, and A. Romanel, The Beta Workbench: a computational tool to study the dynamics of biological systems, Briefings in Bioinformatics 9 (2008), 437–449.

  • R. Gostner, B. Baldacci, M. J. Morine and C. Priami, Graphical modelling tools for systems biology, ACM Computing Surveys 47 (2014).

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.