Conservative Safety Monitors of Stochastic Dynamical Systems

TL;DR

This paper introduces a method that uses design-time probabilistic model checking results combined with runtime state estimates to produce scalable, formal safety estimates for autonomous systems, ensuring safety with well-calibrated probabilities.

Contribution

It presents a novel approach that leverages precomputed model checking results at runtime to estimate safety probabilities in stochastic dynamical systems.

Findings

Method produces well-calibrated safety probabilities

Approach is scalable for real-time safety estimation

Validated on simulated water tank systems

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.