University of Illinois Urbana-Champaign

Bounded Verification with On-the-Fly Discrepancy Computation

Fan, Chuchu; Mitra, Sayan

Content Files
UILU-ENG-15-2201.pdf

Permalink

https://hdl.handle.net/2142/90444

Description

Title
Bounded Verification with On-the-Fly Discrepancy Computation
Author(s)
  • Fan, Chuchu
  • Mitra, Sayan
Issue Date
2015-02
Keyword(s)
  • Formal verification
  • Hybrid systems
  • Reachability
  • Algorithms
Date of Ingest
  • 2016-07-07T15:47:56Z
  • 2017-07-14T23:14:42Z
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 functions,” which are crucial for computing reachtubes from simulations. In this report, we eliminate that requirement by presenting an algorithm for computing piece-wise 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.
Publisher
Coordinated Science Laboratory, University of Illinois at Urbana-Champaign
Series/Report Name or Number
Coordinated Science Laboratory Report no. UILU-ENG-15-2201
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/90444
Sponsor(s)/Grant Number(s)
National Science Foundation (CAR 1054247 and NSF CSR 1016791); Air Force Office of Scientific Research (AFOSR YIP FA9550-12-1-0336)

Owning Collections

Report - Coordinated Science Laboratory PRIMARY