PaperlayerView exact revision on arXiv

Source-linked AI summary

Certifying Almost-Sure Reachability in Unknown MDPs

S Akshay, Suguman Bansal, Gaurav Mahla

arXiv:2610.18119v1cs.LOcs.AI

TL;DR

Specification-guided RL has largely studied learning policies in unknown MDPs, leaving the question of how to certify a fixed policy from samples. This paper studies RSM certificates for almost-sure reachability, finding that rare transitions rule out probabilistic guarantees without further information, while a known p_min bound supports certificate learning. The resulting sufficient condition is conservative in experiments, and the learning guarantee has exponential dependence on D.

  • Problem

    Prior specification-guided RL focuses on policy learning, while whether a fixed policy can be certified from sampling access to an unknown MDP matters for safety-critical deployment.

    Source: §1 · p. 1

  • Method

    The paper studies RSM certificates for almost-sure reachability and learns an expected-hitting-time certificate through an accurate learned model whose certificate can transfer to the true MDP under a known p_min bound.

    Source: §1 · p. 2

  • Results

    Without further information, learning or verifying an RSM certificate cannot have probabilistic guarantees from sampling access alone; with a known p_min bound, a correct certificate can be learned with probabilistic guarantees.

    Source: §1 · p. 2, §6 · p. 7

  • Takeaways & Limitations

    The p_min-based transfer condition is sound but conservative, as learned certificates often remain valid on the true MDP even when the sufficient condition fails.

    Source: §1 · p. 2, §6 · p. 7

    The learning guarantee has sample complexity exponential in D, which is unavailable to the learner and must be replaced by the worst-case bound D ≤ |S| − 1.

    Source: The Learning Guarantee · p. 7

Abstract

