Reachability Verification for Stochastic Discrete-time Dynamical Systems
In this paper we study reachability verification problems of stochastic discrete-time dynamical systems over the infinite time horizon. The reachability verification of interest in this paper is to certify specified lower and upper bounds of the reachability probability, with which the system starting from a designated initial set will enter a desired target set eventually. Existing sufficient conditions for reachability verification over the infinite time horizon are established based on the Doob's non-supermartingle inequality, which are often restrictive. Recently, a set of equations was proposed in [18], to which the solution is able to characterize the exact reachability probability. Inspired by this result, we in this paper propose sufficient conditions for reachability verification based on relaxing this equation. These sufficient conditions are shown to be weaker than the state-of-the-art ones, consequently being capable of providing more opportunities for verifying the reachability property successfully.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Neural Continuous-Time Supermartingale Certificates
We introduce for the first time a neural-certificate framework for continuous-time stochastic dynamical systems. Autonomous learning systems in the physical world demand continuous-time reasoning, yet existing learnable …
Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference
We consider data-driven reachability analysis of discrete-time stochastic dynamical systems using conformal inference. We assume that we are not provided with a symbolic representation of the stochastic system, but inste…
Probabilistic Reachability of Discrete-Time Nonlinear Stochastic Systems
In this paper we study the reachability problem for discrete-time nonlinear stochastic systems. Our goal is to present a unified framework for calculating the probabilistic reachable set of discrete-time systems in the p…
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…
Time-to-reach Bounds for Verification of Dynamical Systems Using the Koopman Spectrum
In this work, we present a novel Koopman spectrum-based reachability verification method for nonlinear systems. Contrary to conventional methods that focus on characterizing all potential states of a dynamical system ove…