TY - JOUR
T1 - Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)
AU - Bogomolov, Sergiy
AU - Forets, Marcelo
AU - Frehse, Goran
AU - Podelski, Andreas
AU - Schilling, Christian
N1 - Publisher Copyright:
© 2022 The Author(s)
PY - 2022/11/22
Y1 - 2022/11/22
N2 - Approximating the set of reachable states of a dynamical system is an algorithmic way to rigorously reason about its safety. Despite progress on efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in practice. 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 are performed in the full dimension. Our method is applicable in both dense- and discrete-time settings. For a set of standard benchmarks, we show a speed-up of up to two orders of magnitude compared to the respective state-of-the-art tools, with only modest loss 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 before.
AB - Approximating the set of reachable states of a dynamical system is an algorithmic way to rigorously reason about its safety. Despite progress on efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in practice. 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 are performed in the full dimension. Our method is applicable in both dense- and discrete-time settings. For a set of standard benchmarks, we show a speed-up of up to two orders of magnitude compared to the respective state-of-the-art tools, with only modest loss 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 before.
KW - Linear time-invariant systems
KW - Reachability analysis
KW - Safety verification
KW - Set recurrence relation
UR - http://www.scopus.com/inward/record.url?scp=85133728528&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2022.104937
DO - 10.1016/j.ic.2022.104937
M3 - Journal article
AN - SCOPUS:85133728528
SN - 0890-5401
VL - 289
JO - Information and Computation
JF - Information and Computation
M1 - 104937
ER -