{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T22:32:50Z","timestamp":1771626770705,"version":"3.50.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,8,7]],"date-time":"2015-08-07T00:00:00Z","timestamp":1438905600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s10009-015-0393-y","type":"journal-article","created":{"date-parts":[[2015,8,6]],"date-time":"2015-08-06T10:54:47Z","timestamp":1438858487000},"page":"449-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Guided search for hybrid systems based on coarse-grained space abstractions"],"prefix":"10.1007","volume":"18","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","published-online":{"date-parts":[[2015,8,7]]},"reference":[{"key":"393_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, T., Ho, P., Nicolin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"393_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Hybrid Systems: Computation and Control (HSCC), pp. 35\u201348 (2002)","DOI":"10.1007\/3-540-45873-5_6"},{"key":"393_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counter-example guided predicate abstraction of hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 250\u2013271 (2003)","DOI":"10.1007\/3-540-36577-X_15"},{"key":"393_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Dang, T., Ivancic, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Hybrid Systems: Computation and Control. pp. 4\u201319 (2003)","DOI":"10.1007\/3-540-36580-X_4"},{"key":"393_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specifications of hybrid systems in charon. In: Hybrid Systems: Computation and Control, pp. 6\u201319 (2000)","DOI":"10.1007\/3-540-46430-1_5"},{"key":"393_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.: Modularity for timed and hybrid systems. In: CONCUR \u201997: Concurrency Theory, pp. 74\u201388. Springer (1997)","DOI":"10.1007\/3-540-63141-0_6"},{"key":"393_CR7","doi-asserted-by":"crossref","unstructured":"Anderson, K., Holte, R., Schaeffer, J.: Partial pattern databases. In: Symposium on abstraction, reformulation, and approximation, pp. 20\u201334 (2007)","DOI":"10.1007\/978-3-540-73580-9_5"},{"issue":"7","key":"393_CR8","doi-asserted-by":"crossref","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 43(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"issue":"7","key":"393_CR9","doi-asserted-by":"crossref","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. Proc. IEEE 88(7), 888\u2013912 (2000)","journal-title":"Proc. IEEE"},{"key":"393_CR10","volume-title":"Convex Analysis and Optimization","author":"D Bertsekas","year":"2003","unstructured":"Bertsekas, D., Nedi, A., Ozdaglar, A., et al.: Convex Analysis and Optimization. Athena Scientific, Belmont (2003)"},{"key":"393_CR11","doi-asserted-by":"crossref","unstructured":"Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Hybrid Systems: Computation and Control, pp 142\u2013156 (2004)","DOI":"10.1007\/978-3-540-24743-2_10"},{"key":"393_CR12","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Donz\u00e9, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Abstraction-based guided search for hybrid systems. In: Model Checking Software, pp. 117\u2013134 (2013)","DOI":"10.1007\/978-3-642-39176-7_8"},{"key":"393_CR13","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: Accepted to Haifa verification conference (2014)","DOI":"10.1007\/978-3-319-13338-6_10"},{"key":"393_CR14","doi-asserted-by":"crossref","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. Computer Aided Verification, pp. 479\u2013494. Springer, New York (2012)"},{"key":"393_CR15","doi-asserted-by":"crossref","unstructured":"Bournez, O., Maler, O., Pnueli, A.: Orthogonal polyhedra: representation and computation. In: Hybrid Systems: Computation and Control, pp 46\u201360. Springer (1999)","DOI":"10.1007\/3-540-48983-5_8"},{"issue":"1","key":"393_CR16","doi-asserted-by":"crossref","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 Trans Autom Control 48(1), 64\u201375 (2003)","journal-title":"IEEE Trans Autom Control"},{"issue":"3","key":"393_CR17","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1111\/0824-7935.00065","volume":"14","author":"JC Culberson","year":"1998","unstructured":"Culberson, J.C., Schaeffer, J.: Pattern databases. Comput. Intell. 14(3), 318\u2013334 (1998)","journal-title":"Comput. Intell."},{"issue":"2","key":"393_CR18","doi-asserted-by":"crossref","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. Form. Methods Syst. Des. 34(2), 183\u2013213 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"393_CR19","doi-asserted-by":"crossref","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. Hybrid Systems III, pp. 138\u2013148. Springer, Berlin (1996)"},{"key":"393_CR20","doi-asserted-by":"crossref","unstructured":"Egerstedt, M.: Behavior-based robotics using hybrid automata. In: Hybrid Systems: Computation and Control, pp. 103\u2013116 (2000)","DOI":"10.1007\/3-540-46430-1_12"},{"key":"393_CR21","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Hybrid Systems: Computation and Control, pp. 381\u2013397 (2004)","DOI":"10.1007\/978-3-540-24743-2_22"},{"issue":"3","key":"393_CR22","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. STTT 10(3), 263\u2013279 (2008)","journal-title":"STTT"},{"key":"393_CR23","doi-asserted-by":"crossref","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. Computer Aided Verification, pp. 379\u2013395. Springer, Berlin (2011)"},{"key":"393_CR24","doi-asserted-by":"crossref","unstructured":"Holte, R.C., Grajkowski, J., Tanner, B.: Hierarchical heuristic search revisited. In: Symposium on abstraction, reformulation and approximation, pp. 121\u2013133 (2005)","DOI":"10.1007\/11527862_9"},{"key":"393_CR25","first-page":"287","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"SK Jha","year":"2007","unstructured":"Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. Hybrid Systems: Computation and Control (HSCC), pp. 287\u2013300. Springer, Berlin (2007)"},{"issue":"3","key":"393_CR26","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/S0167-6911(99)00059-6","volume":"38","author":"KH Johansson","year":"1999","unstructured":"Johansson, K.H., Egerstedt, M., Lygeros, J., Sastry, S.: On the regularization of zeno hybrid automata. Syst. Control Lett. 38(3), 141\u2013150 (1999)","journal-title":"Syst. Control Lett."},{"key":"393_CR27","first-page":"252","volume-title":"Formal Methods","author":"TT 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. Formal Methods, pp. 252\u2013266. Springer, Berlin (2012)"},{"key":"393_CR28","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K.: Nonlinear Systems, 3rd edn. Prentice Hall, Upper Saddle River (2002)","edition":"3"},{"key":"393_CR29","doi-asserted-by":"crossref","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. Tools and Algorithms for the Construction and Analysis of Systems, pp. 203\u2013217. Springer, Berlin (2008)"},{"key":"393_CR30","doi-asserted-by":"crossref","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. Tools and Algorithms for the Construction and Analysis of Systems, pp. 276\u2013290. Springer, Berlin (2011)"},{"key":"393_CR31","doi-asserted-by":"crossref","unstructured":"Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Hybrid Systems: Computation and Control, third international workshop, HSCC 2000, Pittsburgh, March 23\u201325, Proceedings, 202\u2013214 (2000)","DOI":"10.1007\/3-540-46430-1_19"},{"key":"393_CR32","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"},{"issue":"2","key":"393_CR33","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":"393_CR34","doi-asserted-by":"crossref","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)","DOI":"10.1109\/REAL.1999.818833"},{"key":"393_CR35","doi-asserted-by":"crossref","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. Hybrid Systems: Computation and Control, pp. 289\u2013304. Springer, Berlin (1998)"},{"key":"393_CR36","doi-asserted-by":"crossref","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., Vardi, M.: Hybrid systems: from verification to falsification. Computer Aided Verification, pp. 463\u2013476. Springer, Berlin (2007)"},{"key":"393_CR37","doi-asserted-by":"crossref","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. Tools and Algorithms for the Construction and Analysis of Systems, pp. 497\u2013511. Springer, Berlin (2004)"},{"key":"393_CR38","doi-asserted-by":"crossref","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. Tests and Proofs, pp. 153\u2013168. Springer, Berlin (2009)"},{"issue":"1","key":"393_CR39","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Form. Methods Syst. Des. 32(1), 57\u201383 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"393_CR40","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. Hybrid Systems: Computation and Control, pp. 465\u2013478. Springer, Berlin (2002)"},{"issue":"2","key":"393_CR41","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1109\/9.250509","volume":"38","author":"P Varaiya","year":"1993","unstructured":"Varaiya, P.: Smart cars on smart roads: problems of control. IEEE Trans. Autom. Control 38(2), 195\u2013207 (1993)","journal-title":"IEEE Trans. Autom. Control"},{"key":"393_CR42","doi-asserted-by":"publisher","unstructured":"Wehrle, M., Kupferschmid, S.: Downward pattern refinement for timed automata. Int. J. Softw. Tools Technol. Transf. (2014). doi: 10.1007\/s10009-014-0346-x","DOI":"10.1007\/s10009-014-0346-x"},{"key":"393_CR43","doi-asserted-by":"crossref","unstructured":"Zutshi, A., Sankaranarayanan, S., Deshmukh, J., Kapinski, J.: A trajectory splicing approach to concretizing counterexamples for hybrid systems. In: Conference on decision and control (CDC), pp. 3918\u20133925 (2013)","DOI":"10.1109\/CDC.2013.6760488"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0393-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0393-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0393-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T22:14:38Z","timestamp":1748556878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0393-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,7]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["393"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0393-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,7]]}}}