PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python
Loading...
Access rights
openAccess
publishedVersion
URL
Journal Title
Journal ISSN
Volume Title
A4 Artikkeli konferenssijulkaisussa
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Authors
Date
2025
Major/Subject
Mcode
Degree programme
Language
en
Pages
18
Series
Formal Methods - 26th International Symposium, FM 2024, Proceedings, pp. 140-157, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ; Volume 14934 LNCS
Abstract
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 https://github.com/ASAG-ISCAS/PyBDR.Description
Publisher Copyright: © The Author(s) 2025.
Keywords
Other note
Citation
Ding, J, Wu, T, Liang, Z & Xue, B 2025, PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python . in A Platzer, K Y Rozier, M Pradella & M Rossi (eds), Formal Methods - 26th International Symposium, FM 2024, Proceedings . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14934 LNCS, Springer, pp. 140-157, International Symposium on Formal Methods, Milan, Italy, 09/09/2024 . https://doi.org/10.1007/978-3-031-71177-0_10