*
Quick Links|Home|Worldwide
Microsoft*
Search for



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:

  • Simplicity of abstractions
    One attractive feature of process calculi such as the pi-calculus and its biological extensions is the use of a minimal repertoire of computational abstractions which map closely onto real world biological processes. The notions of processes, communication channels and state transitions embodied in the pi-calculus conceptually resemble the biological world of molecules (processes), interaction capabilities (communication channels) and covalent modifications (transitions). Process calculus approaches therefore involve translating a biological reaction scheme into pi-calculus code.
  • Compositionality / Scalability
    The concept allows for modular and compositional modelling. Information on biological systems is often „incomplete“, some of the components have not been fully identified and described, thus is incomplete or inaccurate. A modular approach allows for incorporation of all depth levels of information, replace blank holes of information by abstractions to fill these parts when enough information is available. The purpose of modelling is not only to fit experimental data to an assumed model, but also to refine the model, validate it, gain new insights and guide optimal experiment design. That way the model is also scalable, in vertical (various hierarchy levels of the system) and in horizontal direction (encompassing additional systems).
  • Model can be run on as a computer program
    The description of process algebra based models can easily be put into functional programming languages which allows to run the models (simulation), and debug interactively the models during run (in debug mode) as with any other software programme code. Simulations where parameters and components of the model are altered can be conceived as in-silico experiments.

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:

  • discrete-time Markov chains (DTMCs)
  • continuous-time Markov chains (CTMCs)
  • Markov decision processes (MDPs)

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:

  • University of Birmigham, Prof. Marta Kwiatkowska

Link to project's main web page at University of Birmingham

Back to Andre's home page



©2008 Microsoft Corporation. All rights reserved. Terms of Use |Trademarks |Privacy Statement