Control Synthesis for Multiple Reach-Avoid Tasks via Hamilton-Jacobi Reachability Analysis

Shaoyuan Li; Xiang Yin; Yu Chen

REVIEW 4 major objections 5 minor 1 cited by

Control Synthesis for Multiple Reach-Avoid Tasks via Hamilton-Jacobi Reachability Analysis

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2509.10896 v1 pith:OA5RHZJB submitted 2025-09-13 eess.SY cs.SY

Yu Chen , Shaoyuan Li , Xiang Yin This is my paper · ORCID

classification eess.SYcs.SY

keywords controlsynthesisHamilton-Jacobireachabilitymultiplereach-avoidtaskslineartemporallogicvaluefunctionviscositysolutionnonlinearsystemswithdisturbance

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

What 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.

The 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.

This 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.

Referee Report

4 major / 5 minor

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.

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 (4)

[Section 4, Proposition 1, proof of (⇐), Eq. (24)] 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 6, Proposition 4, induction step] 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 5, Assumption 2 and Remark 3] 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 5, Eq. (33) and Remark 4] 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.

minor comments (5)

[Section 2, Eq. (5)] There is a typo in "we allow the the adversarial environment" which should read "we allow the adversarial environment".
[Section 5, Eq. (29)] 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 7.3] 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 7.4] 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 6.2, Eq. (46)] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the cascade value functions are built by backward induction on the external HJR characterization, not by renaming the paper's own conclusion.

full rationale

The paper's derivation is self-contained in the sense relevant to circularity: Theorem 1 is proved by induction starting from Lemma 1, which directly imports the reach-avoid value-function characterization from the external reference [16]. Each inductive step (Proposition 1) defines h_Phi_{i+1}_RA as the viscosity solution of a new reach-avoid HJ-VI whose target function is min{h_T_{N-i}, h_Phi_i_RA}; this is a well-founded backward recursion over the task sequence, not an assumption of the result being proved. Equation (16) is an induction hypothesis, and the proof attempts to show that the new value function characterizes the enlarged MRA task; regardless of whether that proof is correct, the claim does not reduce by construction to its own input. No fitted parameters are renamed as predictions, and the only self-citation is [12], which is described as a preliminary conference version and is not load-bearing for the main theorems. The LTL construction in equations (49)-(51) is similarly a backward recursion over a high-level plan and is not circular. The flagged quantitative-logic concern about Proposition 1's left-to-right direction, and the differentiability assumption in Section 5, are potential correctness gaps rather than circularity: they concern whether the theorem is true, not whether the output is equivalent to an input by definition.

Assumptions & free parameters 2 free parameters · 7 assumptions · 0 invented entities

The theoretical results depend on standard HJ reachability theorems, Lipschitz regularity assumptions, and a differentiability assumption for the online controller. No new physical entities are posited. The only free parameters are experimental tuning choices in the case studies, not fitted to data for the main theorems.

free parameters (2)

beta threshold in modified control set = 1.2
In Section 7.4, the modified control input set (40) uses beta = 1.2, a hand-chosen safety margin for the unicycle example. This parameter is not part of the central theoretical claim; it is a tuning knob in one case study.
reference controller gains kv, ktheta = not specified
Section 7.4 introduces a reference controller with 'constant gains kv and ktheta' but does not report their values. These are experimental parameters, not used in the main theorems, but their absence hurts reproducibility.

assumptions (7)

