Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)

DOI10.1016/j.ic.2022.104937OpenAlexW4284691246WikidataQ114172427 ScholiaQ114172427MaRDI QIDQ2105418

Goran Frehse, Sergiy Bogomolov, Andreas Podelski, Christian Schilling, Marcelo Forets

Publication date: 8 December 2022

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2022.104937

zbMATH Keywords

reachability analysissafety verificationlinear time-invariant systemsset recurrence relation

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• LAPACK
• SLICOT
• Algorithm 919
• Arb
• Ellipsoidal Toolbox
• SpaceEx
• Julia
• XSpeed
• phipm
• DifferentialEquations.jl
• benchmodred
• JuliaReach
• Mjollnir
• NeuralPDE.jl
• Lazysets.jl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability analysis of linear systems using support functions
• Time-scale decomposition of the reachable set of constrained linear systems
• Overapproximating reachable sets by Hamilton-Jacobi projections
• An algorithm for approximating polyhedra.
• Order-reduction abstractions for safety verification of high-dimensional linear systems
• Simulation-equivalent reachability of large linear systems with inputs
• Conservative time discretization: a comparative study
• From the zonotope construction to the Minkowski addition of convex polytopes
• Julia: A Fresh Approach to Numerical Computing
• Reachability Analysis of Nonlinear Differential-Algebraic Systems
• Flowpipe approximation and clustering in space-time
• Quasi-dependent variables in hybrid automata
• Eliminating spurious transitions in reachability with support functions
• Algorithm 919
• Complexity reduction through a Schur-based decomposition for reachability analysis of linear time-invariant systems
• Asymptotics for Singularly Perturbed Reachable Sets
• Counterexample-Guided Refinement of Template Polyhedra
• The modified method of refined bounds for polyhedral approximation of convex polytopes
• Reachability Analysis of Hybrid Systems Using Support Functions
• Analysis of Some Krylov Subspace Approximations to the Matrix Exponential Operator
• Two Fast Algorithms for Sparse Matrices: Multiplication and Permuted Transposition
• Reachability Analysis Using Polygonal Projections
• Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices
• Arb: Efficient Arbitrary-Precision Midpoint-Radius Interval Arithmetic
• Composing Reachability Analyses of Hybrid Systems for Safety and Stability
• The Reach-and-Evolve Algorithm for Reachability Analysis of Nonlinear Dynamical Systems
• Reachability Analysis of Large Linear Systems With Uncertain Inputs in the Krylov Subspace
• Numerical verification of affine systems with up to a billion dimensions
• JuliaReach
• Hybrid Systems: Computation and Control
• Thread modularity at many levels: a pearl in compositional verification
• Hybrid Systems: Computation and Control
• The principle of minimized iterations in the solution of the matrix eigenvalue problem
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control