{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T18:15:15Z","timestamp":1759515315452},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642314230"},{"type":"electronic","value":"9783642314247"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_27","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"343-361","source":"Crossref","is-referenced-by-count":15,"title":["Timed Relational Abstractions for Sampled Data Control Systems"],"prefix":"10.1007","author":[{"given":"Aditya","family":"Zutshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-36577-X_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counter-Example Guided Predicate Abstraction of Hybrid Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 208\u2013223. Springer, Heidelberg (2003)"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal methods based development of a PCA infusion pump reference model: Generic infusion pump (GIP) project. In: Proc. High Confidence Medical Devices, Software Systems and Medical Device Plug and Play Interoperability (2007)","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"27_CR3","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E. Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica\u00a043, 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: POPL, pp. 211\u2013224. ACM (2007)","DOI":"10.1145\/1190215.1190249"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Bochev, P., Markov, S.: A self-validating numerical method for the matrix exponential. Computing\u00a043(1), 59\u201372","DOI":"10.1007\/BF02243806"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-75596-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic Fault Tree Analysis for Reactive Systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 162\u2013176. Springer, Heidelberg (2007)"},{"issue":"5","key":"27_CR8","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G. Collins","year":"1975","unstructured":"Collins, G.: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: HSCC 2010, pp. 11\u201320. ACM (2010)","DOI":"10.1145\/1755952.1755956"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"2","key":"27_CR13","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin\u00a031(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bulletin"},{"key":"27_CR14","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver. Cf, \n                    \n                      http:\/\/yices.csl.sri.com\/tool-paper.pdf\n                    \n                    \n                   (last viewed January 2009)"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2004","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for Hybrid Systems Verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 326\u2013341. Springer, Heidelberg (2004)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a03414, pp. 291\u2013305. Springer, Heidelberg (2005)"},{"key":"27_CR18","unstructured":"Goldsztejn, A.: On the exponentiation of interval matrices. Preprint (Working Paper) # hal-00411330, version 1. Cf (2009), \n                    \n                      http:\/\/hal.archives-ouvertes.fr\/hal-00411330\/fr\/"},{"issue":"2","key":"27_CR19","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C.L. Guernic","year":"2010","unstructured":"Guernic, C.L., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems\u00a04(2), 250\u2013262 (2010)","journal-title":"Nonlinear Analysis: Hybrid Systems"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI (2009)","DOI":"10.1145\/1542476.1542518"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-Based Approach for Analysis of Hybrid Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 190\u2013203. Springer, Heidelberg (2008)"},{"issue":"2","key":"27_CR22","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in System Design"},{"key":"27_CR23","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control\u00a043, 540\u2013554 (1998)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-48294-6_3","volume-title":"Static Analysis","author":"B. Jeannet","year":"1999","unstructured":"Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic Partitioning in Analyses of Numerical Properties. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 39\u201350. Springer, Heidelberg (1999)"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-46430-1_19","volume-title":"Hybrid Systems: Computation and Control","author":"A.B. Kurzhanski","year":"2000","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal Techniques for Reachability Analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 202\u2013214. Springer, Heidelberg (2000)"},{"key":"27_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"issue":"1","key":"27_CR27","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1137\/S00361445024180","volume":"45","author":"C. Moler","year":"2003","unstructured":"Moler, C., Loan, C.V.: Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM Review\u00a045(1), 161\u2013208 (2003)","journal-title":"SIAM Review"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Moore, R., Kearfott, R.B., Cloud, M.: Introduction to Interval Analysis. SIAM (2009)","DOI":"10.1137\/1.9780898717716"},{"issue":"10","key":"27_CR29","doi-asserted-by":"publisher","first-page":"1230","DOI":"10.1109\/31.7598","volume":"35","author":"E.P. Oppenheimer","year":"1988","unstructured":"Oppenheimer, E.P., Michel, A.N.: Application of interval analysis techniques to linear systems. II. the interval matrix exponential function. IEEE Trans. on Circuits and Systems\u00a035(10), 1230\u20131242 (1988)","journal-title":"IEEE Trans. on Circuits and Systems"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/11730637_38","volume-title":"Hybrid Systems: Computation and Control","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Wagner, S.: Model Checking of Hybrid Systems: From Reachability Towards Stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 507\u2013521. Springer, Heidelberg (2006)"},{"key":"27_CR32","unstructured":"Rushby, J., Lincoln, P., Owre, S., Shankar, N., Tiwari, A.: Symbolic analysis laboratory (sal). Cf, \n                    \n                      http:\/\/www.csl.sri.com\/projects\/sal\/"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Dang, T., Ivan\u010di\u0107, F.: Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 188\u2013202. Springer, Heidelberg (2008)"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-24310-3_22","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan, S., Homaei, H., Lewis, C.: Model-Based Dependability Analysis of Programmable Drug Infusion Pumps. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol.\u00a06919, pp. 317\u2013334. Springer, Heidelberg (2011)"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1007\/978-3-642-22110-1_56","volume-title":"Computer Aided Verification","author":"S. Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan, S., Tiwari, A.: Relational Abstractions for Continuous and Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 686\u2013702. Springer, Heidelberg (2011)"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","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: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"27_CR37","doi-asserted-by":"crossref","unstructured":"Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verification of hybrid dynamical system using checkmate. In: ADPM 2000 (2000), \n                    \n                      http:\/\/www.ece.cmu.edu\/~webk\/checkmate","DOI":"10.1109\/ACC.2000.879487"},{"key":"27_CR38","doi-asserted-by":"crossref","unstructured":"Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: ISSAC, pp. 329\u2013336. ACM (2011)","DOI":"10.1145\/1993886.1993935"},{"key":"27_CR39","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A. Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Formal Methods in Systems Design\u00a032, 57\u201383 (2008)","journal-title":"Formal Methods in Systems Design"},{"key":"27_CR40","unstructured":"Tiwari, A., SRI International: HybridSAL: A tool for abstracting HybridSAL specifications to SAL specifications. Cf (2007) \n                    \n                      http:\/\/sal.csl.sri.com\/hybridsal\/"},{"key":"27_CR41","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2014the quadratic case and beyond. In: Applied Algebra and Error-Correcting Codes (AAECC), vol.\u00a08, pp. 85\u2013101 (1997)","DOI":"10.1007\/s002000050055"},{"key":"27_CR42","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/37.898794","volume":"21","author":"W. Zhang","year":"2001","unstructured":"Zhang, W., Branicky, M.S., Phillips, S.M.: Stability of networked control systems. IEEE Control Systems Magazine\u00a021, 84\u201399 (2001)","journal-title":"IEEE Control Systems Magazine"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:54Z","timestamp":1620129594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}