A Barrier-Based Scenario Approach to Verifying Safety-Critical Systems
Prithvi Akella, Aaron D. Ames
Abstract
We detail an approach to safety-critical verification using barrier functions. Our method requires limited system data to verify a system's ability to keep positive a candidate barrier function <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$h$</tex-math></inline-formula> at discrete-time intervals over its trajectories. Specifically, our method first randomly samples initial conditions and parameters for a controlled, continuous-time system and records the state trajectory at discrete intervals. Then, we evaluate these states under a candidate barrier function <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$h$</tex-math></inline-formula> to determine the constraints for a randomized linear program. The solution to this program provides either a probabilistic verification statement in the aforementioned vein or a counterexample - an instance where the system went unsafe. To showcase our results, we verify the robotarium simulator, identify counterexamples for its hardware counterpart, and experimentally verify the safety of a multi-agent quadrupedal system.