Risk Verification of Stochastic Systems with Neural Network Controllers
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 (violated). We then compute risk metrics over these robustness values to estimate the risk that the NN controller will not satisfy the specification. We are further interested in quantifying the difference in risk between two systems, and we show how the risk estimated from a nominal system can provide an upper bound the risk of a perturbed version of the system. In particular, the tightness of this bound depends on the closeness of the systems in terms of the closeness of their system trajectories. For Lipschitz continuous and incrementally input-to-state stable systems, we show how to exactly quantify system closeness with varying degrees of conservatism, while we estimate system closeness for more general systems from data in our experiments. We demonstrate our risk verification approach on two case studies, an underwater vehicle and an F1/10 autonomous car.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Risk of Stochastic Systems for Temporal Logic Specifications
The wide availability of data coupled with the computational advances in artificial intelligence and machine learning promise to enable many future technologies such as autonomous driving. While there has been a variety …
Autonomous DrivingScalable Synthesis of Verified Controllers in Deep Reinforcement Learning
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 pol…
Deep Reinforcement Learningreinforcement-learningReinforcement LearningReinforcement Learning (RL)Formal Verification of Stochastic Systems with ReLU Neural Network Controllers
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,…
Robot NavigationRisk-sensitive Affine Control Synthesis for Stationary LTI Systems
To address deviations from expected performance in stochastic systems, we propose a risk-sensitive control synthesis method to minimize certain risk measures over the limiting stationary distribution. Specifically, we ex…
Risk-Aware Stability of Discrete-Time Systems
We develop a generalized stability framework for stochastic discrete-time systems, where the generality pertains to the ways in which the distribution of the state energy can be characterized. We use tools from finance a…