Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes
Abstract
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.
Related
- Robust Markov Decision Processes: An Introduction Using Convex Optimization and Game Theory
- Prediction with Five Experts and Geometric Stopping: A Probabilistic Construction and Analytic Verification
- Canonical analytic realizations of hyperbolic determinantal processes
- Novel Unified Variants, Properties, and Applications of Ostrowski, Jensen, and Hermite–Hadamard Inequalities for Generalized (η, p, h)-Convex Stochastic Processes
- Expected mixed volumes of convex hulls of random walks and Lévy processes
BibTeX
@misc{bao2026convexanalytic,
title = {{Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes}},
author = {Han Bao and Shinsaku Sakaue and Kazuki Watanabe},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.17541},
eprint = {2610.17541},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.17541},
note = {CC BY-SA 4.0},
}
RIS
TY - UNPB
TI - Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes
AU - Han Bao
AU - Shinsaku Sakaue
AU - Kazuki Watanabe
PY - 2026
DA - 2026/10/13
PB - arXiv
DO - 10.48550/arxiv.2610.17541
UR - https://arxiv.org/abs/2610.17541
AB - 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.
ER -