A New Framework for Bounding Reachability Probabilities of Continuous-time Stochastic Systems
This manuscript presents an innovative framework for constructing barrier functions to bound reachability probabilities for continuous-time stochastic systems described by stochastic differential equations (SDEs). The reachability probabilities considered in this paper encompass two aspects: the probability of reaching a set of specified states within a predefined finite time horizon, and the probability of reaching a set of specified states at a particular time instant. The barrier functions presented in this manuscript are developed either by relaxing a parabolic partial differential equation that characterizes the exact reachability probability or by applying the Gr\"onwall's inequality. In comparison to the prevailing construction method, which relies on Doob's non-negative supermartingale inequality (or Ville's inequality), the proposed barrier functions provide stronger alternatives, complement existing methods, or fill gaps.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Reachability analysis in stochastic directed graphs by reinforcement learning
We characterize the reachability probabilities in stochastic directed graphs by means of reinforcement learning methods. In particular, we show that the dynamics of the transition probabilities in a stochastic digraph ca…
reinforcement-learningReinforcement LearningReinforcement Learning (RL)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 …
Polynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers
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) contr…
Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees
Probabilistic model checking for Markov decision processes (MDPs) provides quantitative guarantees, but often offers limited insight into why undesired outcomes occur. Probability-raising (PR) causality addresses this by…
GoTube: Scalable Stochastic Verification of Continuous-Depth Models
We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimiza…
global-optimization