Formal Analysis of Gene Networks Using Network Motifs

We developed a theoretical framework to analyse gene regulatory networks. Our framework is based on the formal methods which are well-known techniques to analyse software/hardware systems. Behaviours of gene networks are abstracted into transition systems which has discrete time structure. We characterise possible behaviours of given networks by linear temporal logic (LTL) formulae. By checking the satisfiability of LTL formulae, we analyse whether all/some behaviours of given networks satisfy given biological properties. Due to the complexity of LTL satisfiability checking, analyses of large networks are generally intractable in this method. To mitigate this computational difficulty, we proposed approximate analysis method using network motifs to circumvent the computational difficulty of LTL satisfiability checking. Experiments show that our approximate method is surprisingly efficient.