Formal Verification of Stochastic Systems with ReLU Neural Network Controllers

• URL: http://arxiv.org/abs/2103.05142v1
• Date: Mon, 8 Mar 2021 23:53:13 GMT
• Title: Formal Verification of Stochastic Systems with ReLU Neural Network Controllers
• Authors: Shiqi Sun, Yan Zhang, Xusheng Luo, Panagiotis Vlantis, Miroslav Pajic and Michael M. Zavlanos
• Abstract summary: We address the problem of formal safety verification for cyber-physical systems 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.
• Score: 22.68044012584378
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Sub-linear Regret in Adaptive Model Predictive Control [56.705978425244496]
  We present STT-MPC (Self-Tuning Tube-based Model Predictive Control), an online oracle that combines the certainty-equivalence principle and polytopic tubes. We analyze the regret of the algorithm, when compared to an algorithm initially aware of the system dynamics.
  arXiv  Detail & Related papers  (2023-10-07T15:07:10Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Risk Verification of Stochastic Systems with Neural Network Controllers [0.0]
  We present a data-driven framework for verifying the risk of dynamical systems with neural network (NN) controllers. Given a control system, an NN controller, and a specification equipped with a notion of trace robustness, we collect trajectories from the system. We compute risk metrics over these robustness values to estimate the risk that the NN controller will not satisfy the specification.
  arXiv  Detail & Related papers  (2022-08-26T20:09:55Z)
• Large-Scale Sequential Learning for Recommender and Engineering Systems [91.3755431537592]
  In this thesis, we focus on the design of an automatic algorithms that provide personalized ranking by adapting to the current conditions. For the former, we propose novel algorithm called SAROS that take into account both kinds of feedback for learning over the sequence of interactions. The proposed idea of taking into account the neighbour lines shows statistically significant results in comparison with the initial approach for faults detection in power grid.
  arXiv  Detail & Related papers  (2022-05-13T21:09:41Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• Correct-by-construction reach-avoid control of partially observable linear stochastic systems [7.912008109232803]
  We formalize a robust feedback controller for reach-avoid control of discrete-time, linear time-invariant systems. The problem is to compute a controller that satisfies the required provestate abstraction problem.
  arXiv  Detail & Related papers  (2021-03-03T13:46:52Z)
• Gaussian Process-based Min-norm Stabilizing Controller for Control-Affine Systems with Uncertain Input Effects and Dynamics [90.81186513537777]
  We propose a novel compound kernel that captures the control-affine nature of the problem. We show that this resulting optimization problem is convex, and we call it Gaussian Process-based Control Lyapunov Function Second-Order Cone Program (GP-CLF-SOCP)
  arXiv  Detail & Related papers  (2020-11-14T01:27:32Z)
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming [19.51345816555571]
  We propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.
  arXiv  Detail & Related papers  (2020-04-16T18:48:25Z)
• Closed-loop Parameter Identification of Linear Dynamical Systems through the Lens of Feedback Channel Coding Theory [0.0]
  This paper considers the problem of closed-loop identification of linear scalar systems with Gaussian process noise. We show that the learning rate is fundamentally upper bounded by the capacity of the corresponding AWGN channel. Although the optimal design of the feedback policy remains challenging, we derive conditions under which the upper bound is achieved.
  arXiv  Detail & Related papers  (2020-03-27T17:30:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.