{"id":"4b3357e1-20ff-4b62-ad24-03ed575b930c","arxiv_id":"2411.12019","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A regret-free (sublinear-regret) episodic algorithm for LTL objectives, built on optimistic interval-MDP value iteration for reach-avoid and a graph-learning preprocess requiring a known minimum transition probability.","lead":"The paper presents the first online reinforcement learning algorithm with sublinear regret for maximizing the probability of satisfying linear temporal logic (LTL) specifications on finite Markov decision processes with unknown transitions. It provides finite-episode bounds on how far the learned policy is from optimal, instead of only asymptotic convergence.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 5.1's LTL reduction equates reaching an accepting MEC with satisfying the Rabin condition, but the EVI policy inside an AMEC is arbitrary (Alg. 2, Sec. 5); a tie-break can pick an action that leaves the AMEC, making true satisfaction probability 0 while reach-avoid value is 1.","rationale":"The reader's weakest assumption (B must contain all non-goal MECs, confidence union bound undercount, incomplete pseudocode) identifies real issues, but for the headline LTL result the B condition is actually supplied by graph learning (Alg. 4 puts all non-AMECs into B×), and the union-bound error can be repaired by rescaling δ. The AMEC policy gap is different: it is not a missing technical assumption but a missing semantic step between the reach-avoid objective and the Rabin objective for the fixed learned policy. The optimal values coincide, but regret compares policies' values, and the EVI policy's actions inside accepting MECs are unconstrained by exploration because episodes stop at first hit of G×. This can be fixed by composing the learned reach-avoid policy with a stationary accepting policy inside each AMEC and then bounding the regret of the composition; but as written Theorem 5.1 does not state or prove this. I therefore regard the paper as conditionally acceptable rather than rejecting outright, because the gap appears fixable without changing the overall approach. Agreement with reader: partial, since the reader pointed at the B/MEC condition and confidence accounting but did not identify the AMEC internal-policy issue.","tokens_in":23298,"tokens_out":20999,"duration_ms":228827,"concrete_test":"Run Algorithm 4 with a deterministic tie-break (e.g., pick the smallest-index action) on the 4-state product MDP: s0 --a--> g1; g1 --α--> g2; g1 --β--> b; g2 loops; Rabin accepting condition with K={g2}, J=∅. The AMEC is G×={g1,g2}, B×={b}, and v*=1. If the returned policy uses β at g1, then its true satisfaction probability is 0 in every episode, so R(K)/K does not converge to 0 and Theorem 5.1 fails for this tie-break. As a complementary check, re-read the proof of Theorem 5.1 and locate the line where vk(sinit) in Eq. (1) (Rabin probability under π̃k) is shown to equal P_{π̃k}(reach G× before B×); the proof contains no such argument because Alg. 2's value function at G× is not constrained by the accepting condition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 5 reduces LTL synthesis to reachability of the union G× of accepting MECs. The equality v*(s)=maxπ Pπ(reach G× before B×) holds for values, but Theorem 5.1 needs the stronger statement that the particular policy π̃k returned by EVI has LTL satisfaction probability close to its reach-avoid probability. Algorithm 2 initializes µ0=1 on G× and performs optimistic value iteration as if G× were absorbing; since episodes stop on first visit to G× (Alg. 1), the transition probabilities of actions inside AMECs are never sampled or constrained. The argmax in Alg. 2 at s∈G× is therefore determined only by the tie-breaking rule, not by the Rabin acceptance condition. In a true product MDP, an AMEC may use only a subset of actions at a state; a non-MEC action can leave the AMEC and enter a rejecting end component. Example: s0→g1 with probability 1, g1 has action α→g2 (stays in the AMEC and visits K) and β→b (leaves the AMEC), with Rabin pair K={g2}; both α and β have optimistic value 1 when G× is treated as absorbing. A lexicographic tie-break that picks β yields a policy with reach-avoid value 1 but true LTL satisfaction probability 0, so per-episode regret is 1 and R(K)=K. No step in Alg. 4 replaces the EVI policy inside each AMEC by an accepting policy (one that stays in the MEC and visits K_i infinitely often), and the proof of Theorem 5.1 does not establish that the learned policy is accepting. Thus the stated O(√K) regret bound is for reach-avoid probability, not for the LTL satisfaction probability in Eq. (1). This is the central gap: the full LTL claim collapses unless such a policy transformation is added and analyzed.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an online reinforcement learning algorithm for finite MDPs with unknown transition probabilities and LTL objectives, claiming the first regret-free (sublinear regret) guarantee. The core algorithm (Alg. 1) builds an interval MDP from observations, computes an optimistic reach-avoid policy via extended value iteration (Alg. 2), and executes it for an episode-specific deadline. The LTL extension (Alg. 4) learns the MDP graph (Alg. 5), builds the product with a DRA, identifies accepting and non-accepting MECs, and runs the reach-avoid algorithm on the product. Theorems 4.2 and 5.1 claim O(√K) regret with high probability.","tokens_in":23641,"tokens_out":17898,"duration_ms":179314,"significance":"If the claims were fully correct, this would be a significant advance: it would give the first finite-time, non-asymptotic regret guarantee for LTL policy synthesis in unknown finite MDPs, without requiring a generative model, and it would handle non-communicating product MDPs via a reset mechanism. The paper also supplies explicit confidence intervals, a polynomial graph-learning procedure under a known pmin, and an experimental comparison. However, the LTL reduction has a gap: the policy synthesized by the reach-avoid algorithm is not shown to be accepting inside accepting MECs, so the main theorem is not established as stated.","major_comments":[{"comment":"The reduction from LTL to reach-avoid establishes equality of optimal values, not equality of the EVI policy's reach-avoid probability with its LTL satisfaction probability. Algorithm 1 terminates on first visit to G×, so transitions of actions inside an accepting MEC are never constrained by data, and EVI (Algorithm 2) assigns value 1 to every state in G× and hence to every action available there. A concrete failure: take an AMEC with states g1, g2, g3 and Rabin pair K={g2}, with actions at g1 leading to g2 or g3, and at g3 a self-loop; both actions from g1 have optimistic reach-avoid value 1, but the policy that chooses the path to g3 and then self-loops forever has reach-avoid value 1 and LTL satisfaction probability 0. Thus per-episode regret can be 1 for all K, contradicting the O(√K) bound of Theorem 5.1. The algorithm must compute an accepting policy for each AMEC (one that stays in the AMEC and visits some Ki infinitely often with probability 1) and use it once G× is entered, and Theorem 5.1 must be proved for that composite policy.","section":"Section 5, Algorithm 4; Theorem 5.1"},{"comment":"The pseudocode does not reset the current state to sinit at the start of an episode; it only resets when st∈B. The proof in Section 4.2 repeatedly states that 'every episode starts at sinit', and the regret Δk = v*(sinit)−vk(sinit) is defined for a policy executed from sinit. If an episode ends by deadline at a state outside G∪B, the next episode continues from that state, so the executed trajectories do not match the probabilities vk(sinit), and the martingale arguments over episodes are not justified. Please either add an explicit reset st←sinit at the beginning of each episode in Algorithm 1, or revise the analysis to account for the actual continuation state.","section":"Algorithm 1; Section 4.2"},{"comment":"Lemma B.1's bound Λ requires that B contains every maximal end component whose intersection with G is empty. This is not an assumption of Problem 1, which only gives B as the Avoid states of the until formula, and it is not checked or enforced by Algorithm 1. If the MDP has a closed recurrent class disjoint from G and B, then from states in S\\B there is no positive-probability guarantee of reaching G, and the hitting-time bound (21), hence the logarithmic bound on αK in Lemma 4.4, fails. The reach-avoid theorem must either assume this graph-dependent condition, or Algorithm 1 must first learn the MECs (e.g., using Algorithm 5) and enlarge B accordingly.","section":"Lemma B.1 and Lemma 4.4"},{"comment":"The union bound in the proof of Theorem 4.2 combines the failure probabilities 5δ/6, δ/6, and δ from Lemmas 4.5–4.7, but does not include the δ/3 failure probability of Lemma 4.1 for the event E that the true MDP lies in every Mk. Lemmas 4.5 and 4.7 use the confidence interval (3), which is valid only on E. The proof should either condition on E and add δ/3 to the failure budget, or state explicitly where this δ/3 is already absorbed in the stated probabilities; as written, the claimed confidence 1−2δ does not follow.","section":"Section B.6, proof of Theorem 4.2"},{"comment":"The graph-learning algorithm requires, for every s∈S\\{sinit}, a policy under which s is reachable from sinit with positive probability. For states that are not reachable in the true MDP, no such policy exists, and the outer while loop 'while n(s,a)<n*' can never terminate because the target (s,a) is never visited. The sample-complexity theorem (Theorem A.2) and the algorithm need to handle unreachable states explicitly (e.g., by characterizing the reachable set first or by treating unreachable states as having no outgoing transitions), or the theorem needs an additional assumption that all states are reachable.","section":"Appendix A, Algorithm 5"}],"minor_comments":[{"comment":"The call to Reach in Algorithm 5 contains an empty argument: 'Reach(S, A, s, , δ, pmin)' should be 'Reach(S, A, s, δ, pmin)'.","section":"Algorithm 5"},{"comment":"The caption contains a typo: 'algorithcm' should be 'algorithm'.","section":"Figure 4 caption"},{"comment":"The sentence 'This is ensured by Eq. (6)' is not a direct consequence of the displayed inequality, since Eq. (6) is only an upper bound on v*; the proof should make explicit that the optimistic MDP has value at least v*, so that the greedy policy has positive reachability probability in the optimistic model.","section":"Lemma B.1 proof"}],"recommendation":"major_revision","confidential_remarks":"The LTL gap in Section 5 is the headline issue: the reduction computes reach-avoid optimal values but not LTL-optimal policies. I believe this is fixable by composing the reach-avoid policy with an accepting MEC policy, but the revision must also address the reach-avoid reset inconsistency, the missing B condition in Lemma B.1, and the confidence accounting in Theorem 4.2. Given the novelty of a regret-free LTL synthesis claim, I recommend major revision rather than reject."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the quick take: the paper's headline claim—sublinear regret for LTL synthesis—doesn't survive close reading of Section 5. The reach-avoid core is real and likely correct, but the LTL reduction has a load-bearing gap that the authors need to fix before the main theorem means what it says.\n\nWhat's genuinely new: for reach-avoid (until) formulas on finite MDPs with unknown transitions, the paper gives the first O(√K) regret bound, using optimistic iMDP value iteration with deadlines and resets, and it handles non-communicating MDPs—an advance over Tarbouriech et al. and Fruit et al. The graph-learning preprocessing with pmin is a reasonable extra, and the experiments show fast practical convergence. The writing is mostly clear and the comparison to ω-PAC is fair.\n\nThe problem is Theorem 5.1. The reduction to reachability of accepting MECs is standard for values, but the algorithm never constrains the policy inside those MECs. EVI treats G× as absorbing and episodes stop on first visit, so transitions inside an accepting MEC are never sampled and the returned argmax policy is arbitrary. A tie-break can pick an action that stays in the MEC but never visits the Rabin set K_i (or leaves the AMEC), making the true LTL satisfaction probability zero while the reach-avoid value is one. Then per-episode regret is one and R(K)=K. Nothing in Alg. 4 or the proof of Thm. 5.1 replaces the EVI policy inside each AMEC with an accepting policy. This is fixable—standard MEC theory gives an accepting positional policy, and changing the policy only inside G× doesn't change reach-avoid probabilities—but as written the LTL claim is not established.\n\nThree smaller soft spots. First, Lemma B.1 assumes B contains every non-goal MEC, but Problem 1 doesn't state that; without graph knowledge the user can't supply such a B, so Thm. 4.2 needs an extra assumption or a graph-learning preprocessing step. Second, the confidence bookkeeping in Thm. 4.2 seems to drop the δ/3 from Lemma 4.1; the union bound gives 1-7δ/3 unless the δ's are redefined. That's likely repairable but needs writing out. Third, the graph-learning pseudocode (Algs. 5/6) is rough and the bound leans on the external ω-PAC sample complexity; this part needs tighter presentation.\n\nBottom line: the reach-avoid result deserves a serious referee and likely publication after revision; the LTL theorem needs the AMEC policy fix plus proof-surgery on the union bound. I'd send it to review, but I'd expect major revision.","headline":"The reach-avoid regret bound is a solid, novel start, but the LTL extension's central theorem is not supported: the policy inside accepting MECs is never constrained to be accepting, so the O(√K) regret claim holds only for a reach-avoid surrogate, not for LTL satisfaction.","tokens_in":24303,"tokens_out":8910,"would_cite":true,"duration_ms":87475,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper gives the first regret-free online algorithm for learning LTL controllers on unknown finite MDPs, proving $O(\\sqrt{K})$ regret.","keywords":["regret-free reinforcement learning","LTL synthesis","Markov decision processes","reach-avoid specifications","interval MDP","optimistic value iteration","graph identification","finite-time guarantees"],"falsifier":"Construct an MDP whose only route to the goal is a single edge of transition probability $p_{\\min}/2$, and run Algorithm 1 while feeding the algorithm $p_{\\min}$ as the lower bound. If the normalized regret still vanished, the theorem would be contradicted, because the hitting-time bound $\\Lambda$ relies on every useful transition having probability at least $p_{\\min}^{|S|}$; with the smaller true probability, the number of slow episodes need not stay sublinear.","tokens_in":23009,"feed_emoji":"🎯","tokens_out":9825,"duration_ms":89650,"temperature":0.7,"pith_summary":"This paper claims that an agent can learn a controller for an unknown finite Markov decision process against linear temporal logic (LTL) specifications with a finite-time regret guarantee: after $K$ learning episodes, the accumulated gap from the optimal satisfaction probability is $O(\\sqrt{K})$, so the average gap tends to zero. The guarantee is the first of its kind; earlier LTL reinforcement-learning algorithms only proved asymptotic convergence, which says nothing about how close the current policy is during learning. The paper's route is to reduce general LTL objectives to infinite-horizon reach-avoid problems via automata and graph identification, and to solve the reach-avoid core with an optimistic interval-MDP algorithm that resets from bad states and caps each episode with a deadline. If the proof is right, a designer can stop learning after finitely many episodes and certify how far the current policy is from optimal, with confidence at least $1-2\\delta$.","feed_headline":"LTL controller learning now comes with a finite-time guarantee","feed_subtitle":"An online algorithm provably closes the gap to optimal temporal-logic satisfaction at a predictable rate, not just in the limit.","key_machinery":"The engine is an interval MDP (iMDP): at each episode, all observed transitions are summarized as a confidence interval around the empirical transition probabilities, chosen so the true MDP lies inside with high probability. Extended value iteration then picks, within that interval set, the most optimistic MDP and its optimal reach-avoid policy, a standard optimism-in-the-face-of-uncertainty move. What makes the regret analysis work is a per-episode deadline $H_k$, defined as the smallest $n$ for which a substochastic hitting-time matrix raised to the $n$-th power has norm at most $k^{-1/q}$, together with a reset rule that sends any visit to a bad state back to the initial state. Long (slow) episodes whose deadline is exceeded turn out to be rare enough that their total contribution is sublinear, while short (fast) episodes contribute only through the confidence radii and a martingale term, giving the $O(\\sqrt{K})$ total. For general LTL, a known minimum transition probability $p_{\\min}$ makes the underlying graph learnable in polynomial time, and the graph reveals the maximal end components (MECs) of the product MDP, which are declared accepting or non-accepting and become the goal and bad sets of the reach-avoid reduction.","core_discovery":"The central claim is Theorem 4.2 and Theorem 5.1: for reach-avoid (until) formulas on any finite MDP with unknown transitions, the ZeroReg algorithm (Algorithm 1) achieves regret $R(K)=O(\\sqrt{K})$ with probability at least $1-2\\delta$, and for general LTL formulas the automaton-based reduction (Algorithm 4, using a graph learner that assumes a known lower bound $p_{\\min}$) achieves the same order of regret with probability at least $1-\\delta$. Regret is the accumulated difference between the optimal satisfaction probability and the satisfaction probability of each learned policy. The proof also shows the longest episode grows only logarithmically with $K$, which is what makes the bound genuinely sublinear rather than a disguised $O(K)$. Consequently the normalized regret $R(K)/K$ tends to zero, so a user can stop learning once the normalized regret is below a chosen threshold and trust the current policy to be near-optimal with the stated confidence.","pith_inferences":["Because the proof uses only hitting-time bounds and resets, the same deadline-and-reset scheme is a plausible template for regret guarantees on other undiscounted objectives, such as mean-payoff and average-reward specifications, and on stochastic shortest path problems where the goal is reached almost surely.","The bound grows exponentially in the state count through the parameter $\\Lambda$, so the practical reach of the guarantee is likely limited to small- or medium-sized MDPs even though the asymptotics in $K$ are strong; testing the observed gap against the theorem's constants on larger grids would reveal how much slack the analysis carries.","A direct empirical probe of the graph learner would be to run Algorithm 5 on MDPs whose minimum nonzero probability is exactly $p_{\\min}$ and slightly above it, checking whether the sample-complexity bound is tight or whether the true required samples are far smaller."],"forward_implications":["Reach-avoid synthesis on an unknown finite MDP can be stopped after finitely many episodes with a certified distance to optimal: once $R(K)/K < \\varepsilon$, the average satisfaction probability is within $\\varepsilon$ of optimal with confidence at least $1-2\\delta$.","General LTL objectives inherit the same guarantee through the automaton product, provided the graph has been learned, so infinite-horizon temporal specifications become verifiable during the learning phase rather than only in the limit.","The algorithm works from a fixed initial state without a generative model, which matches control and robotics settings where arbitrary resets are impossible.","Non-communicating MDPs, including the product MDPs that arise from LTL automata, are handled explicitly, because the reset mechanism replaces the communicating-MDP assumption used by earlier UCRL-style algorithms.","The graph learned from $p_{\\min}$ is independent of the LTL formula, so one graph-learning pass can be reused for many specifications on the same dynamics."],"supporting_citations":[{"why":"Supplies the UCRL2 template: confidence intervals around empirical transitions, extended value iteration, and the optimism bound that gives Eq. (6).","marker":"Auer et al., 2008"},{"why":"Supplies the interval-MDP construction, the confidence-set lemma, and the hitting-time lemma that underlie the episode deadlines and slow-episode count.","marker":"Tarbouriech et al., 2020"},{"why":"Supplies the theory of maximal end components, the Rabin automaton semantics for LTL, and the MEC-decomposition algorithm used in the LTL reduction.","marker":"Baier & Katoen, 2008"},{"why":"Supplies the sample bound (Lemma A.1) that certifies when a zero empirical transition count proves the transition is absent, given $p_{\\min}$.","marker":"Voloshin et al., 2022"},{"why":"Supplies the $\\omega$-PAC reachability policy sample complexity used in graph learning, and serves as the empirical baseline.","marker":"Perez et al., 2024"},{"why":"Supplies the E3 exploration scheme that motivates the reachability policies used to visit every state during graph learning.","marker":"Kearns & Singh, 2002"},{"why":"Supplies the matrix-analytic hitting-time bound used to control the probability that an episode exceeds its deadline.","marker":"Latouche & Ramaswami, 1999"},{"why":"Supplies the contraction property of the Bellman operator that guarantees the extended value iteration terminates.","marker":"Bertsekas, 2012"}],"fun_headline_variants":["First finite-time regret bounds for LTL controller learning","Regret-free LTL synthesis with O(sqrt(K)) guarantee","Sublinear regret for temporal-logic control","LTL controller learning closes gap at predictable rate"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole guarantee rests on knowing a positive lower bound $p_{\\min}$ on every nonzero transition probability, plus knowing (or learning in advance) which maximal end components of the MDP cannot reach the goal; if either is missing, the stated $O(\\sqrt{K})$ regret bound is not established.","fun_headline_variants_meta":{"raw":{"variants":["First finite-time regret bounds for LTL controller learning","Regret-free LTL synthesis with O(sqrt(K)) guarantee","Sublinear regret for temporal-logic control","LTL controller learning closes gap at predictable rate"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000686,"raw_usage":{"total_tokens":3099,"prompt_tokens":923,"completion_tokens":2176,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":539,"completion_tokens_details":{"reasoning_tokens":2113}},"tokens_in":539,"tokens_out":2176,"duration_ms":15992,"temperature":1.0,"reasoning_tokens":2113,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:00:26.789748+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct an MDP whose only route to the goal is a single edge of transition probability $p_{\\min}/2$, and run Algorithm 1 while feeding the algorithm $p_{\\min}$ as the lower bound. If the normalized regret still vanished, the theorem would be contradicted, because the hitting-time bound $\\Lambda$ relies on every useful transition having probability at least $p_{\\min}^{|S|}$; with the smaller true probability, the number of slow episodes need not stay sublinear.","supporting_citations":[{"cited_title":"No-regret exploration in goal-oriented reinforcement learning","cited_arxiv_id":null,"evidence_quote":"Supplies the interval-MDP construction, the confidence-set lemma, and the hitting-time lemma that underlie the episode deadlines and slow-episode count."},{"cited_title":"and Katoen, J.-P","cited_arxiv_id":null,"evidence_quote":"Supplies the theory of maximal end components, the Rabin automaton semantics for LTL, and the MEC-decomposition algorithm used in the LTL reduction."},{"cited_title":"M., Chaudhuri, S., and Yue, Y","cited_arxiv_id":null,"evidence_quote":"Supplies the sample bound (Lemma A.1) that certifies when a zero empirical transition count proves the transition is absent, given $p_{\\min}$."},{"cited_title":"and Singh, S","cited_arxiv_id":null,"evidence_quote":"Supplies the E3 exploration scheme that motivates the reachability policies used to visit every state during graph learning."}],"review_version":1}