Proofs from Simulations and Modular Annotations

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 (d). For any two trajectories of A starting d 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 d'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 effective for verification of nonlinear models.