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. Using this abstraction, we propose a method to compute tight bounds on the safety probabilities of nodes in this graph, despite possible over-approximations of the transition probabilities between these nodes. Additionally, using the proposed SMC formula, we devise a heuristic method to refine the abstraction of the system in order to further improve the estimated safety bounds. Finally, we corroborate the efficacy of the proposed method with simulation results considering a robot navigation example and comparison against a state-of-the-art verification scheme.
In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture that is sufficient to implement the optimal Model Predictive Control (MPC) strategy for an LTI system with quadratic cost. Specifically, we propose AReN, an algorithm to generate Assured ReLU Architectures. AReN takes as input an LTI system with quadratic cost specification, and outputs a ReLU NN architecture with the assurance that there exist network weights that exactly implement the associated MPC controller. AReN thus offers new insight into the design of ReLU …
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…
University of Pennsylvania（宾夕法尼亚大学）；Johns Hopkins University（约翰斯·霍普金斯大学）
Complementarity problems, a class of mathematical optimization problems with orthogonality constraints, are widely used in many robotics tasks, such as locomotion and manipulation, due to their ability to model non-smooth phenomena (e.g., contact dynamics). In this paper, we propose a method to analyze the stability of complementarity systems with neural network controllers. First, we introduce a method to represent neural networks with rectified linear unit (ReLU) activations as the solution to a linear complementarity problem. Then, we show that systems with ReLU network controllers have an …
In this paper, we consider the computational complexity of bounding the reachable set of a Linear Time-Invariant (LTI) system controlled by a Rectified Linear Unit (ReLU) Two-Level Lattice (TLL) Neural Network (NN) controller. In particular, we show that for such a system and controller, it is possible to compute the exact one-step reachable set in polynomial time in the size of the TLL NN controller (number of neurons). Additionally, we show that a tight bounding box of the reachable set is computable via two polynomial-time methods: one with polynomial complexity in the size of the TLL and t…
In this paper, we propose a formal controller synthesis approach for integrating a population of plug-in electric vehicles in frequency regulation of power systems. This approach is the first application of formal methods to the smart grids in particular to the frequency regulation of power systems. We design and simulate a novel symbolic controller for the Great Britain power system. The proposed controller enhances the frequency response behaviour of the system when encountered with a large outage event. The symbolic controller guarantees the settlement of the after-event's frequency in the …
Equivalent and Compact Representations of Neural Network Controllers With Decision Trees
Ming Hsieh Department of Electrical and Computer Engineering, University of Southern California（明希德电气与计算机工程学院）；Department of Electrical and Computer Engineering, University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校电气与计算机工程学院）；Department of Electrical Engineering, State University of New York at Albany（纽约州立大学阿尔巴尼分校电气工程学院）
This paper proposes a framework for automatic formal controller synthesis for general hybrid systems with a subset of safety and reachability specifications. The framework uses genetic programming to automatically co-synthesize controllers and candidate Lyapunov-like functions. These candidate Lyapunov-like functions are used to formally verify the control specification, and their correctness is proven using a Satisfiability Modulo Theories solver. The advantages of this approach are: no restriction is made to polynomial systems, the synthesized controllers are expressed as compact expressions…
In this paper, we consider the problem of training neural network (NN) controllers for nonlinear dynamical systems that are guaranteed to satisfy safety and liveness (e.g., reach-avoid) properties. Our approach is to combine model-based design methodologies for dynamical systems with data-driven approaches to achieve this target. We confine our attention to NNs with Rectifier Linear Unit (ReLU) nonlinearity which are known to represent Continuous Piece-Wise Affine (CPWA) functions. Given a mathematical model of the dynamical system, we compute a finite-state abstract model that captures the cl…
In this paper, we consider the problem of repairing a data-trained Rectified Linear Unit (ReLU) Neural Network (NN) controller for a discrete-time, input-affine system. That is we assume that such a NN controller is available, and we seek to repair unsafe closed-loop behavior at one known "counterexample" state while simultaneously preserving a notion of safe closed-loop behavior on a separate, verified set of states. To this end, we further assume that the NN controller has a Two-Level Lattice (TLL) architecture, and exhibit an algorithm that can systematically and efficiently repair such an …
We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the spe…
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…
Radboud University（拉德堡德大学）；University of Oxford（牛津大学）
Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers. Stochastic noise causes aleatoric uncertainty, whereas imprecise knowledge of model parameters leads to epistemic uncertainty. Several approaches use formal abstractions to synthesize policies that satisfy temporal specifications related to safety and reachability. However, the underlying models exclusively capture aleatoric but not epistemic uncertainty, and thus require that model parameters are known precisely. Our contribution to overcoming this restriction is a novel abstraction-based co…
The airworthiness and safety of a non-pedigreed autopilot must be verified, but the cost to formally do so can be prohibitive. We can bypass formal verification of non-pedigreed components by incorporating Runtime Safety Assurance (RTSA) as mechanism to ensure safety. RTSA consists of a meta-controller that observes the inputs and outputs of a non-pedigreed component and verifies formally specified behavior as the system operates. When the system is triggered, a verified recovery controller is deployed. Recovery controllers are designed to be safe but very likely disruptive to the operational …
Learning-based controllers, such as neural network (NN) controllers, can show high empirical performance but lack formal safety guarantees. To address this issue, control barrier functions (CBFs) have been applied as a safety filter to monitor and modify the outputs of learning-based controllers in order to guarantee the safety of the closed-loop system. However, such modification can be myopic with unpredictable long-term effects. In this work, we propose a safe-by-construction NN controller which employs differentiable CBF-based safety layers, and investigate the performance of safe-by-const…
Runtime energy management has become quintessential for multi-sensor autonomous systems at the edge for achieving high performance given the platform constraints. Typical for such systems, however, is to have their controllers designed with formal guarantees on safety that precede in priority such optimizations, which in turn limits their application in real settings. In this paper, we propose a novel energy optimization framework that is aware of the autonomous system's safety state, and leverages it to regulate the application of energy optimization methods so that the system's formal safety…
In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture (number of layers and number of neurons per layer) with the assurance that it is sufficiently parametrized to control a nonlinear system; i.e. control the system to satisfy a given formal specification. This is unlike current techniques, which provide no assurances on the resultant architecture. Moreover, our approach requires only limited knowledge of the underlying nonlinear system and specification. We assume only that the specification can be satisfied by a Lips…
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…
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…
Ludwig Maximilian University of Munich（慕尼黑大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）；Newcastle University（纽卡斯尔大学）
A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This scheme enables one to apply model-free, off-the-shelf reinforcement learning algorithms for finite MDPs to compute optimal strategies for the corresponding continuous-space MDPs without explicitly constructing the finite-state abstraction. The proposed approach is based on abstracting the system with a finite MDP (without constructing it explicitly) with unknown transition probabilities, synthesizing strategies over the abstract MDP, and then mapping the results …
We introduce a novel learning-based approach to synthesize safe and robust controllers for autonomous Cyber-Physical Systems and, at the same time, to generate challenging tests. This procedure combines formal methods for model verification with Generative Adversarial Networks. The method learns two Neural Networks: the first one aims at generating troubling scenarios for the controller, while the second one aims at enforcing the safety constraints. We test the proposed method on a variety of case studies.
In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture (number of layers and number of neurons per layer) with the guarantee that it is sufficiently parametrized to control a nonlinear system. Whereas current state-of-the-art techniques are based on hand-picked architectures or heuristic based search to find such NN architectures, our approach exploits the given model of the system to design an architecture; as a result, we provide a guarantee that the resulting NN architecture is sufficient to implement a controller th…
To mitigate the high energy demand of Neural Network (NN) based Autonomous Driving Systems (ADSs), we consider the problem of offloading NN controllers from the ADS to nearby edge-computing infrastructure, but in such a way that formal vehicle safety properties are guaranteed. In particular, we propose the EnergyShield framework, which repurposes a controller ''shield'' as a low-power runtime safety monitor for the ADS vehicle. Specifically, the shield in EnergyShield provides not only safety interventions but also a formal, state-based quantification of the tolerable edge response time before…
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Stanford University（斯坦福大学）；The Hebrew University of Jerusalem（耶路撒冷希伯来大学）；IT University of Copenhagen（哥本哈根信息技术大学）；Google（谷歌公司）；GE Aerospace Research（GE航空航天研究院）
Vanderbilt University（范德堡大学）；University of Pennsylvania（宾夕法尼亚大学）
This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. F…
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…
In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stochastic games. Concretely, we leverage abstraction-based approaches to construct a supervisor that checks and decides whether or not to accept the inputs provided by the unverified controller, and a safety advisor that provides fallback control inputs to ensure safety whenever the unverified controller is rejected. Moreover, by leveraging an ($ε,δ$)-approximate probabilistic rela…
Systematic design and verification of advanced control strategies for complex systems under uncertainty largely remains an open problem. Despite the promise of blackbox optimization methods for automated controller tuning, they generally lack formal guarantees on the solution quality, which is especially important in the control of safety-critical systems. This paper focuses on obtaining closed-loop performance guarantees for automated controller tuning, which can be formulated as a black-box optimization problem under uncertainty. We use recent advances in non-convex scenario theory to provid…
Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems
Sharif University of Technology（谢里夫理工大学）；Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所（ISTA））；Massachusetts Institute of Technology（麻省理工学院）
The decision logic for the ACAS X family of aircraft collision avoidance systems is represented as a large numeric table. Due to storage constraints of certified avionics hardware, neural networks have been suggested as a way to significantly compress the data while still preserving performance in terms of safety. However, neural networks are complex continuous functions with outputs that are difficult to predict. Because simulations evaluate only a finite number of encounters, simulations are not sufficient to guarantee that the neural network will perform correctly in all possible situations…
