A Barrier-Based Scenario Approach to Verify Safety-Critical Systems

TL;DR

This paper introduces a randomized, barrier-based scenario approach for verifying safety-critical systems that requires limited data and provides probabilistic safety guarantees, demonstrated on robotic and multi-agent systems.

Contribution

The paper presents a novel randomized verification method using barrier functions and linear programming, applicable across different system types with limited data.

Findings

Successfully verified the Robotarium simulator's safety.

Identified counterexamples in hardware implementations.

Validated probabilistic safety guarantees through numerical experiments.

Abstract

In this letter, we detail our randomized approach to safety-critical system verification. Our method requires limited system data to make a strong verification statement. Specifically, our method first randomly samples initial conditions and parameters for a controlled, continuous-time system and records the ensuing state trajectory at discrete intervals. Then, we evaluate these states under a candidate barrier function $h$ to determine the constraints for a randomized linear program. The solution to this program then provides either a probabilistic verification statement or a counterexample. To show the validity of our results, we verify the robotarium simulator and identify counterexamples for its hardware counterpart. We also provide numerical evidence to validate our verification statements in the same setting. Furthermore, we show that our method is system-independent by performing the same verification method on a quadrupedal system in a multi-agent setting as well.