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