{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:18:30Z","timestamp":1768346310282,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030001506","type":"print"},{"value":"9783030001513","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00151-3_15","type":"book-chapter","created":{"date-parts":[[2018,8,25]],"date-time":"2018-08-25T13:54:31Z","timestamp":1535205271000},"page":"252-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems"],"prefix":"10.1007","author":[{"given":"Meilun","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter N.","family":"Mosaad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhikun","family":"She","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bai","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,26]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Belta, C., Ivancic, F. (eds.) Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, Philadelphia, PA, USA, 8\u201311 April 2013, pp. 173\u2013182. ACM (2013)","DOI":"10.1145\/2461328.2461358"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: Proceedings of the 47th IEEE Conference on Decision and Control, CDC 2008, Canc\u00fan, M\u00e9xico, 9\u201311 December 2008, pp. 4042\u20134048. IEEE (2008)","DOI":"10.1109\/CDC.2008.4738704"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45351-2_9","volume-title":"Hybrid Systems: Computation and Control","author":"H Anai","year":"2001","unstructured":"Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 63\u201376. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_9"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the 33rd IEEE Real-Time Systems Symposium, RTSS 2012, San Juan, PR, USA, 4\u20137 December 2012, pp. 183\u2013192. IEEE Computer Society (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S., \u00c1brah\u00e1m, E.: Under-approximate flowpipes for non-linear continuous systems. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 59\u201366. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987596"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Abate, A., Fainekos, G.E. (eds.) Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, 12\u201314 April 2016, pp. 297\u2013306. ACM (2016)","DOI":"10.1145\/2883817.2883838"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, 29 September\u20134 October 2013, pp. 26:1\u201326:10. IEEE (2013)","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-24690-6_13","volume-title":"Software Engineering and Formal Methods","author":"A Eggers","year":"2011","unstructured":"Eggers, A., Ramdani, N., Nedialkov, N., Fr\u00e4nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 172\u2013187. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_13"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-41528-4_29","volume-title":"Computer Aided Verification","author":"C Fan","year":"2016","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531\u2013538. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_29"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: Girard, A., Sankaranarayanan, S. (eds.) Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14\u201316 April 2015, pp. 149\u2013158. ACM (2015)","DOI":"10.1145\/2728606.2728622"},{"key":"15_CR11","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. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 203\u2013212. ACM, New York (2013)","DOI":"10.1145\/2461328.2461361"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11730637_21","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257\u2013271. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_21"},{"key":"15_CR14","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. 3927, pp. 272\u2013286. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11730637_22"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Goubault, E., Mullier, O., Putot, S., Kieffer, M.: Inner approximated reachability analysis. In: Fr\u00e4nzle, M., Lygeros, J. (eds.) 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2014, Berlin, Germany, 15\u201317 April 2014, pp. 163\u2013172. ACM (2014)","DOI":"10.1145\/2562059.2562113"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-642-02658-4_40","volume-title":"Computer Aided Verification","author":"C Guernic Le","year":"2009","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540\u2013554. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_40"},{"issue":"12","key":"15_CR17","doi-asserted-by":"publisher","first-page":"3189","DOI":"10.1016\/j.automatica.2008.05.023","volume":"44","author":"AO Hamadeh","year":"2008","unstructured":"Hamadeh, A.O., Goncalves, J.M.: Reachability analysis of continuous-time piecewise affine systems. Automatica 44(12), 3189\u20133194 (2008)","journal-title":"Automatica"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Huang, Z., Mitra, S.: Computing bounded reach sets from sampled simulation traces. In: Dang, T., Mitchell, I.M. (eds.) Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC 2012, Beijing, China, 17\u201319 April 2012, pp. 291\u2013294. ACM (2012)","DOI":"10.1145\/2185632.2185676"},{"issue":"2","key":"15_CR19","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1109\/9.45168","volume":"35","author":"A Isidori","year":"1990","unstructured":"Isidori, A., Byrnes, C.I.: Output regulation of nonlinear systems. IEEE Trans. Autom. Control 35(2), 131\u2013140 (1990)","journal-title":"IEEE Trans. Autom. Control"},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/978-0-387-74759-0","volume-title":"Encyclopedia of Optimization","author":"DR Jones","year":"2009","unstructured":"Jones, D.R.: Direct global optimization algorithm. In: Floudas, C.A., Pardalos, P.M. (eds.) Encyclopedia of Optimization, 2nd edn, pp. 725\u2013735. Springer, Boston (2009). https:\/\/doi.org\/10.1007\/978-0-387-74759-0","edition":"2"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Korda, M., Henrion, D., Jones, C.N.: Inner approximations of the region of attraction for polynomial dynamical systems. In: Tarbouriech, S., Krstic, M. (eds.) 9th IFAC Symposium on Nonlinear Control Systems, NOLCOS 2013, Toulouse, France, 4\u20136 September 2013, pp. 534\u2013539. International Federation of Automatic Control (2013)","DOI":"10.3182\/20130904-3-FR-2041.00002"},{"issue":"2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1080\/1055678021000012435","volume":"17","author":"AB Kurzhanski","year":"2002","unstructured":"Kurzhanski, A.B., Varaiya, P.: On ellipsoidal techniques for reachability analysis. Part II: internal approximations box-valued constraints. Optim. Methods Softw. 17(2), 207\u2013237 (2002)","journal-title":"Optim. Methods Softw."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Lal, R., Prabhakar, P.: Bounded error flowpipe computation of parameterized linear systems. In: Girault, A., Guan, N. (eds.) 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, 4\u20139 October 2015, pp. 237\u2013246. IEEE (2015)","DOI":"10.1109\/EMSOFT.2015.7318279"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Lhommeau, M., Jaulin, L., Hardouin, L.: Inner and outer approximation of capture basin using interval analysis. In: Zaytoon, J., Ferrier, J., Andrade-Cetto, J., Filipe, J. (eds.) Proceedings of the Fourth International Conference on Informatics in Control, Automation and Robotics, Signal Processing, Systems Modeling and Control, ICINCO 2007, Angers, France, 9\u201312 May 2007, pp. 5\u20139. INSTICC Press (2007)","DOI":"10.5220\/0001625800050009"},{"issue":"7","key":"15_CR25","doi-asserted-by":"publisher","first-page":"2017","DOI":"10.1016\/j.automatica.2013.03.020","volume":"49","author":"JN Maidens","year":"2013","unstructured":"Maidens, J.N., Kaynama, S., Mitchell, I.M., Oishi, M.M.K., Dumont, G.A.: Lagrangian methods for approximating the viability kernel in high-dimensional systems. Automatica 49(7), 2017\u20132029 (2013)","journal-title":"Automatica"},{"issue":"2","key":"15_CR26","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/s10915-007-9174-4","volume":"35","author":"IM Mitchell","year":"2008","unstructured":"Mitchell, I.M.: The flexible, extensible and efficient toolbox of level set methods. J. Sci. Comput. 35(2), 300\u2013329 (2008)","journal-title":"J. Sci. Comput."},{"key":"15_CR27","unstructured":"Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. CoRR, abs\/1605.00604 (2016)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12\u201315 April 2010, pp. 211\u2013220. ACM (2010)","DOI":"10.1145\/1755952.1755983"},{"key":"15_CR29","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. 4590, pp. 463\u2013476. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_48"},{"issue":"2","key":"15_CR30","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10703-015-0225-4","volume":"46","author":"P Prabhakar","year":"2015","unstructured":"Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. Formal Methods Syst. Des. 46(2), 105\u2013134 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"key":"15_CR32","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embedded Comput. Syst. 6(1), 1\u201323 (2007). Article No. 8"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S.: Automatic abstraction of non-linear systems using change of bases transformations. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, 12\u201314 April 2011, pp. 143\u2013152. ACM (2011)","DOI":"10.1145\/1967701.1967723"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-540-24743-2_40","volume-title":"Hybrid Systems: Computation and Control","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600\u2013614. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_40"},{"issue":"10","key":"15_CR35","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1109\/TAC.2013.2263916","volume":"58","author":"TC Wang","year":"2013","unstructured":"Wang, T.C., Lall, S., West, M.: Polynomial level-set method for polynomial system reachable set estimation. IEEE Trans. Autom. Control 58(10), 2508\u20132521 (2013)","journal-title":"IEEE Trans. Autom. Control"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Xue, B., Fr\u00e4nzle, M., Zhan, N.: Under-approximating reach sets for polynomial continuous systems. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC 2018, pp. 51\u201360. ACM, New York (2018)","DOI":"10.1145\/3178126.3178133"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-319-41528-4_25","volume-title":"Computer Aided Verification","author":"B Xue","year":"2016","unstructured":"Xue, B., She, Z., Easwaran, A.: Under-approximating backward reachable sets by polytopes. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 457\u2013476. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_25"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00151-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T15:20:38Z","timestamp":1751815238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00151-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030001506","9783030001513"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00151-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}