BOUNDED VERIFICATION THROUGH DISCREPANCY COMPUTATIONS

A system and methods store initial states and unsafe states (e.g., safety requirements) of a non-linear model of a control system that interacts with a physical system. The system performs simulations of the non-linear model using a set of sampled initial states, to first generate trajectories (numerical approximations of actual behaviors) over bounded time. The system further determines, for respective pairs of neighboring trajectories: an over-approximation of reachable states as an upper bound of a distance between a pair of neighboring trajectories; a linear over-approximation of the reachable states as piece-wise linear segments over a plurality of time intervals; and whether the linear over-approximation overlaps in any of the piece-wise linear segments with the unsafe states, to verify the non-linear model of the control system is safe.