{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:12:34Z","timestamp":1742922754646,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642042430"},{"type":"electronic","value":"9783642042447"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04244-7_26","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T18:17:24Z","timestamp":1252952244000},"page":"319-334","source":"Crossref","is-referenced-by-count":10,"title":["From Model-Checking to Temporal Logic Constraint Solving"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Fages","sequence":"first","affiliation":[]},{"given":"Aur\u00e9lien","family":"Rizk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. Logic in Computer Science, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1385\/CBB:38:3:271","volume":"38","author":"M. Antoniotti","year":"2003","unstructured":"Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics\u00a038, 271\u2013286 (2003)","journal-title":"Cell Biochemistry and Biophysics"},{"issue":"1-2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming\u00a072(1-2), 3\u201321 (2008)","journal-title":"Science of Computer Programming"},{"issue":"suppl. 1","key":"26_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1093\/bioinformatics\/bti1048","volume":"21","author":"G. Batt","year":"2005","unstructured":"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\u00a021(suppl. 1), 19\u201328 (2005)","journal-title":"Bioinformatics"},{"issue":"18","key":"26_CR6","doi-asserted-by":"publisher","first-page":"2415","DOI":"10.1093\/bioinformatics\/btm362","volume":"23","author":"G. Batt","year":"2007","unstructured":"Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics\u00a023(18), 2415\u20132422 (2007)","journal-title":"Bioinformatics"},{"issue":"3","key":"26_CR7","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1016\/j.jtbi.2004.04.003","volume":"229","author":"G. Bernot","year":"2004","unstructured":"Bernot, G., Comet, J.-P., Richard, A., Guespin, J.: A fruitful application of formal methods to biological regulatory networks: Extending thomas\u2019 asynchronous logical approach with temporal logic. Journal of Theoretical Biology\u00a0229(3), 339\u2013347 (2004)","journal-title":"Journal of Theoretical Biology"},{"key":"26_CR8","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/11880646_3","volume-title":"Transactions on Computational Systems Biology VI","author":"M. Calder","year":"2006","unstructured":"Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using the continuous time markow chains. In: Plotkin, G. (ed.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol.\u00a04220, pp. 44\u201367. Springer, Heidelberg (2006); CMSB 2005 Special Issue"},{"key":"26_CR9","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/11880646_4","volume-title":"Transactions on Computational Systems Biology VI","author":"L. Calzone","year":"2006","unstructured":"Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol.\u00a04220, pp. 68\u201394. Springer, Heidelberg (2006); CMSB 2005 Special Issue"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-36481-1_13","volume-title":"Computational Methods in Systems Biology","author":"N. Chabrier","year":"2003","unstructured":"Chabrier, N., Fages, F.: Symbolic model checking of biochemical networks. In: Priami, C. (ed.) CMSB 2003. LNCS, vol.\u00a02602, pp. 149\u2013162. Springer, Heidelberg (2003)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W. Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 450\u2013463. Springer, Heidelberg (2000)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Chen, K.C., Csik\u00e1sz-Nagy, A., Gy\u00f6rffy, B., Val, J., Nov\u00e0k, B., Tyson, J.J.: Kinetic analysis of a molecular model of the budding yeast cell cycle. Molecular Biology of the Cell\u00a011, 396\u2013391 (2000)","DOI":"10.1091\/mbc.11.1.369"},{"key":"26_CR13","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"26_CR14","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Podelski, A.: Constraint-based deductive model checking. STTT\u00a03(3), 250\u2013270 (2001)","journal-title":"STTT"},{"key":"26_CR15","unstructured":"Egerstedt, M., Mishra, B.: (2008)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Kemal S\u00f6nmez, M.: Pathway logic: Symbolic analysis of biological signaling. In: Proceedings of the seventh Pacific Symposium on Biocomputing, January 2002, pp. 400\u2013412 (2002)","DOI":"10.1142\/9789812799623_0038"},{"issue":"1","key":"26_CR17","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.tcs.2008.07.004","volume":"408","author":"F. Fages","year":"2008","unstructured":"Fages, F., Rizk, A.: On temporal logic constraint solving for the analysis of numerical data time series. Theoretical Computer Science\u00a0408(1), 55\u201365 (2008)","journal-title":"Theoretical Computer Science"},{"key":"26_CR18","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-68413-8_7","volume-title":"Formal Methods in Systems Biology","author":"F. Fages","year":"2008","unstructured":"Fages, F., Soliman, S.: From reaction models to influence graphs and back: a theorem. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol.\u00a05054, pp. 90\u2013102. Springer, Heidelberg (2008)"},{"key":"26_CR19","unstructured":"Fages, F., Soliman, S., Rizk, A.: BIOCHAM v2.8 user\u2019s manual. In: INRIA (2009), http:\/\/contraintes.inria.fr\/BIOCHAM"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Proy, Y.e., Roumanoff, P.: Verification of real-time systems using linear relation analysis. In: Formal Methods in System Design, pp. 157\u2013185 (1997)","DOI":"10.1023\/A:1008678014487"},{"issue":"2","key":"26_CR21","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1162\/106365601750190398","volume":"9","author":"N. Hansen","year":"2001","unstructured":"Hansen, N., Ostermeier, A.: Completely derandomized self-adaptation in evolution strategies. Evolutionary Computation\u00a09(2), 159\u2013195 (2001)","journal-title":"Evolutionary Computation"},{"key":"26_CR22","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11885191_3","volume-title":"Computational Methods in Systems Biology","author":"J. Heath","year":"2006","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol.\u00a04210, pp. 32\u201347. Springer, Heidelberg (2006)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013463. Springer, Heidelberg (1997)"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Janssen, M., Van Hentenryck, P., Deville, Y.: A constraint satisfaction approach for enclosing solutions to parametric ordinary differential equations. SIAM Journal on Numerical Analysis\u00a040(5) (2002)","DOI":"10.1137\/S0036142901392316"},{"key":"26_CR25","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1038\/msb4100179","volume":"3","author":"H. Kitano","year":"2007","unstructured":"Kitano, H.: Towards a theory of biological robustness. Molecular Systems Biology\u00a03, 137 (2007)","journal-title":"Molecular Systems Biology"},{"key":"26_CR26","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer\u00a01, 134\u2013152 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"11","key":"26_CR27","doi-asserted-by":"publisher","first-page":"5818","DOI":"10.1073\/pnas.97.11.5818","volume":"97","author":"A. Levchenko","year":"2000","unstructured":"Levchenko, A., Bruck, J., Sternberg, P.W.: Scaffold proteins may biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties. PNAS\u00a097(11), 5818\u20135823 (2000)","journal-title":"PNAS"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"26_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-45099-3_2","volume-title":"Static Analysis","author":"A. Podelski","year":"2000","unstructured":"Podelski, A.: Model checking as constraint solving. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 22\u201337. Springer, Heidelberg (2000)"},{"issue":"9","key":"26_CR31","doi-asserted-by":"publisher","first-page":"1819","DOI":"10.1371\/journal.pcbi.0030184","volume":"3","author":"L. Qiao","year":"2007","unstructured":"Qiao, L., Nachbar, R.B., Kevrekidis, I.G., Shvartsman, S.Y.: Bistability and oscillations in the huang-ferrell model of mapk signaling. PLoS Computational Biology\u00a03(9), 1819\u20131826 (2007)","journal-title":"PLoS Computational Biology"},{"key":"26_CR32","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-88562-7_19","volume-title":"Computational Methods in Systems Biology","author":"A. Rizk","year":"2008","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 251\u2013268. Springer, Heidelberg (2008)"},{"issue":"12","key":"26_CR33","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1093\/bioinformatics\/btp200","volume":"25","author":"A. Rizk","year":"2009","unstructured":"Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. BioInformatics\u00a025(12), 169\u2013178 (2009)","journal-title":"BioInformatics"},{"key":"26_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"B. Tevfik","year":"1997","unstructured":"Tevfik, B., Richard, G., William, P.: Symbolic model checking of infinite state systems using presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state space. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2009"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04244-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T04:15:46Z","timestamp":1739333746000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04244-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042430","9783642042447"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04244-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}