Probabilistic model checking of complex biological pathways

被引：98

作者：

Heath, John ^{[2
]}

Kwiatkowska, Marta ^{[1
]}

Norman, Gethin ^{[1
]}

Parker, David ^{[1
]}

Tymchyshyn, Oksana ^{[3
]}

机构：

[1] Univ Oxford, Comp Lab, Oxford OX1 3QD, England

[2] Univ Birmingham, Sch Biosci, Birmingham B15 2TT, W Midlands, England

[3] Univ Birmingham, Sch Comp Sci, Birmingham B15 2TT, W Midlands, England

来源：

THEORETICAL COMPUTER SCIENCE | 2008年 / 391卷 / 03期

基金：

英国工程与自然科学研究理事会;

关键词：

probabilistic model checking; probabilistic verification; biological pathways; biological modelling;

D O I：

10.1016/j.tcs.2007.11.013

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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. (C) 2007 Elsevier B.V. All rights reserved.

引用

页码：239 / 257

页数：19

共 44 条

[1]

[Anonymous], 2005, EVAL REV

[2]

Aziz A, 1996, LNCS, P269, DOI DOI 10.1007/3-540-61474-5

[3]

BAIER C, 2000, LNCS, V1855, P358

[4] Understanding complex signaling networks through models and metaphors [J].