PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python

Jianqiang Ding*, Taoran Wu, Zhen Liang, Bai Xue

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingsScientificpeer-review

26 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationFormal Methods - 26th International Symposium, FM 2024, Proceedings
EditorsAndre Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi
PublisherSpringer
Pages140-157
Number of pages18
ISBN (Print)978-3-031-71176-3
DOIs
Publication statusPublished - 2025
MoE publication typeA4 Conference publication
EventInternational Symposium on Formal Methods - Milan, Italy
Duration: 9 Sept 202413 Sept 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14934 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Symposium on Formal Methods
Abbreviated titleFM
Country/TerritoryItaly
CityMilan
Period09/09/202413/09/2024

Fingerprint

Dive into the research topics of 'PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python'. Together they form a unique fingerprint.

Cite this