Source-linked AI summary
Q-Learning for Reachability in MEC-Free MDPs
Lu-Chin Chang, Suguman Bansal
TL;DR
Existing asymptotic reachability guarantees rely on model-based transition estimation. Quasar learns reachability model-free on no-EC MDPs, a fragment to which every MDP reduces, and converges with less memory and orders of magnitude fewer benchmark samples than the model-based state of the art.
Problem
Reachability is foundational to specification learning, but prior asymptotic guarantees require model-based transition estimation, which is costly at scale.
Source: §1 · p. 1Method
Quasar adapts Q-learning to learn reachability directly on no-EC MDPs, using expected termination time to recover contraction without estimating transition probabilities.
Source: §1 · pp. 1–2Results
On the standardized benchmark suite, Quasar-BR converges to optimal values while using orders of magnitude fewer samples than the model-based state of the art.
Source: §1 · p. 2Takeaways & Limitations
The no-EC fragment is a building block for general MDPs through the standard MEC quotient, and Quasar is progress toward practical specification-guided RL.
Source: §1 · p. 1, §6 · p. 6The guarantee is established for no-EC MDPs; extending learning to arbitrary MDPs remains the pressing next step.
Source: §2.2 · p. 2, §6 · p. 7
Abstract
from arXiv · showhide
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.
1 Introduction
Reachability is a foundational specification objective, but asymptotic guarantees for it had required model-based learning, whose transition estimates are costly at scale. Quasar gives a model-free alternative for no-EC MDPs, with an asymptotic guarantee, smaller memory use, and strong benchmark results.
1 Introduction
- Reachability is a primitive for richer LTL and ω-regular specifications, while general LTL objectives are not PAC-learnable and some restricted PAC guarantees rely on unobservable MDP quantities.Source: §1 · p. 1
- Prior asymptotic reachability methods are model-based, and their transition-estimate storage and refinement costs become prohibitive on large product MDPs.Source: §1 · p. 1
- Every MDP reduces to the no-EC fragment through the standard MEC quotient, making it a building block for general MDPs.The no-EC condition excludes non-terminal maximal end components.Source: §1 · p. 1
- No optimality-preserving reduction converts reachability to discounted-sum rewards, so its convergence gap must be addressed directly.Source: §1 · p. 2
- Quasar applies a Q-learning-style method directly to reachability, replacing the missing discount-factor contraction with a contraction weighted by expected time to termination.The expected hitting-time weight is intrinsic to the MDP and need not be known or tuned by the learner.Source: §1 · pp. 1–2
- Quasar-BR converges to optimal values on every benchmark while using orders of magnitude fewer samples than the model-based state of the art.The reported benchmark evaluation uses the standardized Quantitative Verification Benchmark Set.Source: §1 · p. 2
- Quasar achieves almost-sure convergence to optimal reachability values on no-EC MDPs using O(|S||A|) space, versus O(|S|^2|A|) for model-based methods.Its guarantee relies only on the structural no-EC assumption, not a numerical parameter of the MDP.Source: §1 · p. 2
2 Preliminaries and Problem Setup
The setup defines reachability learning in an unknown MDP and asks whether it can achieve asymptotic guarantees from simulator access alone. The paper focuses on no-EC MDPs, situates that fragment within general MDPs, and contrasts Quasar with prior approaches.
2.1 Preliminaries
- A reachability value is the probability of eventually visiting the target; asymptotic learning means induced policies approach the optimal initial-state value almost surely.Source: §2.1 · p. 2
2.2 Problem Setup
- The learning problem is to obtain asymptotic guarantees from simulator access without explicitly estimating the unknown transition kernel.Prior algorithms with such guarantees estimate the model and then optimize over it.Source: §2.2 · p. 2
- The no-EC assumption excludes end components containing non-terminal states, and collapsing MECs gives every MDP a no-EC quotient.Source: §2.2 · pp. 2–3
2.3 Related Work
- Prior asymptotic methods estimate a model, whereas Quasar matches their guarantee with one O(|S||A|) table instead of O(|S|^2|A|) transition storage.Source: §2.3 · p. 3
- Reward translations for direct ω-regular learning require a threshold depending on unknown transition probabilities, while Quasar relies only on the no-EC assumption.Source: §2.3 · p. 3
- Reachability maximizes target probability without requiring certainty or minimizing path length, so its contraction analysis does not transfer from stochastic shortest path methods.Source: §2.3 · p. 3
3 Algorithm
Quasar adapts Q-learning to learn optimal reachability values directly from sampled transitions, without discounting or modeling transition probabilities. It uses a compact state-action table, and its backward-replay variant retains the guarantee while propagating updates from episode endings toward the start.
3 Algorithm
- The algorithm learns reachability values directly, with no discount factor, because reachability has no optimality-preserving reduction to discounted-sum rewards.Source: §3 · p. 3
- Quasar updates each visited state-action estimate toward the sampled successor’s maximum value, with terminal values fixed at 1 for targets and 0 for non-targets.The sampled successor provides an unbiased update target without consulting the transition kernel; episodes end at terminals almost surely under the no-EC assumption.Source: §3 · pp. 3–4
- Algorithm 1 runs in O(|S||A|) space, storing state-action value estimates and visit counters rather than transition estimates.Both tables have one entry per non-terminal state-action pair, avoiding the model-based O(|S|^2|A|) storage cost.Source: §3 · p. 4
- Quasar-BR buffers an episode and applies the same updates in reverse order, and a separate proof establishes that it retains the convergence guarantee.Source: §3 · p. 4
- With step size α = 1/N, a backward sweep can carry terminal reward to the initial state in one pass; when the optimum is 1, Quasar-BR is numerically exact within one episode regardless of goal depth.Source: §3 · p. 4
4 Proof of Convergence
The proof establishes convergence by combining a hitting-time-weighted contraction of the Bellman operator with stochastic approximation for sampled updates. Under the stated assumptions, Q estimates converge almost surely to optimal reachability values, and their greedy policies eventually attain the optimal initial-state value exactly.
4 Proof of Convergence
- The proof analyzes Quasar-Naive by relating sampled Q-learning updates to a deterministic contraction perturbed by mean-zero noise.The usual discounted supremum-norm argument does not apply to undiscounted reachability.Source: §4 · p. 4
4.1 The Bellman Optimality Operator
- The Bellman optimality operator averages successor values under the true dynamics, has Q* as its fixed point, and is estimated from one sampled successor.Source: §4.1 · p. 4
4.2 Contraction under a Hitting-Time Weight
- Weighting errors by worst-case expected time to termination makes the Bellman operator contract under the no-EC assumption.The hitting-time weight is finite under that assumption and supplies an MDP-intrinsic analogue of a discount factor.Source: §4.2 · pp. 4–5
4.3 Q-Learning as Stochastic Approximation
- Sampled updates form a stochastic-approximation recursion with unbiased bounded noise; convergence requires infinite visits to every pair and Robbins–Monro step sizes.Under the no-EC assumption, ϵ-greedy exploration with ϵ > 0 supplies infinite visits, allowing the visit-indexed step-size schedule to advance.Source: §4.3 · p. 5
4.4 Convergence
- Under Assumptions 1 and 2, Quasar's Q-learning iterates converge almost surely to the optimal reachability values.The proof combines contraction with a mean-zero noise argument.Source: §4.4 · p. 5
4.5 From Value Convergence to the Asymptotic Guarantee
- Under Assumptions 1 and 2, the induced greedy policies' initial-state values converge to optimality and are eventually exactly optimal.This guarantee concerns the greedy policies, not the permanently exploratory behavior policy, whose value remains bounded away from optimality.Source: §4.5 · p. 6
5 Experiments
The experiments compare Quasar with the prior asymptotic-guarantee method on nine standardized benchmarks. Quasar-BR converges within the 36-hour budget on every benchmark and has lower final error than Staged-PAC on all nine.
5.1 Implementation Details
- Quasar's experiments use a dense Q-table requiring O(|S||A|) memory, inverse-visit-count step sizes, and uniform action sampling.Source: §5.1 · p. 6
5.2 Experimental Setup
- The evaluation covers all nine benchmark models, applying the standard MEC quotient to the three with non-terminal MECs before comparison with Staged-PAC.Runs use five seeds and a 36 h timeout; error is measured against samples consumed.Source: §5.2 · p. 6
5.3 Results
- On all nine benchmarks, Quasar-BR converges within 36 h and finishes with lower error than Staged-PAC; Staged-PAC sustains error below 10^-2 on only two.On those two, Staged-PAC uses 2.8×10^7 samples on ij.3 and 9.3×10^8 on rabin.3, while Quasar-BR needs 5 and 7, respectively.Source: §5.3 · p. 6
- On firewire at goal depth 76, Quasar-Naive ends at error 1.0 after 2.8×10^8 samples, while Quasar-BR reaches error 0 within 215.The passage attributes the divergence to update ordering as goal depth grows; reverse sweeps propagate a corrected value in one pass, unlike online averaging.Source: §5.3 · p. 6
- Every reported finding holds on every random seed, rather than arising from averaging across seeds.Source: §5.3 · p. 6
6 Conclusion
Quasar brings model-free asymptotic guarantees to reachability on no-EC MDPs, using O(|S||A|) memory and improving substantially on model-based state of the art across a standardized benchmark suite. Extending the result to arbitrary MDPs remains an important next step.
6 Conclusion
- Quasar substantially improves on the model-based state of the art across the standardized benchmark suite.Table 1 reports final error after 36 hours and samples needed to sustain initial-state error below 10^-2; entries are medians over five seeds.Source: §6 · p. 6, Table 1 · p. 7
- Quasar provides model-free asymptotic guarantees for reachability on the no-EC fragment of MDPs, with O(|S||A|) memory.The paper presents the no-EC setting as a building block for the general MDP setting via the standard MEC quotient.Source: §6 · p. 6
- Extending reachability learning to arbitrary MDPs is identified as the most pressing next step.The conclusion frames the no-MEC assumption as a building block, while noting that arbitrary MDPs remain to be addressed.Source: §6 · pp. 6–7
A Per-Seed Trajectories
Figures 2 and 3 disaggregate the headline results by seed and show value and Q-error trajectories against samples and wall time.
A Per-Seed Trajectories
- Figures 2 and 3 break the headline results down to individual seeds.Each panel adds a top wall-time axis converted using its median sampling rate, which is near-constant within a run.Source: A Per-Seed Trajectories · p. 10
- The bottom axis shows samples, while a second top axis converts samples to wall time using the panel’s median sampling rate.The conversion is supported by sampling rates that are near-constant within a run.Source: A Per-Seed Trajectories · p. 10
- The per-seed plots report the headline results at the level of individual runs.The wall-time conversion uses each panel’s median sampling rate.Source: A Per-Seed Trajectories · p. 10
B Omitted Proofs
The omitted proofs establish termination and a weighted contraction under the no-EC assumption, then use stochastic approximation to show Q-value convergence and eventual policy optimality.
B Omitted Proofs
- The no-EC assumption implies almost-sure termination under every policy and a uniformly finite expected hitting time.A finite path to a terminal state has positive probability; a geometric tail bound then yields the finite expectation.Source: B Omitted Proofs · p. 10
- The expected termination time Ts supplies a weight under which the undiscounted Bellman operator contracts, without requiring the learner to know or tune that weight.The proof specializes a generic weighted contraction to w = Ts; the expected hitting time plays the role of the discount factor.Source: B Omitted Proofs · p. 10
- Figure 2 tracks per-seed initial-state value against log samples and wall time, while Figure 3 tracks full-table sup-norm Q-error on the same runs.Figure 2’s wall-time axis is aligned using Quasar-BR’s median sampling rate and is indicative only for Quasar-Naive.Source: Figure 2 · p. 11, Figure 3 · p. 12
- The stochastic-approximation argument makes the weighted Q-error converge to zero almost surely, yielding convergence at every reachable state-action pair.The proof controls normalized update noise and inductively shrinks the error bound.Source: B Omitted Proofs · pp. 11–12
- Once Q-estimation error is small enough, greedy policies exclude strictly suboptimal actions and are eventually optimal.Under the no-EC assumption, every Q*-greedy policy is optimal; the proof notes that this assumption is necessary for that conclusion.Source: B Omitted Proofs · pp. 12–13
C Backward-Replay Proof
The proof extends Quasar’s convergence guarantee to backward replay by re-anchoring updates at episode boundaries and bounding the errors introduced by replay. Those errors vanish, allowing the convergence induction to proceed; under a specified optimum-1 condition, one backward sweep also gives exact values.
C Backward-Replay Proof
- Backward replay breaks the original martingale-noise argument because each update reads a table changed by later transitions in the same episode.No choice of filtration restores the martingale property for the raw noise.Source: C Backward-Replay Proof · p. 13
- Re-anchoring each target at the episode-boundary table restores martingale-difference noise, while the bootstrap-row movement is bounded by the episode’s total step size.The proof separately bounds the perturbation from reversing the affine update order; both error terms vanish as the episode budget tends to zero.Source: C Backward-Replay Proof · pp. 13–14
- The proof handles replay reordering by bounding its perturbation at second order in step sizes, then advances the convergence induction using a vanishing error envelope.The affine maps’ order-invariant inherited terms and the vanishing episode budget support the boundary-by-boundary induction.Source: C Backward-Replay Proof · pp. 13–15
- The total step-size budget per episode tends to zero almost surely, making the replay-induced anchoring error vanish.Every pair’s visit count tends to infinity, and the step sizes tend to zero under Assumption 2.Source: C Backward-Replay Proof · p. 13
- Quasar-BR’s iterates converge almost surely to the optimal reachability values under Assumptions 1 and 2.The proof controls errors at episode boundaries; intermediate tables remain within a vanishing distance of those boundary tables.Source: C Backward-Replay Proof · p. 14
- When every pair reachable from the initial state has optimal value 1, Quasar-BR sets the values on the first target-reaching trajectory exactly after one backward sweep.The theorem allows the trajectory to have any length.Source: C Backward-Replay Proof · p. 15
D Reachability versus Stochastic Shortest Path
Reachability and stochastic shortest path (SSP) objectives differ: reachability maximizes the probability of reaching a target, while SSP requires a proper policy and can account for path cost. The examples show that reachability can be defined without any proper policy and can prefer a different policy than SSP.
D Reachability versus Stochastic Shortest Path
- The objectives differ because reachability measures whether the target is reached, whereas SSP minimizes additive path cost to a target reached with certainty.The examples distinguish both the policy requirements and the criteria used to evaluate trajectories.Source: D Reachability versus Stochastic… · p. 15
- Reachability can be well posed when no proper policy exists: in the example, every action leaves positive probability of reaching a non-target sink, yet the best target-reaching probability is 3/4.Action b attains that value; SSP is not defined here because no policy reaches the target with probability one.Source: D Reachability versus Stochastic… · p. 15
- When both objectives are defined, reachability treats a direct path and a longer path as equally optimal if each reaches the target with probability one, while unit-cost SSP prefers the direct path.The chain costs k + 1 under SSP, compared with cost 1 for the direct action.Source: D Reachability versus Stochastic… · p. 15