Bounded verification with on-the-fly discrepancy computation

Chuchu Fan, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Simulation-based verification algorithms can provide formal safety guarantees for nonlinear and hybrid systems. The previous algorithms rely on user provided model annotations called discrepancy function, which are crucial for computing reachtubes from simulations. In this paper, we eliminate this requirement by presenting an algorithm for computing piecewise exponential discrepancy functions. The algorithm relies on computing local convergence or divergence rates of trajectories along a simulation using a coarse over-approximation of the reach set and bounding the maximal eigenvalue of the Jacobian over this over-approximation. The resulting discrepancy function preserves the soundness and the relative completeness of the verification algorithm. We also provide a coordinate transformation method to improve the local estimates for the convergence or divergence rates in practical examples. We extend the method to get the input-to-state discrepancy of nonlinear dynamical systems which can be used for compositional analysis. Our experiments show that the approach is effective in terms of running time for several benchmark problems, scales reasonably to larger dimensional systems, and compares favorably with respect to available tools for nonlinear models.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Proceedings
EditorsBernd Finkbeiner, Geguang Pu, Lijun Zhang
PublisherSpringer
Pages446-463
Number of pages18
ISBN (Print)9783319249520
DOIs
StatePublished - 2015
Event13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 - Shanghai, China
Duration: Oct 12 2015Oct 15 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9364
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
Country/TerritoryChina
CityShanghai
Period10/12/1510/15/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Bounded verification with on-the-fly discrepancy computation'. Together they form a unique fingerprint.

Cite this