# Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes

arXiv: https://arxiv.org/abs/2610.17541 · HTML: https://mlsanity.com/paper/2610.17541/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 33 references that are in the map.
- First posted on arXiv 13 Oct 2026.

## Builds on (most cited first, 5 of 5)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [A Practitioner's Guide to MDP Model Checking Algorithms](https://mlsanity.com/paper/2301.10197/) (2023)
- [Optimistic Value Iteration](https://mlsanity.com/paper/1910.01100/) (2019)
- [Sound Value Iteration](https://mlsanity.com/paper/1804.05001/) (2018)
- [Compositional Value Iteration with Pareto Caching](https://mlsanity.com/paper/2405.10099/) (2024)

## Abstract (arXiv)

Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler. Watanabe and Unno (2026) prove safety by refining an outer approximation of the failure probabilities, where each query bounds a nonnegative weighted sum of the probabilities. Their rule selects weights by the largest Euclidean violation. We present a unified framework to measure violation in an explicitly chosen error unit: directions are scored by the support-function gap between the outer approximation and the safe region, normalized by the support function of the unit. We show that the maximal score, when positive, equals the smallest enlargement of the safe region in multiples of that unit that contains the outer approximation. The Euclidean unit recovers the earlier rule; two new rules are generated by the unit cube and the safe region itself. We experimentally evaluate how the choice of measurement rule affects the performance of safety verification for MDPs.