{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T18:21:25Z","timestamp":1762107685565,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set\u2019s boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_14","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"307-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Inner-Approximate Reachability Computation via\u00a0Zonotopic Boundary Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7779-0096","authenticated-orcid":false,"given":"Dejin","family":"Ren","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1171-7061","authenticated-orcid":false,"given":"Zhen","family":"Liang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1571-4831","authenticated-orcid":false,"given":"Chenyu","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0705-0345","authenticated-orcid":false,"given":"Jianqiang","family":"Ding","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3398-0466","authenticated-orcid":false,"given":"Taoran","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9717-846X","authenticated-orcid":false,"given":"Bai","family":"Xue","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"14_CR1","unstructured":"Althoff, M.: An introduction to cora 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annual Rev. Control, Robot. Autonomous Syst. 4, 369\u2013395 (2021)","journal-title":"Annual Rev. Control, Robot. Autonomous Syst."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: 2008 47th IEEE Conference on Decision and Control, pp. 4042\u20134048. IEEE (2008)","DOI":"10.1109\/CDC.2008.4738704"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bajaj, C.L., Pascucci, V.: Splitting a complex of convex polytopes in any dimension. In: Proceedings of the Twelfth Annual Symposium on Computational Geometry, pp. 88\u201397 (1996)","DOI":"10.1145\/237218.237246"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rner, A.: Oriented matroids. No.\u00a046, Cambridge University Press (1999)","DOI":"10.1017\/CBO9780511586507"},{"issue":"4","key":"14_CR6","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1109\/9.664150","volume":"43","author":"MS Branicky","year":"1998","unstructured":"Branicky, M.S.: Multiple lyapunov functions and other analysis tools for switched and hybrid systems. IEEE Trans. Autom. Control 43(4), 475\u2013482 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR7","unstructured":"Chen, X.: Reachability analysis of non-linear hybrid systems using taylor models. Ph.D. thesis, Fachgruppe Informatik, RWTH Aachen University (2015)"},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3424305","volume":"68","author":"MB Cohen","year":"2021","unstructured":"Cohen, M.B., Lee, Y.T., Song, Z.: Solving linear programs in the current matrix multiplication time. J. ACM (JACM) 68(1), 1\u201339 (2021)","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"14_CR9","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.ejor.2003.04.011","volume":"166","author":"JA Ferrez","year":"2005","unstructured":"Ferrez, J.A., Fukuda, K., Liebling, T.M.: Solving the fixed rank convex quadratic maximization in binary variables by a parallel zonotope construction algorithm. Eur. J. Oper. Res. 166(1), 35\u201350 (2005)","journal-title":"Eur. J. Oper. Res."},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.comgeo.2015.12.001","volume":"54","author":"V Fisikopoulos","year":"2016","unstructured":"Fisikopoulos, V., Penaranda, L.: Faster geometric algorithms via dynamic determinant computation. Comput. Geom. 54, 1\u201316 (2016)","journal-title":"Comput. Geom."},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_19"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2017)","DOI":"10.1145\/3049797.3049811"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Inner and outer reachability for the verification of control systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 11\u201322 (2019)","DOI":"10.1145\/3302504.3311794"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"key":"14_CR15","unstructured":"Herrmann, S., Joswig, M.: Splitting polytopes. arXiv preprint arXiv:0805.0774 (2008)"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Interval analysis. In: Applied interval analysis, pp. 11\u201343. Springer (2001). https:\/\/doi.org\/10.1007\/978-1-4471-0249-6","DOI":"10.1007\/978-1-4471-0249-6"},{"key":"14_CR17","unstructured":"Kabi, B.: Synthesizing invariants: a constraint programming approach based on zonotopic abstraction. Ph.D. thesis, Institut polytechnique de Paris (2020)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., Althoff, M.: Computing non-convex inner-approximations of reachable sets for nonlinear continuous systems. In: 2020 59th IEEE Conference on Decision and Control (CDC), pp. 2130\u20132137. IEEE (2020)","DOI":"10.1109\/CDC42340.2020.9304022"},{"issue":"23","key":"14_CR19","doi-asserted-by":"publisher","first-page":"534","DOI":"10.3182\/20130904-3-FR-2041.00002","volume":"46","author":"M Korda","year":"2013","unstructured":"Korda, M., Henrion, D., Jones, C.N.: Inner approximations of the region of attraction for polynomial dynamical systems. IFAC Proc. Vol. 46(23), 534\u2013539 (2013)","journal-title":"IFAC Proc. Vol."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Lakshmikantham, V., Leela, S., Martynyuk, A.A.: Practical stability of nonlinear systems. World Scientific (1990)","DOI":"10.1142\/1192"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-96142-2_5","volume-title":"Computer Aided Verification","author":"J Li","year":"2018","unstructured":"Li, J., Dureja, R., Pu, G., Rozier, K.Y., Vardi, M.Y.: SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 37\u201344. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_5"},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1090\/S0002-9947-1971-0279689-2","volume":"159","author":"P McMullen","year":"1971","unstructured":"McMullen, P.: On zonotopes. Trans. Am. Math. Soc. 159, 91\u2013109 (1971)","journal-title":"Trans. Am. Math. Soc."},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid Systems: Computation and Control","author":"IM Mitchell","year":"2007","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 428\u2013443. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_34"},{"issue":"3","key":"14_CR24","doi-asserted-by":"publisher","first-page":"509","DOI":"10.2514\/3.60598","volume":"20","author":"D Mortari","year":"1997","unstructured":"Mortari, D.: n-dimensional cross product and its application to the matrix eigenanalysis. J. Guid. Control. Dyn. 20(3), 509\u2013515 (1997)","journal-title":"J. Guid. Control. Dyn."},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Neumaier, A.: The wrapping effect, ellipsoid arithmetic, stability and confidence regions. Springer (1993). https:\/\/doi.org\/10.1007\/978-3-7091-6918-6_14","DOI":"10.1007\/978-3-7091-6918-6_14"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Ren, D., Liang, Z., Wu, C., Ding, J., Wu, T., Xue, B.: Inner-approximate reachability computation via zonotopic boundary analysis. arXiv preprint arXiv:2405.11155 (2024)","DOI":"10.1007\/978-3-031-65633-0_14"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1090\/conm\/178\/01902","volume":"178","author":"J Richter-Gebert","year":"1994","unstructured":"Richter-Gebert, J., Ziegler, G.M.: Zonotopal tilings and the bohne-dress theorem. Contemp. Math. 178, 211\u2013211 (1994)","journal-title":"Contemp. Math."},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Rwth, X.C., Sankaranarayanan, S., \u00c1brah\u00e1m, E.: Under-approximate flowpipes for non-linear continuous systems. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), pp. 59\u201366. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987596"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Sadraddini, S., Tedrake, R.: Linear encodings for polytope containment problems. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 4367\u20134372. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029363"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Schoels, T., Palmieri, L., Arras, K.O., Diehl, M.: An nmpc approach using convex inner approximations for online motion planning with guaranteed collision avoidance. In: 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 3574\u20133580. IEEE (2020)","DOI":"10.1109\/ICRA40945.2020.9197206"},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s10898-008-9334-6","volume":"44","author":"J Wan","year":"2009","unstructured":"Wan, J., Vehi, J., Luo, N.: A numerical approach to design control invariant sets for constrained nonlinear discrete-time systems with guaranteed optimality. J. Global Optim. 44, 395\u2013407 (2009)","journal-title":"J. Global Optim."},{"issue":"4","key":"14_CR32","doi-asserted-by":"publisher","first-page":"1468","DOI":"10.1109\/TAC.2019.2923049","volume":"65","author":"B Xue","year":"2019","unstructured":"Xue, B., Fr\u00e4nzle, M., Zhan, N.: Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Trans. Autom. Control 65(4), 1468\u20131483 (2019)","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR33","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"},{"issue":"1","key":"14_CR34","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1109\/TAC.2023.3274821","volume":"69","author":"B Xue","year":"2024","unstructured":"Xue, B., Zhan, N., Fr\u00e4nzle, M., Wang, J., Liu, W.: Reach-avoid verification based on convex optimization. IEEE Trans. Autom. Control 69(1), 598\u2013605 (2024)","journal-title":"IEEE Trans. Autom. Control"},{"key":"14_CR35","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1016\/j.automatica.2018.06.006","volume":"95","author":"X Yang","year":"2018","unstructured":"Yang, X., Scott, J.K.: A comparison of zonotope order reduction techniques. Automatica 95, 378\u2013384 (2018)","journal-title":"Automatica"},{"key":"14_CR36","unstructured":"Ziegler, G.M.: Lectures on polytopes, vol.\u00a0152. Springer Science & Business Media (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:15:07Z","timestamp":1732479307000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}