Decomposed Reachability Analysis for Nonlinear Systems

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.