Supplementary Material: Order-Reduction Abstraction for Safety Verification of High-Dimensional Linear Systems

Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson

Abstract: Order-reduction is a standard automated approximation technique for computed-aided design, analysis, and simulation of many classes of systems, from circuits to buildings. For a given system, these methods produce a reduced-order system where the dimension of the state-space is smaller, while attempting to preserve behaviors similar to those of the full-order system. To be used as a sound abstraction procedure for formal verification, a measure of the similarity of behavior must be formalized and computed, which we develop in a computational way for a class of linear systems and periodically-switched systems as the main contributions of this paper. We have implemented the order-reduction as a sound abstraction process through a source-to-source model transformation in the HyST tool and use SpaceEx to compute sets of reachable states to verify properties of the full-order system through analysis of the reduced-order system. Our experimental results suggest systems with hundreds of state variables can be reduced to systems with tens of state variables such that the order-reduction overapproximation error is small enough to prove or disprove safety properties of interest, which alleviates the state-space explosion problem for verification of hybrid systems.

Paper submission PDF
The supplementary materials, including a prototype implementation in Matlab and all the SpaceEx model files (full and reduced-order) are available here. The prototype implementation is also implemented as a model transform transformation pass in Hyst (using the option -pass-order-reduction k=10, for example), which amounts effectively to executing the above Matlab scripts using an interface from Java (in which Hyst is written) to the sound order reduction (written in Matlab).