Certifying Almost-Sure Reachability in Unknown MDPs

S Akshay; Suguman Bansal; Gaurav Mahla

cs.LOOct 13, 2026

Certifying Almost-Sure Reachability in Unknown MDPs

Authors: S Akshay, Suguman Bansal, Gaurav Mahla

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

Abstract

{\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.

Figures & tables

Panel of Figure 1 — Figure 1: MDP for Lemma 1

Benchmark	$\eta$	$B$	$\varepsilon^{\prime}$	drift min
Cyclic ( $p{=}0.01$ )	$0.0167$	$200$	$-2.333$	$0.500$
Cyclic (bottleneck)	$0.020$	$82.5$	$-0.650$	$0.783$
Cyclic ( $p{=}0.1$ )	$0.020$	$20$	$\phantom{-}0.600$	$0.933$
DAG-like	$0.010$	$3.132$	$\phantom{-}0.969$	$0.999$
Gridworld	$0.010$	$5.001$	$\phantom{-}0.950$	$0.998$
Chain (RiverSwim)	$0.010$	$15.695$	$\phantom{-}0.843$	$0.997$

Table 1: Transferability across benchmarks, with

\varepsilon^{\prime}=1-B\eta

and drift

{}_{\min}=\min_{s}\big(V(s)-\mathbb{E}_{M}[V(\text{next})]\big)

. The certificate is empirically valid on

M

(drift

{}_{\min}>0

) in every case, yet the sufficient condition

\varepsilon^{\prime}>0

fails wherever a rare transition inflates

B

Appendix figures & tables13 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 2 — Figure 2: Cyclic MDP with all forward probabilities $0.01$ (true kernel $M$ ).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$150$	$148.5$	$149$	$1.5$	$1$
$s_{1}$	$200$	$199.125$	$199$	$0.875$	$1$
$s_{2}$	$150$	$149.5$	$149$	$0.5$	$1$

Appendix

Table 2: Per-state certificate and drift values for the cyclic MDP with all forward probabilities

0.01

Panel of Figure 3 — Figure 3: Cyclic MDP with one bottleneck forward transition of probability $0.01$ (true kernel $M$ ).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$82.5$	$81.225$	$81.5$	$1.275$	$1$
$s_{1}$	$65$	$63.942$	$64$	$1.058$	$1$
$s_{2}$	$37.5$	$36.717$	$36.5$	$0.783$	$1$

Appendix

Table 3: Per-state certificate and drift values for the cyclic MDP with one bottleneck forward probability

0.01

Panel of Figure 4 — Figure 4: Cyclic MDP with forward probabilities $0.1$ (true kernel $M$ ).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$15$	$13.95$	$14$	$1.05$	$1$
$s_{1}$	$20$	$19.017$	$19$	$0.983$	$1$
$s_{2}$	$15$	$14.067$	$14$	$0.933$	$1$

Appendix

Table 4: Per-state certificate and drift values for the cyclic MDP with forward probabilities

0.1

Panel of Figure 5 — Figure 5: DAG-like MDP (true kernel $M$ ).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$3.132$	$2.131$	$2.132$	$1.001$	$1$
$s_{1}$	$2.42$	$1.421$	$1.42$	$0.999$	$1$
$s_{2}$	$1.7$	$0.698$	$0.7$	$1.002$	$1$
$s_{3}$	$1$	$0$	$0$	$1$	$1$

Appendix

Table 5: Per-state certificate and drift values for the DAG-like MDP.

Panel of Figure 6 — Figure 6: Gridworld MDP (true kernel $M$ ; reproduced from the experiment output).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$5.001$	$4.001$	$4.001$	$1.001$	$1$
$s_{2}$	$2.793$	$1.795$	$1.793$	$0.998$	$1$
$s_{4}$	$2.654$	$1.654$	$1.654$	$1$	$1$
$s_{6}$	$2.795$	$1.794$	$1.795$	$1.001$	$1$
$s_{7}$	$1.406$	$0.404$	$0.406$	$1.002$	$1$

Appendix

Table 6: Per-state certificate and drift values for the gridworld MDP.

Panel of Figure 7 — Figure 7: Chain (RiverSwim-style) MDP (true kernel $M$ ).

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$15.695$	$14.692$	$14.695$	$1.003$	$1$
$s_{1}$	$13.195$	$12.198$	$12.195$	$0.997$	$1$
$s_{3}$	$6.664$	$5.657$	$5.664$	$1.007$	$1$
$s_{4}$	$3.333$	$2.33$	$2.333$	$1.003$	$1$

Appendix

Table 7: Per-state certificate and drift values for the chain (RiverSwim-style) MDP.

State	$V(s)$	$\mathbb{E}_{M}[V^{\prime}]$	$\mathbb{E}_{M^{\prime}}[V^{\prime}]$	Drift $(M)$	Drift $(M^{\prime})$
$s_{0}$	$421.467$	$420.445$	$420.467$	$1.021$	$1$
$s_{25}$	$8791.467$	$8790.446$	$8790.467$	$1.021$	$1$
$s_{50}$	$10661.467$	$10660.467$	$10660.467$	$1$	$1$
$s_{75}$	$8364.8$	$8363.778$	$8363.8$	$1.022$	$1$
$s_{98}$	$425.2$	$424.179$	$424.2$	$1.021$	$1$

Appendix

Table 8: Per-state certificate and drift values for the large

100

-state MDP (representative states).

Explore similar work

Q-Learning for Reachability in MEC-Free MDPs
Oct 1, 2026Lu-Chin Chang, Suguman BansalMarkov Decision Processes Reinforcement Learning
Georgia Institute of Technology
Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees
Jun 29, 2026Ryohei Oura, Georgios Fainekos, Hideki Okamoto +1Reachability Analysis Markov Decision Processes
Toyota Research Institute of North America, Toyota Motor North America · Frontier Research Center, Toyota Motor Corporation
Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality
May 23, 2026Amogh Palasamudram, Jakub Svoboda, Suguman Bansal +1Markov Decision Processes Reinforcement Learning
Georgia Institute of Technology, USA · Institute of Science and Technology, Austria · Dartmouth College, USA

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

Q-Learning for Reachability in MEC-Free MDPs

Lu-Chin Chang, Suguman Bansal

Georgia Institute of Technology

Markov Decision Processes Reinforcement Learning Q-Learning Model-Free RL Policy Learning

Open paper AskPDF arXiv

Reinforcement learning (RL) for reachability specifications is fundamental to sequential decision-making. Prior work establishes asymptotic convergence to optimal policies, but only through model-based methods that must explicitly estimate the transition probabilities of the underlying Markov Decision Process (MDP). We present Quasar, the first model-free algorithm with asymptotic guarantees for reachability on the fragment of MDPs free of non-terminal maximal end components (MECs), a building block to which every MDP reduces by the standard MEC quotient. Our algorithm follows the classical Q-learning approach, using temporal-difference updates to converge to an optimal policy without ever learning the transition probabilities. The resulting learner reduces the memory footprint from the O(|S|^2|A|) that model-based methods require to O(|S||A|). On the standardized Quantitative Verification Benchmark Set, our algorithm converges to the optimal policy with orders of magnitude fewer samples than the previous model-based state-of-the-art. Together these results are a concrete step toward the practical deployment of reachability learning and, with it, of specification-guided RL.

Abstract

Explore similar work

Q-Learning for Reachability in MEC-Free MDPs

Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees

Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality