Unbounded-time safety verification of stochastic differential dynamics

DOI10.1007/978-3-030-53291-8_18MaRDI QIDQ2226745zbMATH OpenOpenAlexFDO

Authors Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan

Publication date 9 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2006.01858

zbMATH Keywords

barrier certificatesfailure probability boundstochastic differential equations (SDEs)unbounded safety verification

Mathematics Subject Classification ID

Stochastic ordinary differential equations (aspects of stochastic analysis) (60H10) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety specification over the infinite time horizon. SDEs are mathematical models of stochastic processes that capture how states evolve continuously in time. They are widely used in numerous applications such as engineered systems (e.g., modeling how pedestrians move in an intersection), computational finance (e.g., modeling stock option prices), and ecological processes (e.g., population change over time). Previously the safety verification problem has been tackled over finite and infinite time horizons using a diverse set of approaches. The approach in this paper attempts to connect the two views by first identifying a finite time bound, beyond which the probability of a safety violation can be bounded by a negligibly small number. This is achieved by discovering an exponential barrier certificate that proves exponentially converging bounds on the probability of safety violations over time. Once the finite time interval is found, a finite-time verification approach is used to bound the probability of violation over this interval. We demonstrate our approach over a collection of interesting examples from the literature, wherein our approach can be used to find tight bounds on the violation probability of safety properties over the infinite time horizon.

Recommendations

• Safety verification of piecewise-deterministic Markov processes
• A barrier function approach to finite-time stochastic system verification and control
• Temporal logic verification of stochastic systems using barrier certificates
• Safety verification for probabilistic hybrid systems
• Safety of stochastic systems: an analytic and computational approach

Cited in

(6)

• Automatic verification of stability and safety for delay differential equations
• Safety verification of piecewise-deterministic Markov processes
• Safety criteria for aperiodically forced systems
• Safety verification for regime-switching jump diffusions via barrier certificates
• Verified propagation of imprecise probabilities in non-linear ODEs
• A new framework for bounding reachability probabilities of continuous-time stochastic systems

This page was built for publication: Unbounded-time safety verification of stochastic differential dynamics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226745)