论文标题
基于模型检查的系统生物学模型的分析框架
A Model Checking-based Analysis Framework for Systems Biology Models
论文作者
论文摘要
生物系统通常被建模为具有时间不变参数的普通微分方程（ODE）系统。但是，细胞信号事件或药理干预措施可能会改变细胞状态并诱导系统的多模式动力学。此类系统自然建模为混合自动机，该系统具有多种操作模式，并在每种模式下具有特定的非线性动力学。在本文中，我们介绍了一个支持模型检查的框架，而不是可以建模并分析单模生物系统和多模式生物系统。我们解决了系统生物学中的中心问题 - 识别参数值以使模型满足所需的行为 - 使用有限的模型检查。我们诉诸于解决可满足性理论（SMT）问题和可及性问题的不可证明性问题的Delta决策程序。我们的框架可以实现多个分析任务，包括模型校准和伪造，治疗策略识别以及Lyapunov稳定性分析。我们使用前列腺癌进展，心脏细胞动作电位和辐射疾病的案例研究证明了这些方法的应用。
Biological systems are often modeled as a system of ordinary differential equations (ODEs) with time-invariant parameters. However, cell signaling events or pharmacological interventions may alter the cellular state and induce multi-mode dynamics of the system. Such systems are naturally modeled as hybrid automata, which possess multiple operational modes with specific nonlinear dynamics in each mode. In this paper we introduce a model checking-enabled framework than can model and analyze both single- and multi-mode biological systems. We tackle the central problem in systems biology--identify parameter values such that a model satisfies desired behaviors--using bounded model checking. We resort to the delta-decision procedures to solve satisfiability modulo theories (SMT) problems and sidestep undecidability of reachability problems. Our framework enables several analysis tasks including model calibration and falsification, therapeutic strategy identification, and Lyapunov stability analysis. We demonstrate the applicablitliy of these methods using case studies of prostate cancer progression, cardiac cell action potential and radiation diseases.
