{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:35:12Z","timestamp":1761510912756},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,12,5]],"date-time":"2007-12-05T00:00:00Z","timestamp":1196812800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2008,2]]},"DOI":"10.1007\/s10703-007-0044-3","type":"journal-article","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T16:11:48Z","timestamp":1196957508000},"page":"57-83","source":"Crossref","is-referenced-by-count":82,"title":["Abstractions for hybrid systems"],"prefix":"10.1007","volume":"32","author":[{"given":"Ashish","family":"Tiwari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,12,5]]},"reference":[{"issue":"3","key":"44_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho P-H, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138(3):3\u201334","journal-title":"Theor Comput Sci"},{"key":"44_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Henzinger TA, Ho P-H Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman et al [17], pp 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Dang T, Ivancic F Counter-example guided predicate abstraction of hybrid systems. In: Garavel and Hatcliff [13], pp 208\u2013223","DOI":"10.1007\/3-540-36577-X_15"},{"key":"44_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Dang T, Ivancic F Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler and Pnueli [31]","DOI":"10.1007\/3-540-36580-X_4"},{"issue":"2","key":"44_CR5","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur R, Henzinger T, Lafferriere G, Pappas GJ (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(2):971\u2013984","journal-title":"Proc IEEE"},{"key":"44_CR6","series-title":"Proceedings. Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/b96398","volume-title":"Hybrid systems: computation and control","author":"R Alur","year":"2004","unstructured":"Alur R, Pappas GJ (eds) (2004) Hybrid systems: computation and control, 7th international workshop, HSCC 2004, Philadelphia, PA, March 25\u201327, 2004, Proceedings. Lecture notes in computer science, vol 2993. Springer, Berlin"},{"key":"44_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Proc of the 7th intl conf on tools and algorithms for the construction and analysis of systems, TACAS 2001","author":"T Ball","year":"2001","unstructured":"Ball T, Podelski A, Rajamani SK (2001) Boolean and Cartesian abstraction for model checking C programs. In: Proc of the 7th intl conf on tools and algorithms for the construction and analysis of systems, TACAS 2001. Lecture notes in computer science. Springer, Berlin, pp 268\u2013283"},{"key":"44_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-48983-5_10","volume-title":"HSCC","author":"A Chutinan","year":"1999","unstructured":"Chutinan A, Krogh BH (1999) Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager FW, van Schuppen JH (eds) HSCC. Lecture notes in computer science, vol 1569. Springer, Berlin, pp 76\u201390"},{"issue":"9","key":"44_CR9","doi-asserted-by":"crossref","first-page":"1401","DOI":"10.1109\/9.948467","volume":"46","author":"A Chutinan","year":"2001","unstructured":"Chutinan A, Krogh BH (2001) Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans Autom Control 46(9):1401\u20131410","journal-title":"IEEE Trans Autom Control"},{"key":"44_CR10","doi-asserted-by":"crossref","unstructured":"Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Garavel and Hatcliff [13], pp 192\u2013207","DOI":"10.1007\/3-540-36577-X_14"},{"key":"44_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Proc 2nd GI conf automata theory and formal languages","author":"GE Collins","year":"1975","unstructured":"Collins GE (1975) Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Proc 2nd GI conf automata theory and formal languages. Lecture notes in computer science, vol 33. Springer, Berlin, pp 134\u2013183"},{"key":"44_CR12","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-64358-3_34","volume-title":"HSCC","author":"T Dang","year":"1998","unstructured":"Dang T, Maler O (1998) Reachability analysis via face lifting. In: Henzinger TA, Sastry S (eds) HSCC. Lecture notes in computer science, vol 1386. Springer, Berlin, pp 96\u2013109"},{"key":"44_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X","volume-title":"9th intl conf on tools and algorithms for the construction and analysis of systems, TACAS 2003","author":"H Garavel","year":"2003","unstructured":"Garavel H, Hatcliff J (eds) (2003) In: 9th intl conf on tools and algorithms for the construction and analysis of systems, TACAS 2003. Lecture notes in computer science, vol 2619. Springer, Berlin"},{"key":"44_CR14","series-title":"LNCS","first-page":"232","volume-title":"Hybrid systems: computation and control, HSCC 2001","author":"R Ghosh","year":"2001","unstructured":"Ghosh R, Tomlin CJ (2001) Lateral inhibition through delta-notch signaling: a piecewise affine hybrid model. In: Hybrid systems: computation and control, HSCC 2001. LNCS, vol 2034. Springer, Berlin, pp 232\u2013246"},{"issue":"4","key":"44_CR15","doi-asserted-by":"crossref","first-page":"1125","DOI":"10.1109\/25.330177","volume":"43","author":"D Godbole","year":"1994","unstructured":"Godbole D, Lygeros J (1994) Longitudinal control of the lead car of a platoon. IEEE Trans Veh Technol 43(4):1125\u20131135","journal-title":"IEEE Trans Veh Technol"},{"key":"44_CR16","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Proc 9th conference on computer-aided verification (CAV\u201997)","author":"S Graf","year":"1997","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed) Proc 9th conference on computer-aided verification (CAV\u201997). Lecture notes in computer science, vol 1254. Springer, Berlin, pp 72\u201383"},{"key":"44_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-57318-6","volume-title":"Hybrid systems","author":"RL Grossman","year":"1993","unstructured":"Grossman RL, Nerode A, Ravn AP, Rischel H (eds) (1993) In: Hybrid systems. Lecture notes in computer science, vol 736. Springer, Berlin"},{"issue":"3","key":"44_CR18","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"44_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger MR, Henzinger TA, Kopke PW (1995) Computing simulations on finite and infinite graphs. In: Proc 36th annual IEEE symp on foundations of computer science FOCS, pp 453\u2013462","DOI":"10.1109\/SFCS.1995.492576"},{"key":"44_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-60084-1_85","volume-title":"Proc 22nd intl colloquium on automata, languages, and programming, ICALP 1995","author":"TA Henzinger","year":"1995","unstructured":"Henzinger TA (1995) Hybrid automata with finite bisimulations. In: Proc 22nd intl colloquium on automata, languages, and programming, ICALP 1995. Lecture notes in computer science, vol 944. Springer, Berlin, pp 324\u2013335"},{"key":"44_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-60045-0_53","volume-title":"Computer aided verification, Proc of the 7th intl conf, CAV \u201995","author":"TA Henzinger","year":"1995","unstructured":"Henzinger TA, Ho P-H (1995) Algorithmic analysis of nonlinear hybrid systems. In: Wolper P (ed) Computer aided verification, Proc of the 7th intl conf, CAV \u201995. Lecture notes in computer science, vol 939. Springer, Berlin, pp 225\u2013238"},{"key":"44_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger TA, Ho P-H (1995) A note on abstract interpretation strategies for hybrid automata. In: Antsaklis P, Kohn W, Nerode A (eds) Hybrid systems II. Lecture notes in computer science, vol 999. Springer, Berlin, pp 252\u2013264"},{"key":"44_CR23","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Ho P-H, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. IEEE Trans Autom Control 43:540\u2013554","journal-title":"IEEE Trans Autom Control"},{"key":"44_CR24","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What\u2019s decidable about hybrid automata? J Comput Syst Sci 57:94\u2013124","journal-title":"J Comput Syst Sci"},{"key":"44_CR25","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/BFb0020961","volume-title":"Hybrid systems III","author":"TA Henzinger","year":"1996","unstructured":"Henzinger TA, Wong-Toi H (1996) Linear phase-portrait approximations for nonlinear systems. In: Alur R, Henzinger T, Sontag ED (eds) Hybrid systems III. Lecture notes in computer science, vol 1066. Springer, Berlin, pp 377\u2013388"},{"key":"44_CR26","doi-asserted-by":"crossref","unstructured":"Hong H (1990) An improvement of the projection operator in cylindrical algebraic decomposition. In: Proc ISAAC 90, pp 261\u2013264","DOI":"10.1145\/96877.96943"},{"key":"44_CR27","unstructured":"Krogh BH, Stursberg O On efficient representation and computation of reachable sets for hybrid systems. In Maler and Pnueli [31]"},{"issue":"3","key":"44_CR28","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere G, Pappas GJ, Yovine S (2001) Symbolic reachability computations for families of linear vector fields. J Symb Comput 32(3):231\u2013253","journal-title":"J Symb Comput"},{"key":"44_CR29","unstructured":"Lazard D (1990) An improved projection for cylindrical algebraic decomposition. Technical report, Informatique, Universite Paris IV, F-75252 Paris Cedex 05, France"},{"key":"44_CR30","first-page":"88","volume-title":"Proc of the 12th intl workshop on qualitative reasoning","author":"T Loeser","year":"1998","unstructured":"Loeser T, Iwasaki Y, Fikes R (1998) Safety verification proofs for physical systems. In: Proc of the 12th intl workshop on qualitative reasoning. AAAI Press, Menlo Park, pp 88\u201395. Also published as a Knowledge Systems Lab, Stanford University, technical report KSL-98-14"},{"key":"44_CR31","series-title":"Proceedings. Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36580-X","volume-title":"Hybrid systems: computation and control","author":"O Maler","year":"2003","unstructured":"Maler O, Pnueli A (eds) (2003) In: Hybrid systems: computation and control, 6th international workshop, HSCC 2003 Prague, Czech Republic, April 3\u20135, 2003. Proceedings. Lecture notes in computer science, vol 2623. Springer, Berlin"},{"key":"44_CR32","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/S0747-7171(88)80010-5","volume":"5","author":"S McCallum","year":"1988","unstructured":"McCallum S (1988) An improved projection operator for cylindrical algebraic decomposition of three dimensional space. J Symb Comput 5:141\u2013161","journal-title":"J Symb Comput"},{"key":"44_CR33","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In: Proc. 2nd IJCAI, pp 481\u2013489"},{"key":"44_CR34","unstructured":"M\u00f6ller MO, Rue\u00df H, Sorea M (2002) Predicate abstraction for dense real-time systems. Electron Notes Theor Comput Sci 65(6). http:\/\/www.elsevier.com\/locate\/entcs\/volume65.html"},{"key":"44_CR35","doi-asserted-by":"crossref","unstructured":"Nicollin X, Olivero A, Sifakis J, Yovine S An approach to the description and analysis of hybrid systems. In Grossman et al [17], pp 149\u2013178","DOI":"10.1007\/3-540-57318-6_28"},{"key":"44_CR36","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/3-540-58179-0_45","volume-title":"Proc of the 6th computer-aided verification, CAV","author":"A Olivero","year":"1994","unstructured":"Olivero A, Sifakis J, Yovine S (1994) Using abstractions for the verification of linear hybrid systems. In: Proc of the 6th computer-aided verification, CAV. Lecture notes in computer science, vol 818. Springer, Berlin, pp 81\u201394"},{"key":"44_CR37","unstructured":"Parrilo PA (2000) Structured semidefinite programs and semialgebraic geometric methods in robustness and optimization. PhD thesis, California Institute of Technology, Pasadena"},{"key":"44_CR38","unstructured":"Parrilo PA, Sturmfels B (2003) Minimizing polynomial functions. In: Algorithmic and quantitative real algebraic geometry. DIMACS series in discrete mathematics and theoretical computer science, vol\u00a060, pp\u00a083\u201399. http:\/\/www\/arxiv.org\/abs\/math.OC\/0103170"},{"key":"44_CR39","doi-asserted-by":"crossref","unstructured":"Prajna S (2003) Barrier certificates for nonlinear model validation. In: Proc IEEE conference on decision and control","DOI":"10.1109\/CDC.2003.1273063"},{"key":"44_CR40","doi-asserted-by":"crossref","unstructured":"Prajna S, Jadbabaie A Safety verification of hybrid systems using barrier certificates. In Alur and Pappas [6], pp 477\u2013492","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"44_CR41","unstructured":"Prajna S, Papachristodoulou A, Parrilo PA (2002) SOSTOOLS: sum of square optimization toolbox for MATLAB, http:\/\/www.cds.caltech.edu\/sostools"},{"key":"44_CR42","unstructured":"Puri A, Varaiya P (1995) Driving safely in smart cars. In: Proc of the 1995 American control conference"},{"key":"44_CR43","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/BFb0031568","volume-title":"Hybrid systems IV","author":"J Raisch","year":"1997","unstructured":"Raisch J, O\u2019Young S (1997) A totally ordered set of discrete abstractions for a given hybrid or continuous system. In: Hybrid systems IV. Lecture notes in computer science, vol 1273. Springer, Berlin, pp 342\u2013360"},{"key":"44_CR44","first-page":"91","volume":"92","author":"B Shults","year":"1997","unstructured":"Shults B, Kuipers BJ (1997) Proving properties of continuous systems: qualitative simulation and temporal logic. AI J 92:91\u2013129","journal-title":"AI J"},{"key":"44_CR45","unstructured":"Sokolsky O, Hong HS Qualitative modeling of hybrid systems. In: Proc of the Montreal workshop, 2001. Available from http:\/\/www.cis.upenn.edu\/~rtg\/rtg_papers.htm"},{"key":"44_CR46","unstructured":"Tabuada P (2004) Flatness and finite bisimulations in continuous time. In: Proc 16th intl symp on mathematical theory of networks and systems"},{"key":"44_CR47","volume-title":"A decision method for elementary algebra and geometry","author":"A Tarski","year":"1948","unstructured":"Tarski A (1948) A decision method for elementary algebra and geometry, 2nd edn. University of California Press, Berkeley","edition":"2"},{"key":"44_CR48","first-page":"40","volume-title":"Proc CADE-19 workshop on pragmatics of decision procedures in automated deduction, PDPAR 2003","author":"A Tiwari","year":"2003","unstructured":"Tiwari A (2003) Abstraction based theorem proving: an example from the theory of reals. In: Proc CADE-19 workshop on pragmatics of decision procedures in automated deduction, PDPAR 2003. INRIA, Nancy, pp 40\u201352"},{"key":"44_CR49","doi-asserted-by":"crossref","unstructured":"Tiwari A Approximate reachability for linear systems. In Maler and Pnueli [31], pp 514\u2013525","DOI":"10.1007\/3-540-36580-X_37"},{"key":"44_CR50","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"HSCC","author":"A Tiwari","year":"2002","unstructured":"Tiwari A, Khanna G (2002) Series of abstractions for hybrid automata. In: Tomlin C, Greenstreet MR (eds) HSCC. Lecture notes in computer science, vol 2289. Springer, Berlin, pp 465\u2013478"},{"key":"44_CR51","doi-asserted-by":"crossref","unstructured":"Tiwari A, Khanna G Nonlinear systems: approximating reach sets. In: Alur and Pappas [6], pp 600\u2013614","DOI":"10.1007\/978-3-540-24743-2_40"},{"key":"44_CR52","volume-title":"Nonlinear systems analysis","author":"M Vidyasagar","year":"1993","unstructured":"Vidyasagar M (1993) Nonlinear systems analysis. Prentice Hall, New York"},{"key":"44_CR53","doi-asserted-by":"crossref","unstructured":"Yazarel H, Pappas GJ (2004) Geometric programming relaxations for linear system reachability. In: Proc 2004 American control conference","DOI":"10.23919\/ACC.2004.1383661"},{"key":"44_CR54","unstructured":"Yazarel H, Prajna S, Pappas GJ (2004) S.O.S. for safety. In: Proc 43rd IEEE conference on decision and control, vol\u00a01, pp\u00a0461\u2013466"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0044-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-007-0044-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0044-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-007-0044-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,5]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["44"],"URL":"https:\/\/doi.org\/10.1007\/s10703-007-0044-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12,5]]}}}