Order-Reduction Abstractions for Safety Verification of High-Dimensional Linear Systems

TL;DR

This paper introduces a formal, computational method for order-reduction of high-dimensional linear systems, enabling effective safety verification by preserving behavior similarity and reducing computational complexity.

Contribution

It develops a formal measure of behavior similarity for order-reduction of linear systems and implements a sound abstraction process integrated with existing verification tools.

Findings

Systems with thousands of variables reduced to tens of variables

Order-reduction maintains small overapproximation error

Enables safety verification of high-dimensional systems

Abstract

Order-reduction is a standard automated approximation technique for computer-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 original system. To be used as a sound abstraction 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 on the order of a thousand 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 using current reachability analysis tools. Our results illustrate this approach is effective to alleviate the state-space explosion problem for verification of high-dimensional linear systems.