Monotonic Safety for Scalable and Data-Efficient Probabilistic Safety Analysis

TL;DR

This paper proposes a monotonic safety assumption to reduce non-determinism in probabilistic models, significantly improving the scalability and data efficiency of safety analysis for autonomous systems with machine learning components.

Contribution

It introduces a novel monotonic safety-based method to simplify probabilistic models, enabling faster and more data-efficient safety verification while maintaining conservative estimates.

Findings

Speed-ups of an order of magnitude in model checking

Reduced data requirements for statistical model checking

Maintains acceptable accuracy even when assumptions are approximate

Abstract

Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in probabilistic models, but probabilistic model checking of such models is difficult to scale -- largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model checking (SMC) has been proposed to address the scalability issue. However it requires large amounts of data to account for the aforementioned non-determinism, which in turn limits its scalability. This work introduces a general technique for reduction of non-determinism based on assumptions of "monotonic safety'", which define a partial order between system states in terms of their probabilities of being safe. We exploit these assumptions to remove non-determinism from controller/plant models to drastically speed up probabilistic model checking and statistical model checking while providing provably conservative estimates as long as the safety is indeed monotonic. Our experiments demonstrate model-checking speed-ups of an order of magnitude while maintaining acceptable accuracy and require much less data for accurate estimates when running SMC -- even when monotonic safety does not perfectly hold and provable conservatism is not achieved.