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 - 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/Territory | Germany |
City | Berlin |
Period | 4/15/14 → 4/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