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.
School of Aeronautics and Astronautics（航空航天学院）；Purdue University（普渡大学）
Model-based reinforcement learning (RL) has emerged as a promising tool for developing controllers for real world systems (e.g., robotics, autonomous driving, etc.). However, real systems often have constraints imposed on their state space which must be satisfied to ensure the safety of the system and its environment. Developing a verification tool for RL algorithms is challenging because the non-linear structure of neural networks impedes analytical verification of such models or controllers. To this end, we present a novel safety verification framework for model-based RL controllers using re…
For the implementations of controllers on digital processors, certain limitations, e.g. in the instruction set and register length, need to be taken into account, especially for safety-critical applications. This work aims to provide a computer-certified inductive definition for the control functions that are implemented on such processors accompanied with the fixed-point data type in a proof assistant. Using these inductive definitions we formally ensure correct realization of the controllers on a digital processor. Our results guarantee overflow-free computations of the implemented control a…
Obtaining prescribed accuracy bounds in super-twisting sliding mode control loops often falls short in terms of the applicability of the controller in high-performance systems. This is due to the fact that the selection of the controller gains that are derived from the conditions for finite-time convergence may be too restrictive in connection to actuator limitations and induced chatter. Previous work has shown that in case of periodic perturbations, there can be a systematic selection of much lower controller gains that guarantees boundedness of the closed-loop solutions within predetermined …
In this paper we consider the safety verification and safe controller synthesis problems for nonlinear control systems. The Control Barrier Certificates (CBC) approach is proposed as an extension to the Barrier certificates approach. Our approach can be used to characterize the control invariance of a given set in terms of safety of a general nonlinear control system subject to input constraints. From the point of view of controller design, the proposed method provides an approach to synthesize a safe control law that guarantees that the trajectories of the system starting from a given initial…
There has been significant recent interest in devising verification techniques for learning-enabled controllers (LECs) that manage safety-critical systems. Given the opacity and lack of interpretability of the neural policies that govern the behavior of such controllers, many existing approaches enforce safety properties through shield, a dynamic monitoring-and-repairing mechanism that ensures a LEC does not emit actions that would violate desired safety conditions. These methods, however, have been shown to have significant scalability limitations because verification costs grow as problem di…
In this work, we address the problem of formal safety verification for stochastic cyber-physical systems (CPS) equipped with ReLU neural network (NN) controllers. Our goal is to find the set of initial states from where, with a predetermined confidence, the system will not reach an unsafe configuration within a specified time horizon. Specifically, we consider discrete-time LTI systems with Gaussian noise, which we abstract by a suitable graph. Then, we formulate a Satisfiability Modulo Convex (SMC) problem to estimate upper bounds on the transition probabilities between nodes in the graph. Us…
In the current control design of safety-critical autonomous systems, formal verification techniques are typically applied after the controller is designed to evaluate whether the required properties (e.g., safety) are satisfied. However, due to the increasing system complexity and the fundamental hardness of designing a controller with formal guarantees, such an open-loop process of design-then-verify often results in many iterations and fails to provide the necessary guarantees. In this paper, we propose a correct-by-construction control learning framework that integrates the verification int…
University of Pennsylvania（宾夕法尼亚大学）；Rensselaer Polytechnic Institute（伦斯勒理工学院）
Motivated by the fragility of neural network (NN) controllers in safety-critical applications, we present a data-driven framework for verifying the risk of stochastic dynamical systems with NN controllers. Given a stochastic control system, an NN controller, and a specification equipped with a notion of trace robustness (e.g., constraint functions or signal temporal logic), we collect trajectories from the system that may or may not satisfy the specification. In particular, each of the trajectories produces a robustness value that indicates how well (severely) the specification is satisfied (v…
This paper describes a verification case study on an autonomous racing car with a neural network (NN) controller. Although several verification approaches have been proposed over the last year, they have only been evaluated on low-dimensional systems or systems with constrained environments. To explore the limits of existing approaches, we present a challenging benchmark in which the NN takes raw LiDAR measurements as input and outputs steering for the car. We train a dozen NNs using two reinforcement learning algorithms and show that the state of the art in verification can handle systems wit…
Northwestern University（西北大学）；UC Berkeley（加州大学伯克利分校）；University of Liverpool（利物浦大学）；Yale University（耶鲁大学）
In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties (e.g., safety, stability) under the learned controller. However, as existing methods typically apply formal verification \emph{after} the controller has been learned, it is sometimes difficult to obtain any certificate, even after many iterations between learning and verification. To address this challenge, we propose a framework that jointly conducts reinforcement learning and formal verification by formulating and solving a novel bilevel optimization problem, which…
Princeton University（普林斯顿大学）；Google AI Princeton（谷歌人工智能普林斯顿分部）
We consider the problem of generating maximally adversarial disturbances for a given controller assuming only blackbox access to it. We propose an online learning approach to this problem that \emph{adaptively} generates disturbances based on control inputs chosen by the controller. The goal of the disturbance generator is to minimize \emph{regret} versus a benchmark disturbance-generating policy class, i.e., to maximize the cost incurred by the controller as well as possible compared to the best possible disturbance generator \emph{in hindsight} (chosen from a benchmark policy class). In the …
University of Southern California（南加州大学）；Toyota Research Institute North America（丰田北美研究院）
Signal Temporal Logic (STL) has become a popular tool for expressing formal requirements of Cyber-Physical Systems (CPS). The problem of verifying STL properties of neural network-controlled CPS remains a largely unexplored problem. In this paper, we present a model for the verification of Neural Network (NN) controllers for general STL specifications using a custom neural architecture where we map an STL formula into a feed-forward neural network with ReLU activation. In the case where both our plant model and the controller are ReLU-activated neural networks, we reduce the STL verification p…
Bounded Model Checking of State-Space Digital Systems: The Impact of Finite Word-Length Effects on the Implementation of Fixed-Point Digital Controllers Based on State-Space Modeling
Control Lyapunov functions (CLFs) and control barrier functions (CBFs) are widely used tools for synthesizing controllers subject to stability and safety constraints. Paired with online optimization, they provide stabilizing control actions that satisfy input constraints and avoid unsafe regions of state-space. Designing CLFs and CBFs with rigorous performance guarantees is computationally challenging. To certify existence of control actions, current techniques not only design a CLF/CBF, but also a nominal controller. This can make the synthesis task more expensive, and performance estimation …
University of Oxford（牛津大学）；Paderborn University（帕德博恩大学）
Hamilton-Jacobi reachability methods for safety-critical control have been well studied, but the safety guarantees derived rely on the accuracy of the numerical computation. Thus, it is crucial to understand and account for any inaccuracies that occur due to uncertainty in the underlying dynamics and environment as well as the induced numerical errors. To this end, we propose a framework for modeling the error of the value function inherent in Hamilton-Jacobi reachability using a Gaussian process. The derived safety controller can be used in conjuncture with arbitrary controllers to provide a …
Neural networks have become state-of-the-art for computer vision problems because of their ability to efficiently model complex functions from large amounts of data. While neural networks can be shown to perform well empirically for a variety of tasks, their performance is difficult to guarantee. Neural network verification tools have been developed that can certify robustness with respect to a given input image; however, for neural network systems used in closed-loop controllers, robustness with respect to individual images does not address multi-step properties of the neural network controll…
In this paper, we consider the problem of formally verifying a Neural Network (NN) based autonomous landing system. In such a system, a NN controller processes images from a camera to guide the aircraft while approaching the runway. A central challenge for the safety and liveness verification of vision-based closed-loop systems is the lack of mathematical models that captures the relation between the system states (e.g., position of the aircraft) and the images processed by the vision-based NN controller. Another challenge is the limited abilities of state-of-the-art NN model checkers. Such mo…
Run Time Assurance (RTA) Systems are online verification mechanisms that filter an unverified primary controller output to ensure system safety. The primary control may come from a human operator, an advanced control approach, or an autonomous control approach that cannot be verified to the same level as simpler control systems designs. The critical feature of RTA systems is their ability to alter unsafe control inputs explicitly to assure safety. In many cases, RTA systems can functionally be described as containing a monitor that watches the state of the system and output of a primary contro…
Safe and Reliable Training of Learning-Based Aerospace Controllers
Stanford University（斯坦福大学）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）；IT University of Copenhagen（哥本哈根 IT 大学）；Google（谷歌）；GE Aerospace Research（GE航空航天研究院）；Center for AI Safety（人工智能安全中心）；Air Force Research Laboratory（空军研究实验室）
Learning Surrogate LPV State-Space Models with Uncertainty Quantification
Eindhoven University of Technology（埃因霍温理工大学）；European Space Agency, ESTEC（欧洲航天局ESTEC）；HUN-REN Institute for Computer Science and Control（HUN-REN计算机科学与控制研究所）
With the growing interest in deploying robots in unstructured and uncertain environments, there has been increasing interest in factoring risk into safety-critical control development. Similarly, the authors believe risk should also be accounted in the verification of these controllers. In pursuit of sample-efficient methods for uncertain black-box verification then, we first detail a method to estimate the Value-at-Risk of arbitrary scalar random variables without requiring \textit{apriori} knowledge of its distribution. Then, we reformulate the uncertain verification problem as a Value-at-Ri…
In this paper, we consider the problem of verifying safety constraint satisfaction for single-input single-output systems with uncertain transfer function coefficients. We propose a new type of barrier function based on a vector norm. This type of barrier function has a measurable upper bound without full state availability. An identifier-based estimator allows an exact bound for the uncertainty-based component of the barrier function estimate. Assuming that the system is safe initially allows an exponentially decreasing bound on the error due to the estimator transient. Barrier function and e…
Southwest University（西南大学）；University of Surrey（萨里大学）；University of York（约克大学）
We provide a novel approach to synthesize controllers for nonlinear continuous dynamical systems with control against safety properties. The controllers are based on neural networks (NNs). To certify the safety property we utilize barrier functions, which are represented by NNs as well. We train the controller-NN and barrier-NN simultaneously, achieving a verification-in-the-loop synthesis. We provide a prototype tool nncontroller with a number of case studies. The experiment results confirm the feasibility and efficacy of our approach.
