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.

翻译：为自主系统生成准确的运行时安全估计，对于确保其持续普及至关重要。然而，对系统未来行为进行穷举推理通常在运行时过于复杂。为了实现可扩展且形式化的安全估计，我们提出了一种在运行时利用设计时模型检测结果的方法。具体而言，我们将系统建模为概率自动机（PA），并在设计时计算PA状态上的有界时间可达概率。在运行时，我们将状态估计的分布与模型检测结果相结合，生成有界时间安全估计。我们论证：若估计的状态分布是良好校准的，则该方法可产生良好校准的安全概率。我们在模拟水箱系统上对该方法进行了评估。