Qualitative analysis of gene regulatory networks by temporal logic
Qualitative analysis of gene regulatory networks by temporal logic
复制标题
DOI：
10.1016/j.tcs.2015.06.017
复制
发表时间：
2015-08-23
影响因子：
1.1
通讯作者：
Yonezaki, Naoki
中科院分区：
文献类型：
--
作者：
Ito, Sohei;Ichinose, Takuma;Yonezaki, Naoki
在这篇文章中，我们提出了一种新的形式主义来建模和分析基因调控网络，使用一种成熟的形式验证技术。我们用线性时序逻辑(LTL)中的逻辑公式对网络的可能行为进行建模。通过检查LTL的可满足性，可以检查某些或所有行为是否满足给定的生物属性，这在诸如常微分方程法之类的定量分析中是困难的。由于LTL可满足性检验的复杂性，在该方法中对大型网络的分析通常是一个难题。为了减轻这种计算难度，我们开发了两种方法。一种是模块化检查方法，我们将网络划分为子网络，分别检查它们，然后将它们整合在一起。另一种是近似分析方法，在这种方法中，我们用更简单的公式指定行为，压缩或扩展网络可能的行为。在近似方法中，我们聚焦于网络主题，并给出了网络主题的近似描述。我们通过实验证实，这两种方法都改进了大型网络的分析。(C)2015年提交人。爱思唯尔出版公司(Elsevier B.V.)
In this article we propose a novel formalism to model and analyse gene regulatory networks using a well-established formal verification technique. We model the possible behaviours of networks by logical formulae in linear temporal logic (LTL). By checking the satisfiability of LTL, it is possible to check whether some or all behaviours satisfy a given biological property, which is difficult in quantitative analyses such as the ordinary differential equation approach. Owing to the complexity of LTL satisfiability checking, analysis of large networks is generally intractable in this method. To mitigate this computational difficulty, we developed two methods. One is a modular checking method where we divide a network into subnetworks, check them individually, and then integrate them. The other is an approximate analysis method in which we specify behaviours in simpler formulae which compress or expand the possible behaviours of networks. In the approximate method, we focused on network motifs and presented approximate specifications for them. We confirmed by experiments that both methods improved the analysis of large networks. (C) 2015 The Authors. Published by Elsevier B.V.