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

Oct 1, 2026

Q-Learning for Reachability in MEC-Free MDPs

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.

Lu-Chin Chang, Suguman Bansal

Georgia Institute of Technology

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

Ask PDF

Jun 29, 2026

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

Probabilistic model checking for Markov decision processes (MDPs) provides quantitative guarantees, but often offers limited insight into why undesired outcomes occur. Probability-raising (PR) causality addresses this by identifying states whose visitation increases the probability of reaching designated states. Existing PR-cause identification methods, however, use MDP modifications not well-suited for learning: the gap between conditional and unconditional reachability probabilities can be hard to detect from transition samples, and construction requires reachability probabilities of the MDP, which are unavailable when transition probabilities are unknown. We study unknown MDPs and propose a learning approach with probabilistic guarantees for PR-cause identification. Our key ingredient is a restart-based MDP modification that reduces PR-cause checking to two conditional reachability queries without using reachability values of the original MDP. We prove correctness, establish sample-complexity bounds, and develop an anytime learning-and-checking algorithm based on two-sided value iteration that progressively classifies states as causal, non-causal, or undecided. Experiments on two benchmarks demonstrate reliable and fast identification of PR causes.

Ryohei Oura, Georgios Fainekos, Hideki Okamoto +1

Toyota Research Institute of North America, Toyota Motor North America · Frontier Research Center, Toyota Motor Corporation

Reachability Analysis Markov Decision Processes Markov Models Causal Reasoning Causal Inference

Ask PDF

May 23, 2026

Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality

Reinforcement learning (RL) for reachability specifications is fundamental in sequential decision-making, yet theoretical guarantees remain less explored. A recent work achieves asymptotic convergence to optimal policies. However, this approach provides limited insight into convergence dynamics. In this work, we present an alternative approach that provides deeper theoretical insights into convergence. Our approach builds on PAC learning with assumptions. PAC learning guarantees near-optimal policies with high confidence in finite time but requires knowing internal MDP parameters like minimum transition probability. We argue that while these parameters are unknown in RL, they can be iteratively refined and estimated with increasing accuracy. By iteratively satisfying PAC conditions, we show that exact optimality can be achieved in the limit. Empirical evaluations on standard benchmarks validate our theoretical insights into convergence dynamics.

Amogh Palasamudram, Jakub Svoboda, Suguman Bansal +1

Georgia Institute of Technology, USA · Institute of Science and Technology, Austria · Dartmouth College, USA

Markov Decision Processes Reinforcement Learning

Ask PDF