Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
This paper studies finite-time safety and reach-avoid verification for stochastic discrete-time dynamical systems. The aim is to ascertain lower and upper bounds of the probability that, within a predefined finite-time horizon, a system starting from an initial state in a safe set will either exit the safe set (safety verification) or reach a target set while remaining within the safe set until the first encounter with the target (reach-avoid verification). We introduce novel barrier-like sufficient conditions for characterizing these bounds, which either complement existing ones or fill gaps. Finally, we demonstrate the efficacy of these conditions on two examples.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
In this paper, we examine necessary and sufficient barrier-like conditions for infinite-horizon safety verification and reach-avoid verification of stochastic discrete-time systems, derived through a relaxation of Bellma…
Reach-avoid Verification using Lyapunov Densities
Reach-avoid analysis combines the construction of safety and specific progress guarantees, and is able to formalize many important engineering problems. In this paper we study the reach-avoid verification problem of syst…
A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems
Ensuring safety through set invariance has proven to be a valuable method in various robotics and control applications. This paper introduces a comprehensive framework for the safe probabilistic invariance verification o…
Learning Predictive Safety Filter via Decomposition of Robust Invariant Set
Ensuring safety of nonlinear systems under model uncertainty and external disturbances is crucial, especially for real-world control tasks. Predictive methods such as robust model predictive control (RMPC) require solvin…
Model Predictive ControlReinforcement Learning (RL)Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees
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 sa…