JuliaReach: a Toolbox for Set-Based Reachability

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.

Accepted in Proceedings of HSCC'19: 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC'19)

References in corpus (1)

• Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices

Cited by in corpus (17)

• Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
• Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data
• Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
• Reachability analysis of linear hybrid systems via block decomposition
• Shielded Reinforcement Learning for Hybrid Systems
• Conservative Time Discretization: A Comparative Study
• Combining Set Propagation with Finite Element Methods for Time Integration in Transient Solid Mechanics Problems
• Axiomatization of Compact Initial Value Problems: Open Properties
• Reachability of weakly nonlinear systems using Carleman linearization
• Dionysos.jl: a Modular Platform for Smart Symbolic Control
• Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions
• Automatic and Scalable Safety Verification using Interval Reachability with Subspace Sampling
• Adaptive Parameter Tuning for Reachability Analysis of Linear Systems
• The inverse problem for neural networks
• The Reachability Problem for Neural-Network Control Systems
• Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation
• Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach