×

Qualitative analysis of gene regulatory networks by temporal logic. (English) Zbl 1329.92049

Summary: 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.

MSC:

92C42 Systems biology, networks
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Lamport, L.; Wolper, P., Realizable and unrealizable specifications of reactive systems, (ICALP ’89: Proceedings of the 16th International Colloquium on Automata, Languages and Programming. ICALP ’89: Proceedings of the 16th International Colloquium on Automata, Languages and Programming, LNCS, vol. 372 (1989), Springer-Verlag: Springer-Verlag London, UK), 1-17
[2] Alon, U., An Introduction To Systems Biology: Design Principles Of Biological Circuits (2006), Chapman and Hall/CRC · Zbl 1141.92002
[3] Alon, U., Network motifs: theory and experimental approaches, Nat. Rev. Genet., 8, 6, 450-461 (June 2007)
[4] Antoniotti, M.; Policriti, A.; Ugel, N.; Mishra, B., Model building and model checking for biochemical processes, Cell Biochem. Biophys., 38, 3, 271-286 (2003)
[5] Aoshima, T.; Sakuma, K.; Yonezaki, N., An efficient verification procedure supporting evolution of reactive system specifications, (Proceedings of the 4th International Workshop on Principles of Software Evolution. Proceedings of the 4th International Workshop on Principles of Software Evolution, IWPSE ’01 (2001), ACM: ACM New York, NY, USA), 182-185
[6] Aoshima, T.; Yonezaki, N., An efficient tableau-based verification method with partial evaluation for reactive system specifications, (Proceedings of the 10th European-Japanese Conference on Information Modelling and Knowledge Bases (2000)), 363-374 · Zbl 1004.68095
[7] Batt, G.; Belta, C.; Weiss, R., Temporal logic analysis of gene networks under parameter uncertainty, IEEE Trans. Automat. Control, 53, 215-229 (2008) · Zbl 1366.92077
[8] Batt, G.; Ropers, D.; de Jong, H.; Geiselmann, J.; Mateescu, R.; Page, M.; Schneider, D., Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli, Bioinformatics, 21, Suppl. 1, i19-i28 (2005)
[9] Bernot, G.; Comet, J. P.; Richard, A.; Guespin, J., Application of formal methods to biological regulatory networks: extending Thomas’ asynchronous logical approach with temporal logic, J. Theoret. Biol., 229, 3, 339-347 (2004) · Zbl 1440.92036
[10] Chabrier, N.; Fages, F., Symbolic model checking of biochemical networks, (Computational Methods in Systems Biology. Computational Methods in Systems Biology, CMSB’ 03. Computational Methods in Systems Biology. Computational Methods in Systems Biology, CMSB’ 03, LNCS, vol. 2602 (2003), Springer-Verlag), 149-162 · Zbl 1112.92312
[11] Ciocchetta, F.; Hillston, J., Bio-PEPA: a framework for the modelling and analysis of biological systems, Theoret. Comput. Sci., 410, 3065-3084 (August 2009) · Zbl 1173.68041
[12] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), MIT Press
[13] Croft, D.; O’Kelly, G.; Wu, G.; Haw, R.; Gillespie, M.; Matthews, L.; Caudy, M.; Garapati, P.; Gopinath, G.; Jassal, B.; Jupe, S.; Kalatskaya, I.; Mahajan, S.; May, B.; Ndegwa, N.; Schmidt, E.; Shamovsky, V.; Yung, C.; Birney, E.; Hermjakob, H.; D’Eustachio, P.; Stein, L., Reactome: a database of reactions, pathways and biological processes, Nucleic Acids Res., 39, Database-Issue, 691-697 (2011)
[14] de Jong, H.; Geiselmann, J.; Hernandez, G.; Page, M., Genetic network analyzer: qualitative simulation of genetic regulatory networks, Bioinformatics, 19, 3, 336-344 (2003)
[15] Elowitz, M. B.; Leibler, S., A synthetic oscillatory network of transcriptional regulators, Nature, 403, 335-338 (2000)
[16] Emerson, E. Allen, Temporal and modal logic, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) (1990), MIT Press), 995-1072 · Zbl 0900.03030
[17] Fages, F.; Soliman, S.; Chabrier-Rivier, N., Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM, J. Biol. Phys. Chem., 4, 64-73 (2004)
[18] Glass, L.; Kauffman, S. A., Co-operative components, spatial localization and oscillatory cellular dynamics, J. Theoret. Biol., 34, 2, 219-237 (February 1972)
[19] Glass, L.; Kauffman, S. A., The logical analysis of continuous, non-linear biochemical control networks, J. Theoret. Biol., 39, 1, 103-129 (April 1973)
[20] Govan, J. R.W.; Deretic, V., Microbial pathogenesis in cystic fibrosis: mucoid Pseudomonas aeruginosa and Burkholderia cepacia, Microbiol. Rev., 60, 539-574 (1996)
[21] Govan, J. R.W.; Harris, G. S., Pseudomonas aeruginosa and cystic fibrosis: unusual bacterial adaptation and pathogenesis, Microbiol. Sci., 3, 10, 302-308 (1986)
[22] Guespin, J.; Bernot, G.; Comet, J. P.; Mérieau, A.; Richard, A.; Hulen, C.; Polack, B., Epigenesis and dynamic similarity in two regulatory networks in Pseudomonas aeruginosa, Acta Biotheor., 52, 4, 379-390 (2004)
[23] Guespin, J.; Kaufman, M., Positive feedback circuits and adaptive regulations in bacteria, Acta Biotheor., 49, 4, 207-218 (2001)
[24] Hagihara, S.; Yonezaki, N., Completeness of verification methods for approaching to realizable reactive specifications, (Proceedings of 1st Asian Working Conference on Verified Software. Proceedings of 1st Asian Working Conference on Verified Software, AWCVS’06, vol. 348 (2006)), 242-257, UNU-IIST technical report
[25] Heath, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Tymchyshyn, O., Probabilistic model checking of complex biological pathways, Theoret. Comput. Sci., 391, 239-257 (February 2008) · Zbl 1133.68043
[26] Hinton, A.; Kwiatkowska, M.; Norman, G.; Parker, D., PRISM: a tool for automatic verification of probabilistic systems, (Hermanns, H.; Palsberg, J., Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’06. Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’06, LNCS, vol. 3920 (2006), Springer), 441-444
[27] Ito, S.; Ichinose, T.; Shimakawa, M.; Izumi, N.; Hagihara, S.; Yonezaki, N., Modular analysis of gene networks by linear temporal logic, J. Integr. Bioinform., 10, 2 (2013)
[28] Ito, S.; Ichinose, T.; Shimakawa, M.; Izumi, N.; Hagihara, S.; Yonezaki, N., Qualitative analysis of gene regulatory networks using network motifs, (Proceedings of the 4th International Conference on Bioinformatics Models, Methods and Algorithms. Proceedings of the 4th International Conference on Bioinformatics Models, Methods and Algorithms, BIOINFORMATICS2013 (2013)), 15-24
[29] Ito, S.; Izumi, N.; Hagihara, S.; Yonezaki, N., Qualitative analysis of gene regulatory networks by satisfiability checking of linear temporal logic, (Proceedings of the 10th IEEE International Conference on Bioinformatics & Bioengineering. Proceedings of the 10th IEEE International Conference on Bioinformatics & Bioengineering, BIBE2010 (2010)), 232-237
[30] Kanehisa, M.; Goto, S.; Sato, Y.; Furumichi, M.; Tanabe, M., KEGG for integration and interpretation of large-scale molecular data sets, Nucleic Acids Res., 40, D109-D114 (2012)
[31] Karp, P. D.; Riley, M.; Paley, S. M.; Pellegrini-Toole, A., The MetaCyc database, Nucleic Acids Res., 30, 1, 59-61 (2002)
[32] Kaufman, M.; Urbain, J.; Thomas, R., Towards a logical analysis of the immune response, J. Theoret. Biol., 114, 4, 527-561 (1985)
[33] Kaufman, S. A., Metabolic stability and epigenesis in randomly constructed genetic nets, J. Theoret. Biol., 22, 3, 437-467 (1969)
[34] Kwiatkowska, M.; Norman, G.; Parker, D., Using probabilistic model checking in systems biology, SIGMETRICS Perf. Eval. Rev., 35, 4, 14-21 (2008)
[35] Mori, R.; Yonezaki, N., Several realizability concepts in reactive objects, (Information Modeling and Knowledge Bases IV (1993)), 407-424
[36] Peled, D.; Wilke, T., Stutter-invariant temporal properties are expressible without the next-time operator, Inform. Process. Lett., 63, 5, 243-246 (1997) · Zbl 1337.68170
[37] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, (POPL ’89: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1989), ACM: ACM New York, NY, USA), 179-190
[38] Priami, C.; Regev, A.; Shapiro, E.; Silverman, W., Application of a stochastic name-passing calculus to representation and simulation of molecular processes, Inform. Process. Lett., 80, 25-31 (October 2001) · Zbl 0997.92018
[39] Rabinovich, A., On translations of temporal logic of actions into monadic second-order logic, Theoret. Comput. Sci., 193, 197-214 (February 1998) · Zbl 0896.03026
[40] Rozier, K. Y.; Vardi, M. Y., LTL satisfiability checking, (Proceedings of the 14th International SPIN Conference on Model Checking Software. Proceedings of the 14th International SPIN Conference on Model Checking Software, LNCS, vol. 4595 (2007), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 149-167
[42] Schaub, M. A.; Henzinger, T. A.; Fisher, J., Qualitative networks: a symbolic approach to analyze biological signaling networks, BMC Syst. Biol., 1, 4 (2007)
[43] Schurr, M. J.; Martin, D. W.; Mudd, M. H.; Deretic, V., Gene cluster controlling conversion to alginate-overproducing phenotype in Pseudomonas aeruginosa: functional analysis in a heterologous host and role in the instability of mucoidy, J. Bacteriol., 176, 3375-3382 (1994)
[44] Sistla, A. P.; Clarke, E. M., The complexity of propositional linear temporal logics, J. ACM, 32, 733-749 (July 1985) · Zbl 0632.68034
[45] Somenzi, F.; Bloem, R., Efficient Büchi automata from LTL formulae, (Proceedings of the 12th International Conference on Computer Aided Verification. Proceedings of the 12th International Conference on Computer Aided Verification, LNCS, vol. 1855 (2000), Springer-Verlag: Springer-Verlag London, UK), 248-263 · Zbl 0974.68086
[46] Thomas, R., Boolean formalization of genetic control circuits, J. Theoret. Biol., 42, 3, 563-585 (1973)
[47] Thomas, R.; Kaufman, M., Multistationarity, the basis of cell differentiation and memory. II. Logical analysis of regulatory networks in terms of feedback circuits, Chaos, 11, 1, 180-195 (2001) · Zbl 0997.92012
[48] Thomas, W., Automata on infinite objects, (van Leeuwen, Jan, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) (1990), MIT Press), 133-164 · Zbl 0900.68316
[49] Vanitha, V.; Yamashita, K.; Fukuzawa, K.; Yonezaki, N., A method for structuralisation of evolutional specifications of reactive systems, (ICSE 2000, The Third International Workshop on Intelligent Software Engineering. ICSE 2000, The Third International Workshop on Intelligent Software Engineering, WISE3 (2000)), 30-38
[50] Vardi, M. Y.; Wolper, P., Reasoning about infinite computations, Inform. and Comput., 115, 1-37 (November 1994) · Zbl 0827.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.