Paper Info
Title
Probabilistic model checking of complex biological pathways
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. Finally, we outline a number of exact and approximate techniques to enable the verification of larger and more complex pathways and apply several of them to the FGF case study.
Year
DOI
Venue
2008
10.1016/j.tcs.2007.11.013
Theor. Comput. Sci.
Keywords
DocType
Volume
detailed analysis,probabilistic model checking,biological pathways,fgf case study,formal verification technique,complex pathway,probabilistic verification,complex biological pathway,signalling pathway,detailed description,complex biological system,probabilistic model checker,case study,biological modelling,probabilistic model,fibroblast growth factor,formal verification,biological systems,communication protocol,distributed algorithm
Journal
391
Issue
ISSN
ISBN
3
Theoretical Computer Science
3-540-46166-3
Citations 
PageRank 
References 
131
6.44
26
Authors
5
Search Limit
100131
Name
Order
Citations
PageRank
John Heath123520.77
Marta Z. Kwiatkowska26118322.21
Gethin Norman34163193.68
David Parker44018184.00
Oksana Tymchyshyn51548.35