Exact Model-Free Policy Iteration for Co-safe LTL Planning

What the math gives to ML

The paper provides a constructive way to solve model-free reachability reinforcement learning despite the fact that the undiscounted Bellman operator is noncontractive and its fixed-point equation has multiple solutions. Its key mechanism is a two-stage procedure: use a discounted surrogate, whose Bellman operator is a contraction, to identify states that are provably irrelevant or dead for the reachability objective, then clamp those states and perform undiscounted stochastic policy evaluation followed by greedy policy improvement. This transfers directly to sparse-terminal RL and sc-LTL control by replacing unstable undiscounted TD bootstrapping with a discounted support-identification phase plus a proper undiscounted evaluation phase. The experimentally falsifiable signature is that the clamped evaluator should converge to the reachability probability while ordinary undiscounted Q-learning can converge to different fixed points depending on initialization and sampling.