2022/09/19 by Prithvi Akella, Akella, Prithvi, Wyatt Ubellacker +3 · 1 citation
Computer Science · Engineering · #Embedded Systems Design Techniques #FOS: Electrical engineering #Formal Methods in Verification #Real-time simulation and control systems #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2209.09337
openalex publication_date 2022/09/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.