Probabilistic model checking of complex biological pathways
Probabilistic model checking of complex biological pathways
复制标题
DOI：
10.1016/j.tcs.2007.11.013
复制
发表时间：
2008-02-14
影响因子：
1.1
通讯作者：
Tymchyshyn, Oksana
中科院分区：
文献类型：
--
作者：
Heath, John;Kwiatkowska, Marta;Tymchyshyn, Oksana
概率模型检查是一种正式的验证技术，已成功应用于来自广泛领域的系统的分析，包括安全和通信协议，分布式算法和电源管理。在本文中，我们说明了其适用于复杂的生物系统：FGF（成纤维细胞生长因子）信号通路。我们详细说明了如何在概率模型检查器棱镜中建模该案例研究，讨论了这样做时出现的一些问题，并展示了我们如何研究该模型的丰富定量属性选择。我们在几种不同的情况下为案例研究提供了实验结果，并提供了详细的分析，说明了如何使用这种方法来更好地理解途径的动力学。最后，我们概述了许多精确和近似技术，以实现较大且更复杂的途径的验证，并将其中一些应用于FGF案例研究。 （c）2007 Elsevier B.V.保留所有权利。
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.