JuliaReach: a Toolbox for Set-Based Reachability

TL;DR

JuliaReach addresses the need for a fast, prototype-friendly toolbox for set-based reachability of continuous and hybrid dynamical systems. It couples LazySets, a lazy/concrete convex-set library, with Reachability, a framework for post operators, both implemented in Julia to balance high-level expressiveness with near-compiled performance. The approach leverages lazy set representations to scale to high dimensions while enabling on-demand concretization, demonstrated through case studies on LTI and hybrid systems and by benchmarking discrete-post operators against SpaceEx. Together, the work provides a reusable, extensible platform for rapid prototyping of reachability algorithms and their convex-set implementations, with broad practical impact for formal verification and safety analysis.

Abstract

We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.

Figures (5)

• Figure 1: Description of the overapproximation algorithm. We start with box directions ($\pm d_1$ and $\pm d_2$) and then check for each angle if the distance between the support vector of the original set and the vertex is less than an error bound $\varepsilon$.
• Figure 2: Decomposition of the $1{,}000$-dimensional set Y, projected onto $x_1$ and $x_{50}$, with polytope approximations of different precision: $\varepsilon = \textrm{Inf}$ (box directions, blue), $\varepsilon = 0.1$ (green), and $\varepsilon = 0.001$ (red). Runtimes are 55 ms, 195 ms and 2 s, respectively.
• Figure 3: Reachability plot of a two-mode hybrid system. The colors represent location 1 (blue) and location 2 (red), respectively.
• Figure 4: Hybrid automaton model of a 2-dimensional oscillator and an $m$-dimensional filter.
• Figure 5: Output for the filtered oscillator model with different filter dimension $m$, using Reachability with the lazy discrete-post operator with overapproximation. Left: $m=4$. Right: $m=16$.