Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices
arXiv:1801.09526 · doi:10.1145/3178126.3178128
Abstract
Approximating the set of reachable states of a dynamical system is an algorithmic yet mathematically rigorous way to reason about its safety. Although progress has been made in the development of efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in the industrial setting. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach set computations such that set operations are performed in low dimensions, while matrix operations like exponentiation are carried out in the full dimension. Our method is applicable both in dense- and discrete-time settings. For a set of standard benchmarks, it shows a speed-up of up to two orders of magnitude compared to the respective state-of-the art tools, with only modest losses in accuracy. For the dense-time case, we show an experiment with more than 10.000 variables, roughly two orders of magnitude higher than possible with previous approaches.
References in corpus (1)
Cited by in corpus (10)
- JuliaReach: a Toolbox for Set-Based Reachability
- Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis
- Numerical Verification of Affine Systems with up to a Billion Dimensions
- LazySets.jl: Scalable Symbolic-Numeric Set Computations
- Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets
- Reachability analysis of linear hybrid systems via block decomposition
- Combining Set Propagation with Finite Element Methods for Time Integration in Transient Solid Mechanics Problems
- Conservative Time Discretization: A Comparative Study
- Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions
- Adaptive Parameter Tuning for Reachability Analysis of Linear Systems