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 language | English (US) |
|---|---|
| Pages | 183-192 |
| Number of pages | 10 |
| DOIs | |
| State | Published - Jan 1 2014 |
| Event | 17th 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 2014 → Apr 17 2014 |
Other
| Other | 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, Part of the 7th Cyber Physical Systems, CPS Week 2014 |
|---|---|
| Country | Germany |
| City | Berlin |
| Period | 4/15/14 → 4/17/14 |
Fingerprint
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
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 conference › Paper
}
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 -