Order-reduction abstractions for safety verification of high-dimensional linear systems

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

Research output: Contribution to journalArticle

6 Scopus citations

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. 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 asymptotic stable linear 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 thousand 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 using current reachability analysis tools. Our results illustrate this approach is effective in tackling the state-space explosion problem for verification of high-dimensional linear systems.

Original languageEnglish (US)
Pages (from-to)443-461
Number of pages19
JournalDiscrete Event Dynamic Systems: Theory and Applications
Volume27
Issue number2
DOIs
StatePublished - Jun 1 2017
Externally publishedYes

Keywords

  • Abstraction
  • Model reduction
  • Order reduction
  • Reachability analysis
  • Verification

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Modeling and Simulation
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Order-reduction abstractions for safety verification of high-dimensional linear systems'. Together they form a unique fingerprint.

  • Cite this