{"id":"6a4a6f1b-ef7c-4d19-8503-0c1a825b9852","arxiv_id":"1908.01896","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new task representation makes sequential robot plans reactive and robust by always running the most downstream available operator, with a probabilistic convergence guarantee.","lead":"This paper presents Robust Logical-Dynamical Systems, a task representation where a robot executes the most downstream available operator, automatically creating retry and recovery behaviors. It proves a convergence bound and demonstrates the approach on kitchen manipulation tasks in simulation and on a real robot.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's proof is under-specified: p_i is not defined as conditional on entry, so the p^N multiplication is unjustified without either independence or a chain-rule formalization; the proof also models failures as full resets, which Alg. 1 does not guarantee.","rationale":"The reader's conditional verdict remains appropriate. The independence concern is not the most precise diagnosis: under a natural conditional-on-entry reading, Theorem 1's p^N step is justified by the chain rule, so adding an independence assumption is not the right fix. The real issue is that the paper never defines the probability space or states whether p_i is conditional on entry, and the proof's reset-to-start model is not exactly the execution semantics of Algorithm 1. These are formalization gaps, not necessarily fatal errors: the theorem is likely correct under a charitable formalization, but the proof as written is incomplete. Empirical results are not affected. No code release and small trial counts are secondary. Since the reader already assigned CONDITIONAL and asked for clarification, no verdict change is needed; the requested revision should be to formalize p_i and the failure-reset assumption rather than merely to assert independence.","tokens_in":12160,"tokens_out":22161,"duration_ms":225079,"concrete_test":"Formalize Theorem 1 with an explicit probability space: for a complete RLDC, define p_i(s) as the probability that executing operator i from any state s in L_i^P reaches L_i^E before infeasibility, with p_i(s) >= p > 0. Verify analytically whether P(E_1 and ... and E_N) >= p^N follows from the chain rule without any independence assumption. Then run a simulation of the N=2, p=0.5 RLDC under two semantics: (a) failures reset to the start (L_i^P = L_i^R), and (b) failures allow same-state re-entry (L_i^P strictly weaker than L_i^R). Compare measured E[T] with N/p^N = 8 and check whether the tail bound P(K >= k) <= (1-p^N)^k holds in both cases; if E[T] > 8 or the tail bound fails, the theorem's proof needs revision.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central theorem's proof in Section IV-B multiplies per-operator success probabilities p_i to obtain p^N for a single pass through the chain. This step is valid only under one of two readings. If p_i is an unconditional marginal probability, multiplying requires independence (or a comparable positive-dependence assumption), which the paper neither states nor justifies. If p_i is instead intended as a lower bound on the probability of a controlled transition conditional on entering operator i, then the product follows from the chain rule without independence, but the paper never says so, and the proof's language ('with probability p_i') leaves the conditioning implicit. A further gap: the proof assumes every uncontrolled transition sends the system 'all the way back to the start' and treats attempts as independent geometric trials. Algorithm 1 permits re-entering the same operator when L_i^P remains true after L_i^R fails, so the stated pointwise formula for P_k is not the actual distribution of uncontrolled transitions. The expectation bound E[T] <= N/p^N may still be salvageable by a stochastic-dominance argument, but the proof as written does not establish it.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Robust Logical-Dynamical Systems (RLDS), a reactive task-execution representation in which a plan is represented as a chain of operators, each with an entry condition, run condition, effect, and an associated low-level policy. The authors contribute an algorithm for composing RLDS from sequential plans, a method for computing implicit logical conditions (Algorithm 2), a simple STRIPS-style planner integrated with RLDS execution (Algorithm 3), and a theoretical convergence result (Theorem 1) that claims almost-sure convergence to the goal with expected number of transitions bounded by N/p^N. The framework is evaluated in a simulated kitchen manipulation task with YCB objects, comparing linear execution, replanning, and reactive RLDS execution under nominal and adversarial conditions, and in a real-world demonstration with a Franka Panda arm.","tokens_in":12384,"tokens_out":8398,"duration_ms":94041,"significance":"If Theorem 1 can be stated and proved rigorously, the RLDS framework would provide a formal probabilistic convergence guarantee for reactive task execution with recovery, a property that is difficult to establish for behavior trees and related reactive frameworks. The paper also demonstrates a working integration with low-level Riemannian motion policies, automatic plan composition, and experiments with adversarial interference, which are valuable practical contributions. However, the central proof currently rests on unstated probabilistic assumptions about independence and reset behavior, and the execution algorithm does not fully match the model used in the proof. The theoretical contribution is therefore contingent on a repair of the theorem's statement and proof.","major_comments":[{"comment":"The definition of p_i is ambiguous, and the proof multiplies per-operator probabilities to obtain p^N. If p_i is a marginal probability of a controlled transition, the product requires an independence assumption across successive operator executions, which is neither stated nor justified. If p_i is instead intended as a lower bound on the probability of a controlled transition conditional on entering operator i, then the product can be justified by the chain rule, but the paper never states this conditional interpretation, nor does it define p_i uniformly over the continuous states from which operator i can be entered. In addition, the geometric model p_k = (1 - p^N)^k p^N assumes that each uncontrolled transition resets the system to the initial state and that successive runs are independent and identically distributed; these renewal assumptions are not stated. As written, Theorem 1 is not a theorem about the system described by Algorithm 1.","section":"Section IV-B, Theorem 1 proof"},{"comment":"The execution loop can fail to select any operator. When the current operator o_j becomes non-runnable, the first branch is blocked for i = j by the guard o_i != o_{t-1}, and if no other operator is enterable, the for loop completes without assigning o_t. The subsequent call to Step pi_i(x_t) then uses the leftover loop variable i, which is not a well-defined current operator. The completeness condition union_i L_i^P = S does not prevent this situation, because the currently guarded operator is excluded from re-entry. The algorithm needs an explicit default transition or a re-entry rule, and this rule must be consistent with the reset model used in the proof of Theorem 1.","section":"Section IV-C, Algorithm 1"},{"comment":"In the expectation derivation, the proof writes E[T] <= sum_{k=0}^infinity (k+1)N P_k, where P_k was previously defined as the cumulative probability of reaching the goal with at most k uncontrolled transitions. As written, this is not a valid expectation; the sum over cumulative probabilities diverges. The intended computation works with the exact-trial probabilities p_k = (1 - p^N)^k p^N, and the surrounding algebra shows that the stated result can be recovered. This notational error should be corrected, and the derivation should be rewritten using exact probabilities.","section":"Section IV-B, expectation bound"}],"minor_comments":[{"comment":"The notation uses the implication arrow between conditions that are also treated as sets of states; the paper should state explicitly that L_i^E => L_{i+1}^P means inclusion of the corresponding sets, i.e., L_i^E subset of L_{i+1}^P.","section":"Section IV-A, Eq. (1)"},{"comment":"The set-builder notation L_i^I = {rho in L_{i+1}^P union L_{i+1}^I forall rho not in L_i^E} is nonstandard; it should be written as {rho in L_{i+1}^P union L_{i+1}^I : rho not in L_i^E}.","section":"Section V-B, Algorithm 2"},{"comment":"The experimental section does not state how many trials were run per condition, and no statistical significance tests are reported. The differences in completion time between replanning and reactive execution are within one standard deviation, so the claim that reactive execution is 'more efficient' should be tempered or supported by a larger trial count.","section":"Section VI-B and Table I"},{"comment":"The phrase 'converging exponentially in the number of uncontrolled transitions k' is imprecise; the proof establishes that the cumulative success probability after at most k uncontrolled transitions is 1 - (1 - p^N)^{k+1}, which is an exponential approach to 1 in k. The theorem statement should state this explicitly.","section":"Section IV-B, Theorem 1 statement"},{"comment":"The real-world experiments are described qualitatively; reporting the number of trials, the number of failures, and the types of interference encountered would make the demonstration more reproducible and easier to assess.","section":"Section VI-D, real-world experiments"}],"recommendation":"major_revision","confidential_remarks":"The main theorem is the paper's central differentiator relative to behavior trees and other reactive frameworks. If the proof gap concerning independence and reset behavior cannot be closed within the scope of the revision, the paper's theoretical contribution would be substantially weakened, and the published version should clearly reposition the convergence claim as conditional on a renewal model. The notational issue in the expectation bound is easy to fix, but the ambiguity in the definition of p_i and the mismatch between Algorithm 1 and the proof model require careful reworking."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The genuinely new thing here is the RLDS formulation: splitting entry conditions from run conditions, and especially the backward-propagation of implicit conditions (Algorithm 2). I don't think that specific mechanism is in the BT/FSM/PDDL literature they cite, and it gives a clean way to turn a sequential plan into a reactive program with automatic fallback. The equivalence-to-BTs observation is a nice sanity check, and the framework does capture the practical notion of 'jump ahead when a later precondition is already true' more directly than a hand-built BT. On the empirical side, the real-world demo with adversarial interference is credibly reported, and the reactive plan matching or beating replanning is plausible.\n\nThe soft spots are real but not fatal. The proof of Theorem 1 is under-specified. The per-operator probability p_i is introduced without saying whether it is conditional on entering the operator. If it is unconditional, then multiplying p^N across N steps assumes independence (or something comparably strong), which the paper never states. If it is meant as conditional-on-entry, then the product follows by the chain rule, but the text doesn't say that. Either way, the proof as written doesn't establish the bound for the algorithm as described. The stress-test note is also right that Algorithm 1 can re-enter the same operator, not always reset to the start, so the geometric-trials model in the proof is not literally the system's behavior. I think the theorem can be salvaged — a stochastic-dominance argument with resets being the worst case would probably do it — but it needs rewriting.\n\nMinor points: no code or data released, which matters for reproducibility. The simulation comparison lacks a behavior-tree baseline, which would have been the natural competitor. The paper's own claims about 'theoretical guarantees' are therefore somewhat ahead of what the proof actually delivers.\n\nOverall: the framework is a solid, honest contribution to reactive task execution. It is not a new capability class — it is a cleaner way to build robust behavior that BTs and FSMs can express with more effort. The paper deserves a serious referee, but the referee should send it back for a fixed Theorem 1 proof and a bit more experimental discipline.","headline":"A useful reactive-execution framework with a genuinely new condition-propagation algorithm, but the headline convergence theorem has a fixingable proof gap and the empirical section is thin.","tokens_in":12877,"tokens_out":562,"would_cite":true,"duration_ms":7831,"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":"Task plans compiled into logical-dynamical chains converge to their goal with probability one when each step succeeds with nonzero bounded probability.","keywords":["robust logical-dynamical systems","behavior trees","reactive task execution","robot manipulation","task planning","convergence guarantee","markov logical state"],"falsifier":"Run a chain in simulation with $N=3$ operators where a failed operator pushes the continuous state further from the next precondition, so retry success probabilities decrease with each failure. If the mean number of transitions to reach the goal exceeds $N/p^N$ for the measured $p$, the independence assumption in the Theorem 1 proof is violated.","tokens_in":11974,"feed_emoji":"🤖","tokens_out":4749,"duration_ms":48122,"temperature":0.7,"pith_summary":"This paper proposes Robust Logical-Dynamical Systems (RLDS), a way to represent a robot task plan as a sequence of operators, each with entry conditions, run conditions, and effects. The central claim is that such a chain can be built automatically from an ordinary sequential plan and still behave reactively, retrying or skipping steps as the world changes. The paper further claims a convergence guarantee: if every operator induces a successful transition with probability at least p>0, the chain reaches its goal with probability one, and the expected number of transitions is at most N/p^N. The practical payoff is that recovery behaviors arise from the representation itself instead of being hand-wired into a finite state machine or behavior tree. A case study on a kitchen manipulation task supports this with simulated and real-world trials under adversarial interference.","feed_headline":"Reactive robot plans reach their goal with probability one","feed_subtitle":"A chain of logical operators bounds expected retries by N/p^N, no matter how often the world interferes.","key_machinery":"The central object is the Robust Logical-Dynamical Chain (RLDC), a sequence of operators $o_i = (L^P_i, L^R_i, L^E_i, \\pi_i)$ whose local chaining condition is $L^E_i \\Rightarrow L^P_{i+1} \\Rightarrow L^R_{i+1}$. Execution always favors the most downstream enterable operator, which implements both progress toward the goal and automatic fallback to earlier recovery operators when conditions fail. The theoretical analysis models each operator as either producing a controlled transition (its effect becomes satisfied) or an uncontrolled transition (the run becomes infeasible and the system resets to some enterable state), with the probability of controlled transitions bounded below by $p$. This abstraction is what lets the paper reduce convergence to a probabilistic argument over repeated traversals of the chain.","core_discovery":"The paper's discovery is that reactive robustness can be engineered by construction: a sequence of operators that obeys the chaining condition $L^E_i \\Rightarrow L^P_{i+1} \\Rightarrow L^R_{i+1}$ turns any sequential plan into a self-recovering controller. At every control tick the system picks the most downstream operator whose entry condition holds, and if the current run becomes infeasible it jumps to the most downstream enterable operator, which usually means backing up and retrying. The main theoretical result, Theorem 1, states that if each operator induces a controlled transition with probability $p_i \\geq p > 0$, the chain reaches the goal condition $L_G$ with probability 1, and the expected transition count is bounded by $N/p^N$. The proof treats each uncontrolled transition as a fresh attempt at traversing the whole chain, so the convergence rate is exponential in the number of uncontrolled transitions.","pith_inferences":["The proof multiplies per-step success probabilities, which presumes failures are independent across attempts; a natural extension would state Theorem 1 under conditional independence or a Markov assumption on the failure process, and the bound would likely still hold with a modified $p$.","If the probabilities $p_i$ are not fixed but depend on the continuous state, the geometric-trial argument no longer applies directly; estimating $p_i$ online from observed transitions could yield an adaptive version that reorders operators by reliability.","The same chain formalism could be applied outside robotics to any reactive discrete-event system whose actions have bounded success probabilities, such as automated assembly or dialogue managers, though the paper does not explore those domains.","A practical test of the bound: instrument a deployed RLDS to record the number of uncontrolled transitions before success; if the empirical distribution deviates strongly from the geometric form used in the proof, the independence assumption is being violated in that environment."],"forward_implications":["A sequential plan written as a list of operators can be compiled into an RLDS, so reactive recovery does not require manually programming fallback connections.","In the kitchen manipulation case study, reactive execution matched replanning on success rate while completing tasks faster, and it coped with a human closing the drawer or shoving the robot without replanning.","Because RLDS execution re-evaluates logical conditions at every tick, the system can skip ahead when a later step's preconditions become true, for example when an object accidentally lands in the drawer.","The convergence theorem gives a bound on expected time to goal, $N/p^N$, that can be used a priori to decide whether a chain of operators is reliable enough for a task.","Any Behavior Tree can be expressed as an RLDS and vice versa, so the framework inherits the expressiveness of Behavior Trees while adding a formal convergence statement."],"supporting_citations":[{"why":"Defines Behavior Trees and their composition rules, the main baseline the RLDS is compared against.","marker":"[4]"},{"why":"Supplies the low-level motion policy framework used by the case-study operators.","marker":"[5]"},{"why":"Defines the planning-domain language whose operator structure the RLDS mirrors.","marker":"[17]"},{"why":"Introduces the STRIPS planning formalism that the plan-and-execute algorithm builds on.","marker":"[25]"},{"why":"Provides the object dataset used in the simulated and real manipulation experiments.","marker":"[27]"},{"why":"Supplies the tracking technique used to estimate robot and cabinet state in the real-world trials.","marker":"[28]"},{"why":"Supplies the object pose detector used in the real-world experiments.","marker":"[29]"}],"fun_headline_variants":["RLDS turns sequential task plans into self-recovering controllers","Reactive robots with probability-one goal convergence via RLDS","Robust logical-dynamical systems: guaranteed goal reachability","Chain logical operators to make robot plans always converge"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that each operator's success probability $p_i$ stays bounded below by $p$ and that successive attempts are independent enough that the proof's multiplication $p^N$ is valid; if failures are correlated, the bound could fail.","fun_headline_variants_meta":{"raw":{"variants":["RLDS turns sequential task plans into self-recovering controllers","Reactive robots with probability-one goal convergence via RLDS","Robust logical-dynamical systems: guaranteed goal reachability","Chain logical operators to make robot plans always converge"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000269,"raw_usage":{"total_tokens":1588,"prompt_tokens":877,"completion_tokens":711,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":493,"completion_tokens_details":{"reasoning_tokens":645}},"tokens_in":493,"tokens_out":711,"duration_ms":8330,"temperature":1.0,"reasoning_tokens":645,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:59:44.256533+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a chain in simulation with $N=3$ operators where a failed operator pushes the continuous state further from the next precondition, so retry success probabilities decrease with each failure. If the mean number of transitions to reach the goal exceeds $N/p^N$ for the measured $p$, the independence assumption in the Theorem 1 proof is violated.","supporting_citations":[{"cited_title":"Behavior trees in robotics and AI: An introduction,","cited_arxiv_id":null,"evidence_quote":"Defines Behavior Trees and their composition rules, the main baseline the RLDS is compared against."},{"cited_title":"Pddl—the planning domain definition language,","cited_arxiv_id":null,"evidence_quote":"Defines the planning-domain language whose operator structure the RLDS mirrors."},{"cited_title":"STRIPS: A new approach to the appli- cation of theorem proving to problem solving,","cited_arxiv_id":null,"evidence_quote":"Introduces the STRIPS planning formalism that the plan-and-execute algorithm builds on."},{"cited_title":"Yale-CMU-Berkeley dataset for robotic manipulation research,","cited_arxiv_id":null,"evidence_quote":"Provides the object dataset used in the simulated and real manipulation experiments."},{"cited_title":"DART: Dense Articulated Real-Time Tracking,","cited_arxiv_id":null,"evidence_quote":"Supplies the tracking technique used to estimate robot and cabinet state in the real-world trials."}],"review_version":1}