from arXiv · show

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{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 \emph{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 \emph{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.

1 Introduction

The paper shifts specification-guided RL from learning an optimal policy to learning or verifying a correctness certificate for a fixed policy in an unknown MDP. It finds that rare transitions prevent probabilistic guarantees from sampling alone, while a known p_min bound enables a model-based learning route.

1 Introduction

  • The paper asks whether a fixed policy’s correctness certificate can be learned or verified from samples, complementing prior work focused on policy synthesis in unknown MDPs.The question is motivated by the prospect of certifying a deployed controller without building an environment model, including in safety-critical domains.Source: §1 · pp. 1–2
  • For almost-sure reachability, an RSM is a nonnegative state rank that strictly decreases in expectation outside the target, witnessing that the policy reaches the target with probability 1.For finite MDPs, an RSM is a sound and complete witness to this property.Source: §1 · p. 1
  • Without further information about the MDP, neither a correct RSM certificate nor verification of a candidate can be guaranteed from sampling access alone.A transition that makes progress toward the target may have arbitrarily small probability and remain unseen for arbitrarily long.Source: §1 · pp. 1–2
  • With a known p_min bound, learning an accurate model and computing its expected-hitting-time function yields a certificate that transfers to the true MDP under an explicit approximation-error threshold.The expected-hitting-time function decreases by exactly one in expectation on the learned model.Source: §1 · p. 2
  • Earlier certificate-learning work assumes a known model, whereas this paper studies certificate learning and verification when only samples from the unknown transition kernel are available.Prior unknown-MDP guarantees cited here concern learning policies; the paper instead fixes the policy and examines its certificate.Source: §1 · p. 2

2 Preliminaries

The preliminaries define almost-sure reachability certificates and establish why producing or checking an RSM is the central task. For finite MDPs, an RSM exists exactly when the fixed policy reaches the target almost surely from every state.

2 Preliminaries

  • A supermartingale has conditional expectation that does not increase over time, and a nonnegative supermartingale is unlikely to rise far above its starting value.The paper uses this classical fact to rule out avoiding the target forever when an RSM exists.Source: §2 · pp. 2–3
  • An RSM is a nonnegative function whose expected value decreases by at least ε at every non-target state; its existence implies almost-sure reachability.The paper’s completeness result requires reachability with probability 1 from every state, not only the initial state.Source: §2 · p. 3
  • For finite MDPs, an RSM exists if and only if the fixed policy reaches the target almost surely from every state.The expected hitting-time function is finite and gives a 1-RSM when that all-state reachability condition holds.Source: §2 · p. 3
  • Because the RSM decrease condition is an expectation over the transition kernel, it is directly checkable when the model is known but must be evaluated through a learned model when it is unknown.This motivates the paper’s linked questions of learning, verifying, and transferring certificates.Source: §2 · p. 3

3 Learning RSMs under an Unknown Model

The section shows that rare progress transitions make RSM learning and verification impossible with probabilistic guarantees under a sample budget based only on MDP size. The obstruction arises because the transition needed to establish progress may remain unobserved arbitrarily long.

3 Learning RSMs under an Unknown Model

  • The result depends on the sampling model: the learner interacts through samples and does not see the transition kernel.The task fixes a policy and target and asks for a correct RSM certificate with probabilistic guarantees.Source: §3 · p. 3
  • The three-state construction makes the sole progress transition q1→q2 necessary to distinguish a reachability-valid MDP from one where the target is unreachable.Until that transition is observed, the sampled sub-MDP is indistinguishable from one in which q1 only self-loops and q2 is unreachable.Source: §3 · p. 3, Figure 1 · p. 3
  • For general unknown finite MDPs, no sample-complexity bound based only on |S|, |A|, and 1/δ suffices to learn a correct RSM with high probability.The lower bound depends on an unknown transition probability ε that can be arbitrarily small.Source: §3 · p. 4
  • The probability of observing the progress transition within N samples depends on ε, so the required sample count diverges as ε approaches zero.The argument lower-bounds the event of missing the transition by a sequence of self-loops at q1.Source: §3 · p. 4
  • For general unknown finite MDPs, no sampling-based verifier has a sample bound depending only on |S|, |A|, and 1/δ.Without witnessing the rare progress transition, a verifier cannot distinguish a valid candidate from an invalid one within such a budget.Source: §3 · p. 4

4 Learning RSMs under a Known pmin

A known lower bound pmin on nonzero transition probabilities removes the rare-transition barrier while leaving zero-probability transitions unrestricted. The approach combines an expected hitting-time certificate, transferability, and model learning into an end-to-end guarantee.

  • The restriction requires every nonzero transition probability to be at least the known pmin, while leaving zero-probability transitions unrestricted.Source: §4 · p. 4
  • The argument first makes progress observable, then bounds and transfers an expected hitting-time RSM, and finally assembles an end-to-end learning guarantee.Source: §4 · p. 4
  • The four-step construction culminates in a probabilistic guarantee for learning a transferable certificate from sampling access.Source: §4 · p. 4

The pmin Restriction and Observing Progress

With a known lower bound pmin on nonzero transition probabilities, progress toward the target can be observed in finitely many samples. The paper constructs an expected hitting-time RSM, establishes conditions for transferring it from a learned model, and uses them to give a learning guarantee.

The pmin Restriction and Observing Progress

The Expected Hitting-Time Certificate

Transferability

  • A bounded ε′-RSM transfers from the learned model to the true model when η < ε′/B, with the decrease becoming ε′ − Bη.Source: Transferability · p. 6
  • For the expected hitting-time certificate, pmin supplies a checkable approximation threshold by bounding the learned model’s certificate values.Source: Transferability · p. 6

The Learning Guarantee

  • An expected hitting-time RSM certificate can be learned with probability at least 1 − δ under the known pmin assumption.Source: The Learning Guarantee · p. 6
  • The learning procedure approximates the model, computes its expected hitting-time certificate, and transfers that certificate to the true MDP.Source: The Learning Guarantee · p. 7
  • The guarantee is not an efficiency claim: sample complexity is exponential in D, which is unavailable to the learner and may require the worst-case bound |S| − 1.Source: The Learning Guarantee · p. 7

5 Empirical Evaluation of Transferability

Across seven MDP benchmarks, the certificate has positive true-MDP drift even when the sufficient transfer condition fails. Rare progress transitions inflate the bound and make that condition conservative.

Setup

  • The evaluation tests whether ε′ = 1−Bη > 0 holds and whether certificates remain valid when it fails, using driftmin > 0 as the validity criterion.The certificate is computed on a learned model M′, then the kernel is perturbed to obtain the true MDP M.Source: §5 · p. 7

Benchmarks

  • The seven benchmarks span three cyclic MDPs, a DAG-like MDP, a gridworld, a RiverSwim-style chain, and a large sparse 100-state MDP.The suite includes both benign progress structures and rare transitions that can inflate B.Source: §5 · p. 7

Observations

  • driftmin stays positive (never below 0.5) in every benchmark, including all three where ε′ < 0.For the all-0.01 cyclic MDP, η = 0.0167 gives ε′ = −2.333; the 100-state model gives ε′ = −105.667.Source: §5 · p. 7
  • For the DAG-like, gridworld, chain, and p=0.1 cyclic models, ε′ is comfortably positive, indeed close to 1.These models have non-vanishingly small forward probabilities, so B stays small.Source: §5 · p. 7

6 Conclusion

The paper concludes that a known pmin bound makes an expected-hitting-time RSM certificate learnable, checkable, and transferable. The supplementary measure-theoretic background reviews standard probability concepts used in the main text.

6 Conclusion

  • A known pmin bound recovers a learnable, checkable, and transferable expected-hitting-time certificate for almost-sure reachability.The conclusion identifies improving the exponential dependence on D and extending the approach to reach-avoid and full LTL specifications as future work.Source: §6 · p. 7

Measure-Theoretic Background

  • A σ-algebra is a collection of events closed under complements and countable unions; for countable sample spaces, the power set is the default choice.Generated σ-algebras encode the information revealed by observations.Source: Measure-Theoretic Background · p. 10
  • Conditional expectation is the operation used in the defining inequality of a supermartingale, while a filtration represents information available up to each time.For the MDP under a fixed policy, the main text uses the history of the observed state trajectory as its filtration.Source: Measure-Theoretic Background · p. 10

B Benchmark Details

The supplementary benchmark material gives exact kernels and per-state certificate and drift values; the all-0.01 cyclic case illustrates how rare progress affects transfer.

B Benchmark Details

  • The supplementary material reports each benchmark’s exact transition kernel and per-state certificate and drift values, with larger benchmarks represented by a subset of states.Reported quantities are computed by exact linear-algebra solves and are deterministic.Source: B Benchmark Details · p. 10
  • The expected hitting time is computed as the unique solution of a linear system, so the reported benchmark quantities involve no randomness.Source: B Benchmark Details · p. 10

Cyclic MDP, all forward probabilities 0.01

  • In the four-state cycle targeting s4, rare forward transitions of order 0.01 inflate expected hitting time and B, making the transfer margin negative despite positive true-MDP drift.The states overwhelmingly self-loop, and progress occurs only through the rare forward transitions.Source: Cyclic MDP, all forward probabilities… · p. 10

Cyclic MDP, one bottleneck forward probability

The benchmark examples show how progress dynamics affect the sufficient transfer condition: rare transitions can defeat it, while more regular progress keeps B small enough for provable transfer.

Cyclic MDP, one bottleneck forward probability

  • A single rare forward transition suffices to inflate B and defeat the sufficient condition, although true-MDP drift remains positive.The other forward probabilities in this four-state cyclic variant are raised to 0.1.Source: Cyclic MDP, one bottleneck forward… · pp. 10–11

Cyclic MDP, forward probabilities 0.1

DAG-like MDP

  • In the acyclic five-state MDP, steady forward progress keeps B small and the certificate transfers with a comfortable margin.The target is the absorbing state s5.Source: DAG-like MDP · p. 11

Gridworld MDP

  • In the 3 × 3 gridworld, high-probability rightward or downward moves toward s8 keep B small, so the certificate provably transfers.Small-probability lateral slips or self-loops are also part of the fixed-policy dynamics.Source: Gridworld MDP · p. 11

Chain (RiverSwim-style) MDP

  • The six-state RiverSwim-style chain’s certificate transfers provably despite occasional backward drift, as interior states predominantly self-loop and advance moderately toward s6.Source: Chain (RiverSwim-style) MDP · p. 11

Large 100-state MDP

The large benchmark is a sparse 100-state MDP with a rare transition that makes the sufficient condition fail, although the true-MDP drift remains positive at every state.

Large 100-state MDP

  • The benchmark has 100 states and is reported through a representative per-state slice rather than a drawn automaton.Its structure contains a single rare transition.Source: Large 100-state MDP · p. 11
  • A single rare transition raises the certificate bound B enough to fail the sufficient condition, while true-MDP drift stays positive at every state.The passage attributes the large B to the rare transition; the table reports representative states.Source: Large 100-state MDP · p. 11

C Omitted Proofs

The supplement collects proofs omitted from the main paper and restates each proof with the statement it establishes.

C Omitted Proofs

  • The supplement collects omitted proofs and restates each alongside the statement it establishes.Source: C Omitted Proofs · p. 11

Proofs from Section 2

The proofs show that an RSM guarantees almost-sure reachability, and that when reachability holds from every state, expected hitting time supplies a 1-RSM.

Proofs from Section 2

  • An RSM forces almost-sure reachability by constructing a nonnegative supermartingale that would grow without bound if the target were missed.The proof applies a maximal inequality and lets its threshold tend to infinity to show the probability of never reaching the target is zero.Source: Proofs from Section 2 · p. 11
  • If reachability holds from every state in a finite MDP, the hitting time has finite expectation from every state.A shortest path to the target has length at most |S|−1 and is followed with probability at least q^(|S|−1), yielding a geometric tail across blocks.Source: Proofs from Section 2 · p. 12
  • The expected hitting-time function is nonnegative, zero on the target, and decreases by exactly one in expectation outside it, so it is a 1-RSM.The one-step decomposition follows from the Markov property of the chain induced by the memoryless policy.Source: Proofs from Section 2 · p. 12

Proofs from Section 4

The proofs derive finite-sample path-observation bounds and show how expected-hitting-time certificates transfer from a learned model to the true MDP; the appendices also formulate general certificate learning and RSMs for stochastic systems.

Proofs from Section 4

  • With maximum progress-path length D, each D-step block reaches the target with probability at least (pmin)^D, yielding a finite sample bound for observing a path.Using D ≤ n−1, N ≥ (n−1) · log(δ)/log(1−(pmin)^(n−1)) samples suffice for a path to T to be observed with probability at least 1−δ.Source: Proofs from Section 4 · p. 12
  • The expected hitting time on the learned model is a 1-RSM, and approximation error η reduces its true-model expected decrease from 1 to 1−Bη.Thus transfer holds when η < 1/B, provided the certificate bound B is finite.Source: Proofs from Section 4 · p. 14
  • Assuming η ≤ pmin/2 preserves progress-path edges in the learned model with probability at least pmin/2, allowing an a-priori bound on B and a sufficient transfer threshold.The proof bounds B by D/(pmin/2)^D; the pmin assumption is used to bound the certificate, not by the transfer mechanism itself.Source: Proofs from Section 4 · p. 14

D The General Certification-Learning Framework

  • A certification-learning algorithm interacts with the unknown kernel only through samples and iteratively outputs certificate estimates for a fixed policy.Its probabilistic guarantee uses a sample-complexity budget that works uniformly over tasks of a given size; efficiency requires polynomial h.Source: D The General Certification-Learning… · p. 14

E Ranking Supermartingales for Stochastic Systems

  • For stochastic systems, an RSM is a nonnegative function whose expected value decreases by at least ε outside the target, and its existence guarantees almost-sure reachability.The framework specializes the stochastic-system update to MDP transitions under a fixed policy.Source: E Ranking Supermartingales for… · pp. 14–15
Loading 2610.18119v1…