standard math Existence and uniqueness of trajectories for system (1) under measurable control and disturbance functions and non-anticipative strategies.
Invoked throughout Section 2.1 and in every trajectory argument; standard ODE theory under boundedness, uniform continuity in t, and Lipschitz continuity in x.
domain assumption The HJR characterization from Fisac et al. [16]: the value function h_RA solving the HJ-VI (8) satisfies h_RA(x,t) >= 0 iff x is in the reach-avoid feasible set (6).
Used as Lemma 1 and as the base case of the induction in Proposition 1. The paper relies on this external theorem without reproving it.
domain assumption Assumption 1: for each target and safe region there exists a Lipschitz continuous function whose super-level set is exactly that region.
Required to translate set-membership conditions (10) into value-function inequalities throughout Sections 4 and 5. Stated in Section 4 before equation (12).
ad hoc to paper Assumption 2: the computed value functions are differentiable on R^n x [0,T].
Introduced in Section 5 to define the control law (30) and prove Proposition 2. The paper acknowledges only almost-everywhere differentiability and informally refers to [13] for a nonsmooth remedy, so this is a technical assumption particular to this paper's synthesis proof.
standard math For scLTL\Circle tasks, the accepting language of the formula is captured by a deterministic finite-state automaton, and the word semantics are stutter-insensitive.
Standard automata-theoretic results cited in Section 6.1 from [2,6]; used to define high-level plans and to justify the construction in (46)-(51).
domain assumption The trajectory word L(xi) as defined in Definition 1 is finite; trajectories generating infinitely many labels in finite horizon are excluded.
Definition 1 explicitly excludes such trajectories, but the paper gives no conditions on the system dynamics or labeling function to guarantee this excludes only measure-zero cases. Load-bearing for the LTL word semantics in Section 6.
domain assumption The target sets T_i in the LTL construction are closed.
Section 6.2 states 'we assume without loss of generality, that Ti in (46) is closed', which is used in the first-crossing arguments of Proposition 4. Presented as a mild topological assumption.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Control Synthesis for Multiple Reach-Avoid Tasks via Hamilton-Jacobi Reachability Analysis." pith.science (2026). https://pith.science/paper/OA5RHZJB

@misc{pith2026250910896,
  author       = {Pith},
  title        = {Pith review of: Control Synthesis for Multiple Reach-Avoid Tasks via Hamilton-Jacobi Reachability Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OA5RHZJB}},
  note         = {Machine review of arXiv:2509.10896}
}

read the original abstract

We investigate the control synthesis problem for continuous-time time-varying nonlinear systems with disturbance under a class of multiple reach-avoid (MRA) tasks. Specifically, the MRA task requires the system to reach a series of target regions in a specified order while satisfying state constraints between each pair of target arrivals. This problem is more challenging than standard reach-avoid tasks, as it requires considering the feasibility of future reach-avoid tasks during the planning process. To solve this problem, we define a series of value functions by solving a cascade of time-varying reach-avoid problems characterized by Hamilton-Jacobi variational inequalities. We prove that the super-level set of the final value function computed is exactly the feasible set of the MRA task. Additionally, we demonstrate that the control law can be effectively synthesized by ensuring the non-negativeness of the value functions over time. We also show that the Linear temporal logic task control synthesis problems can be converted to a collection of MRA task control synthesis problems by properly defining each target and state constraint set of MRA tasks. The effectiveness of the proposed approach is illustrated through four case studies on robot planning problems under time-varying nonlinear systems with disturbance.

Figures

Figures reproduced from arXiv: 2509.10896 by the authors.

