Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Probabilistic Model Checking of Complex Biological Pathways

J. Heath1, M. Kwiatkowska2, G. Norman2, D. Parker2 and O. Tymchyshyn2

(1)  School of Biosciences,  
(2)  School of Computer Science University of Birmingham, Birmingham, B15 2TT, UK
Abstract
Probabilistic model checking is a formal verification technique that has been successfully applied to the analysis of systems from a broad range of domains, including security and communication protocols, distributed algorithms and power management. In this paper we illustrate its applicability to a complex biological system: the FGF (Fibroblast Growth Factor) signalling pathway. We give a detailed description of how this case study can be modelled in the probabilistic model checker PRISM, discussing some of the issues that arise in doing so, and show how we can thus examine a rich selection of quantitative properties of this model. We present experimental results for the case study under several different scenarios and provide a detailed analysis, illustrating how this approach can be used to yield a better understanding of the dynamics of the pathway.
Supported in part by EPSRC grants GR/S72023/01, GR/S11107 and GR/S46727 and Microsoft Research Cambridge contract MRL 2005-44.

Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.110 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)