Conservative Safety Monitors of Stochastic Dynamical Systems

2023/01/26 by Matthew Cleaveland, Cleaveland, Matthew, Oleg Sokolsky +5 · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Software Reliability and Analysis Research #Software Testing and Debugging Techniques

paper · pdf · doi:10.48550/arxiv.2301.11330

openalex publication_date 2023/01/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01

Abstract

Generating accurate runtime safety estimates for autonomous systems is vital to ensuring their continued proliferation. However, exhaustive reasoning about future behaviors is generally too complex to do at runtime. To provide scalable and formal safety estimates, we propose a method for leveraging design-time model checking results at runtime. Specifically, we model the system as a probabilistic automaton (PA) and compute bounded-time reachability probabilities over the states of the PA at design time. At runtime, we combine distributions of state estimates with the model checking results to produce a bounded time safety estimate. We argue that our approach produces well-calibrated safety probabilities, assuming the estimated state distributions are well-calibrated. We evaluate our approach on simulated water tanks.

Cited by

• Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy
• How Safe Will I Be Given What I Saw? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy

Related

• Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis
• Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions
• Runtime Monitoring for Markov Decision Processes
• A Barrier-Based Scenario Approach to Verify Safety-Critical Systems
• Probabilistic Guarantees for Safe Deep Reinforcement Learning