SIGNAL -Stochastic process algebra for biochemical signaling pathway analysis

This project aimed to develop a novel approach to analytic pathway modelling based on the stochastic process algebra PEPA. The objectives were to
1) create appropriate theories of abstraction and approximation for pathway models
2) develop models of spatial aspects of pathways
3) realise analysis techniques via accessible tools for pathway models.

By implementing rigorous, systematic mappings between system representations and dynamic analysis tools, using stochastic process algebra, we developed
a) alternative views of a system with formal guarantees of equivalence
b) component-wise abstraction of models to reduce complexity
c) early detection of modelling errors via static analysis, and
d) investigation of models via a wider range of different analyses encompassing techniques not currently used in this domain.

A fundamental driver for the work was developing applications and case studies with a variety of signalling and other types of biochemical pathways.

In this project we developed robust modelling techniques to help biology researchers understand the intracellular processes that they were studying. These techniques allowed the modeller to describe the behaviour that they know and link it to data collected in laboratory experiments, rather than having to work at the level of explicit mathematical models. Unlike mathematical models such as ordinary differential equations, they modelling techniques can be equipped with automated tools to correct their consistency and suggest simplifications.

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.