화학공학소재연구정보센터
IEEE Transactions on Automatic Control, Vol.62, No.7, 3518-3523, 2017
Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis
In this technical note, we propose a set-boundary based method to verify reach-avoid properties of non-linear dynamical systems with parametric uncertainty, which works under the assumption that the initial set is a compact set. In comparison to the conventional approach employing safely overapproximating state extrapolation on the full volume of the initial set, our boundary-based method applies such state extrapolation only to the initial set's boundary, and thus to a set of significantly smaller volume. This can help enhance precision and reduce computational burden when solving reach-avoid verification problems, especially for cases with large initial sets and/or large time horizons. Furthermore, our boundary-based method lifts existing reachability-analysis techniques with their often confined geometric representations of reachable sets (like interval boxes, zonotopes, polyhedra, ellipsoids) to considerably more complex geometric shapes, where the boundary of the set is representable as a finite union of such shapes. The resulting benefits brought by our boundary-based method in reach-avoid verification are illustrated through several examples.