TY - GEN
T1 - Reachability Analysis of Nonlinear Systems Using Hybridization and Dynamics Scaling
AU - Li, Dongxu
AU - Bak, Stanley
AU - Bogomolov, Sergiy
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.
AB - Reachability analysis techniques aim to compute which states a dynamical system can enter. The analysis of systems described by nonlinear differential equations is known to be particularly challenging. Hybridization methods tackle this problem by abstracting nonlinear dynamics with piecewise linear dynamics around the reachable states, with additional inputs to ensure overapproximation. This reduces the analysis of a system with nonlinear dynamics to the one with piecewise affine dynamics, which have powerful analysis methods. In this paper, we present improvements to the hybridization approach based on a dynamics scaling model transformation. The transformation aims to reduce the sizes of the linearization domains, and therefore reduces overapproximation error. We showcase the efficiency of our approach on a number of nonlinear benchmark instances, and compare our approach with Flow*.
UR - https://www.scopus.com/pages/publications/85090170700
U2 - 10.1007/978-3-030-57628-8_16
DO - 10.1007/978-3-030-57628-8_16
M3 - Conference contribution
AN - SCOPUS:85090170700
SN - 9783030576271
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 265
EP - 282
BT - Formal Modeling and Analysis of Timed Systems - 18th International Conference, FORMATS 2020, Proceedings
A2 - Bertrand, Nathalie
A2 - Jansen, Nils
PB - Springer
T2 - 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020
Y2 - 1 September 2020 through 3 September 2020
ER -