[HKN+06] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. In C. Priami (editor), Proc. Computational Methods in Systems Biology (CMSB'06), volume 4210 of Lecture Notes in Bioinformatics, pages 32-47, Springer Verlag. October 2006. [ps.gz] [pdf] [bib] [Analyses the FGF (Fibroblast Growth Factor) signalling pathway using PRISM.]
Downloads:  ps.gz ps.gz (277 KB)  pdf pdf (429 KB)  bib bib
Notes: Supplementary material available at supporting website:

Further information and verification results also available from the PRISM case study page. The original publication is available at link.springer.com.
Links: [Google] [Google Scholar]
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.