{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T04:13:30Z","timestamp":1749615210084,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_23","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T02:11:57Z","timestamp":1474423917000},"page":"405-421","source":"Crossref","is-referenced-by-count":1,"title":["Temporal Logic Verification for Delay Differential Equations"],"prefix":"10.1007","author":[{"given":"Peter","family":"Nazier Mosaad","sequence":"first","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Bai","family":"Xue","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"issue":"1","key":"23_CR1","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-25942-0_4","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"G Babin","year":"2015","unstructured":"Babin, G., A\u00eft-Ameur, Y., Nakajima, S., Pantel, M.: Refinement and proof based development of\u00a0systems characterized by continuous functions. In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 55\u201370. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25942-0_4"},{"key":"23_CR3","unstructured":"Bellman, R., Cooke, K.L.: Differential-difference equations. Technical report R-374-PR, The RAND Corporation, Santa Monica, California, January 1963"},{"issue":"4","key":"23_CR4","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M Berz","year":"1998","unstructured":"Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliable Comput."},{"key":"23_CR5","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1201\/b20053-5","volume-title":"From Action Systems to Distributed Systems - The Refinement Approach","author":"MJ Butler","year":"2016","unstructured":"Butler, M.J., Abrial, J.-R., Banach, R.: Modelling and refining hybrid systems in Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action Systems to Distributed Systems - The Refinement Approach, pp. 29\u201342. Chapman and Hall\/CRC, Boca Raton (2016)"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th International Conference on Decision and Control (CDC 1998) (1998)","DOI":"10.1109\/CDC.1998.758642"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-88387-6_14"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/11867340_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"GE Fainekos","year":"2006","unstructured":"Fainekos, G.E., Girard, A., Pappas, G.J.: Temporal logic verification using simulation. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 171\u2013186. Springer, Heidelberg (2006)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for finite state sequences in metric spaces. Technical report MS-CIS-06-05, Dept. of CIS, Univ. of Pennsylvania (2006)","DOI":"10.1007\/11940197_12"},{"issue":"4","key":"23_CR11","doi-asserted-by":"crossref","first-page":"867","DOI":"10.1103\/PhysRevLett.82.867","volume":"82","author":"J Fort","year":"1999","unstructured":"Fort, J., M\u00e9ndez, V.: Time-delayed theory of the neolithic transition in Europe. Phys. Rev. Lett. 82(4), 867 (1999)","journal-title":"Phys. Rev. Lett."},{"key":"23_CR12","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiability, Boolean Model. Comput. - Special Issue on SAT\/CP Integr. 1, 209\u2013236 (2007)","journal-title":"J. Satisfiability, Boolean Model. Comput. - Special Issue on SAT\/CP Integr."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, pp. 105\u2013112. IEEE, 20\u201323 October 2013","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005)"},{"key":"23_CR15","doi-asserted-by":"crossref","DOI":"10.1515\/9780691221793","volume-title":"From Clocks to Chaos: The Rhythms of Life","author":"L Glass","year":"1988","unstructured":"Glass, L., Mackey, M.C.: From Clocks to Chaos: The Rhythms of Life. Princeton University Press, Princeton (1988)"},{"issue":"1\u20132","key":"23_CR16","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0167-2789(87)90058-3","volume":"29","author":"K Ikeda","year":"1987","unstructured":"Ikeda, K., Matsumoto, K.: High-dimensional chaotic behavior in systems with time-delayed feedback. Physica D 29(1\u20132), 223\u2013235 (1987)","journal-title":"Physica D"},{"issue":"4","key":"23_CR17","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-642-24310-3_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240\u2013255. Springer, Heidelberg (2011)"},{"key":"23_CR19","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/10984413_12","volume-title":"New Directions and Applications in Control Theory","author":"AB Kurzhanski","year":"2005","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Kurzhanski, A.B., Varaiya, P. (eds.) New Directions and Applications in Control Theory. LNCIS, vol. 321, pp. 193\u2013205. Springer, Heidelberg (2005)"},{"key":"23_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14938-2","volume-title":"Dynamics of Nonlinear Time-Delay Systems","author":"M Lakshmanan","year":"2011","unstructured":"Lakshmanan, M., Senthilkumar, D.V.: Dynamics of Nonlinear Time-Delay Systems. Springer, Heidelberg (2011)"},{"issue":"2","key":"23_CR21","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"23_CR22","unstructured":"Lohner, R.: Einschlie\u00dfung der L\u00f6sung gew\u00f6hnlicher Anfangs- und Randwertaufgaben. Ph.D. thesis, Fakult\u00e4t f\u00fcr Mathematik der Universit\u00e4t Karlsruhe, Karlsruhe (1988)"},{"issue":"4300","key":"23_CR23","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1126\/science.267326","volume":"197","author":"MC Mackey","year":"1977","unstructured":"Mackey, M.C., Glass, L., et al.: Oscillation and chaos in physiological control systems. Science 197(4300), 287\u2013289 (1977)","journal-title":"Science"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_1"},{"key":"23_CR25","first-page":"103","volume-title":"Error in Digital Computation","author":"RE Moore","year":"1965","unstructured":"Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation, vol. II, pp. 103\u2013140. Wiley, New York (1965)"},{"issue":"1","key":"23_CR26","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1137\/050638448","volume":"45","author":"M Neher","year":"2007","unstructured":"Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236\u2013262 (2007)","journal-title":"SIAM J. Numer. Anal."},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, pp. 188\u2013197. IEEE Computer Society, 26\u201329 June 2005","DOI":"10.1109\/LICS.2005.33"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008)"},{"key":"23_CR29","unstructured":"Scheiber, K.: iSAT3 Manual, April 2014"},{"key":"23_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). doi: 10.1007\/3-540-40922-X_8"},{"key":"23_CR31","unstructured":"Stauning, O.: Automatic validation of numerical solutions. Ph.D. thesis, Technical University of Denmark, Lyngby (1997)"},{"issue":"2","key":"23_CR32","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/j.chaos.2004.11.012","volume":"25","author":"M Szyd\u0142owski","year":"2005","unstructured":"Szyd\u0142owski, M., Krawiec, A.: The stability problem in the kaldor-kalecki business cycle model. Chaos, Solitons & Fractals 25(2), 299\u2013305 (2005)","journal-title":"Chaos, Solitons & Fractals"},{"issue":"3","key":"23_CR33","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1016\/S0960-0779(99)00207-6","volume":"12","author":"M Szyd\u0142owski","year":"2001","unstructured":"Szyd\u0142owski, M., Krawiec, A., Tobo\u0142a, J.: Nonlinear oscillations in business cycle model with time lags. Chaos, Solitons & Fractals 12(3), 505\u2013517 (2001)","journal-title":"Chaos, Solitons & Fractals"},{"key":"23_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/978-3-319-21668-3_20","volume-title":"Computer Aided Verification","author":"L Zou","year":"2015","unstructured":"Zou, L., Fr\u00e4nzle, M., Zhan, N., Nazier Mosaad, P.: Automatic verification of stability and safety for delay differential equations. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part II. LNCS, vol. 9207, pp. 338\u2013355. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T20:22:35Z","timestamp":1749586955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}