Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces Quasar, the first model-free algorithm to achieve asymptotic convergence guarantees for reachability specifications in MEC-free Markov Decision Processes (MDPs). By adapting Q-learning's temporal-difference updates, Quasar bypasses explicit transition probability estimation, significantly reducing memory requirements and sample complexity compared to prior model-based approaches. Empirical results on the Quantitative Verification Benchmark Set demonstrate orders of magnitude fewer samples needed for optimal policy convergence.
Model-free Q-learning now guarantees optimal reachability policies in a broad class of MDPs, slashing sample complexity and memory needs.
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.