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.
Figures & tables
Benchmark
Quasar-BR
Quasar-Naive
Staged-PAC
MDP
∣S∣
∣S×A∣
d
V∗(i0)
Final error
Samples to <10−2 error
Final error
Samples to <10−2 error
Final error
Samples to <10−2 error
ij.3
7
12
2
1
9×10−13
5
1.3×10−4
147
6.9×10−3
2.8×107
philosophers.3
956
3 342
4
1
0
15
1.5×10−5
3.2×106
2.0×10−2
—
rabin.3
27 766
45 636
4
1
0
7
1.7×10−5
3.2×106
7.2×10−3
9.3×108
ij.10
1 023
5 120
9
1
2×10−11
68
5.5×10−1
—
1.1×10−1
—
consensus.2
272
400
12
1
6×10−12
100
7.9×10−1
—
3.9×10−2
—
Table 1: Benchmark MDPs and head-to-head results. d = BFS goal depth of i0 . † = trained on the MEC-quotient, sizes reported post-collapse. Final error is measured after 36 h, and “samples to <10−2 error” is the number of samples needed to sustain that error, with — marking a benchmark on which it was never sustained. All entries are medians over 5 seeds.
Figure 1: Value estimate at the initial state vs. samples on all nine benchmarks (seed mean; shaded band = min–max range over seeds; 5 seeds per series). Quasar-BR and Quasar-Naive against the Staged-PAC baseline: the shaded band with dashed edges is the baseline’s own output, its [L,U] bounds; the solid curve is the midpoint 21(L+U) , our minimax point readout of the interval; horizontal line = V∗(i0) . All three series run a 36 h wall. † = MEC-quotient input.
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 2: Per-seed value estimate at the initial state vs. samples: one line per run, 10 runs per panel — 5 Quasar-BR seeds and 5 Quasar-Naive seeds. Bottom axis: samples (log). Top axis: wall time (log), aligned via the Quasar-BR runs’ median sampling rate (samples/sec is near-constant within a run; indicative only for Quasar-Naive , which paces differently).
Figure 3: Per-seed full-table sup-norm ∥Qt−Q∗∥∞ , same runs and colors as Figure 2 .
Figure 4: A reachability instance that is not an SSP instance. From i0 , actions a and b each split their mass between the target g and the sink d . No policy reaches g with probability one, so no proper policy exists, yet the reachability value 43 is well defined and attained by b .