mlsanityData to 14 Oct 2026

Certifying Almost-Sure Reachability in Unknown MDPs

arXiv 2610.18119 ↗First posted 13 Oct 2026cs.LO cs.AIcited by 0

On the map: Deep reinforcement learning methods → Safe and constrained RL

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.

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.

Builds on

7 of 19 references.

References · 7

  1. 2019PAC Statistical Model Checking for Markov Decision Processes and Stochastic Gamescited by 32
  2. 2021Stability Verification in Stochastic Control Systems via Neural Network Supermartingalescited by 26
  3. 2023Compositional Policy Learning in Stochastic Control Systems with Formal Guaranteescited by 14
  4. 2023A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPscited by 13
  5. 2015Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Propertiescited by 4
  6. 2019Farkas certificates and minimal witnesses for probabilistic reachability constraintscited by 3
  7. 2024Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Propertiescited by 2

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026Reinforcement Learning for Reachability: Guaranteeing Asymptotic Optimality
  2. 2026Robust Shielding for Safe Reinforcement Learning
  3. 2026Value Functions as Supermartingale Certificates
  4. 2025Probabilistic Shielding for Safe Reinforcement Learning
  5. 2026Scenario Generation for Risk-Aware Reinforcement Learning with Probably Approximately Safe Guarantees
  6. 2026Finite Constant Frontiers and Auditable Regret Certificates for Average-Reward Reinforcement Learning
  7. 2025Provably Optimal Reinforcement Learning under Safety Filtering
  8. 2026On the Sample Complexity of Discounted Reinforcement Learning with Optimized Certainty Equivalents