arXiv：cs.AI· Han Bao, Shinsaku Sakaue, Kazuki Watanabe·· 1 天前
MDP 安全验证的查询选择：一种凸分析视角
Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes
AI 导读
针对 Markov 决策过程（MDP）安全验证中 Watanabe 和 Unno（2026）按最大欧氏违反度选择权重的规则，本文提出统一框架，将方向按外近似与安全区域间的支撑函数差、以显式选定的误差单位归一化后打分。最大得分为正时等于包含外近似所需的安全区域最小放大倍数；单位立方体与安全区域本身可生成两条新规则，实验评估了不同度量规则对验证性能的影响。
正文
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.
| Subjects: | Optimization and Control (math.OC); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2610.17541 [math.OC] |
| (or arXiv:2610.17541v1 [math.OC] for this version) | |
| https://doi.org/10.48550/arXiv.2610.17541 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Han Bao [view email]
[v1]
Tue, 13 Oct 2026 01:09:51 UTC (26 KB)
来源：arXiv：cs.AI · arxiv.org