{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T00:27:07Z","timestamp":1768350427042,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642391750","type":"print"},{"value":"9783642391767","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_8","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T04:58:44Z","timestamp":1369889924000},"page":"117-134","source":"Crossref","is-referenced-by-count":8,"title":["Abstraction-Based Guided Search for Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Sergiy","family":"Bogomolov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Donz\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goran","family":"Frehse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Grosu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hamed","family":"Ladan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Wehrle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","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, T., Ho, P., Nicolin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"8_CR2","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":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-36580-X_4","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 4\u201319. Springer, Heidelberg (2003)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-46430-1_5","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2000","unstructured":"Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specifications of hybrid systems in charon. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 6\u201319. Springer, Heidelberg (2000)"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-540-73580-9_5","volume-title":"Abstraction, Reformulation, and Approximation","author":"K. Anderson","year":"2007","unstructured":"Anderson, K., Holte, R., Schaeffer, J.: Partial pattern databases. In: Miguel, I., Ruml, W. (eds.) SARA 2007. LNCS (LNAI), vol.\u00a04612, pp. 20\u201334. Springer, Heidelberg (2007)"},{"issue":"7","key":"8_CR6","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(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"issue":"7","key":"8_CR7","doi-asserted-by":"publisher","first-page":"888","DOI":"10.1109\/5.871300","volume":"88","author":"A. Balluchi","year":"2000","unstructured":"Balluchi, A., Benvenuti, L., Benedetto, M.D.D., Pinello, C., Sangiovanni-Vincentelli, A.L.: Automotive engine control and hybrid systems: challenges and opportunities. Proceedings of the IEEE\u00a088(7), 888\u2013912 (2000)","journal-title":"Proceedings of the IEEE"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-540-24743-2_10","volume-title":"Hybrid Systems: Computation and Control","author":"A. Bhatia","year":"2004","unstructured":"Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 142\u2013156. Springer, Heidelberg (2004)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-642-31424-7_35","volume-title":"Computer Aided Verification","author":"S. Bogomolov","year":"2012","unstructured":"Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 479\u2013494. Springer, Heidelberg (2012)"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"C. Chutinan","year":"2003","unstructured":"Chutinan, C., Krogh, B.: Computational techniques for hybrid system verification. IEEE Transactions on Automatic Control\u00a048(1), 64\u201375 (2003)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"3","key":"8_CR11","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1111\/0824-7935.00065","volume":"14","author":"J.C. Culberson","year":"1998","unstructured":"Culberson, J.C., Schaeffer, J.: Pattern databases. Computational Intelligence\u00a014(3), 318\u2013334 (1998)","journal-title":"Computational Intelligence"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s10703-009-0066-0","volume":"34","author":"T. Dang","year":"2009","unstructured":"Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods in System Design\u00a034(2), 183\u2013213 (2009)","journal-title":"Formal Methods in System Design"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/BFb0020941","volume-title":"Hybrid Systems III","author":"A. Deshpande","year":"1996","unstructured":"Deshpande, A., Godbole, D., G\u00f6ll\u00fc, A., Varaiya, P.: Design and evaluation of tools for automated highway systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 138\u2013148. Springer, Heidelberg (1996)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-46430-1_12","volume-title":"Hybrid Systems: Computation and Control","author":"M. Egerstedt","year":"2000","unstructured":"Egerstedt, M.: Behavior based robotics using hybrid automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 103\u2013116. Springer, Heidelberg (2000)"},{"key":"8_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":"8_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., et al.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/BFb0020961","volume-title":"Hybrid Systems III","author":"T. Henzinger","year":"1996","unstructured":"Henzinger, T., Wong-Toi, H.: Linear phase-portrait approximations for nonlinear hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 377\u2013388. Springer, Heidelberg (1996)"},{"key":"8_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/11527862_9","volume-title":"Abstraction, Reformulation and Approximation","author":"R.C. Holte","year":"2005","unstructured":"Holte, R.C., Grajkowski, J., Tanner, B.: Hierarchical heuristic search revisited. In: Zucker, J.-D., Saitta, L. (eds.) SARA 2005. LNCS (LNAI), vol.\u00a03607, pp. 121\u2013133. Springer, Heidelberg (2005)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-32759-9_22","volume-title":"FM 2012: Formal Methods","author":"T.T. Johnson","year":"2012","unstructured":"Johnson, T.T., Green, J., Mitra, S., Dudley, R., Erwin, R.S.: Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-78800-3_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Hoffmann, J., Larsen, K.G.: Fast directed model checking via russian doll abstraction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 203\u2013217. Springer, Heidelberg (2008)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-19835-9_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Wehrle, M.: Abstractions and pattern databases: The quest for succinctness and accuracy. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 276\u2013290. Springer, Heidelberg (2011)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Larsen, B.J., Burns, E., Ruml, W., Holte, R.: Searching without a heuristic: Efficient use of abstraction. In: AAAI Conference on Artificial Intelligence (2010)","DOI":"10.1609\/aaai.v24i1.7563"},{"key":"8_CR23","unstructured":"Livadas, C., Lygeros, J., Lynch, N.A.: High-level modelling and analysis of tcas. In: IEEE Real-Time Systems Symposium, pp. 115\u2013125 (1999)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/3-540-64358-3_46","volume-title":"Hybrid Systems: Computation and Control","author":"J. Lygeros","year":"1998","unstructured":"Lygeros, J., Pappas, G.J., Sastry, S.: An approach to the verification of the center-tracon automation system. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386, pp. 289\u2013304. Springer, Heidelberg (1998)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-540-73368-3_48","volume-title":"Computer Aided Verification","author":"E. Plaku","year":"2007","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: From verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 463\u2013476. Springer, Heidelberg (2007)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-24730-2_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Qian","year":"2004","unstructured":"Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 497\u2013511. Springer, Heidelberg (2004)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02949-3_12","volume-title":"Tests and Proofs","author":"S. Ratschan","year":"2009","unstructured":"Ratschan, S., Smaus, J.-G.: Finding errors of hybrid systems by optimising an abstraction-based quality estimate. In: Dubois, C. (ed.) TAP 2009. LNCS, vol.\u00a05668, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Varaiya, P.: Smart cars on smart roads: problems of control. IEEE Trans. Automatic Control 38(2) (1993)","DOI":"10.1109\/9.250509"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,1]],"date-time":"2023-07-01T20:42:17Z","timestamp":1688244137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}