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.

主权项

1. A system comprising:
a processing device; non-transitory, computer-readable medium storing a set of initial states and a set of unsafe states of a non-linear model of a control system that is to interact with a physical system, and further storing the non-linear model and instructions; wherein the processing device is to execute the instructions to compute a piece-wise, exponential discrepancy function of the non-linear model comprising to:
(i) perform a simulation of the non-linear model using a set of sampled states from the set of initial states, to generate a plurality of trajectories over bounded time, wherein a trajectory is a set of numerical approximations of behaviors of the physical system;(ii) determine, for respective pairs of neighboring trajectories from the plurality of trajectories:
(a) an over-approximation of reachable states of the physical system as an upper bound of a distance between a pair of neighboring trajectories, wherein the distance approaches zero (“0”) as initial states of the pair of neighboring trajectories approach each other;(b) a linear over-approximation of the reachable states as piece-wise linear segments over a plurality of time intervals; and(c) 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.