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

Fingerprint

Nonlinear dynamical systems
Trajectories
Dynamical systems
Acoustic waves
Experiments

Keywords

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

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Control and Systems Engineering

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

Proofs from simulations and modular annotations. / Huang, Zhenqi; Mitra, Sayan.

2014. 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.

Research output: Contribution to conferencePaper

Huang, Z & Mitra, S 2014, 'Proofs from simulations and modular annotations' 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, 4/15/14 - 4/17/14, pp. 183-192. https://doi.org/10.1145/2562059.2562126
Huang Z, Mitra S. Proofs from simulations and modular annotations. 2014. 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
Huang, Zhenqi ; Mitra, Sayan. / Proofs from simulations and modular annotations. 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.10 p.
@conference{eeb420dbab1d480aa858f71fd2c7b8cd,
title = "Proofs from simulations and modular annotations",
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).",
keywords = "Compositional verification, Dynamical systems, Input-to-state stability, Simulation-based verification",
author = "Zhenqi Huang and Sayan Mitra",
year = "2014",
month = "1",
day = "1",
doi = "10.1145/2562059.2562126",
language = "English (US)",
pages = "183--192",
note = "17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, Part of the 7th Cyber Physical Systems, CPS Week 2014 ; Conference date: 15-04-2014 Through 17-04-2014",

}

TY - CONF

T1 - Proofs from simulations and modular annotations

AU - Huang, Zhenqi

AU - Mitra, Sayan

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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).

AB - 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).

KW - Compositional verification

KW - Dynamical systems

KW - Input-to-state stability

KW - Simulation-based verification

UR - http://www.scopus.com/inward/record.url?scp=84899765343&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84899765343&partnerID=8YFLogxK

U2 - 10.1145/2562059.2562126

DO - 10.1145/2562059.2562126

M3 - Paper

AN - SCOPUS:84899765343

SP - 183

EP - 192

ER -