Process Algebra Approaches to Collective Dynamics

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics


The aim of this scientific research programme is to help to understand how we can predict the dynamic behaviour of a population when we can model the behaviour of the individuals.There are application areas in many scientific fields for a question such as this, but one of the most important is in biology. Biologists study cells, reagents, molecules, and molecular complexes in order to gain insights into growth and change. Here carefully defined models have increasing importance because more and more biological research is now being done using computer-based analysis. That form of research complements the biological research which is traditional laboratory science, based on controlled experiments, data gathering, and observation. Models allow the biologists to try to make sense of the data they have observed, forming hypotheses which may then be tested in further experiments. Their research findings inspire the design of new drugs and treatments which fight illness and improve human and animal health.Scientists need languages in order to communicate effectively and unambiguously. The models developed by biologists are often written in the mathematical notation for calculus invented by Leibniz, as differential equations. Whilst this notation has many virtues it is not always the most intuitive to use, and can be far removed from the cellular processes being described. So biologists have been investigating the use of other system description languages, from other areas of science.Computer science has more experience than the other sciences in formal language design. In computer science formal languages have been used for a variety of purposes, one of which is the design and validation of programs. One class of languages which have been used for this purpose are process algebras, which as well as features for describing systems, come equipped with techniques for comparing systems and proving properties about them. Formal languages such as process algebras do not evolve naturally in the way that human languages do. Instead, they need to be carefully designed.This fellowship will bring the benefits of the experience of computer science in formal language design to the design of a new process algebra for modelling biological systems, the language BioSPA. One crucial aspect of this new language will be its use of mathematically quantified randomness. In every living thing is a controlled amount of randomness because living things are fuelled by chemical reactions. Systems of chemical reactions evolve stochastically because of the inherent randomness of thermal molecular motion.The BioSPA language will be supported by software tools which will allow biologists to see their models in a number of ways. For example, as a Markov process, a mathematical process which randomly moves between a number of distinct states, or as a series of ordinary differential equations. For either representation it will be possible to trace a possible evolution of the system or to solve the model numerically. The latter could allow a biologist to predict a key value at a specific time, such as the concentration of a particular molecule after ten minutes.A unique feature of the BioSPA language will be that it will also be possible to systematically prove properties of models in the language in order to ensure that they represent the system which the biologists wish to study. This strong, well-designed language will help to ensure the correctness of biological research and the validity of its results, with attendant benefits for medical and pharmaceutical research leading to improvements in the prevention and treatment of illness.


10 25 50
publication icon
Ciocchetta F (2008) Modelling co-transcriptional cleavage in the synthesis of yeast pre-rRNA in Theoretical Computer Science

publication icon
Ciocchetta F (2009) Integrated Simulation and Model-Checking for the Analysis of Biochemical Systems in Electronic Notes in Theoretical Computer Science

publication icon
Ciocchetta F (2010) Bio-PEPA for Epidemiological Models in Electronic Notes in Theoretical Computer Science

publication icon
Ciocchetta F (2009) Bio-PEPA: A framework for the modelling and analysis of biological systems in Theoretical Computer Science

publication icon
Ciocchetta F (2009) Some Investigations Concerning the CTMC and the ODE Model Derived From Bio-PEPA in Electronic Notes in Theoretical Computer Science

publication icon
Geisweiller N (2008) Relating continuous and discrete PEPA models of signalling pathways in Theoretical Computer Science

Description A new stochastic process algebra, Bio-PEPA, was defined and equipped with a number of analysis techniques. Each of these relied on a different mathematical interpretation of the model description but these interpretations were shown to be the same. The analysis techniques allowed the dynamic behaviour of the system to be studied and predictions made of how it might behave under perturbations. The modelling formalism was applied to a number of biological and other application domain examples.
Exploitation Route The Bio-PEPA language has generated interested both in the intended application domain of biochemical pathways and more broadly. It has been used for modelling the movement of people, and in the EU FP7 project QUANTICOL it is being used to model transport systems. There has been follow-on funding from Microsoft Research Cambridge for a PhD student, to develop a related language for modelling ecological systems, which will build on Bio-PEPA but add stronger representation of spatial informatio
Sectors Agriculture, Food and Drink,Digital/Communication/Information Technologies (including Software),Healthcare,Transport

Description The PEPA stochastic process algebra has been used for performance analysis of a wide range of systems since its introduction in 1994. However, the scale of system which could be considered was limited by the problem of state space explosion in the discrete state space used to analyse the behaviour of systems. The fluid flow approximation technique proposed by Hillston is suitable for models of systems with large numbers of similar components. Moreover using the process algebra, the convergence of the discrete model to the continuous has been proved by construction, rather than having to be established on a model-by-model basis. Furthermore, the approach is supported by software tools making it accessible, even to those unfamiliar with the underlying mathematics. The approach has been used in a number of modelling studies by other academics, some working in collaboration with industry. Moreover the original research work has stimulated the work of other researchers and the papers reporting it are highly cited.
First Year Of Impact 2007
Sector Digital/Communication/Information Technologies (including Software),Education
Impact Types Cultural

Title Bio-PEPA tool 
Description This Eclipse Plug-in has an editor to support the construction of Bio-PEPA models and a variety of static and dynamic analysis tools. 
Type Of Technology Software 
Year Produced 2009 
Open Source License? Yes  
Impact The availability of the tools has encouraged other groups to use the Bio-PEPA language and also the language and tool are used in post-graduate teaching at a number of Universities worldwide.