×

Modeling and querying biomolecular interaction networks. (English) Zbl 1071.68098

Summary: We introduce a formalism to represent and analyze protein-protein and protein-DNA interaction networks. We illustrate the expressivity of this language by proposing a formal counterpart of Kohn’s compilation on the mammalian cell-cycle control. This effectively turns an otherwise static knowledge into a discrete transition system incorporating a qualitative description of the dynamics. We then propose to use the Computation Tree Logic (CTL) as a query language for querying the possible behaviors of the system. We provide examples of biologically relevant queries expressed in CTL about the mammalian cell-cycle control and show the effectiveness of symbolic model checking tools to evaluate CTL queries in this context.

MSC:

68U20 Simulation (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
92C40 Biochemistry, molecular biology

Software:

NuSMV
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G.J. Pappas, H. Rubin, J. Schug, Hybrid modeling and simulation of biomolecular networks, in: Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2034, Springer, Berlin, 2001, pp. 19-32.; R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G.J. Pappas, H. Rubin, J. Schug, Hybrid modeling and simulation of biomolecular networks, in: Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2034, Springer, Berlin, 2001, pp. 19-32. · Zbl 0993.92010
[2] A. Bockmayr, A. Courtois, Using hybrid concurrent constraint programming to model dynamic biological systems, in: 18th Internat. Conf. on Logic Programming, Copenhagen, Springer, Berlin, 2002, pp. 85-99.; A. Bockmayr, A. Courtois, Using hybrid concurrent constraint programming to model dynamic biological systems, in: 18th Internat. Conf. on Logic Programming, Copenhagen, Springer, Berlin, 2002, pp. 85-99. · Zbl 1045.68527
[3] L. Cardelli, Brane calculi, ENTCS Proc. of Bio-Concur, 2003, to appear.; L. Cardelli, Brane calculi, ENTCS Proc. of Bio-Concur, 2003, to appear.
[4] N. Chabrier, F. Fages, The biochemical abstract machine BIOCHAM, in: C. Christophe, H.P. Lenhof, M.F. Sagot (Eds.), Proc. European Conf. Computational Biology, ECCB’03, Paris, France, September 2003, pp. 597-599. System available at; N. Chabrier, F. Fages, The biochemical abstract machine BIOCHAM, in: C. Christophe, H.P. Lenhof, M.F. Sagot (Eds.), Proc. European Conf. Computational Biology, ECCB’03, Paris, France, September 2003, pp. 597-599. System available at · Zbl 1088.68817
[5] N. Chabrier, F. Fages, Symbolic model checking of biochemical networks, in: C. Priami (Ed.), Proc. Internat. Workshop on Computational Methods in Systems Biology, CMSB’03, Rovereto, Italy, Lecture Notes in Computer Science, Springer, Berlin, February 2003, pp. 149-162.; N. Chabrier, F. Fages, Symbolic model checking of biochemical networks, in: C. Priami (Ed.), Proc. Internat. Workshop on Computational Methods in Systems Biology, CMSB’03, Rovereto, Italy, Lecture Notes in Computer Science, Springer, Berlin, February 2003, pp. 149-162. · Zbl 1112.92312
[6] W. Chan, Temporal logic queries, in: Proc. 12th Internat. Conf. Computer Aided Verification CAV’00, Chicago, USA, Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 2000, pp. 450-463.; W. Chan, Temporal logic queries, in: Proc. 12th Internat. Conf. Computer Aided Verification CAV’00, Chicago, USA, Lecture Notes in Computer Science, Vol. 1855, Springer, Berlin, 2000, pp. 450-463. · Zbl 0974.68525
[7] M. Chiaverini, V. Danos, A formalization of Kohn’s molecular map; available at www.pps.jussieu.fr/ bioconcu/kohn_map.html; M. Chiaverini, V. Danos, A formalization of Kohn’s molecular map; available at www.pps.jussieu.fr/ bioconcu/kohn_map.html
[8] A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an opensource tool for symbolic model checking, in: Proc. Internat. Conf. Computer-Aided Verification, CAV’2002, Copenhagen, Denmark, July 2002.; A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an opensource tool for symbolic model checking, in: Proc. Internat. Conf. Computer-Aided Verification, CAV’2002, Copenhagen, Denmark, July 2002. · Zbl 1010.68766
[9] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), MIT Press: MIT Press Cambridge, MA
[10] V. Danos, J. Krivine, Formal molecular biology done in CCS, in: Proc. BIO-CONCUR’03, Marseille, France, Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam, 2003, to appear.; V. Danos, J. Krivine, Formal molecular biology done in CCS, in: Proc. BIO-CONCUR’03, Marseille, France, Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam, 2003, to appear.
[11] V. Danos, C. Laneve, Core formal molecular biology, in: Proc. 12th European Symp. on Programming, ESOP’03, Lecture Notes in Computer Science, Vol. 2618, Springer, Berlin, April 2003, pp. 302-318.; V. Danos, C. Laneve, Core formal molecular biology, in: Proc. 12th European Symp. on Programming, ESOP’03, Lecture Notes in Computer Science, Vol. 2618, Springer, Berlin, April 2003, pp. 302-318. · Zbl 1033.92013
[12] V. Danos, C. Laneve, Graphs for formal molecular biology, in: Proc. First Internat. Workshop on Computational Methods in Systems Biology, CMSB’03, Lecture Notes in Computer Science, Vol. 2602, Springer, Berlin, February 2003, pp. 34-46.; V. Danos, C. Laneve, Graphs for formal molecular biology, in: Proc. First Internat. Workshop on Computational Methods in Systems Biology, CMSB’03, Lecture Notes in Computer Science, Vol. 2602, Springer, Berlin, February 2003, pp. 34-46. · Zbl 1053.92021
[13] G. Delzanno, A. Podelski, Model checking in CLP, in: Proc. 5th Internat. Conf. on Tools and Algorithms for Construction and Analysis of Systems TACAS’99, Lecture Notes in Computer Science, Vol. 1579, Springer, Berlin, January 1999, pp. 223-239.; G. Delzanno, A. Podelski, Model checking in CLP, in: Proc. 5th Internat. Conf. on Tools and Algorithms for Construction and Analysis of Systems TACAS’99, Lecture Notes in Computer Science, Vol. 1579, Springer, Berlin, January 1999, pp. 223-239.
[14] S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer, K. Sonmez, Pathway logic: symbolic analysis of biological signaling, in: Proc. Pacific Symp. on Biocomputing, January 2002, pp. 400-412.; S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer, K. Sonmez, Pathway logic: symbolic analysis of biological signaling, in: Proc. Pacific Symp. on Biocomputing, January 2002, pp. 400-412.
[15] E.A. Emerson, in: J. van Leeuwen (Ed.), Temporal and Modal Logic, North-Holland, Amsterdam, MIT Press, Cambridge, MA, 1990, pp. 995-1072.; E.A. Emerson, in: J. van Leeuwen (Ed.), Temporal and Modal Logic, North-Holland, Amsterdam, MIT Press, Cambridge, MA, 1990, pp. 995-1072. · Zbl 0900.03030
[16] R. Ghosh, C. Tomlin, Lateral inhibition through delta-notch signaling: a piecewise affine hybrid model, in: Springer (Ed.), Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2034, Springer, Berlin, 2001, pp. 232-246.; R. Ghosh, C. Tomlin, Lateral inhibition through delta-notch signaling: a piecewise affine hybrid model, in: Springer (Ed.), Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, Vol. 2034, Springer, Berlin, 2001, pp. 232-246. · Zbl 0997.92010
[17] A. Gurfinkel, M. Chechik, B. Devereux, Temporal logic query checking: a tool for model exploration, IEEE Trans. Software Eng. (2003) (Special FSE’02 Issue).; A. Gurfinkel, M. Chechik, B. Devereux, Temporal logic query checking: a tool for model exploration, IEEE Trans. Software Eng. (2003) (Special FSE’02 Issue).
[18] R. Hofestädt, S. Thelen, Quantitative modeling of biochemical networks, in: In Silico Biology, Vol. 1, 1998, pp. 39-53.; R. Hofestädt, S. Thelen, Quantitative modeling of biochemical networks, in: In Silico Biology, Vol. 1, 1998, pp. 39-53.
[19] S. Hornus, Ph. Schnoebelen, On solving temporal logic queries, in: Proc. 9th Internat. Conf. Algebraic Methodology and Software Technology AMAST’02, Saint Gilles les Bains, Reunion Island, France, Lecture Notes in Computer Science, Vol. 2422, Springer, Berlin, 2002, pp. 163-177.; S. Hornus, Ph. Schnoebelen, On solving temporal logic queries, in: Proc. 9th Internat. Conf. Algebraic Methodology and Software Technology AMAST’02, Saint Gilles les Bains, Reunion Island, France, Lecture Notes in Computer Science, Vol. 2422, Springer, Berlin, 2002, pp. 163-177. · Zbl 1275.68093
[20] de Jong, H., Modeling and simulation of genetic regulatory systemsa literature review, J. Comput. Biol, 9, 1, 69-105 (2001)
[21] Kohn, K. W., Molecular interaction map of the mammalian cell cycle control and DNA repair systems, Mol. Biol. Cell, 10, 8, 703-734 (1999)
[22] F. Laroussinie, N. Marley, Ph. Schnoebelen, On model checking durational Kripke structures, in: Proc. 5th Internat. Conf. on Foundations of Software Science and Computation Structures FOSSACS’02, Grenoble, France, Lecture Notes in Computer Science, Vol. 2303, Springer, Berlin, 2002, pp. 264-279.; F. Laroussinie, N. Marley, Ph. Schnoebelen, On model checking durational Kripke structures, in: Proc. 5th Internat. Conf. on Foundations of Software Science and Computation Structures FOSSACS’02, Grenoble, France, Lecture Notes in Computer Science, Vol. 2303, Springer, Berlin, 2002, pp. 264-279.
[23] R. Maimon, S. Browning, Diagrammatic notation and computational structure of gene networks, in: Proc. 2nd Internat. Conf. on Systems Biology, 2001.; R. Maimon, S. Browning, Diagrammatic notation and computational structure of gene networks, in: Proc. 2nd Internat. Conf. on Systems Biology, 2001.
[24] H. Matsuno, A. Doi, M. Nagasaki, S. Miyano, Hybrid Petri net representation of gene regulatory network, in: Pacific Symp. on Biocomputing, Vol. 5, 2000, pp. 338-349.; H. Matsuno, A. Doi, M. Nagasaki, S. Miyano, Hybrid Petri net representation of gene regulatory network, in: Pacific Symp. on Biocomputing, Vol. 5, 2000, pp. 338-349.
[25] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes I and II, Inform. and Comput, 100, 1, 41, 42.78 (1992)
[26] A. Regev, E.M. Panina, W. Silverman, L. Cardelli, E. Shapiro, Bioambients: an abstraction for biological compartments, Theoret. Comput. Sci. (2003) to appear.; A. Regev, E.M. Panina, W. Silverman, L. Cardelli, E. Shapiro, Bioambients: an abstraction for biological compartments, Theoret. Comput. Sci. (2003) to appear. · Zbl 1069.68569
[27] A. Regev, W. Silverman, E. Shapiro, Representation and simulation of biochemical processes using the pi-calculus process algebra, in: Proc. Pacific Symp. of Biocomputing, 2001, pp. 6:459-470.; A. Regev, W. Silverman, E. Shapiro, Representation and simulation of biochemical processes using the pi-calculus process algebra, in: Proc. Pacific Symp. of Biocomputing, 2001, pp. 6:459-470.
[28] Schoeberl, B.; Eichler-Jonsson, C.; Gilles, E. D.; Müller, G., Computational modeling of the dynamics of the map kinase cascade activated by surface and internalized EGF receptors, Nature Biotechnol, 20, 370-375 (2002)
[29] Shankar, U. A., An introduction to assertionnal reasoning for concurrent systems, ACM Comput. Surveys, 3, 25, 225-262 (1993)
[30] D. Thieffry, R. Thomas, Qualitative analysis of gene networks, in: R.B. Altman, A.K. Dunker, L. Hunter, T.E. Klein (Eds.), Pacific Symp. Biocomputing, Vol. 3, World Scientific, Singapore, 1998, pp. 77-88.; D. Thieffry, R. Thomas, Qualitative analysis of gene networks, in: R.B. Altman, A.K. Dunker, L. Hunter, T.E. Klein (Eds.), Pacific Symp. Biocomputing, Vol. 3, World Scientific, Singapore, 1998, pp. 77-88.
[31] D. Wang, E. Clarke, Y. Zhu, J. Kukula, Using cutwidth to improve symbolic simulation and boolean satisfiability, in: Proc. HLDVT’2001, 2001.; D. Wang, E. Clarke, Y. Zhu, J. Kukula, Using cutwidth to improve symbolic simulation and boolean satisfiability, in: Proc. HLDVT’2001, 2001.
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.