Bounded verification through discrepancy computations

Sayan Mitra (Inventor), Chuchu Fan (Inventor), Zhenqi Huang (Inventor)

Research output: Patent

Abstract

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.
Original languageEnglish (US)
U.S. patent number10061876
StatePublished - Aug 28 2018

Fingerprint

Dive into the research topics of 'Bounded verification through discrepancy computations'. Together they form a unique fingerprint.

Cite this