On temporal logic constraint solving for analyzing numerical data time series. (English) Zbl 1160.68545
Summary: Temporal logics and model-checking have proved successful in expressing biological properties of complex biochemical systems, and automatically verify their satisfaction, in both qualitative and quantitative models. In this article, we go beyond model-checking and present a constraint solving algorithm for quantifier-free first-order temporal logic formulae, with constraints over the reals. This algorithm computes the domain of the real valued variables occurring in a formula that makes it true in a model. We illustrate this approach for the automatic generation of a temporal logic specification from biological data time series. We provide a set of biologically relevant patterns of formulae, and apply them to numerical data time series of models of the cell cycle control and MAPK signal transduction. We show in these examples that this approach infers automatically semi-qualitative, semi-quantitative information about concentration thresholds, amplitude of oscillations, stability properties, checkpoints and influences between species.
MSC:
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
| 68W05 | Nonnumerical algorithms |
| 03B44 | Temporal logic |
References:
| [1] | Antoniotti, Marco; Policriti, Alberto; Ugel, Nadia; Mishra, Bud, Model building and model checking for biochemical processes, Cell Biochemistry and Biophysics, 38, 271-286 (2003) |
| [2] | Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu, Model checking genetic regulatory networks using gna and cadp, in: Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN’2004, Barcelona, Spain, April 2004; Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu, Model checking genetic regulatory networks using gna and cadp, in: Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN’2004, Barcelona, Spain, April 2004 · Zbl 1125.68384 |
| [3] | Bernot, Gilles; Comet, Jean-Paul; Richard, Adrien; Guespin, J., A fruitful application of formal methods to biological regulatory networks: Extending thomas’ asynchronous logical approach with temporal logic, Journal of Theoretical Biology, 229, 3, 339-347 (2004) · Zbl 1440.92036 |
| [4] | Calder, Muffy; Vyshemirsky, Vladislav; Gilbert, David; Orton, Richard, Analysis of signalling pathways using the continuous time markow chains, (Plotkin, Gordon, Transactions on Computational Systems Biology VI. Transactions on Computational Systems Biology VI, Lecture Notes in BioInformatics, vol. 4220 (2006), Springer-Verlag), 44-67, (CMSB’05 special issue) |
| [5] | Calzone, Laurence; Chabrier-Rivier, Nathalie; Fages, François; Soliman, Sylvain, Machine learning biochemical networks from temporal logic properties, (Plotkin, Gordon, Transactions on Computational Systems Biology VI. Transactions on Computational Systems Biology VI, Lecture Notes in BioInformatics, vol. 4220 (2006), Springer-Verlag), 68-94, (CMSB’05 special issue) |
| [6] | Calzone, Laurence; Fages, François; Soliman, Sylvain, BIOCHAM: An environment for modeling biological systems and formalizing experimental knowledge, BioInformatics, 22, 14, 1805-1807 (2006) |
| [7] | Cardelli, Luca, Brane calculi-interactions of biological membranes, (Danos, Vincent; Schächter, Vincent, CMSB’04: Proceedings of the Second International Workshop on Computational Methods in Systems Biology. CMSB’04: Proceedings of the Second International Workshop on Computational Methods in Systems Biology, Lecture Notes in BioInformatics, vol. 3082 (2004), Springer-Verlag), 257-280 · Zbl 1088.68657 |
| [8] | Chabrier, Nathalie; Fages, François, Symbolic model checking of biochemical networks, (Priami, Corrado, CMSB’03: Proceedings of the First Workshop on Computational Methods in Systems Biology. CMSB’03: Proceedings of the First Workshop on Computational Methods in Systems Biology, March 2003, Rovereto, Italy. CMSB’03: Proceedings of the First Workshop on Computational Methods in Systems Biology. CMSB’03: Proceedings of the First Workshop on Computational Methods in Systems Biology, March 2003, Rovereto, Italy, Lecture Notes in Computer Science, vol. 2602 (2003), Springer-Verlag), 149-162 · Zbl 1112.92312 |
| [9] | Chabrier-Rivier, Nathalie; Chiaverini, Marc; Danos, Vincent; Fages, François; Schächter, Vincent, Modeling and querying biochemical interaction networks, Theoretical Computer Science, 325, 1, 25-44 (2004) · Zbl 1071.68098 |
| [10] | Chen, Katherine C.; Csikász-Nagy, Attila; Györffy, Bela; Val, John; Novàk, Bela; Tyson, John J., Kinetic analysis of a molecular model of the budding yeast cell cycle, Molecular Biology of the Cell, 11 (2000), 396-391 |
| [11] | Clarke, Edmund M.; Grumberg, Orna; Peled, Doron A., Model Checking (1999), MIT Press |
| [12] | Danos, Vincent; Laneve, Cosimo, Formal molecular biology, Theoretical Computer Science, 325, 1, 69-110 (2004) · Zbl 1071.68041 |
| [13] | Steven Eker, Merrill Knapp, Keith Laderoute, Patrick Lincoln, José Meseguer, M. Kemal Sönmez, Pathway logic: Symbolic analysis of biological signaling, in: Proceedings of the Seventh Pacific Symposium on Biocomputing, January 2002, pp. 400-412; Steven Eker, Merrill Knapp, Keith Laderoute, Patrick Lincoln, José Meseguer, M. Kemal Sönmez, Pathway logic: Symbolic analysis of biological signaling, in: Proceedings of the Seventh Pacific Symposium on Biocomputing, January 2002, pp. 400-412 |
| [14] | Fages, François, Temporal logic constraints in the biochemical abstract machine biocham (invited talk), (Proceedings of Logic Based Program Synthesis and Transformation, LOPSTR’05. Proceedings of Logic Based Program Synthesis and Transformation, LOPSTR’05, September 2005. Proceedings of Logic Based Program Synthesis and Transformation, LOPSTR’05. Proceedings of Logic Based Program Synthesis and Transformation, LOPSTR’05, September 2005, Lecture Notes in Computer Science, vol. 3901 (2005), Springer-Verlag: Springer-Verlag London, UK) · Zbl 1156.68377 |
| [15] | Fages, François, From syntax to semantics in systems biology — towards automated reasoning tools, Transactions on Computational Systems Biology IV, 3939, 68-70 (2006) |
| [16] | Fages, François; Soliman, Sylvain; Chabrier-Rivier, Nathalie, Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM, Journal of Biological Physics and Chemistry, 4, 2, 64-73 (2004) |
| [17] | Gilbert, David; Heiner, Monika; Lehrack, Sebastian, A unifying framework for modelling and analysing biochemical pathways using petri nets, (CMSB’07: Proceedings of the Fifth International Conference on Computational Methods in Systems Biology. CMSB’07: Proceedings of the Fifth International Conference on Computational Methods in Systems Biology, Lecture Notes in Computer Science, vol. 4695 (2007), Springer-Verlag) · Zbl 1260.68268 |
| [18] | Heath, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Tymchyshyn, O., Probabilistic model checking of complex biological pathways, (Proc. Computational Methods in Systems Biology. Proc. Computational Methods in Systems Biology, CMSB’06. Proc. Computational Methods in Systems Biology. Proc. Computational Methods in Systems Biology, CMSB’06, Lecture Notes in Computer Science, vol. 4210 (2006), Springer-Verlag), 32-47 |
| [19] | Iftach Nachman, Aviv Regev, Nir Friedman, Inferring quantitative models of regulatory networks from expression data, in: ISMB/ECCB (Supplement of Bioinformatics), 2004, pp. 248-256; Iftach Nachman, Aviv Regev, Nir Friedman, Inferring quantitative models of regulatory networks from expression data, in: ISMB/ECCB (Supplement of Bioinformatics), 2004, pp. 248-256 |
| [20] | Nickovic, Dejan; Maler, Oded, Amt: A property-based monitoring tool for analog systems, (Proceedings of 5th International Conference on Formal Modelling and Analysis of Times Systems, FORMATS’07. Proceedings of 5th International Conference on Formal Modelling and Analysis of Times Systems, FORMATS’07, Salzburg, Austria. Proceedings of 5th International Conference on Formal Modelling and Analysis of Times Systems, FORMATS’07. Proceedings of 5th International Conference on Formal Modelling and Analysis of Times Systems, FORMATS’07, Salzburg, Austria, Lecture Notes in Computer Science (2007), Springer-Verlag) · Zbl 1109.68518 |
| [21] | Andrew Phillips, Luca Cardelli, A correct abstract machine for the stochastic pi-calculus. Transactions on Computational Systems Biology, 2005 (special issue of BioConcur 2004); Andrew Phillips, Luca Cardelli, A correct abstract machine for the stochastic pi-calculus. Transactions on Computational Systems Biology, 2005 (special issue of BioConcur 2004) |
| [22] | Reddy, V. N.; Mavrovouniotis, M. L.; Liebman, M. N., Petri net representations in metabolic pathways, (Hunter, L.; Searls, D. B.; Shavlik, J. W., Proceedings of the 1st International Conference on Intelligent Systems for Molecular Biology. Proceedings of the 1st International Conference on Intelligent Systems for Molecular Biology, ISMB (1993), AAAI Press), 328-336 |
| [23] | Regev, Aviv; Panina, Ekaterina M.; Silverman, William; Cardelli, Luca; Shapiro, Ehud, Bioambients: An abstraction for biological compartments, Theoretical Computer Science, 325, 1, 141-167 (2004) · Zbl 1069.68569 |
| [24] | Aviv Regev, William Silverman, Ehud Y. Shapiro, Representation and simulation of biochemical processes using the pi-calculus process algebra, in: Proceedings of the Sixth Pacific Symposium of Biocomputing, 2001, pp. 459-470; Aviv Regev, William Silverman, Ehud Y. Shapiro, Representation and simulation of biochemical processes using the pi-calculus process algebra, in: Proceedings of the Sixth Pacific Symposium of Biocomputing, 2001, pp. 459-470 |
| [25] | Xu, Rui; Hu, Xiao; Wunsch, Donald C., Inference of genetic regulatory networks from time series gene expression data, JCNN, 2, 1215-1220 (2004) |
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.
