Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions
Shenghua Feng, Jie An, Fanjiang Xu
Abstract
Stochastic dynamical systems have emerged as fundamental models across numerous application domains, providing powerful mathematical representations for capturing uncertain system behavior. In this paper, we address the problem of runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations, i.e., estimating the probability that the system satisfies a given safety or reach-avoid specification. Unlike traditional approaches that rely solely on offline models, we propose a framework that incorporates real-time observations to dynamically refine probability estimates for safety and reach-avoid events. By introducing observation-aware barrier functions, our method adaptively updates probability bounds as new observations are collected, combining efficient offline computation with online backward iteration. This approach enables rigorous and responsive prediction of safety and reach-avoid probabilities under uncertainty. In addition to the theoretical guarantees, experimental results on benchmark systems demonstrate the practical effectiveness of the proposed method.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext a2d9b2e0-e9ef-4e64-8d90-6e531c00caf9Builds on6
- Optimistic Value IterationArnd Hartmanns, Benjamin Lucien KaminskiCAV 2020 · 62 citations
- Learning Control Policies for Stochastic Systems with Reach-Avoid GuaranteesDorde Zikelic, Mathias Lechner, Thomas A. Henzinger, Krishnendu ChatterjeeAAAI 2023 · 50 citations
- Stability Verification in Stochastic Control Systems via Neural Network SupermartingalesMathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, Thomas A. HenzingerAAAI 2022 · 45 citations
- Sound and Complete Proof Rules for Probabilistic TerminationRupak Majumdar, V. R. SathiyanarayanaPOPL 2025 · 16 citations
- Unbounded-Time Safety Verification of Stochastic Differential DynamicsShenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan et al.CAV 2020 · 11 citations
Related papers
- Runtime Monitors for Markov Decision ProcessesSebastian Junges, Hazem Torfah, Sanjit A. SeshiaCAV 2021 · 25 citations
- Safely Learning Controlled Stochastic DynamicsLuc Brogat-Motte, Alessandro Rudi, Riccardo BonalliNeurIPS 2025 · 2 citations
- Multi-Robot Collision Avoidance under Uncertainty with Probabilistic Safety Barrier CertificatesWenhao Luo, Wen Sun, Ashish KapoorNeurIPS 2020 · 102 citations
- Probabilistic Robustness Certificates against Adversarial AttacksSara Taheri, Majid ZamaniICML 2026
- Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier FunctionsRayan Mazouz, Karan Muvvala, Akash Ratheesh, Luca Laurenti et al.NeurIPS 2022 · 44 citations
