Simulation-driven reachability using matrix measures

Chuchu Fan, James Kapinski, Xiaoqing Jin, Sayan Mitra

Research output: Contribution to journalArticlepeer-review

Abstract

Simulation-driven verification can provide formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set overapproximations from a set of initial states through numerical simulations and sensitivity analysis. This article addresses this problem by providing algorithms for computing discrepancy functions as the upper bound on the sensitivity, that is, the rate at which trajectories starting from neighboring states converge or diverge. The algorithms rely on computing local bounds on matrix measures as the exponential change rate of the discrepancy function. We present two techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function, and therefore, the conservativeness of the overapproximation, is locally minimized. The proposed algorithms enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy functions give soundness and relative completeness of the overall simulation-driven safety-bounded verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the algorithms.

Original languageEnglish (US)
Article number21
JournalACM Transactions on Embedded Computing Systems
Volume17
Issue number1
DOIs
StatePublished - Dec 2017

Keywords

  • Discrepancy function
  • Embedded System
  • Matrix measures
  • Nonlinear System
  • Reachability

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Simulation-driven reachability using matrix measures'. Together they form a unique fingerprint.

Cite this