|
Probabilistic Symbolic Model Checking in Systems Biology
Concepts have been developed by computer scientists to formally describe complex software systems which allows for abstractions. There are similarities between mobile interactive communications systems and processes & networks in biological systems on a cellular and molecular level. Therefore, the concepts for describing communication systems – including process algebra [= process calculi] - recently have been applied to the description and simulation of biological processes. These software engineering concepts are usually supported by simulation and analysis tools with which their dynamics can be investigated. Models of biological systems have to consider stochastic behaviour (e.g. variations in quantities, concentrations and reaction rates). Regev & Shapiro [Nature 419, 2002] have proposed using the stochastic pi-calculus “molecule-as-computation” paradigm and constituted a particularly appealing method for modelling of cellular and molecular networks, such as signalling and metabolic pathways as well as gene regulation. The BioSPI system is a simulation platform for stochastic pi-calculus implemented at the Weizmann Institute. The latest version implements the Gillespie algorithm for stochastic behaviour and allows to obtain a full record of the time evolution of the system. The SPiM (Stochastic Pi-calculus abstract Machine) is a simulation platform for the stochastic pi-calculus based on an abstract machine implemented by Andrew Phillips, Microsoft Research. The process algebra features which benefit modelling of cellular and molecular biological systems are:
The goal of this project is to extend the existing model checker PRISM, so model checking on models in Computational Biology can be performed. PRISM is a probabilistic model checker being developed at the University of Birmingham. The tool is designed for the analysis of probabilistic systems. It supports three models:
In order to make PRISM applicable to Computational Biology models, the support for SBML (Systems Biology Markup Language) models and mobility concepts will be added. Collaborators:
Link to project's main web page at University of Birmingham |