{"id":"8d3d107b-0a48-45a4-8a6b-719481284346","arxiv_id":"1909.00526","paper_version":4,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"TL-RRT* is a tree-based, abstraction-free sampling planner for multi-robot LTL tasks, claimed to be probabilistically complete and asymptotically optimal.","lead":"TL-RRT* grows sampling trees in the combined space of robot positions and Büchi automaton states to synthesize multi-robot plans for linear temporal logic tasks without building a discrete abstraction of the environment. The paper claims probabilistic completeness and asymptotic optimality for both unbiased and biased versions, with simulations showing faster planning than three existing methods.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The biased suffix construction cannot find accepting cycles whose chosen Büchi state appears only once per period, so the completeness and optimality claims for the biased variant (Corollaries 6.4 and 6.6) are unsupported.","rationale":"The reader's rationale identified the biased suffix gap as the load-bearing weakness, and I agree that it is the decisive issue for the paper's central claim. However, the reader's formal 'weakest_assumption' was Assumption 6.2, the label-stability condition at region boundaries, rather than the automaton-cycle coverage gap. The two are distinct: the biased suffix problem invalidates the biased-variant guarantees even in a world where Assumption 6.2 holds. The unbiased algorithm may be salvageable, since it uses Eq. (9) to close cycles through arbitrary Büchi transitions into the root state, but the abstract and contributions explicitly claim completeness and asymptotic optimality for the algorithm with and without bias. The experimental section also relies on the biased variant for scalability, so this is not a peripheral claim. The proof gap is concrete: Appendix D reduces the biased-suffix correctness to 'RRT* is probabilistically complete and finds return paths', but the return path is required to be observation-free, and no argument shows that every accepting lasso can be routed through a non-root state carrying the root's accepting Büchi component plus an observation-free path to the root. The proposed fix of replacing the biased suffix with the same Eq. (9) goal set would likely restore correctness, but that is not what the paper proves. A REJECT verdict is appropriate because the central advertised guarantee for the biased algorithm is not established and the described algorithm is incomplete for natural LTL formulas such as repeated visits to two regions. I did not base the assessment on disagreement with any consensus, nor on any ad hominem reading; the issue is an internal mismatch between the algorithm's cycle-detection rule and the accepting-cycle structure of Büchi automata.","tokens_in":69157,"tokens_out":17240,"duration_ms":318919,"concrete_test":"Run the released TL-RRT* code on a two-region workspace with the LTL formula φ = □♦a ∧ □♦b, using a degeneralized NBA whose accepting state qF is reachable only on b and has no b-self-loop, so the accepting cycle is qF --a--> q' --b--> qF. Start the robot outside both regions, give the biased variant a large iteration budget, and record whether any plan is returned. Then run the unbiased variant on the same setup. If the unbiased variant returns a plan and the biased variant does not, the biased suffix's observation-free-return restriction is confirmed as the cause. To isolate the mechanism further, instrument the biased suffix to also accept the Eq. (9) goal set; if plans then appear, the missing automaton transition into the root is confirmed.","verdict_should_be":"REJECT","load_bearing_attack":"The paper's headline claim covers both unbiased and biased TL-RRT* (Theorems 6.3/6.5 and Corollaries 6.4/6.6). The unbiased suffix construction closes an accepting cycle through the goal set Qsuf_goal defined in Eq. (9): any product state from which an automaton transition into the root's Büchi state is enabled. The biased variant in Section V-B replaces this with a different construction: it stores only nodes whose Büchi component equals the root's accepting state and then requires an observation-free geometric return path to the root, treating all labeled regions as obstacles. This strictly restricts the class of accepting cycles that can be found. Standard accepting lassos can have the chosen accepting state exactly once per period; for example, a degeneralized NBA for □♦a∧□♦b can have an accepting cycle qF --a--> q' --b--> qF with qF appearing only at the period boundary and no self-loop under the root label. The biased suffix has no non-root qF node at which to attach the observation-free return, so it cannot complete this cycle. Corollary 6.4's proof in Appendices B and D argues only that biased sampling makes the tree dense and that RRT* can find continuous return paths; it never proves that the biased suffix's automaton-level cycle construction covers all accepting runs. Thus the central claim that both variants are probabilistically complete and asymptotically optimal fails as stated, even if Assumption 6.2 were granted.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes TL-RRT*, a sampling-based planner for multi-robot systems under global LTL−© specifications. It grows trees in the product of the continuous free workspace and the Büchi automaton, avoiding discrete abstractions, and extracts prefix-suffix plans from accepting nodes. A biased sampling variant, guided by shortest paths in the Büchi automaton, is introduced to accelerate plan construction. The paper claims probabilistic completeness and asymptotic optimality for both the unbiased and biased variants (Theorems 6.3 and 6.5, Corollaries 6.4 and 6.6) and reports simulations comparing favorably with SMC, RRG, and synergistic methods.","tokens_in":69470,"tokens_out":14714,"duration_ms":155761,"significance":"If the claims were correct, the contribution would be significant: an abstraction-free tree-based LTL planner with probabilistic completeness and asymptotic optimality, plus a biased variant that scales to larger teams. The paper has real strengths: the product-space tree construction is a natural extension of RRT*; the unbiased suffix closing via a direct transition into the root is a clean lasso construction; the biased sampling mechanism is described in concrete detail; and the experimental section includes comparisons to established methods with code availability stated. However, the central correctness claims are not established as written. The biased suffix construction restricts accepting cycles to a special class, and the key Assumption 6.2 fails in general labeled environments. These issues affect the headline claims and require substantial revision.","major_comments":[{"comment":"The biased suffix construction does not realize general accepting lassos. The algorithm stores only nodes whose Büchi component equals the root's accepting state and then connects them to the root by RRT* paths that treat all labeled regions as obstacles. Therefore the only accepting cycles it can close are those in which the accepting state is re-entered and then followed by an observation-free segment that keeps the automaton in that accepting state until the root. This excludes lassos in which the accepting state must be exited immediately through a labeled transition. For example, a standard degeneralized NBA for □♦a∧□♦b has an accepting state qF with transitions qF --a--> q1 and q1 --b--> qF and no qF --∅--> qF self-loop; the qF state is visited in a position labeled a, so the label-free geometric return required by Section V-B either does not exist or changes the infinite word by omitting the required visit to a. Appendix B argues only that RRT* can find continuous return paths and that biased sampling densifies the tree; it never proves that the automaton-level cycle set generated by storing same-Büchi-component nodes covers all accepting runs. Consequently Corollaries 6.4 and 6.6 are unsupported.","section":"Section V-B, Corollaries 6.4 and 6.6"},{"comment":"Assumption 6.2 fails at boundaries of labeled regions. For any reachable product state (x,qB) with x ∈ ∂𝓁j, every ball Bδ(x) contains positions whose observation differs from L(x), and those positions need not be pairable with the same Büchi state qB or reachable from the root. Since Theorems 6.3 and 6.5 invoke Assumption 6.2 for every state along candidate paths, the results are conditional on an assumption that is not implied by the environment model in Definition 3.1 and Assumption 6.1. The paper should either prove Assumption 6.2 for the considered class of environments or explicitly restrict the theorems to label-stable paths, for example paths with positive clearance from every region boundary, and justify why such paths suffice for the claimed completeness and optimality.","section":"Section VI, Assumption 6.2"},{"comment":"The asymptotic optimality proof is incomplete as written. Appendix C states 'We omit the details due to space limitations' for event E3_n, which is needed to bound the cost of the reconstructed path by (1+ε)J(τ*) and to rule out zig-zag approximations. The argument that P(E1_n|E2_n) → 0 also treats cn, the number of balls crossed by a boundary, as 'small' without a formal bound; this is a geometric and probabilistic quantity that deserves a rigorous analysis. Theorem 6.5 therefore rests on an omitted proof step.","section":"Appendix C, proof of Theorem 6.5"},{"comment":"The connection radius rn(VT) uses a constant γ_TL-RRT* whose lower bound contains the unknown optimal cost J(τ*). Section VII-A acknowledges that (7) cannot be computed and replaces it with the heuristic radius (17) in the experiments. Thus the implemented algorithm does not run in the parameter regime of Theorem 6.5, and the experiments support only the heuristic version. The paper should specify how γ_TL-RRT* is chosen before planning, or state the theorem as an existence result for all sufficiently large γ and treat the practical radius separately.","section":"Section IV-A, Eq. (7)-(8)"}],"minor_comments":[{"comment":"The symbol P is used both for the product Büchi automaton and for the set of goal nodes in Algorithm 1; these uses should be renamed to avoid confusion.","section":"General"},{"comment":"The sentence describing the biased suffix construction is ambiguous: it is unclear whether a node whose Büchi component equals the root's accepting state is added to the tree in addition to being stored in the set P.","section":"Section V-B"},{"comment":"Table III is difficult to read: several columns are visually merged, and the remark that 'the 0 standard deviation is dropped' is unexplained. Please reformat the tables and state what each column contains.","section":"Tables II and III"},{"comment":"There are typos such as 'prune NBA' for 'pruned NBA' and 'succesive' for 'successive'; a copyedit pass is needed.","section":"Section V-A"},{"comment":"The notation in Eq. (7) and Eq. (17) uses different exponents (1/(dim+1) versus 1/dim). The text explains this, but a short comment near the definitions would prevent reader confusion.","section":"Section VI"}],"recommendation":"major_revision","confidential_remarks":"The biased-suffix issue is severe and affects the central claims. I would ask the authors either to redesign the biased suffix construction so that it searches a general product-level cycle, or to restrict the claims of Corollaries 6.4 and 6.6 to the class of lassos the current construction can realize. The omitted E3_n proof and the handling of Assumption 6.2 at region boundaries should also be addressed before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper has a genuinely new idea and a real gap. The new idea is TL-RRT*: growing RRT*-style trees directly in the product of the continuous workspace and the Büchi automaton, with no discrete abstraction of mobility. That combination is not in the cited literature, and the unbiased variant's prefix-suffix construction (via Eq. 9) is a clean way to close accepting cycles. The numerical comparisons against SYN, RRG, and SMC are extensive, and the biased version is clearly faster and lower-cost in practice. I would not dispute the novelty or the engineering value.\n\nThe soft spot is the biased suffix construction in Section V-B. The unbiased version closes the cycle through any product state that can transition back to the root's Büchi state. The biased version stores only nodes whose Büchi component equals the root's accepting state, then returns through an observation-free path that treats all labeled regions as obstacles. That only works when the accepting state can be maintained under the empty/true label. Standard Büchi automata for formulas like □♦a∧□♦b do not have that property: the accepting state can appear once per period, with the cycle passing through other states. The biased construction cannot realize those cycles, so the completeness and optimality claims for the biased variant (Corollaries 6.4 and 6.6) are unsupported. The proof in Appendix B shows that biased sampling makes the tree dense, but it never shows that the restricted suffix construction covers all accepting runs.\n\nTwo secondary issues. Assumption 6.2 (label stability around every reachable product state) fails at region boundaries, where an arbitrarily small move changes the observation. The proofs lean on it, so the guarantees are conditional on a condition that is not met in typical environments. And the theoretical radius (7) depends on the unknown optimal cost J(τ*); the experiments use the heuristic radius (17), so the theorem does not directly apply to the implementation.\n\nThe unbiased variant may be salvageable under a cleaner assumption. The biased variant needs a different suffix strategy or a restricted class of Büchi automata. As it stands, the paper overclaims for the biased algorithm.\n\nWho should read it: roboticists and formal-methods folks working on sampling-based LTL synthesis. It is worth citing for the tree-in-product-space idea. I would send it to peer review because the core idea is publishable after heavy revision, but I would not accept the biased guarantees as stated.","headline":"Novel abstraction-free LTL planner with a real completeness gap in the biased suffix construction.","tokens_in":69977,"tokens_out":7049,"would_cite":true,"duration_ms":64894,"reading_group":"yes","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 proposes TL-RRT*, an abstraction-free sampling-based planner that grows trees over the product of robot positions and Büchi automaton states, and proves it probabilistically complete and asymptotically optimal for multi-robot…","keywords":["multi-robot planning","linear temporal logic","Büchi automaton","sampling-based motion planning","RRT*","optimal control synthesis","probabilistic completeness","asymptotic optimality"],"falsifier":"Construct a workspace where the unique shortest path satisfying the LTL formula skims along the boundary between two labeled regions, so every neighborhood of the optimal path contains points with different observations. Run unbiased TL-RRT* with growing iteration limits and record whether the tree ever adds a node with the required Büchi state within a small distance of that boundary and whether the returned cost converges to $(1+\\epsilon)J^*$; if the success probability stays bounded away from 1, the label-stability assumption is the limiting step.","tokens_in":68931,"feed_emoji":"🤖","tokens_out":6980,"duration_ms":69355,"temperature":0.7,"pith_summary":"This paper proposes TL-RRT*, a sampling-based planner for multi-robot systems under Linear Temporal Logic (LTL) tasks that avoids the usual discrete abstraction of the workspace. The method grows randomized trees directly in the product of the continuous configuration space and the Büchi automaton representing the task, first finding a prefix that reaches an accepting automaton state and then a cycle that forms the infinite suffix. The paper claims that both the unbiased version and a biased version—which steers samples along shortest paths to accepting states in the automaton—are probabilistically complete and asymptotically optimal. If these guarantees hold, temporal-logic planning would no longer be limited by the size of an abstraction and could scale to large robot teams and complex tasks.","feed_headline":"Sampling can solve multi-robot temporal-logic tasks with no grid abstraction","feed_subtitle":"A tree over robot positions and automaton states is shown complete and near-optimal, scaling to dozens of robots.","key_machinery":"The central object is the tree $\\mathcal{T}$ whose nodes are product states $q_P=(x,q_B)\\in W^N_{\\mathrm{free}}\\times Q_B$ and whose edges are valid product transitions: a continuous move $x\\to x'$ combined with a Büchi transition $q_B\\xrightarrow{L(x)}q'_B$ enabled by the observation at the starting position. Three mechanisms carry the argument: Extend/Rewire with a connection radius $r_n(V_\\mathcal{T})$, which keeps the structure a tree while improving costs; the prefix-suffix decomposition of satisfying plans, which turns the infinite-horizon LTL task into two reachability problems; and biased sampling, which selects nodes close to accepting Büchi states and steers new samples toward the labeled regions required by the next automaton transition. The optimality proof covers a robust near-optimal product path by shrinking balls and shows that, with the stated radius, every ball eventually contains a sample whose label preserves the needed Büchi transition.","core_discovery":"The central claim is that optimal multi-robot LTL planning can be solved by RRT*-style tree search over the product state space $W^N_{\\mathrm{free}}\\times Q_B$, without constructing a discrete transition system. The tree grows by sampling configurations, steering toward them, and connecting a new node to the minimum-cost feasible parent in a neighborhood (Extend), then rewiring neighbors (Rewire); an edge is valid only if the straight-line motion is obstacle-free, crosses each labeled region boundary at most once, and the label enables a Büchi transition. The same construction, repeated with a root at an accepting state, produces a suffix cycle. The main theorems assert that as the iteration limits go to infinity, the probability of finding a feasible plan goes to 1, and the cost of the returned plan is at most $(1+\\epsilon)$ times optimal, for both unbiased and biased sampling, with a larger connection radius required in the biased case.","pith_inferences":["The label-stability assumption suggests a concrete hybrid extension: combine tree sampling with boundary-aware states or local cell decomposition near region boundaries, so that optimal paths which hug a boundary can still be approximated without the assumption failing.","The biased-sampling machinery depends only on having a distance metric over automaton states, so it could be ported to other automata (for example, parity or Rabin automata) or to non-Euclidean cost functions, with the same two-hop steering structure.","Because the proof's connection radius uses the unknown optimal cost, a practical refinement would be to estimate $J^*$ adaptively from the current tree costs, or to use radius zero for initial feasibility and then switch to a rewiring radius for refinement; the paper's simulations already show radius zero is effective for scalability.","A testable extension would add observation noise or require the robots to stay inside small neighborhoods of waypoints; the paper's Remark 4.1 suggests such robustness informally, and the same prefix-suffix tree construction could be re-run with inflated regions to quantify the resulting cost loss."],"forward_implications":["For LTL tasks without the next operator, TL-RRT* returns a prefix-suffix plan whose continuous execution provably satisfies the formula, covering sequencing, surveillance, and intermittent-connectivity tasks directly in continuous space.","With either unbiased or biased sampling, the probability of finding a feasible plan tends to 1 as the iteration limit grows, so no precomputed discrete abstraction is needed for completeness.","The biased variant is claimed to scale to dozens of robots (experiments go up to 56 robots) and to find lower-cost first feasible plans than the RRG, synergistic, and SMC baselines.","As the number of iterations grows, the returned plan's cost satisfies $J \\le (1+\\epsilon)J^*$, so longer runs trade computation for near-optimality.","Because only trees are stored, retrieving a plan is $O(|V_\\mathcal{T}|)$, avoiding the graph-search overhead of product-automaton methods."],"supporting_citations":[{"why":"Supplies the RRT* extend/rewire machinery and the optimality framework that TL-RRT* adapts to a product state space.","marker":"[6]"},{"why":"Provides the corrected proof technique, including robust paths and ball covering, used in the asymptotic-optimality proofs.","marker":"[47]"},{"why":"Supplies the RRT nearest-neighbor growth argument that the completeness proof adapts to one-hop-reachable product states.","marker":"[4]"},{"why":"Provides LTL semantics, the translation of LTL to Büchi automata, and the prefix-suffix structure of satisfying plans.","marker":"[11]"},{"why":"Introduces the idea of biasing sampling toward shortest paths to accepting Büchi states that the biased version builds on.","marker":"[30]"},{"why":"Details that biased sampling scheme, including NBA pruning and two-hop successor selection, extended here to continuous spaces.","marker":"[31]"},{"why":"Supplies the RRG baseline and the transition condition that a segment crosses each region boundary at most once.","marker":"[42]"},{"why":"Supplies the synergistic high-level/low-level planner baseline whose discrete abstraction TL-RRT* avoids.","marker":"[43]"},{"why":"Supplies the satisfiability-modulo-convex (SMC) baseline used for runtime and cost comparisons.","marker":"[38]"}],"fun_headline_variants":["Tree search replaces grids for multi-robot LTL synthesis","Abstraction-free LTL planning scales to dozens of robots","RRT* proves optimal for temporal logic multi-robot tasks","Sampling trees solve LTL tasks without discrete abstractions","No grid abstraction: Tree search yields optimal LTL plans"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that around every reachable position a small neighborhood exists in which the robot sees the same regions and the same Büchi transitions remain enabled—a condition that generally fails on the boundary of a labeled region.","fun_headline_variants_meta":{"raw":{"variants":["Tree search replaces grids for multi-robot LTL synthesis","Abstraction-free LTL planning scales to dozens of robots","RRT* proves optimal for temporal logic multi-robot tasks","Sampling trees solve LTL tasks without discrete abstractions","No grid abstraction: Tree search yields optimal LTL plans"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000561,"raw_usage":{"total_tokens":2671,"prompt_tokens":962,"completion_tokens":1709,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":578,"completion_tokens_details":{"reasoning_tokens":1626}},"tokens_in":578,"tokens_out":1709,"duration_ms":12056,"temperature":1.0,"reasoning_tokens":1626,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T05:48:00.108112+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a workspace where the unique shortest path satisfying the LTL formula skims along the boundary between two labeled regions, so every neighborhood of the optimal path contains points with different observations. Run unbiased TL-RRT* with growing iteration limits and record whether the tree ever adds a node with the required Büchi state within a small distance of that boundary and whether the returned cost converges to $(1+\\epsilon)J^*$; if the success probability stays bounded away from 1, the label-stability assumption is the limiting step.","supporting_citations":[{"cited_title":"Revisiting the asymptotic optimality of rrt,","cited_arxiv_id":null,"evidence_quote":"Provides the corrected proof technique, including robust paths and ball covering, used in the asymptotic-optimality proofs."},{"cited_title":"Rrt-connect: An efficient approach to single-query path planning,","cited_arxiv_id":null,"evidence_quote":"Supplies the RRT nearest-neighbor growth argument that the completeness proof adapts to one-hop-reachable product states."},{"cited_title":"Baier and J.-P","cited_arxiv_id":null,"evidence_quote":"Provides LTL semantics, the translation of LTL to Büchi automata, and the prefix-suffix structure of satisfying plans."},{"cited_title":"Temporal logic optimal control for large-scale multi-robot sys- tems: 10 400 states and beyond,","cited_arxiv_id":null,"evidence_quote":"Introduces the idea of biasing sampling toward shortest paths to accepting Büchi states that the biased version builds on."},{"cited_title":"Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,","cited_arxiv_id":null,"evidence_quote":"Details that biased sampling scheme, including NBA pruning and two-hop successor selection, extended here to continuous spaces."},{"cited_title":"Sampling-based temporal logic path plan- ning,","cited_arxiv_id":null,"evidence_quote":"Supplies the RRG baseline and the transition condition that a segment crosses each region boundary at most once."},{"cited_title":"Sampling-based motion planning with temporal goals,","cited_arxiv_id":null,"evidence_quote":"Supplies the synergistic high-level/low-level planner baseline whose discrete abstraction TL-RRT* avoids."},{"cited_title":"Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming,","cited_arxiv_id":null,"evidence_quote":"Supplies the satisfiability-modulo-convex (SMC) baseline used for runtime and cost comparisons."}],"review_version":1}