Decomposed Reachability Analysis for Nonlinear Systems

Document Type

Article

Publication Date

11-2016

Publication Source

IEEE Real-Time Systems Symposium

Abstract

We introduce an approach to conservatively abstract a nonlinear continuous system by a hybrid automaton whose continuous dynamics are given by a decomposition of the original dynamics. The decomposed dynamics is in the form of a set of lower-dimensional ODEs with time-varying uncertainties whose ranges are defined by the hybridization domains.

We propose several techniques in the paper to effectively compute abstractions and flowpipe overapproximations. First, a novel method is given to reduce the overestimation accumulation in a Taylor model flowpipe construction scheme. Then we present our decomposition method, as well as the framework of on-the-fly hybridization. A combination of the two techniques allows us to handle much larger, nonlinear systems with comparatively large initial sets. Our prototype implementation is compared with existing reachability tools for offline and online flowpipe construction on challenging benchmarks of dimensions ranging from 7 to 30. Our code has successfully passed the artifact evaluation

Inclusive pages

13-24

ISBN/ISSN

9781509053032

Comments

Permission documentation on file.

Publisher

Institute of Electrical and Electronics Engineers

Peer Reviewed

yes


Share

COinS