{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T21:31:03Z","timestamp":1779139863379,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_35","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"479-494","source":"Crossref","is-referenced-by-count":13,"title":["A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx"],"prefix":"10.1007","author":[{"given":"Sergiy","family":"Bogomolov","sequence":"first","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":"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":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-45351-2_6","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2001","unstructured":"Alur, R., Belta, C., Ivan\u010di\u0107, F., Kumar, V., Mintz, M., Pappas, G.J., Rubin, H., Schug, J.: Hybrid Modeling and Simulation of Biomolecular Networks. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 19\u201332. Springer, Heidelberg (2001)"},{"key":"35_CR2","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.A., Ho, P.H., 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"},{"issue":"7","key":"35_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(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"issue":"7","key":"35_CR4","doi-asserted-by":"publisher","first-page":"888","DOI":"10.1109\/5.871300","volume":"88","author":"A. Balluchi","year":"2000","unstructured":"Balluchi, A., Benvenuti, L., Di Benedetto, M.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":"35_CR5","doi-asserted-by":"crossref","unstructured":"Barbano, P., Spivak, M., Feng, J., Antoniotti, M., Misra, B.: A coherent framework for multi-resolution analysis of biological networks with memory: Ras pathway, cell cycle and immune system. National Academy of Science, 6245\u20136250 (2005)","DOI":"10.1073\/pnas.0500554102"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-71493-4_8","volume-title":"Hybrid Systems: Computation and Control","author":"G. Batt","year":"2007","unstructured":"Batt, G., Belta, C., Weiss, R.: Model Checking Genetic Regulatory Networks with Parameter Uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 61\u201375. Springer, Heidelberg (2007)"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-24743-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"C. Belta","year":"2004","unstructured":"Belta, C., Finin, P., Habets, L.C.G.J.M., Hal\u00e1sz, \u00c1.M., Imieli\u0144ski, M., Kumar, R.V., Rubin, H.: Understanding the Bacterial Stringent Response Using Reachability Analysis of Hybrid Systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 111\u2013125. Springer, Heidelberg (2004)"},{"key":"35_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":"35_CR9","unstructured":"Branicky, M.S., Curtiss, M.M.: Nonlinear and hybrid control via RRTs. In: Symp. on Mathematical Theory of Networks and Systems (2002)"},{"issue":"1","key":"35_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.H.: Computational techniques for hybrid system verification. IEEE Transactions on Automatic Control\u00a048(1), 64\u201375 (2003)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-71493-4_16","volume-title":"Hybrid Systems: Computation and Control","author":"A. Donz\u00e9","year":"2007","unstructured":"Donz\u00e9, A., Maler, O.: Systematic Simulation Using Sensitivity Analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 174\u2013189. Springer, Heidelberg (2007)"},{"issue":"1","key":"35_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s10009-008-0092-z","volume":"11","author":"K. Dr\u00e4ger","year":"2009","unstructured":"Dr\u00e4ger, K., Finkbeiner, B., Podelski, A.: Directed model checking with distance-preserving abstractions. International Journal on Software Tools for Technology Transfer\u00a011(1), 27\u201337 (2009)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"35_CR13","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer\u00a05(2), 247\u2013267 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"35_CR14","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":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"35_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":"35_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1007\/978-3-540-71493-4_64","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2007","unstructured":"Frehse, G., Maler, O.: Reachability Analysis of a Switched Buffer Network. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 698\u2013701. Springer, Heidelberg (2007)"},{"issue":"1","key":"35_CR18","first-page":"170","volume":"1","author":"R. Ghosh","year":"2004","unstructured":"Ghosh, R., Tomlin, C.J.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modeling: Delta-notch protein signaling. IEEE Transactions on Systems Biology\u00a01(1), 170\u2013183 (2004)","journal-title":"IEEE Transactions on Systems Biology"},{"key":"35_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11730637_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Girard","year":"2006","unstructured":"Girard, A., Pappas, G.J.: Verification Using Simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 272\u2013286. Springer, Heidelberg (2006)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R. Grosu","year":"2011","unstructured":"Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From Cardiac Cells to Genetic Regulatory Networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"issue":"3","key":"35_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R. Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Communications of the ACM (CACM)\u00a052(3), 1\u201310 (2009)","journal-title":"Communications of the ACM (CACM)"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: ACM Symposium on Theory of Computing, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"35_CR23","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":"35_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1007\/978-3-540-71209-1_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Kupferschmid","year":"2007","unstructured":"Kupferschmid, S., Dr\u00e4ger, K., Hoffmann, J., Finkbeiner, B., Dierks, H., Podelski, A., Behrmann, G.: Uppaal\/DMC \u2013 Abstraction-Based Heuristics for Directed Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 679\u2013682. Springer, Heidelberg (2007)"},{"key":"35_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11691617_3","volume-title":"Model Checking Software","author":"S. Kupferschmid","year":"2006","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI Planning Heuristic for Directed Model Checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 35\u201352. Springer, Heidelberg (2006)"},{"key":"35_CR26","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":"35_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-540-70545-1_53","volume-title":"Computer Aided Verification","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Wehrle, M., Nebel, B., Podelski, A.: Faster Than Uppaal? In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 552\u2013555. Springer, Heidelberg (2008)"},{"key":"35_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-540-24743-2_44","volume-title":"Hybrid Systems: Computation and Control","author":"P. Lincoln","year":"2004","unstructured":"Lincoln, P., Tiwari, A.: Symbolic Systems Biology: Hybrid Modeling and Analysis of Biological Networks. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 660\u2013672. Springer, Heidelberg (2004)"},{"issue":"1","key":"35_CR29","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N. Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid I\/O automata. Inf. and Comp.\u00a0185(1), 103\u2013157 (2003)","journal-title":"Inf. and Comp."},{"key":"35_CR30","unstructured":"Maler, O., Yovine, S.: Hardware timing verification using kronos. In: Israeli Conference on Computer Systems and Software Engineering (1996)"},{"key":"35_CR31","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":"35_CR32","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":"35_CR33","doi-asserted-by":"crossref","unstructured":"Ratschan, S., Smaus, J.G.: Verification-Integrated falsification of Non-Deterministic hybrid systems. In: Analysis and Design of Hybrid Systems (2006)","DOI":"10.1016\/B978-008044613-4.50067-7"},{"key":"35_CR34","doi-asserted-by":"crossref","unstructured":"Silva, B., Stursberg, O., Krogh, B., Engell, S.: An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In: IEEE Conf. on Decision and Control, pp. 2867\u20132874 (2001)","DOI":"10.1109\/CDC.2001.980711"},{"key":"35_CR35","doi-asserted-by":"crossref","unstructured":"Singh, A., Hespanha, J.: Models for generegulatory networks using polynomial stochastic hybrid systems. In: CDC 2005 (2005)","DOI":"10.1007\/978-3-540-31954-2_21"},{"key":"35_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-03237-0_8","volume-title":"Static Analysis","author":"M. Wehrle","year":"2009","unstructured":"Wehrle, M., Helmert, M.: The Causal Graph Revisited for Directed Model Checking. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 86\u2013101. Springer, Heidelberg (2009)"}],"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_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T09:30:48Z","timestamp":1743586248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}