Qualitative analysis of gene regulatory networks by temporal logic
Theoretical Computer Science(2015)
摘要
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. We propose a novel qualitative method for analysing gene networks based on formal verification technique.Behaviours and properties of networks are described in temporal logic formulae.By checking satisfiability of the formula, we can analyse properties of the network.To improve the efficiency of analysis we developed the modular and approximate method.
更多查看译文
关键词
Systems biology,Gene regulatory networks,Temporal logic,Reactive system verification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络