{"id":"c3071533-9672-4d86-b5b7-dafb14cb9e0e","arxiv_id":"2509.10896","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"The feasible states for a sequence of reach-avoid tasks under disturbances are exactly the super-level set of a value function built from a cascade of Hamilton-Jacobi variational inequalities.","lead":"This paper presents a method for planning a robot or vehicle that must visit several target zones in a fixed order while staying safe, even when the system has uncertain disturbances. It computes the set of states from which such a mission is possible, using a sequence of Hamilton-Jacobi equations, and provides a controller that keeps the mission feasible online.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's exactness proof has a quantifier shift in Proposition 1's (⇐) direction: a single successful play is used to infer the universal robust-feasibility condition (16). The cascade characterization and the synthesis built on it are therefore not established as written.","rationale":"The paper's headline contribution is the exact feasible-set characterization of MRA tasks (Theorem 1), and Algorithm 1's soundness is presented as a consequence of it. The reader's weakest assumption targets Assumption 2 and the differentiability of the value functions used in the synthesis law. That concern attaches to Theorem 2 and to Remark 3, and the paper partly de-risks it by conditioning Theorem 2 on the existence of a feedback law satisfying (33). The quantifier issue in Proposition 1 attaches to Theorem 1 itself: the proof's (⇐) direction infers a universal robust-feasibility statement from a single successful play under one disturbance strategy. Equation (16) defines h_RA^{Φ_i} ≥ 0 as 'for every γ there exists u', so an existential play cannot discharge the universal quantifier. This is not a minor notation slip; without a strategy-concatenation or determinacy argument, the cascade set could be strictly larger than the true MRA set, which would make the control synthesis filter unsound. The theorem may well be true—dynamic programming principles for reach-avoid games suggest it is—but the proof as written does not establish it. Since the gap is repairable in principle and the case studies are consistent with the claimed behavior, the appropriate verdict remains conditional rather than rejection. I therefore leave the reader's CONDITIONAL verdict unchanged, while flagging a different, more central weakness than the one identified in the reader's weakest_assumption.","tokens_in":22983,"tokens_out":23207,"duration_ms":233296,"concrete_test":"Implement a small finite-state version of the game, e.g., scalar x_{k+1}=x_k+u_k+d_k with u_k,d_k∈{-1,0,1}, horizon 2 or 3, and two ordered targets. Exhaustively enumerate all non-anticipative disturbance strategies and compute the brute-force MRA set defined by (11). Separately compute the cascade set defined by (17) using the same state and target encoding. If the two sets differ, the cascade characterization is false and Algorithm 1 is unsound. If they coincide, Theorem 1 survives, but its proof still needs the missing strategy-concatenation lemma before the exactness claim is rigorous. Either outcome settles whether the quantifier shift is a presentational gap or a substantive error.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Proposition 1, (⇐) direction, is the step that makes Theorem 1 an exact characterization rather than a conservative one, and it contains a quantifier shift. After fixing an arbitrary γ∈Γ[t0,T] and a control u satisfying the full task, the proof reaches x'=ξ^{u,γ}_{x,t}(t_{N-i}) and observes that the same control/strategy pair satisfies the i-tail task. It then states: 'from (16) we know that h_RA^{Φ_i}(x',t_{N-i}) ≥ 0.' But (16) is the robust feasibility equivalence: h_RA^{Φ_i}(x,t) ≥ 0 iff for every γ'∈Γ[t,T] there exists some u' such that ξ^{u',γ'}_{x,t} satisfies the tail task. Existence of a successful play against the one particular strategy γ does not imply this universal property. What is needed is a strategy-concatenation lemma showing that, when the global MRA task is winnable from x0 against all disturbance strategies, any forced first-arrival state must already lie in the robust feasible set of the remaining subtask. Without such a lemma, the target min{h_{T_{N-i}}, h_RA^{Φ_i}} in (17) could admit states that are reachable only by luck against one strategy, making the cascade set an over-approximation. This threatens Theorem 1, and therefore also the correctness of Algorithm 1, independently of Assumption 2. The differentiability issue flagged by the reader is real, but it is secondary: even with full differentiability, the quantifier gap in the proof of exactness would remain.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper studies continuous-time nonlinear control systems with bounded disturbances and a class of sequential temporal tasks called multiple reach-avoid (MRA) tasks: the system must visit N target regions in a prescribed order while staying in associated safe regions between consecutive arrivals. The main theoretical claim is that the feasible set of an MRA task is characterized exactly as the super-level set of a value function obtained by solving a cascade of time-varying reach-avoid Hamilton-Jacobi variational inequalities (Theorem 1). A control synthesis algorithm is then proposed that maintains the current value function nonnegative over time (Theorem 2), and a conversion from syntactically co-safe LTL specifications to MRA tasks is given, with a soundness result (Theorem 3 and Proposition 4). The paper closes with four numerical case studies on single-integrator, double-integrator, spacecraft rendezvous, and unicycle systems.","tokens_in":23323,"tokens_out":23560,"duration_ms":209390,"significance":"If Theorem 1 and Theorem 2 were established as stated, the paper would provide an exact, non-conservative functional characterization of a nontrivial class of sequential temporal tasks for time-varying nonlinear systems with disturbances, together with an online control filter that can be combined with arbitrary reference controllers. The cascade construction is natural, the LTL connection is useful, and the four case studies provide meaningful empirical support. The results are not accompanied by machine-checked proofs or public code, but the simulations are reproducible in principle. However, the central exactness proof contains a quantifier-shift error that is load-bearing for Theorem 1 and propagates to the LTL results; this must be resolved before the main claims can be accepted.","major_comments":[{"comment":"The step \"Then from (16) we know that h_RA^{Φ_i}(ξ_{x,t}^{u,γ}(t_{N-i}), t_{N-i}) ≥ 0\" is a quantifier shift. Property (16) says that h_RA^{Φ_i}(x,t) ≥ 0 holds if and only if for every disturbance strategy γ' in Γ[t,T] there exists a control u' that completes the i-tail task. The proof has exhibited only one successful play against one particular tail strategy induced by the original γ and u. A single successful play does not imply the universal robust-feasibility condition in (16); what is missing is a strategy-concatenation lemma showing that the first-arrival state itself lies in the robust feasible set of the tail task. Since Theorem 1 is used as the initial condition in Theorem 2 and in the LTL soundness argument, this gap affects the exactness claim and the correctness of Algorithm 1 as written.","section":"Section 4, Proposition 1, proof of (⇐), Eq. (24)"},{"comment":"The same quantifier shift appears in the induction step of Proposition 4. From a word realized under one fixed γ and u, the proof concludes that the state x' at the first arrival to the relevant target satisfies x' ∈ MRA(¯Φ_{[t_{N-i},t_1]}^i). Membership in MRA requires robustness against all tail disturbance strategies, which is not a consequence of one successful word. This invalidates the exact equality (52) as proved and consequently weakens the statement of Theorem 3. A rigorous proof would need to quantify over all tail strategies and construct the appropriate concatenated disturbance strategy, rather than inferring robustness from a single play.","section":"Section 6, Proposition 4, induction step"},{"comment":"The control synthesis results in Propositions 2 and 3 and Theorem 2 rely on the value functions h_RA^{Φ_i} being differentiable on R^n × [0,T]. Hamilton-Jacobi reach-avoid value functions are in general only Lipschitz continuous and differentiable almost everywhere. Remark 3 gestures at sub/superdifferential generalizations from [13], but no proof is given that the monotonicity argument (30)-(31), the nonemptiness result of Proposition 3, or the switching argument in Theorem 2 remain valid with generalized derivatives. Because the guarantee that b never decreases is exactly ˙b ≥ 0, this missing nonsmooth argument is load-bearing for Algorithm 1. The paper should either prove the synthesis step under viscosity or generalized-gradient semantics, or state the differentiability condition as a standing restriction and identify a concrete class of problems where it is satisfied.","section":"Section 5, Assumption 2 and Remark 3"},{"comment":"Even under Assumption 2, Theorem 2 assumes that \"c_b in Proposition 2 can be found,\" while Proposition 3 only establishes pointwise nonemptiness of the set-valued map S_b(x,t). The paper does not prove existence of a measurable and appropriately regular selection satisfying (33). The references [1,21] cited in Remark 4 concern control-barrier-function quadratic programs with specific regularity assumptions; a selection argument adapted to the set S_b in (30) is needed. Without such an argument, the online control law in Algorithm 1 is not fully justified.","section":"Section 5, Eq. (33) and Remark 4"}],"minor_comments":[{"comment":"There is a typo in \"we allow the the adversarial environment\" which should read \"we allow the adversarial environment\".","section":"Section 2, Eq. (5)"},{"comment":"The target function h_{T_{N-i+1}}(x) in (29) is written without the time argument, but the targets are time-varying and Assumption 1 defines h_{T_i} on R^n × [0,T]. This should be h_{T_{N-i+1}}(x,t) for consistency.","section":"Section 5, Eq. (29)"},{"comment":"The gravitational parameter is stated as \"μ = 3.986×10^14×302 [m^3/min^2]\"; this expression appears to be a typo, since the standard value of μ for Earth is 3.986×10^14 m^3/s^2. The units and the factor 302 should be checked and corrected.","section":"Section 7.3"},{"comment":"The phrase \"denoted as 'constant' and 'switch\"' contains a stray quotation mark and should be cleaned up; the meaning of \"switch\" also becomes clear only later in the paragraph and would benefit from a one-sentence explanation.","section":"Section 7.4"},{"comment":"The LTL conversion in (46) defines target and safe sets through the labeling function L(x), so the regions are time-invariant, whereas the MRA framework accommodates time-varying target and safe sets. The paper should clarify whether the LTL reduction is intentionally restricted to time-invariant labeling regions.","section":"Section 6.2, Eq. (46)"}],"recommendation":"major_revision","confidential_remarks":"The main issue is not the differentiability assumption but the quantifier structure of the feasibility definition. The authors should be asked to reconcile (6), (11), and (16) with the standard HJR game semantics in [16], and to supply a rigorous induction based on a strategy-concatenation lemma, or explicitly weaken the exactness claims. If the intended feasible set is the set of states from which a single feedback strategy exists against all disturbances, then the definitions and all theorems need to be restated accordingly. The LTL section inherits the same quantifier problem and should be revised together with Section 4."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about arXiv:2509.10896. First, the idea is genuinely useful: they formalize sequential reach-avoid tasks by cascading standard HJ reach-avoid problems, treating the feasible set of future sub-tasks as a time-varying target. That is a natural extension and could become a building block for LTL control synthesis. Second, the proof of the main exactness theorem (Theorem 1, via Proposition 1) has a quantifier-shift gap. On reading the (⇐) direction of Proposition 1, the authors take a single successful control u against one disturbance strategy γ and infer the robust feasibility condition (16) for the tail task at the arrival state. But (16) requires a guarantee against all non-anticipative strategies. Existence of one winning play against the particular γ does not give that. Without a strategy-concatenation lemma, the cascade set may be an over-approximation, and Theorem 1 is not established as written. The stress-test note is correct.\n\nWhat the paper does well: the recursive construction of value functions is elegant, the relation to LTL via high-level plans is sensible (sound, not complete, and the authors say so), and the four case studies are illustrative. They also ship a numerical validation for the single-integrator case, comparing against an analytic feasible set, which is a good reproducibility instinct. The differentiability assumption (Assumption 2) is a real but secondary issue: the synthesis argument rests on gradients existing at visited states, and the nonsmooth relaxation is only a gesture to the literature.\n\nThe soft spots, in order: the quantifier gap in Proposition 1; Assumption 2 and the informal nonsmooth handling; the LTL reduction's completeness caveat (the authors are honest about it, but the enumeration over plans is only practical for acyclic automata); and the case studies lack baseline comparisons or error analysis. None of these are fatal if the gap is fixable—and I suspect it is, because the characterization is likely true and can be proven with a more careful concatenation argument—but the paper as written does not yet establish its main claim.\n\nThis paper is for researchers working on HJ reachability for temporal tasks. It deserves a serious referee: the gap is specific and addressable, and the idea is worth developing. I would send it out, but the referee should demand a fixed proof of Proposition 1 and a rigorous nonsmooth synthesis statement.","headline":"Elegant cascade formulation for sequential reach-avoid, but the main exactness proof has a quantifier-shift gap that must be fixed before Theorem 1 is established.","tokens_in":23858,"tokens_out":2772,"would_cite":false,"duration_ms":22283,"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":"A cascade of Hamilton-Jacobi inequalities exactly characterizes the set of starting states from which an ordered sequence of reach-avoid tasks can be completed.","keywords":["control synthesis","Hamilton-Jacobi reachability","multiple reach-avoid tasks","reach-avoid","linear temporal logic","value function","viscosity solution","nonlinear systems with disturbance"],"falsifier":"Take a system where a reach-avoid value function is nondifferentiable at a reachable state with $b(x,t)\\ge 0 > h_b^T(x,t)$, and check whether the generalized-derivative control set in (30)/(38) is nonempty and whether the closed-loop value $b$ stays nonnegative until $h_b^T\\ge 0$. An explicit state where $S_b(x,t)=\\emptyset$, or an online trajectory where $b$ drops below zero, would falsify Theorem 2; the paper's Proposition 3 predicts no such state exists wherever the classical gradient exists.","tokens_in":22743,"feed_emoji":"🎯","tokens_out":5729,"duration_ms":53895,"temperature":0.7,"pith_summary":"The paper targets a continuous-time, time-varying nonlinear control system with bounded disturbance and a task that says: visit target regions $T_1,\\dots,T_N$ in order, staying inside safe regions $G_1,\\dots,G_N$ between consecutive arrivals. Its central claim is that the set of states from which this multiple reach-avoid (MRA) task is feasible is exactly the super-level set of one function $h_{RA}^{\\Phi_N}$, computed by solving $N$ standard reach-avoid Hamilton-Jacobi variational inequalities in reverse order, with the feasible set of the remaining subtask used as a dynamic target. It then claims that Algorithm 1, which keeps the current value function nonnegative until each stage target is reached, completes the whole task under any bounded disturbance. If these results stand, ordered multi-target and co-safe linear temporal logic specifications for nonlinear systems become tractable through exact value-function computation plus a simple online control filter, without abstraction.","feed_headline":"Value-function cascade nails ordered reach-avoid feasibility","feed_subtitle":"Backward-solved future subtasks give exact feasibility; keeping the margin nonnegative finishes every target under disturbance.","key_machinery":"The central object is a cascade of Hamilton-Jacobi variational inequalities, one per stage. Each cascade step treats the feasible set of the future subtask, namely the super-level set of the previously computed value function, as part of a time-varying target, then computes a new value function whose nonnegativity encodes feasibility of the combined subtask. The online mechanism is monotonicity: controls are drawn from $S_b(x,t)$, the set of inputs making $\\frac{d}{dt} b(x(t),t)\\ge 0$ under the worst-case disturbance, so the current value function acts as a nondecreasing margin of task feasibility, and Proposition 2 guarantees the stage target is hit by the horizon.","core_discovery":"The paper establishes an exact dynamic-programming recursion for feasibility. Define $h_{RA}^{\\Phi_i}$ as the viscosity solution of the Hamilton-Jacobi variational inequality (8) for a time-varying reach-avoid problem whose target function is $\\min\\{h_{T_{N-i+1}}, h_{RA}^{\\Phi_{i-1}}\\}$ for $i>1$ and whose safe function is $h_{G_{N-i+1}}$. Proposition 1 shows by concatenating control inputs that $h_{RA}^{\\Phi_{i+1}}(x,t)\\ge 0$ exactly when a trajectory from $(x,t)$ can complete the last $i+1$ stages; Theorem 1 closes the induction at $h_{RA}^{\\Phi_N}(x,0)\\ge 0$ iff $x\\in \\mathrm{MRA}(0,T,\\mathcal{T},\\mathcal{G})$. The synthesis side uses the same functions online: choose a control so the time derivative of the active value function $b$ never goes negative, wait until the stage target $h_b^T$ is reached, then switch to the next value function; Theorem 2 asserts this finishes all $N$ targets under every disturbance.","pith_inferences":["If the recursion is exact, it gives a continuous-state analog of backward reachability over automata: one could derive the same kind of exact value-function recursion for larger fragments of temporal logic, replacing heuristic temporal-logic trees by repeated Hamilton-Jacobi solves.","The monotone-margin control law is structurally a time-varying control barrier function whose barrier is the task value; a natural stress test is to combine it with learning-based Hamilton-Jacobi approximations and measure whether small approximation errors break the nonnegativity guarantee.","For stochastic systems, the same backward recursion would need probability thresholds instead of hard zero super-levels, so the exact set characterization is unlikely to carry over unchanged; the expected extension would be sound but not exact."],"forward_implications":["The feasible set for any ordered sequence of reach-avoid objectives can be computed exactly by solving $N$ Hamilton-Jacobi variational inequalities backward, instead of using conservative approximations or heuristic temporal-logic trees.","Algorithm 1 acts as a task-satisfaction filter: any reference controller can be retained, with the quadratic program in (38) choosing the closest admissible input, so MRA guarantees can be added to existing planners.","Co-safe linear temporal logic specifications can be enforced by picking a high-level plan in the corresponding finite automaton and running the resulting MRA controller; when the automaton has no nontrivial cycles, enumerating bounded high-level plans makes the LTL synthesis sound and complete.","The guarantees hold for time-varying targets and constraints and for bounded disturbances modeled as non-anticipative strategies, covering moving obstacles, actuator saturation, and adversarial environment behavior."],"supporting_citations":[{"why":"Supplies the single reach-avoid Hamilton-Jacobi variational inequality and the equivalence between its super-level set and the feasible set, used as Lemma 1 and in every cascade step.","marker":"[16]"},{"why":"Provides the Hamilton-Jacobi reachability viscosity-solution formulation and non-anticipative disturbance strategies that define the value function in (7)-(9).","marker":"[3]"},{"why":"Gives the robust control barrier-value function construction and the super/subdifferential replacement used when $b$ is not differentiable in Remark 3 and in the QP control law.","marker":"[13]"},{"why":"Constructs a finite automaton accepting exactly the good prefixes of a syntactically co-safe LTL formula, which underlies the LTL-to-MRA conversion in Section 6.","marker":"[6]"},{"why":"Cited for the regularity conditions that make the QP control law Lipschitz in state and uniformly continuous in time, needed by Proposition 2's feedback function.","marker":"[1]"}],"fun_headline_variants":["Exact feasibility for ordered reach-avoid via HJ cascade","Hamilton-Jacobi controller for ordered reach-avoid tasks","Cascading HJ value functions guarantee ordered reach-avoid","Guaranteed completion of ordered reach-avoid under disturbance","Ordered reach-avoid solved exactly by HJ value recursion"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The controller guarantee assumes every reach-avoid value function is differentiable on the whole state-time domain, but the paper proves differentiability only almost everywhere and gestures at super/subdifferential replacements without giving the nonsmooth proof, so trajectories that hit nondifferentiable points are not fully covered.","fun_headline_variants_meta":{"raw":{"variants":["Exact feasibility for ordered reach-avoid via HJ cascade","Hamilton-Jacobi controller for ordered reach-avoid tasks","Cascading HJ value functions guarantee ordered reach-avoid","Guaranteed completion of ordered reach-avoid under disturbance","Ordered reach-avoid solved exactly by HJ value recursion"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000821,"raw_usage":{"total_tokens":3616,"prompt_tokens":990,"completion_tokens":2626,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":606,"completion_tokens_details":{"reasoning_tokens":2546}},"tokens_in":606,"tokens_out":2626,"duration_ms":16088,"temperature":1.0,"reasoning_tokens":2546,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:53:29.987360+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a system where a reach-avoid value function is nondifferentiable at a reachable state with $b(x,t)\\ge 0 > h_b^T(x,t)$, and check whether the generalized-derivative control set in (30)/(38) is nonempty and whether the closed-loop value $b$ stays nonnegative until $h_b^T\\ge 0$. An explicit state where $S_b(x,t)=\\emptyset$, or an online trajectory where $b$ drops below zero, would falsify Theorem 2; the paper's Proposition 3 predicts no such state exists wherever the classical gradient exists.","supporting_citations":[{"cited_title":"Hamilton-jacobi reachability: A brief overview and recent advances","cited_arxiv_id":null,"evidence_quote":"Provides the Hamilton-Jacobi reachability viscosity-solution formulation and non-anticipative disturbance strategies that define the value function in (7)-(9)."},{"cited_title":"Choi, Donggun Lee, Koushil Sreenath, Claire J","cited_arxiv_id":null,"evidence_quote":"Gives the robust control barrier-value function construction and the super/subdifferential replacement used when $b$ is not differentiable in Remark 3 and in the QP control law."},{"cited_title":"Formal methods for discrete-time dynamical systems , volume 89","cited_arxiv_id":null,"evidence_quote":"Constructs a finite automaton accepting exactly the good prefixes of a syntactically co-safe LTL formula, which underlies the LTL-to-MRA conversion in Section 6."},{"cited_title":"Control barrier function based quadratic programs for safety critical systems","cited_arxiv_id":null,"evidence_quote":"Cited for the regularity conditions that make the QP control law Lipschitz in state and uniformly continuous in time, needed by Proposition 2's feedback function."}],"review_version":2}