DaDRA: A Python Library for Data-Driven Reachability Analysis

TL;DR

DaDRA is a Python library enabling data-driven reachability analysis with probabilistic guarantees, applicable to complex, real-world systems where traditional methods are impractical.

Contribution

The paper introduces DaDRA, a novel Python library that performs data-driven reachability analysis with probabilistic guarantees for complex systems.

Findings

Successfully applied to chaotic systems

Handles nonlinear dynamics and disturbances

Demonstrates practical utility in real-world scenarios

Abstract

Reachability analysis is used to determine all possible states that a system acting under uncertainty may reach. It is a critical component to obtain guarantees of various safety-critical systems both for safety verification and controller synthesis. Though traditional approaches to reachability analysis provide formal guarantees of the reachable set, they involve complex algorithms that require full system information, which is impractical for use in real world settings. We present DaDRA, a Python library that allows for data-driven reachability analysis with arbitrarily robust probabilistic guarantees. We demonstrate the practical functionality of DaDRA on various systems including: an analytically intractable chaotic system, benchmarks for systems with nonlinear dynamics, and a realistic system acting under complex disturbance signals and controlled with an intricate controller across multiple dimensions.