@inproceedings{HuangMitra:HSCC2014,
author = {Huang, Zhenqi and Mitra, Sayan},
title = {Proofs from simulations and modular annotations},
year = {2014},
isbn = {9781450327329},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2562059.2562126},
doi = {10.1145/2562059.2562126},
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 deterministic dynamical system M(δ). For any two trajectories of A starting δ distance apart, we show that one of them bloated by a factor determined by the trajectory of M contains the other. Further, by choosing appropriately small δ's the overapproximations computed by the above method can be made arbitrarily precise. Using the above results we develop a sound and relatively complete algorithm for bounded safety verification of nonlinear ODEs. Our preliminary experiments with a prototype implementation of the algorithm show that the approach can be effective for verification of nonlinear models.},
booktitle = {Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control},
pages = {183–192},
numpages = {10},
keywords = {compositional verification, dynamical systems, input-to-state stability, simulation-based verification},
location = {Berlin, Germany},
series = {HSCC '14}
}