Q-Learning for Reachability in MEC-Free MDPs
Reinforcement learning for reachability specifications has been limited to model-based methods that explicitly estimate transition probabilities. This paper introduces Quasar, a model-free Q-learning variant that provably converges to optimal reachability policies on MDPs without non-terminal maximal end components, using only $O(|S||A|)$ memory. By replacing the missing discount factor with an intrinsic expected hitting time, the authors obtain a weighted contraction and demonstrate orders-of-magnitude sample improvements over the state of the art.
The paper makes a compelling theoretical advance: it closes a genuine gap by giving the first model-free asymptotic convergence guarantee for reachability on no-EC MDPs. The analysis is elegant and the empirical gains over the model-based Staged-PAC baseline are dramatic on the QVBS suite. Yet the restriction to the no-EC fragment, while standard in formal verification, still sidesteps the hardest model-free challenge of learning under unknown end components, and the experiments lean heavily on a carefully engineered backward-replay variant rather than the analyzed online algorithm.
The hitting-time weighted contraction is a genuinely new analytical tool that directly addresses why classical discounted Q-learning proofs fail at $\gamma=1$. The memory reduction from $O(|S|^2|A|)$ to $O(|S||A|)$ is clean and practically important for large product MDPs, and the empirical evaluation on the standardized QVBS shows Quasar-BR reaching numerical exactness within tens to hundreds of samples on several benchmarks.
The no-EC assumption is structural, but the paper's claim that every MDP reduces to this fragment via the MEC quotient understates a key obstacle: computing the quotient generally requires knowledge of the underlying graph or transition structure, which contradicts the pure model-free premise when the MDP is truly unknown. The distinction between the analyzed Quasar-Naive and the reported Quasar-BR is also sharp: the naive version fails to converge on deeper benchmarks like firewire, leaving error at $1.0$, while the backward-replay proof requires a separate non-trivial argument because the updates read already-overwritten entries. Finally, the convergence threshold $\eta$ and the truncation horizon $H=10|S\setminus S_{\mathcal{G}}|$ are hand-tuned experimental details that are not justified theoretically.
The evidence supports the core claim that model-free reachability learning can outperform model-based sampling in sample efficiency on the tested fragment. Table 1 shows Quasar-BR outperforming Staged-PAC on every benchmark, often by orders of magnitude. However, the comparison is partially confounded by the fact that Quasar-BR with first-visit step size $\alpha=1$ performs exact value iteration along a sampled path, which is closer to a model-free planning sweep than to traditional RL. The authors acknowledge that the baseline's reported error on csma is misleading because its initial bounds $[0,1]$ happen to center on $V^*=0.5$, making the speedup conservative.
While the experimental benchmarks are drawn from the public Quantitative Verification Benchmark Set and the competing Staged-PAC code is open-source, the paper provides no code repository, no seed-level hyperparameter sweep, and no implementation details for the backward-replay buffer management. The step-size schedule $\alpha=1/N(s,a)$ and $\epsilon=1$ action selection are stated, but the stopping rule and checkpointing grid are underspecified. Without released source code for Quasar, independent reproduction of the exact sample counts and convergence curves would be difficult.
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.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.