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. 


In oder to run all code in this prototype we need to:

1. Install mpt version 2.6 

2. Install Mattise 

This prototype uses mpt 2.6 to visualize safety specifications defined by polytopes and ellipsoids. 

Note that the newest version of mpt is mpt3 do not use class of polytopes anymore (it use polyhydron instead). 

Thus we need to install mpt version 2.6 for this version of prototype.
 

*** Tip for install mpt version 2.6 and mattise 

- download these packets from the repository of this protoype 

- use setpath and add with subfolder to add these packet into matlab 

- read readme files in these packets for further information 

3. Reproduce paper results:

*** run the order reduction prototype and produce comparisons to Matisse and simulation-based error bound estimation

- run script create_all_sys.m to create all systems

- run script run_all_sys.m to run order reduction and bisimulation for all system 

- run print_latex to print the experiment table 

- run plot_iss and plot_smcs to produce figures for these benchmarks

 

