# Certifying Almost-Sure Reachability in Unknown MDPs

arXiv: https://arxiv.org/abs/2610.18119 · HTML: https://mlsanity.com/paper/2610.18119/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 7 of its 19 references that are in the map.
- First posted on arXiv 13 Oct 2026.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

## Builds on (most cited first, 7 of 7)

- [PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games](https://mlsanity.com/paper/1905.04403/) (2019)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs](https://mlsanity.com/paper/2310.12248/) (2023)
- [Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties](https://mlsanity.com/paper/1505.01180/) (2015)
- [Farkas certificates and minimal witnesses for probabilistic reachability constraints](https://mlsanity.com/paper/1910.10636/) (2019)
- [Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties](https://mlsanity.com/paper/2405.04015/) (2024)

## Abstract (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 pmin 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 pmin-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.