Source-linked AI summary
JuliaReach: a Toolbox for Set-Based Reachability
Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, Christian Schilling
TL;DR
Set-based reachability needs reusable implementations that support rigorous analysis without sacrificing prototyping efficiency or runtime performance. JuliaReach addresses this with the Reachability and LazySets packages, combining lazy and concrete convex-set computation; its case studies report efficient analyses, while the approach remains subject to design choices about lazy versus approximate intersections.
Problem
Set-based reachability tools often lack shared code, while researchers must balance prototyping convenience against compiled-language performance.
Method
JuliaReach combines a Julia-based Reachability framework for continuous and hybrid systems with LazySets, which supports lazy and concrete convex-set representations and overapproximation.
Results
All discrete-post operators outperform SpaceEx on the biggest filtered-oscillator model instances, while lazy-intersection approaches scale better than concrete polytope intersection.
Takeaways & Limitations
JuliaReach supports reusable reachability development by combining lazy high-dimensional operations with explicit low-dimensional approximations for complex problems.
Takeaways & Limitations
For more directions, there is no clear recipe for which intersections should remain lazy and which should be overapproximated.
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
JuliaReach addresses fragmented reachability implementations by providing a Julia-based toolbox that combines reusable infrastructure, convex-set calculus, and rapid prototyping with high performance.
- 1 INTRODUCTION: The toolbox responds to the lack of a shared code base across flowpipe-construction tools by offering a flexible interface and reusable implementation foundation.The stated goal is to let researchers prototype related approaches without starting from scratch.
- 1 INTRODUCTION: Julia is presented as a compromise between compiled-language performance and interpreted-language prototyping convenience through interactive execution and JIT compilation.The paper contrasts this with compilation overhead in C++ and performance or two-language issues in Python.
- 1 INTRODUCTION: JuliaReach is an open-source Julia toolbox for rapid prototyping of set-based reachability approaches.It targets rigorous analysis of dynamical systems and is designed around reusable software infrastructure.
- 1 INTRODUCTION: Its Reachability package provides infrastructure for continuous and hybrid-system algorithms, including decomposition for LTI systems and interleaving continuous and discrete-post operators.These implementations serve as proof-of-concept algorithms within the framework.
- 1 INTRODUCTION: JuliaReach includes documentation, testing, extensibility, and peer-reviewed continuous integration to support both end users and developers.The toolbox is distributed through Julia packages and can be installed with one command.
2 THE LAZYSETS LIBRARY
LazySets provides concrete and lazy representations of convex sets, allowing operations to remain unevaluated and later be overapproximated for visualization or analysis. Its approximation tools combine high-dimensional lazy computation with explicit low-dimensional representations.
- 2 THE LAZYSETS LIBRARY: Multiple dispatch over LazySet{N} lets the library switch between floating-point and exact numeric types while generating type-specific JIT-compiled code.This design allows new set types and generic functions to share common interfaces.
- 2 THE LAZYSETS LIBRARY: LazySets supports common convex-set representations and lazy wrappers for operations including convex hulls, Minkowski sums, maps, intersections, and Cartesian products.Concrete representations include polyhedra, polytopes, zonotopes, ellipsoids, balls, and hyperrectangles.
- 2 THE LAZYSETS LIBRARY: Lazy operations defer explicit construction and evaluate support vectors recursively, such as applying a linear map through M · σ(M^Td,S) or decomposing Minkowski sums.Explicit alternatives remain available for operations such as linear maps and Minkowski sums.
- 2.2 From lazy to concrete set representation: The Approximations module converts lazy sets to concrete overapproximations and can combine high-dimensional lazy sets with explicit low-dimensional projections.This supports visualization or verification of properties involving only selected variables.
- 2.2 From lazy to concrete set representation: The overapproximate function uses supporting directions and Kamenev’s method to approximate a 2D set within a specified Hausdorff-distance error bound.It can operate on nested lazy sets that implement support-function evaluation.
- 2.2 From lazy to concrete set representation: For a 1,000-dimensional example, approximation runtimes increase from 55 ms at ε = Inf to 195 ms at ε = 0.1 and 2 s at ε = 0.001.The approximations are shown for the projection onto x1 and x50, with increasing precision across the three ε values.
3 THE REACHABILITY PACKAGE
The Reachability package provides infrastructure and interfaces for implementing continuous and hybrid-system reachability algorithms, including continuous and discrete post operators. It supports both concrete and lazy operator implementations, with lazy computation scaling well for support vectors in a single direction.
- 3.1 Infrastructure: Reachability supplies infrastructure for custom reachability algorithms on continuous and hybrid systems modeled as hybrid automata.Its interfaces include solver backends, post operators, reach-set wrappers, and standard hybrid-system utilities.
- 3.2 Continuous-Post Operators: Continuous-post operators return reach tubes as sequences of ReachSets containing sets paired with uncertain time intervals.Algorithms receive a continuous model, a ReachSet, and options such as step count and step size.
- 3.2 Continuous-Post Operators: The package supports large-scale sparse LTI analysis by decomposing systems into low-dimensional blocks and solving many smaller reachability problems.The decomposition introduces approximation error but is intended for large-scale systems.
- 3.3 Discrete-Post Operators: Hybrid reachability interleaves continuous-post and discrete-post operators, with discrete transitions overapproximating assigned guarded states restricted to target invariants.The solve function implements this interleaving for supplied post operators.
- 3.3 Discrete-Post Operators: The package implements concrete polytope intersections and a lazy operator that can overapproximate intersections when materializing a concrete set.The lazy operator evaluates only the highest nesting level with line search and uses coarser heuristics below it.
- 3.3 Discrete-Post Operators: Purely lazy intersection handling scales very well for one support-vector direction, but lacks a clear strategy for choosing lazy versus overapproximated intersections across multiple directions.The package compares concrete, fully lazy, and fully overapproximated variants in a case study; the plotted two-mode system distinguishes locations by blue and red colors.
4 CASE STUDY
The case studies demonstrate JuliaReach's rapid-prototyping workflow for continuous and hybrid reachability, then compare discrete-post operators on a filtered oscillator. The lazy-intersection approaches scale better than concrete polytope intersection, and all operators outperform SpaceEx on the largest instances.
- 4.1 Working with the LazySets Library: The first case study re-implements Girard's LTI zonotope reachability algorithm and extends it to a two-mode hybrid system using LazySets.The extension uses guard-triggered transitions and zonotope order reduction with an upper bound of 10 generators.
- 4.1 Working with the LazySets Library: The hybrid case study analyzes reachable states over [0, 4] with time step δ = 0.001, taking 0.25 seconds.Transitions are taken as soon as an intersection with a guard is detected.
- 4.2 Working with the Reachability Framework: The second case study compares alternative discrete-post operators in Reachability using a parameterized filtered oscillator with filter dimension m.The model combines a two-dimensional switched oscillator with an m-dimensional filter whose output amplitude decreases as m increases.
- 4.2 Working with the Reachability Framework: The benchmark fixes four jumps and uses δ = 0.01, with intervals [0, 20] for filters up to dimension four and [0, 99] for higher dimensions.The evaluation compares Reachability operators with SpaceEx under the stated hardware and model settings.
- 4.2 Working with the Reachability Framework: All operators outperform SpaceEx on the biggest filtered-oscillator instances, while lazy-intersection approaches scale much better than concrete polytope intersection.The benchmark uses Table 1 runtimes for different Reachability operators and SpaceEx.
5 CONCLUSION
JuliaReach provides a Julia-based environment for developing reachability algorithms, combining the Reachability framework with the LazySets convex-set library. Future work will extend Reachability with additional post operators, including one exploiting low-dimensional continuous-post outputs.
- 5 CONCLUSION: JuliaReach combines the Reachability framework with the standalone LazySets library for convex-set calculus in a Julia environment.The toolbox is presented as a new environment for developing reachability algorithms for dynamical systems.
- 5 CONCLUSION: Future work will add more Reachability post operators, including one that exploits the low-dimensional output of the continuous-post operator in the hybrid loop.
A HYBRID REACHABILITY IMPLEMENTATION
The hybrid implementation embeds LazySets operations in a simple algorithm that alternates continuous successor computation with guard checks and transition propagation. A queue manages locations and pending states until reachable results are collected.
- A HYBRID REACHABILITY IMPLEMENTATION: ReachHybrid initializes a queue with the initial states and repeatedly processes queued states while the queue is nonempty.
- A HYBRID REACHABILITY IMPLEMENTATION: The implementation computes continuous successors, checks their intersection with outgoing guards, and enqueues nonempty transitioned states for further exploration.
- A HYBRID REACHABILITY IMPLEMENTATION: Each outgoing transition is tested by iterating through its guard and target-location pairs.