Decomposed Reachability Analysis for Nonlinear Systems
IEEE Real-Time Systems Symposium
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
Copyright © 2016, IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Institute of Electrical and Electronics Engineers
Chen, Xin and Sankaranarayanan, Sriram, "Decomposed Reachability Analysis for Nonlinear Systems" (2016). Computer Science Faculty Publications. 130.