{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:07:11Z","timestamp":1743030431909,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present PyBDR, a Python reachability analysis toolkit based on set-boundary analysis, which centralizes on widely-adopted set propagation techniques for formal verification, controller synthesis, state estimation, etc. It employs boundary analysis of initial sets to mitigate the wrapping effect during computations, thus improving the performance of reachability analysis algorithms without significantly increasing computational costs. Beyond offering various set representations such as polytopes and zonotopes, our toolkit particularly excels in interval arithmetic by extending operations to the tensor level, enabling efficient parallel interval arithmetic computation and unifying vector and matrix intervals into a single framework. Furthermore, it features symbolic computation of derivatives of arbitrary order and evaluates them as real or interval-valued functions, which is essential for approximating behaviours of nonlinear systems at specific time instants. Its modular architecture design offers a series of building blocks that facilitate the prototype development of reachability analysis algorithms. Comparative studies showcase its strengths in handling verification tasks with large initial sets or long time horizons. The toolkit is available at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/ASAG-ISCAS\/PyBDR\">https:\/\/github.com\/ASAG-ISCAS\/PyBDR<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_10","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"140-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["PyBDR: Set-Boundary Based Reachability Analysis Toolkit in\u00a0Python"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0705-0345","authenticated-orcid":false,"given":"Jianqiang","family":"Ding","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3398-0466","authenticated-orcid":false,"given":"Taoran","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1171-7061","authenticated-orcid":false,"given":"Zhen","family":"Liang","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,9,13]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Alanwar, A., Said, H., Althoff, M.: Distributed secure state estimation using diffusion Kalman filters and reachability analysis. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 4133\u20134139. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029929"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013182 (2013)","DOI":"10.1145\/2461328.2461358"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Althoff, M.: An introduction to CORA 2015. In: Proceedings of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151. EasyChair (2015). https:\/\/doi.org\/10.29007\/zbkv, https:\/\/easychair.org\/publications\/paper\/xMm","DOI":"10.29007\/zbkv"},{"key":"10_CR4","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. Ann. Rev. Control Robot. Auton. Syst. 4, 369\u2013395 (2021)","journal-title":"Ann. Rev. Control Robot. Auton. Syst."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Althoff, M., Grebenyuk, D.: Implementation of interval arithmetic in CORA 2016. In: Proceedings of the 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 91\u2013105 (2016)","DOI":"10.29007\/w19b"},{"issue":"10","key":"10_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2507771.2507783","volume":"56","author":"M Althoff","year":"2013","unstructured":"Althoff, M., Rajhans, A., Krogh, B.H., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. Commun. ACM 56(10), 97\u2013104 (2013)","journal-title":"Commun. ACM"},{"key":"10_CR7","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":"10_CR8","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: HyLAA: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 173\u2013178 (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-63387-9_20","volume-title":"Computer Aided Verification","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 401\u2013420. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_20"},{"issue":"3","key":"10_CR10","first-page":"46","volume":"19","author":"RW Beard","year":"2008","unstructured":"Beard, R.W.: Quadrotor dynamics and control. Brigham Young Univ. 19(3), 46\u201356 (2008)","journal-title":"Brigham Young Univ."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39\u201344 (2019)","DOI":"10.1145\/3302504.3311804"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-13338-6_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Bogomolov","year":"2014","unstructured":"Bogomolov, S., et al.: Assume-guarantee abstraction refinement meets hybrid systems. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 116\u2013131. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_10"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1146\/annurev-control-060117-104941","volume":"1","author":"M Chen","year":"2018","unstructured":"Chen, M., Tomlin, C.J.: Hamilton-Jacobi reachability: some recent theoretical advances and applications in unmanned airspace management. Ann. Rev. Control Robot. Auton. Syst. 1, 333\u2013358 (2018)","journal-title":"Ann. Rev. Control Robot. Auton. Syst."},{"key":"10_CR14","unstructured":"Chen, R.T., Rubanova, Y., Bettencourt, J., Duvenaud, D.K.: Neural ordinary differential equations. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"key":"10_CR15","unstructured":"Chen, X.: Reachability analysis of non-linear hybrid systems using taylor models. Ph.D. thesis, Fachgruppe Informatik, RWTH Aachen University (2015)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"10_CR17","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"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: Algorithm 852: Realpaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. (TOMS) 32(1), 138\u2013156 (2006)","journal-title":"ACM Trans. Math. Softw. (TOMS)"},{"issue":"7825","key":"10_CR19","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1038\/s41586-020-2649-2","volume":"585","author":"CR Harris","year":"2020","unstructured":"Harris, C.R., et al.: Array programming with NumPy. Nature 585(7825), 357\u2013362 (2020). https:\/\/doi.org\/10.1038\/s41586-020-2649-2","journal-title":"Nature"},{"key":"10_CR20","unstructured":"Khalil, H.K.: Nonlinear Systems. Prentice Hall, Upper Saddle River (NJ), 3. ed., international ed. edn. (2000)"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"K\u00fchn, W.: Zonotope dynamics in numerical quality control. In: Hege, HC., Polthier, K. (eds.) Mathematical Visualization: Algorithms, Applications and Numerics, pp. 125\u2013134. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-662-03567-2_10","DOI":"10.1007\/978-3-662-03567-2_10"},{"key":"10_CR22","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 Le Guernic","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"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-031-35257-7_15","volume-title":"Theoretical Aspects of Software Engineering","author":"Z Liang","year":"2023","unstructured":"Liang, Z., Ren, D., Liu, W., Wang, J., Yang, W., Xue, B.: Safety verification for neural networks based on set-boundary analysis. In: David, C., Sun, M. (eds.) Theoretical Aspects of Software Engineering, pp. 248\u2013267. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35257-7_15"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Liu, E.I., W\u00fcrsching, G., Klischat, M., Althoff, M.: CommonRoad-Reach: a toolbox for reachability analysis of automated vehicles. In: 2022 IEEE 25th International Conference on Intelligent Transportation Systems (ITSC), pp. 2313\u20132320. IEEE (2022)","DOI":"10.1109\/ITSC55140.2022.9922232"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Manzanas Lopez, D., Musau, P., Hamilton, N.P., Johnson, T.T.: Reachability analysis of a general class of neural ordinary differential equations. In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems. FORMATS 2022. LNCS, vol. 13465. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_15","DOI":"10.1007\/978-3-031-15839-1_15"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","DOI":"10.7717\/peerj-cs.103"},{"issue":"7","key":"10_CR27","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"IM Mitchell","year":"2005","unstructured":"Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"10_CR28","unstructured":"Moore, R.E.: Interval Analysis, vol.\u00a04. Prentice-Hall Englewood Cliffs (1966)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Park, J., \u00d6zg\u00fcner, \u00dc.: Model based controller synthesis using reachability analysis that guarantees the safety of autonomous vehicles in a convoy. In: 2012 IEEE International Conference on Vehicular Electronics and Safety (ICVES 2012), pp. 134\u2013139. IEEE (2012)","DOI":"10.1109\/ICVES.2012.6294257"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-26287-1_1","volume-title":"Hardware and Software: Verification and Testing","author":"R Ray","year":"2015","unstructured":"Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., Grosu, R.: XSpeed: accelerating reachability analysis on multi-core processors. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 3\u201318. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26287-1_1"},{"key":"10_CR31","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. In: To appear in Computer Aided Verification: 36th International Conference, CAV 2024 (2024)","DOI":"10.1007\/978-3-031-65633-0_14"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Rump, S.M. (1999). INTLAB \u2014 INTerval LABoratory. In: Csendes, T. (eds) Developments in Reliable Computing. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-1247-7_7","DOI":"10.1007\/978-94-017-1247-7_7"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-57288-8_20","volume-title":"NASA Formal Methods","author":"S Schupp","year":"2017","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Makhlouf, I.B., Kowalewski, S.: HyPro: A C++\u00a0library of state set representations for hybrid systems reachability analysis. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 288\u2013294. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_20"},{"key":"10_CR34","unstructured":"Sch\u00fcrmann, B.: Using reachability analysis in controller synthesis for safety-critical systems. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2022)"},{"issue":"1","key":"10_CR35","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1109\/JPROC.2011.2165329","volume":"100","author":"Y Susuki","year":"2011","unstructured":"Susuki, Y., et al.: A hybrid system approach to the analysis and design of power grid dynamic performance. Proc. IEEE 100(1), 225\u2013239 (2011)","journal-title":"Proc. IEEE"},{"issue":"2","key":"10_CR36","doi-asserted-by":"publisher","first-page":"7912","DOI":"10.1016\/j.ifacol.2023.10.028","volume":"56","author":"C Tang","year":"2023","unstructured":"Tang, C., Althoff, M.: Formal verification of robotic contact tasks via reachability analysis. IFAC-PapersOnLine 56(2), 7912\u20137919 (2023)","journal-title":"IFAC-PapersOnLine"},{"issue":"7","key":"10_CR37","doi-asserted-by":"publisher","first-page":"3518","DOI":"10.1109\/TAC.2016.2615599","volume":"62","author":"B Xue","year":"2016","unstructured":"Xue, B., Easwaran, A., Cho, N.J., Fr\u00e4nzle, M.: Reach-avoid verification for nonlinear systems based on boundary analysis. IEEE Trans. Autom. Control 62(7), 3518\u20133523 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"key":"10_CR38","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":"10_CR39","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1109\/TAC.2020.2977993","volume":"66","author":"B Xue","year":"2020","unstructured":"Xue, B., Wang, Q., Feng, S., Zhan, N.: Over-and underapproximating reach sets for perturbed delay differential equations. IEEE Trans. Autom. Control 66(1), 283\u2013290 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Yang, B., Stipanovic, D.: Nonlinear Systems: Recent Developments and Advances (2023)","DOI":"10.5772\/intechopen.100717"},{"issue":"2008","key":"10_CR41","first-page":"1","volume":"754","author":"D Zuras","year":"2008","unstructured":"Zuras, D., et al.: IEEE standard for floating-point arithmetic. IEEE Std. 754(2008), 1\u201370 (2008)","journal-title":"IEEE Std."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:12:07Z","timestamp":1726121527000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}