Dynamics-aware subspace identification for decomposed aggregation in the reachability analysis of hybrid automata.

Hybrid automata are an emerging formalism used to model sampled-data control Cyber-Physical Systems (CPS), and analyze their behavior using reachability analysis. This is because hybrid automata provide a richer and more flexible modeling framework, compared to traditional approaches. However, modern state-of-the-art tools struggle to analyze such systems, due to the computational complexity of the reachability algorithm, and due to the introduced overapproximation error. These shortcomings are largely attributed (but not limited) to the aggregation of sets. In this paper we propose a subspace identification approach for decomposed aggregation in the reachability analysis of hybrid automata with linear dynamics. Our key contribution is the observation that the choice of a good subspace basis does not only depend on the sets being aggregated, but also on the continuous-time dynamics of an automaton. With this observation in mind, we present a dynamics-aware sub-space identification algorithm that we use to construct tight decomposed convex hulls for the aggregated sets. Our approach is evaluated on two practically relevant hybrid automata models of sampled-data CPS that have been shown to be difficult to analyze by modern state-of-the-art tools. Specifically, we show that for these models our approach can improve the accuracy of the reachable set by up-to 10 times when compared to standard Principal Component Analysis (PCA), for which finding a fixed point is not guaranteed. We also show that while the computational complexity is increased, a fixed-point is found earlier.