SIGNAL: Stochastic process algebra for biochemical signalling pathway analysis

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


The science of computational Systems Biology uses computer modellingof living organisms to help us understand those process at work insidewhich we cannot directly see or measure. Based on experimentallydetermined data, a systems biologist invents a model of how they thinkthat things work. The model is usually analysed by one of two kindsof computer simulation: stochastic or deterministic. In a stochasticsimulation the mathematical theory of probability is used to express adegree of uncertainty about how fast reactions happen or thequantities of reactants which are in use. In a deterministicsimulation the theory of ordinary differential equations is used togive an efficient continuous approximation of very large numbers ofmolecular elements. Computational modelling is helpful here becauselaboratory-based experimentation is an extremely expensive,time-consuming and labour-intensive process. An important subject forcomputational modelling is signal transduction.Signal transduction pathways are biochemical pathways which allowcells to sense a stimulus and communicate a signal to the nucleus,which then makes a suitable response. They are complicated signallingprocesses with built-in feedback mechanisms. Signalling pathways areembedded in larger networks and are involved in important processessuch as proliferation, cell growth, movement, cell communication, andprogrammed cell death (apoptosis). Malfunction results in a largenumber of diseases including cancer, diabetes and many others. Despiteenormous experimental advances in recent years there is still anabsence of good, predictive pathway models which can guideexperimentation and drug development. To date, models either encodestatic aspects such as which proteins have the potential to interact,or provide simulations of system dynamics using ordinary differentialequations.We will develop a novel approach to analytic pathway modelling basedon our experience of modelling concurrent computing systems. The keyidea is that pathways have stochastic, computational content. We willmodel pathways using stochastic process algebras which denotecontinuous time Markov chains thus affording new quantitative analysisand new ways to structure pathways and reason about incompletebehaviour.


10 25 50

publication icon
Caravagna G (2012) Bio-PEPAd: A non-Markovian extension of Bio-PEPA in Theoretical Computer Science

publication icon
Caravagna G (2010) Modeling biological systems with delays in Bio-PEPA in Electronic Proceedings 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) Investigating modularity in the analysis of process algebra models of biochemical systems in Electronic Proceedings in Theoretical Computer Science

publication icon
Clark A (2012) Formal methods for checking the consistency of biological models. in Advances in experimental medicine and biology

publication icon
Galpin V (2011) A semi-quantitative equivalence for abstracting from fast reactions in Electronic Proceedings in Theoretical Computer Science

Description The developed Bio-PEPA process algebra modelling language was shown to support robust modelling for biochemical processes. The language can be equipped with static analysis techniques to allow the automated detection of errors and inconsistencies in models. Semantic equivalences were developed which allowed models to be simplified in useful ways which preserve key aspects of behaviour but reduce the computational burden of system analysis. Moreover an extended version of Bio-PEPA was defined with enriched support for spatial modelling. The language also supported formal stochastic model checking via the PRISM tool.

All these features allowed detailed analysis of biological processes. The ease of developing both a stochastic and a deterministic interpretation of a model, allowed these to be compared, and supported the investigation of the impact of stochasticity of biological processes such as the circardian rhythm in the alga Ostreoccocus tauri.
Exploitation Route Bio-PEPA is being taken up within the QUANTICOL project for experimental models of smart transport systems. This has informed the design of a new modelling language with enhanced capabilities for spatial modelling.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Pharmaceuticals and Medical Biotechnology,Transport

Description Microsoft PhD Scholarship
Amount £35,000 (GBP)
Organisation Microsoft Research 
Department Microsoft Research Cambridge
Sector Private
Country United Kingdom
Start 10/2012 
End 09/2015
Description Royal Society of London
Amount £10,029 (GBP)
Funding ID JP090562 
Organisation The Royal Society 
Sector Charity/Non Profit
Country United Kingdom
Start 04/2010 
End 03/2012
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.