Safety-Critical Controller Verification via Sim2Real Gap Quantification

TL;DR

This paper introduces a method to quantify the sim2real gap in models, enabling the synthesis and verification of controllers with high safety guarantees on hardware, reducing the need for extensive real-world testing.

Contribution

The authors develop a probabilistic approach to identify the sim2real gap and incorporate it into uncertain models for safe controller synthesis and verification.

Findings

Successfully applied on Robotarium and quadruped platforms.

Achieves high-probability safety guarantees without extensive hardware testing.

Provides a systematic way to quantify model inaccuracy for control verification.

Abstract

The well-known quote from George Box states that: "All models are wrong, but some are useful." To develop more useful models, we quantify the inaccuracy with which a given model represents a system of interest, so that we may leverage this quantity to facilitate controller synthesis and verification. Specifically, we develop a procedure that identifies a sim2real gap that holds with a minimum probability. Augmenting the nominal model with our identified sim2real gap produces an uncertain model which we prove is an accurate representor of system behavior. We leverage this uncertain model to synthesize and verify a controller in simulation using a probabilistic verification approach. This pipeline produces controllers with an arbitrarily high probability of realizing desired safe behavior on system hardware without requiring hardware testing except for those required for sim2real gap identification. We also showcase our procedure working on two hardware platforms - the Robotarium and a quadruped.