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

Han Bao; Shinsaku Sakaue; Kazuki Watanabe

math.OCOct 13, 2026

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

Authors: Han Bao, Shinsaku Sakaue, Kazuki Watanabe

Organizations: The Institute of Statistical Mathematics · Tohoku University · RIKEN AIP · CyberAgent · National Institute of Informatics

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.

Figures & tables

Panel of Figure 1 — Figure 1: An example MDP representing a toy probabilistic system. Here $t_{1}$ and $t_{2}$ are failure states.

Rule	Error unit $E$	$h_{E}(w)$
$L^{2}$	$E_{2}$ in ( 9 )	$\lVert w\rVert_{2}$
$L^{\infty}$	$E_{\infty}=[0,1]^{d}$	$\lVert w\rVert_{1}=1$
gauge	$S$	$h_{S}(w)$

Table 1: Error units and normalizers for

w\in\triangle_{d}

. The gauge choice (

E=S

) requires

h_{S}>0

on this simplex.

Panel of Figure 2 — Figure 2: Different error units select different query directions for the same safe region $S$ ( dark gray ) and outer approximation $U$ ( light gray ). The violet regions show the smallest enlargements $S+\epsilon E$ containing $U$ : $\epsilon=\sqrt{5}/4$ for $E=E_{2}$ , $1/2$ for $E=E_{\infty}$ , and $3$ for $E=S$ . At $x_{*}=(3/4,1/4)$ , the teal arrows are outward normals to these enlargements, giving the normalized weights $w_{*}=(2/3,1/3)$ , $(1,0)$ , and $(1/2,1/2)$ . The dashed segments join $x_{*}$ to the common nearest point $q_{*}=(1/4,0)$ for the $L^{2}$ and $L^{\infty}$ cases.

Expected	Method	D ( $\uparrow$ )	U ( $\downarrow$ )	$N$ ( $\downarrow$ )	$W$ (sec)	$T$ (sec)
safe	$L^{2}$ ( Watanabe and Unno,, 2026 )	10	2	247	3044.879	3316.6
	$L^{\infty}$	9	3	284	606.262	893.7
	Gauge	12	0	78	39.046	105.3
	LK- $\epsilon$ ( Lammel and Küfer,, 2023 )	5	7	441	4242.446	4880.7
	LK- $\gamma$ ( Lammel and Küfer,, 2023 )	9	3	312	3608.969	4161.0
unsafe	$L^{2}$ ( Watanabe and Unno,, 2026 )	12	0	58	36.112	88.7

Table 2: All 24 model/specification pairs, grouped by expected label (12 cases per group). D and U count decisive and unknown results.

N,W,T

sum queries, query selection time, and runtime over all 12 runs in each row.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Benchmark	Expected	$d$	$L^{2}$	$L^{\infty}$	Gauge	LK- $\epsilon$	LK- $\gamma$
Gridworld	safe	4	8	11	3	14	6
Gridworld	safe	6	16	16	3	49	9
Gridworld	safe	8	38	$50^{\dagger}$	6	$50^{\dagger}$	16
Gridworld	safe	10	$23^{\dagger}$	$42^{\dagger}$	4	$50^{\dagger}$	26
Robot mission	safe	4	5	5	4	6	6
Robot mission	safe	6	7	7	6	7	7

Appendix

Table 3: Oracle calls on all 24 benchmark cases. The dimension

d

is the number of target states in MDPs. A dagger ( † ) marks an unknown result.

Explore similar work

Certifying Almost-Sure Reachability in Unknown MDPs
Oct 13, 2026S Akshay, Suguman Bansal, Gaurav MahlaMarkov Decision Processes Reachability Analysis
Department of Computer Science and Engineering, Indian Institute of Technology Bombay, Mumbai, India · School of Computer Science, Georgia Institute of Technology, Atlanta, GA, USA
Quantitative Analysis of $ω$ -Regular Robust MDPs
Aug 26, 2026Ali Asadi, Krishnendu Chatterjee, Ehsan Kafshdar Goharshady +3Robust Markov Decision Processes Sequential Decision Making
Institute of Science and Technology Austria
Evaluation Metrics for Safe Reinforcement Learning
Sep 14, 2026Lindsay Spoor, Aske Plaat, Thomas MoerlandRL Benchmarks Constrained RL
Leiden Institute of Advanced Computer Science, Leiden University, Leiden, the Netherlands

Oct 13, 2026J/K move · Enter open · S save

Certifying Almost-Sure Reachability in Unknown MDPs

S Akshay, Suguman Bansal, Gaurav Mahla

Department of Computer Science and Engineering, Indian Institute of Technology Bombay, Mumbai, India · School of Computer Science, Georgia Institute of Technology, Atlanta, GA, USA

Markov Decision Processes Reachability Analysis

Open paper AskPDF arXiv

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with learning an optimal policy against a formal specification in an unknown {\em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one verify that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the {\em almost-sure reachability property}, whose correctness is witnessed by a {\em ranking supermartingale (RSM)} certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound

p_{\min}

on nonzero transition probabilities, a correct certificate can be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the

p_{\min}

-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

Abstract

Explore similar work

Certifying Almost-Sure Reachability in Unknown MDPs

Quantitative Analysis of ωωω-Regular Robust MDPs

Evaluation Metrics for Safe Reinforcement Learning

Quantitative Analysis of $ω$ -Regular Robust MDPs