Proofs from simulations and modular annotations

Zhenqi Huang, Sayan Mitra

Research output: Contribution to conferencePaper

Abstract

We present a modular technique for simulation-based bounded verification for nonlinear dynamical systems. We introduce the notion of input-to-state discrepancy of each subsystem Ai in a larger nonlinear dynamical system A which bounds the distance between two (possibly diverging) trajectories of Ai in terms of their initial states and inputs. Using the IS discrepancy functions, we construct a low dimensional deter- ministic dynamical system M(fi). For any two trajectories of A starting fi distance apart, we show that one of them bloated by a factor determined by the trajectory of M con- tains the other. Further, by choosing appropriately small fi's the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we de- velop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary ex- periments with a prototype implementation of the algorithm show that the approach can be efiective for verification of nonlinear models. Copyright is held by the owner/author(s).

Original languageEnglish (US)
Pages183-192
Number of pages10
DOIs
StatePublished - Jan 1 2014
Event17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, Part of the 7th Cyber Physical Systems, CPS Week 2014 - Berlin, Germany
Duration: Apr 15 2014Apr 17 2014

Other

Other17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, Part of the 7th Cyber Physical Systems, CPS Week 2014
CountryGermany
CityBerlin
Period4/15/144/17/14

Keywords

  • Compositional verification
  • Dynamical systems
  • Input-to-state stability
  • Simulation-based verification

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Control and Systems Engineering

Fingerprint Dive into the research topics of 'Proofs from simulations and modular annotations'. Together they form a unique fingerprint.

  • Cite this

    Huang, Z., & Mitra, S. (2014). Proofs from simulations and modular annotations. 183-192. Paper presented at 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, Part of the 7th Cyber Physical Systems, CPS Week 2014, Berlin, Germany. https://doi.org/10.1145/2562059.2562126