**Figure 2.** Simulation Results of Case Studies. further confirm the situation of the docking site by camera. Therefore, the feasible state set is given by G = {(x, y, vx, vy) ∈ R 4 | x, y ∈ [−50, 0], vx, vy ∈ [0, 3]} and the two target sets are defined by R1 = {(x, y, vx, vy) ∈ R 4 | x ∈ [−40, −20], y ∈ [−15, 0]}, R2 = {(x, y, vx, vy) ∈ R 4 | x, y ∈ [−5, 0], vx, vy ∈ [0, 2]}. The overall MRA task is described by Φ = (0, 60,(R1… view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Exact Decomposition of Adversarial Dual-Objective Value Functions, with Applications to Optimal Drug Dosing
eess.SY 2026-07 accept novelty 6.0 of 10

Adversarial reach-always-avoid and reach-reach value functions decompose exactly into standard reach/avoid value functions in continuous-time finite-horizon games.

Reference graph

Works this paper leans on

39 extracted references · 35 canonical work pages · cited by 1 Pith paper

[13]

Choi, Donggun Lee, Koushil Sreenath, Claire J

Jason J. Choi, Donggun Lee, Koushil Sreenath, Claire J. Tomlin, and Sylvia L. Herbert. Robust control barrier–value functions for safety-critical control. In 2021 60th IEEE Conference on Decision and Control (CDC) , pages 6814– 6821, 2021

work page 2021
[1]

Control barrier function based quadratic programs for safety critical systems

Aaron D Ames, Xiangru Xu, Jessy W Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs for safety critical systems. IEEE Transactions on Automatic Control, 62(8):3861–3876, 2016

work page 2016
[2]

Principles of model checking

Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008

2008
[3]

Hamilton-jacobi reachability: A brief overview and recent advances

Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. Hamilton-jacobi reachability: A brief overview and recent advances. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , pages 2242–2253. IEEE, 2017

work page 2017
[4]

Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, volume 12

Martino Bardi, Italo Capuzzo Dolcetta, et al. Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, volume 12. Springer, 1997

1997
[5]

Formal Methods for Control Synthesis: An Optimization Perspective

Calin Belta and Sadra Sadraddini. Formal Methods for Control Synthesis: An Optimization Perspective. Annual Review of Control, Robotics, and Autonomous Systems , 2(1):115–140, 2019

work page 2019
[6]

Formal methods for discrete-time dynamical systems , volume 89

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. Formal methods for discrete-time dynamical systems , volume 89. Springer, 2017

work page 2017
[7]

Formal Methods in Manufacturing

Javier Campos, Carla Seatzu, and Xiaolan Xie. Formal Methods in Manufacturing . CRC press, 2018

work page 2018

Show all 39 references

[8]

Verifying safety of an autonomous spacecraft rendezvous mission

Nicole Chan and Sayan Mitra. Verifying safety of an autonomous spacecraft rendezvous mission. EPiC Series in Computing, 48:20–32, 2017

2017
[9]

Robust sequential trajectory planning under disturbances and adversarial intruder

Mo Chen, Somil Bansal, Jaime F Fisac, and Claire J Tomlin. Robust sequential trajectory planning under disturbances and adversarial intruder. IEEE Transactions on Control Systems Technology, 27(4):1566–1582, 2018

2018
[10]

Signal temporal logic meets reachability: Connections and applications

Mo Chen, Qizhan Tam, Scott C Livingston, and Marco Pavone. Signal temporal logic meets reachability: Connections and applications. In International Workshop on the Algorithmic Foundations of Robotics , pages 581–601. Springer, 2018

2018
[11]

Hamilton–jacobi reachability: Some recent theoretical advances and applications in unmanned airspace management

Mo Chen and Claire J Tomlin. Hamilton–jacobi reachability: Some recent theoretical advances and applications in unmanned airspace management. Annual Review of Control, Robotics, and Autonomous Systems , 1:333–358, 2018

2018
[12]

Control synthesis for multiple reach-avoid tasks via hamilton-jacobi reachability analysis

Yu Chen, Shaoyuan Li, and Xiang Yin. Control synthesis for multiple reach-avoid tasks via hamilton-jacobi reachability analysis. In 2025 IEEE 64th Conference on Decision and Control (CDC). IEEE, 2025

2025
[14]

Prescribed-time reach-avoid-stay specifications for unknown systems: A spatiotemporal tubes approach

Ratnangshu Das and Pushpak Jagtap. Prescribed-time reach-avoid-stay specifications for unknown systems: A spatiotemporal tubes approach. IEEE Control Systems Letters, 8:946–951, 2024

2024
[15]

Symbolic control for autonomous docking of marine surface vessels

Elizabeth Dietrich, Emir Cem Gezer, Bingzhuo Zhong, Murat Arcak, Majid Zamani, Roger Skjetne, and Asgeir Johan Sørensen. Symbolic control for autonomous docking of marine surface vessels. arXiv:2501.13199, 2025

2025 arXiv
[16]

Reach-avoid problems with time-varying dynamics, targets and constraints

Jaime F Fisac, Mo Chen, Claire J Tomlin, and S Shankar Sastry. Reach-avoid problems with time-varying dynamics, targets and constraints. In Proceedings of the 18th international conference on hybrid systems: computation and control, pages 11–20, 2015

2015
[17]

Temporal logic trees for model checking and control synthesis of uncertain discrete-time systems

Yulong Gao, Alessandro Abate, Frank J Jiang, Mirco Giacobbe, Lihua Xie, and Karl Henrik Johansson. Temporal logic trees for model checking and control synthesis of uncertain discrete-time systems. IEEE Transactions on Automatic Control, 67(10):5071–5086, 2021

2021
[18]

A differential game approach to planning in adversarial scenarios: A case study on capture-the-flag

Haomiao Huang, Jerry Ding, Wei Zhang, and Claire J Tomlin. A differential game approach to planning in adversarial scenarios: A case study on capture-the-flag. In 2011 IEEE International Conference on Robotics and Automation, pages 1451–1456. IEEE, 2011

2011
[19]

Guaranteed completion of complex tasks via temporal logic trees and hamilton-jacobi reachability

Frank J Jiang, Kaj Munhoz Arfvidsson, Chong He, Mo Chen, and Karl H Johansson. Guaranteed completion of complex tasks via temporal logic trees and hamilton-jacobi reachability. arXiv preprint arXiv:2404.08334 , 2024

2024 arXiv
[20]

A fully automated framework for control of linear systems from temporal logic specifications

Marius Kloetzer and Calin Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transactions on Automatic Control , 53(1):287–297, 2008

2008
[21]

Control barrier functions for signal temporal logic tasks

Lars Lindemann and Dimos V Dimarogonas. Control barrier functions for signal temporal logic tasks. IEEE control systems letters , 3(1):96–101, 2018

2018
[22]

Finite abstractions with robustness margins for temporal logic-based control synthesis

Jun Liu and Necmiye Ozay. Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Analysis: Hybrid Systems , 22:1–15, 2016

2016
[23]

Hamilton–jacobi formulation for reach–avoid differential games

Kostas Margellos and John Lygeros. Hamilton–jacobi formulation for reach–avoid differential games. IEEE Transactions on Automatic Control , 56(8):1849–1861, 2011. 15

2011
[24]

Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges

Noushin Mehdipour, Matthias Althoff, Radboud Duintjer Tebbens, and Calin Belta. Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges. Automatica, 152:110692, 2023

2023
[25]

Smooth converse lyapunov-barrier theorems for asymptotic stability with safety constraints and reach-avoid- stay specifications

Yiming Meng, Yinan Li, Maxwell Fitzsimmons, and Jun Liu. Smooth converse lyapunov-barrier theorems for asymptotic stability with safety constraints and reach-avoid- stay specifications. Automatica, 144:110478, 2022

2022
[26]

Stochastic lyapunov- barrier functions for robust probabilistic reach-avoid-stay specifications

Yiming Meng and Jun Liu. Stochastic lyapunov- barrier functions for robust probabilistic reach-avoid-stay specifications. IEEE Transactions on Automatic Control , 69(8):5470–5477, 2024

2024
[27]

A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games

Ian M Mitchell, Alexandre M Bayen, and Claire J Tomlin. A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on automatic control, 50(7):947–957, 2005

2005
[28]

Control of Cyber-Physical-Systems with logic specifications: A formal methods approach

Giordano Pola and Maria Domenica Di Benedetto. Control of Cyber-Physical-Systems with logic specifications: A formal methods approach. Annual Reviews in Control , 47:178–192, 2019

2019
[29]

Feedback refinement relations for the synthesis of symbolic controllers

Gunther Reissig, Alexander Weber, and Matthias Rungger. Feedback refinement relations for the synthesis of symbolic controllers. IEEE Transactions on Automatic Control , 62(4):1781–1796, 2016

2016
[30]

Control of mobile robots using barrier functions under temporal logic specifications

Mohit Srinivasan and Samuel Coogan. Control of mobile robots using barrier functions under temporal logic specifications. IEEE Transactions on Robotics , 37(2):363– 374, 2020

2020
[31]

Robust stl control synthesis under maximal disturbance sets

Joris Verhagen, Lars Lindemann, and Jana Tumova. Robust stl control synthesis under maximal disturbance sets. arXiv preprint arXiv:2404.05535, 2024

2024 arXiv
[32]

Optimization-based trajectory generation with linear temporal logic specifications

Eric M Wolff, Ufuk Topcu, and Richard M Murray. Optimization-based trajectory generation with linear temporal logic specifications. In 2014 IEEE International Conference on Robotics and Automation (ICRA) , pages 5319–5325. IEEE, 2014

2014
[33]

Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems

Tichakorn Wongpiromsarn, Ufuk Topcu, and Andrew Lamperski. Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Transactions on Automatic Control, 61(11):3344–3355, 2015

2015
[34]

Reach-avoid verification based on convex optimization

Bai Xue, Naijun Zhan, Martin Fr¨ anzle, Ji Wang, and Wanwei Liu. Reach-avoid verification based on convex optimization. IEEE Transactions on Automatic Control , 69(1):598–605, 2024

2024
[35]

Formal synthesis of controllers for safety-critical autonomous systems: Developments and challenges

Xiang Yin, Bingzhao Gao, and Xiao Yu. Formal synthesis of controllers for safety-critical autonomous systems: Developments and challenges. arXiv preprint arXiv:2402.13075, 2024

2024 arXiv
[36]

Continuous- time control synthesis under nested signal temporal logic specifications

Pian Yu, Xiao Tan, and Dimos V Dimarogonas. Continuous- time control synthesis under nested signal temporal logic specifications. IEEE Transactions on Robotics , 2024

2024
[37]

Model predictive monitoring of dynamical systems for signal temporal logic specifications

Xinyi Yu, Weijie Dong, Shaoyuan Li, and Xiang Yin. Model predictive monitoring of dynamical systems for signal temporal logic specifications. Automatica, 160:111445, 2024

2024
[38]

Formal synthesis of controllers for uncertain linear systems against-regular properties: A set-based approach

Bingzhuo Zhong, Majid Zamani, and Marco Caccamo. Formal synthesis of controllers for uncertain linear systems against-regular properties: A set-based approach. IEEE Transactions on Automatic Control , 69(1):214–229, 2024

2024
[39]

Efficient path planning algorithms in reach-avoid problems

Zhengyuan Zhou, Jerry Ding, Haomiao Huang, Ryo Takei, and Claire Tomlin. Efficient path planning algorithms in reach-avoid problems. Automatica, 89:28–36, 2018. 16

2018

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [13]

Choi, Donggun Lee, Koushil Sreenath, Claire J

Jason J. Choi, Donggun Lee, Koushil Sreenath, Claire J. Tomlin, and Sylvia L. Herbert. Robust control barrier–value functions for safety-critical control. In 2021 60th IEEE Conference on Decision and Control (CDC) , pages 6814– 6821, 2021

work page 2021

[2] [1]

Control barrier function based quadratic programs for safety critical systems

Aaron D Ames, Xiangru Xu, Jessy W Grizzle, and Paulo Tabuada. Control barrier function based quadratic programs for safety critical systems. IEEE Transactions on Automatic Control, 62(8):3861–3876, 2016

work page 2016

[3] [2]

Principles of model checking

Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008

2008

[4] [3]

Hamilton-jacobi reachability: A brief overview and recent advances

Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. Hamilton-jacobi reachability: A brief overview and recent advances. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , pages 2242–2253. IEEE, 2017

work page 2017

[5] [4]

Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, volume 12

Martino Bardi, Italo Capuzzo Dolcetta, et al. Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, volume 12. Springer, 1997

1997

[6] [5]

Formal Methods for Control Synthesis: An Optimization Perspective

Calin Belta and Sadra Sadraddini. Formal Methods for Control Synthesis: An Optimization Perspective. Annual Review of Control, Robotics, and Autonomous Systems , 2(1):115–140, 2019

work page 2019

[7] [6]

Formal methods for discrete-time dynamical systems , volume 89

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. Formal methods for discrete-time dynamical systems , volume 89. Springer, 2017

work page 2017

[8] [7]

Formal Methods in Manufacturing

Javier Campos, Carla Seatzu, and Xiaolan Xie. Formal Methods in Manufacturing . CRC press, 2018

work page 2018