Pith. sign in

REVIEW 3 major objections 5 minor 45 references

Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Temporal logic robot tasks become a provably correct QP sequence

desk verdict Worth reading for the LTL-to-CBF-QP pipeline, but the headline infeasibility result is wrong as stated and the main theorem's feasibility assumptions are uncharacterized. read the letter →

arxiv 1908.04903 v2 pith:ZVEQRKOU submitted 2019-08-14 cs.RO

Mohit Srinivasan , Samuel Coogan This is my paper · ORCID
classification cs.RO
keywords controlbarrierfunctionslineartemporallogicquadraticprogramsmobilerobotsfinite-timereachabilitysafetyinvariancemulti-robotsystemslassotraces
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

This paper claims that a large class of robotic motion-planning specifications written in a fragment of linear temporal logic (LTL_robotic) can be compiled automatically into a finite sequence of constrained reachability tasks, each encoded as a quadratic program whose constraints are control barrier functions. The central guarantee is Theorem 2: if every such quadratic program is feasible, then the trace of the resulting robot trajectory satisfies the original specification. The framework avoids the usual step of building a finite abstraction or automaton of the state space, so the controller runs in real time. A separate contribution addresses infeasibility: multiple finite-time barrier functions can be composed into one weighted-sum constraint with a strictly larger feasible set, and conflicting safety constraints can be prioritized by penalizing their slack.

What carries the argument

The load-bearing object is the lasso-type constrained reachability sequence (Definition 7), a prefix-suffix string of reachability tasks $R(\Sigma_j,\Gamma_j)$ with compatibility $\Gamma_j \subseteq \Sigma_{j+1}$; it converts a temporal-logic specification into a list of set-reaching chores that barrier functions can certify. The active mechanism is the control-barrier-function quadratic program: zeroing control barrier functions render each $\Sigma_j$ forward invariant, finite-time convergence control barrier functions force finite-time arrival at each $\Gamma_j$, and Theorem 1's composite constraint allows the sum of weighted barrier derivatives to grow even when individual barrier functions dip, which enlarges the feasible set. Algorithm 2 repeatedly solves these QPs and switches objectives when $x \in \Gamma_j$.

What would settle it

Take a control-affine robot whose single goal region is surrounded by an obstacle so that the safety ZCBF and the reachability FCBF conflict, and run Algorithm 2 with the hard QP (7); if the solver returns infeasible at any state before the goal is reached, the unconditional claim that Algorithm 2 synthesizes a satisfying trajectory is false. The same experiment applied to the relaxed QP (19) can show a trace that violates a required safety proposition, exactly the failure the paper notes after Theorem 2.

Watch

Extended reading notes

Core claim

The paper's central claim is that an LTL_robotic specification of the form $\phi = \phi_{\mathrm{globe}} \wedge \phi_{\mathrm{reach}} \wedge \phi_{\mathrm{rec}} \wedge \phi_{\mathrm{act}}$ can be turned into a lasso-type constrained reachability sequence $R_{\mathrm{lasso}}$, where each $R_j = R(\Sigma_j,\Gamma_j)$ asks the robot to reach $\Gamma_j$ in finite time while staying inside $\Sigma_j$, with the compatibility condition $\Gamma_j \subseteq \Sigma_{j+1}$ linking consecutive steps. Algorithm 1 builds this sequence from the specification and a chosen enumeration of the reachability and recurrence index sets; Algorithm 2 solves the corresponding quadratic programs online, switching to the next objective when the state enters the current target set. The proof of Theorem 2 runs through the notion of a descendant of the lasso template: any trace respecting the safety sets and visiting the prescribed goals in finite time satisfies the specification (Proposition 3), and the barrier-function constraints enforce exactly those conditions whenever the QPs remain feasible. The paper also claims Theorem 1, a composite finite-time control barrier function condition that guarantees finite-time reachability of the intersection $\Gamma$ using a weighted sum of derivatives of bounded barrier functions plus individual constraints for the remaining ones, and Corollary 1 says the resulting feasible control set is a superset of the separate-constraint approach.

Load-bearing premise

The guarantee is conditional on the quadratic program staying feasible at every state until each target set is reached; the paper derives no condition on the dynamics or the specification that ensures this, and it concedes that the relaxed QP (19) may violate the specification when its slack variables are nonzero.

Editorial extensions

If this is right

  • A robot can execute an LTL_robotic task by solving only a sequence of small quadratic programs, with no automaton or grid abstraction of the workspace.
  • Theorem 1 implies that multiple finite-time reachability goals can be pursued in one QP constraint, so a robot may temporarily move away from one goal to satisfy safety or connectivity before reaching all goals.
  • When safety constraints conflict with reachability, the relaxed QP (19) keeps the FCBF constraints hard and relaxes ZCBFs by weighted slack, so the robot still reaches its goal while minimally violating lower-priority safety.
  • Because each QP is strongly convex, per-step computation remains on the millisecond scale, making the approach suitable for on-board real-time control of mobile robots.

Reading between the lines

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

  • If a cheap offline check of QP feasibility along expected trajectories could be added, Theorem 2 would become a practical certificate rather than a conditional guarantee; the paper leaves this check open.
  • The compatibility condition $\Gamma_j \subseteq \Sigma_{j+1}$ is never verified by Algorithm 1, so a natural diagnostic is to compute these set inclusions symbolically; violations would show the lasso template was chosen inconsistently.
  • The lasso template enumeration is arbitrary, so ordering goals by workspace proximity could reduce switching events and the risk of crossing an infeasible region.
  • Because recurrence and persistence are included, the same framework could extend to reactive tasks of the form always(A implies eventually B) if time-varying barrier functions were introduced, a direction the paper does not pursue.
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.

Referee Report

3 major / 5 minor

Summary. The paper proposes a control framework for mobile robots under a fragment of linear temporal logic (LTL_robotic) using control barrier functions (CBFs) encoded as quadratic program (QP) constraints. The authors introduce composite finite-time convergence barrier functions (FCBFs) to enlarge the feasible set relative to encoding each FCBF separately, and a prioritization scheme for zeroing CBFs (ZCBFs) when safety constraints conflict. They give algorithms that translate an LTL_robotic specification into a lasso-type constrained reachability sequence and then into a sequence of QPs, and they prove that, if the QPs are feasible, the generated trajectory satisfies the specification. A multi-robot case study with simulations and experiments is included. The central guarantee is conditional on QP feasibility and on the lasso sequence satisfying the compatibility condition of Definition 7, and the paper explicitly notes that the relaxed QP may no longer guarantee the specification.

Significance. If the main results were correct, the abstraction-free, CBF-based synthesis pipeline for this LTL fragment would be a useful contribution to the robotics and formal-methods literature, and the simulation/experimental validation on the Robotarium is valuable evidence of practical implementability. The paper also gives direct proofs rather than merely citing prior work, and the overall architecture from LTL specification to QP constraints is clearly described. However, the key claimed contribution that composition of FCBFs yields a larger feasible set is false as stated for the FCBFs defined in the paper, and the main correctness theorem rests on compatibility and feasibility assumptions that Algorithm 1 does not verify. These issues are load-bearing for the paper's stated contributions.

major comments (3)
  1. [Section IV-A, Eqs. (16)-(17), Corollary 1] The feasible-set comparison in Corollary 1 is made against the wrong constraint and is false for the FCBFs defined in the paper. Definition 2 and the motivating QP (12) require the term γ sign(h_i)|h_i|^ρ, but the set U(x) defined in (16) drops the factor |h_i|^ρ. These constraints are not equivalent: for -1 < h_i < 0 the exponentiated bound is weaker than γ, while for h_i < -1 it is stronger. The proof of Corollary 1 uses the no-exponent bound to conclude that (13) holds; with the actual exponentiated constraint the available lower bound is γ|h_i|^ρ, and the inclusion U_ind ⊆ U_comp does not follow. A concrete counterexample is ẋ = u, h1 = h2 = -x, ρ = 0.5, γ = 1, α1 = α2 = 1, x = 0.01. The individual FCBF constraints are satisfied by u = -0.15, since -u - 0.1 = 0.05 ≥ 0, but the composite constraint (13) evaluates to 0.3 - 1 = -0.7 < 0. Thus the stated primary contribution of a 'larger feasible set' for finite-time reachability is not established for the FCBFs actually defined in the paper.
  2. [Section V, Definition 7, Algorithm 1, Theorem 2] Theorem 2 depends on the lasso-type constrained reachability sequence satisfying the compatibility condition Γ_j ⊆ Σ_{j+1} for all j, but Algorithm 1 constructs R_lasso without checking this inclusion. The proof of Theorem 2 invokes the conditions of Definition 9 without verifying that R_lasso is a valid lasso-type sequence under Definition 7. If Γ_j is not a subset of Σ_{j+1}, a trajectory that reaches Γ_j at the switching instant may leave Σ_{j+1}, and the ZCBF forward-invariance argument for the next reachability objective has no valid initial condition. Algorithm 1 should either check this compatibility explicitly or be accompanied by a proof that the LTL_robotic fragment and the proposed construction always produce such a sequence; otherwise a feasible run of Algorithm 2 need not yield a valid lasso-type sequence.
  3. [Section V, Theorem 2 and the remark after its proof] The central guarantee is conditional on QP (7) being feasible at every state along the trajectory until each target is reached, but no conditions on the dynamics, specification, or barrier functions are derived that imply this property. The relaxed QP (19) is not a remedy because, as the paper itself states, nonzero slack variables ε can violate the corresponding safety propositions and then Theorem 2 no longer applies. For a framework aimed at guaranteeing feasibility of the controller, the authors should either give sufficient conditions for persistent feasibility of (7), or state precisely the class of instances for which the guarantee applies and how violations of this premise are to be detected online.
minor comments (5)
  1. [Section V-B, Algorithm 1] The notation J1 and J4 is used in the pseudocode before these sets are formally defined; please define Jψ1K and Jψ4K directly at the start of the algorithm description.
  2. [Section II-B, after Eq. (8)] The literal notation π_i = ¬π_i is difficult to parse; please use a consistent overline or bar notation throughout, including in Definition 9 and Algorithm 1.
  3. [Section IV-B, Remark 2] There is a typo in 'then then the ith ZCBF has higher priority' that should be corrected.
  4. [Section VI, Fig. 3 caption] The phrase 'moves temporarily away from target 1 temporarily' repeats the adverb; please rephrase.
  5. [Section VI, Eq. (30)] The lasso sequence in the case study is stated without explicitly verifying the compatibility inclusions Γ_i ⊆ Σ_{i+1}; if these hold for this example, a one-line verification would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No material circularity: the main correctness claims are proved in-paper from external CBF results; the known feasibility gap and the Corollary 1 comparison issue are correctness concerns, not circular reductions.

full rationale

The paper's derivation chain is not circular. Propositions 1 and 2 import ZCBF invariance and FCBF finite-time convergence from [9] and [12]; these are external, parameter-free results with stated assumptions, and they do not presuppose the target specification. Theorem 1 (composite FCBF) is proved directly in the text: assuming (13)-(14), the proof integrates the weighted sum and uses boundedness of the bounded h_i to contradict non-reachability; no fitted parameter or self-citation carries the argument. Corollary 1 attempts to show U-bar subset U using comparison with (16); even if the comparison is mathematically inaccurate because (16) omits the |h_i|^rho term present in the paper's own Definition 2, that is an internal correctness issue, not a circular definition or a prediction that equals its input. The lasso construction (Definition 7, Algorithm 1, Proposition 3) is a compositional certificate: Algorithm 1 builds a sequence from the specification's J sets, Definition 9's descendant conditions are matched to the semantics, and Proposition 3 verifies each LTL conjunct case by case; Theorem 2 then transfers CBF reachability/invariance guarantees to those conditions. This is a standard certificate-style proof, not self-definitional circularity. The paper explicitly conditions Theorem 2 on feasibility of Algorithm 2 and warns that relaxed QP (19) may violate the specification when slacks are nonzero, so no feasibility guarantee is smuggled in. The only self-citation, [13], is for the preliminary composite-FCBF idea, but Theorem 1 is restated and proven here, making the citation non-load-bearing. Score 0.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The framework's contributions are algorithmic; it introduces no new physical entities or data-fitting parameters. The listed free parameters are standard tuning knobs for barrier functions and QPs; their values are not reported, which hampers exact reproduction.

free parameters (4)
  • gamma (γ) and rho (ρ) for FCBFs = not reported
    Convergence parameters in the FCBF condition (4) and Theorem 1; chosen by the designer, values not given for the case study.
  • extended class K functions αi = not reported
    Tuning functions in ZCBF constraints (3) and in the relaxed QP (19); left to the designer.
  • priority weight matrix W = not reported
    Weights on slack variables in (19), used to prioritize safety constraints; the example changes wA and wB to generate different trajectories but does not report numeric values.
  • connectivity constants δ1, δ2 = not reported
    Constants in d_conn (28) for the case study connectivity constraint; no values given.
assumptions (5)
  • domain assumption System dynamics are control-affine with locally Lipschitz f and g (Eq. 1)
    All barrier and QP theory in the paper assumes this model.
  • domain assumption For each atomic proposition π there is a C^1 h_π with JπK = {x | h_π(x) ≥ 0} and L_g h_π(x) ≠ 0 for all x (Section III)
    Used to encode all propositions and their negations as barrier functions; the measure-zero boundary is ignored.
  • standard math ZCBFs guarantee forward invariance (Prop. 1, from [9]) and FCBFs guarantee finite-time convergence with bound (Prop. 2, from [12])
    Background results adopted wholesale from the CBF literature without proof.
  • domain assumption The QP (7) is feasible at every state encountered along the trajectory (Theorem 2)
    The theorem is conditional on this; no check or condition is provided, and the relaxed QP is noted to void the guarantee.
  • ad hoc to paper The composite barrier functions h_i are bounded above by M_i (Theorem 1)
    Needed for the contradiction argument that the weighted sum cannot grow unbounded; not guaranteed for arbitrary barrier functions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications." pith.science (2026). https://pith.science/paper/ZVEQRKOU

@misc{pith2026190804903,
  author       = {Pith},
  title        = {Pith review of: Control of Mobile Robots Using Barrier Functions Under Temporal Logic Specifications},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZVEQRKOU}},
  note         = {Machine review of arXiv:1908.04903}
}
read the original abstract

In this paper, we propose a framework for the control of mobile robots subject to temporal logic specifications using barrier functions. Complex task specifications can be conveniently encoded using linear temporal logic. In particular, we consider a fragment of linear temporal logic which encompasses a large class of motion planning specifications for a robotic system. Control barrier functions have recently emerged as a convenient tool to guarantee reachability and safety for a system. In addition, they can be encoded as affine constraints in a quadratic program. In this paper, a fully automatic framework which translates a user defined specification in temporal logic to a sequence of barrier function based quadratic programs is presented. In addition, with the aim of alleviating infeasibility scenarios, we propose methods for composition of barrier functions as well as a prioritization based control method to guarantee feasibility of the controller. We prove that the resulting system trajectory synthesized by the proposed controller satisfies the given specification. Robotic simulation and experimental results are provided in addition to the theoretical framework.

Figures

Figures reproduced from arXiv: 1908.04903 by the authors.

Figure 1
Figure 1. Suppose R1 is sensing information from R2 and hence must always stay within the sensing radius of R2. Suppose we have two regions of interest A, B and the base C. Let D represent a corridor in the state space (denoted by the dotted lines in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. A family of trajectories for the robot generated by [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. A still shot of the trajectories for the robots [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 41 canonical work pages

  1. [1]

    Towards formal synthesis of reactive controllers for dexter- ous robotic manipulation,

    S. Chinchali, S. C. Livingston, U. Topcu, J. W. Burdick, and R. M. Murray, “Towards formal synthesis of reactive controllers for dexter- ous robotic manipulation,” in 2012 IEEE International Conference on Robotics and Automation , May 2012, pp. 5183–5189

    work page 2012

  2. [2]

    Hierarchical task and motion planning in the now,

    L. P. Kaelbling and T. Lozano-P ´erez, “Hierarchical task and motion planning in the now,” in 2011 IEEE International Conference on Robotics and Automation , May 2011, pp. 1470–1477

    work page 2011

  3. [3]

    Safe certificate-based ma- neuvers for teams of quadrotors using differential flatness,

    L. Wang, A. D. Ames, and M. Egerstedt, “Safe certificate-based ma- neuvers for teams of quadrotors using differential flatness,” in 2017 IEEE International Conference on Robotics and Automation (ICRA) , May 2017, pp. 3293–3298

    work page 2017

  4. [4]

    Trustworthy cyber infrastructure for the power grid (tcip-g),

    “Trustworthy cyber infrastructure for the power grid (tcip-g),” Mar

    work page

  5. [5]

    Your first look inside amazon’s robot warehouse of tomorrow,

    M. Simon, “Your first look inside amazon’s robot warehouse of tomorrow,” Jun 2019. [Online]. Available: https://www.wired.com/story/ amazon-warehouse-robots/

    work page 2019

  6. [6]

    Available: https://www.dhs.gov/cisa/ critical-infrastructure-sectors

    [Online]. Available: https://www.dhs.gov/cisa/ critical-infrastructure-sectors

    work page

  7. [7]

    Interior methods for nonlinear optimization,

    A. Forsgren, P. E. Gill, and M. H. Wright, “Interior methods for nonlinear optimization,” SIAM review, vol. 44, no. 4, pp. 525–597, 2002

    2002

  8. [8]

    Control barrier function based quadratic programs with application to adaptive cruise control,

    A. D. Ames, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs with application to adaptive cruise control,” in 53rd IEEE Conference on Decision and Control , Dec 2014, pp. 6271– 6278

    work page 2014

Show all 45 references
  1. [9]

    Robustness of control barrier functions for safety critical control,

    X. Xu, P. Tabuada, J. W. Grizzle, and A. D. Ames, “Robustness of control barrier functions for safety critical control,” arXiv preprint arXiv:1612.01554, 2016

    2016 arXiv

  2. [10]

    Safety barrier certificates for collisions-free multirobot systems,

    L. Wang, A. D. Ames, and M. Egerstedt, “Safety barrier certificates for collisions-free multirobot systems,” IEEE Transactions on Robotics , vol. 33, no. 3, pp. 661–674, June 2017. 2Video of Robotarium experiment -https://youtu.be/EK1Zxcg-eSE 3Code for Robotarium experiment- ht...

    2017

  3. [11]

    Safety barrier certificates for het- erogeneous multi-robot systems,

    L. Wang, A. Ames, and M. Egerstedt, “Safety barrier certificates for het- erogeneous multi-robot systems,” in 2016 American Control Conference (ACC), July 2016, pp. 5213–5218

    2016

  4. [12]

    Formally correct composition of coordinated behaviors using control barrier certificates,

    A. Li, L. Wang, P. Pierpaoli, and M. Egerstedt, “Formally correct composition of coordinated behaviors using control barrier certificates,” in 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE, 2018, pp. 3723–3729

    2018

  5. [13]

    Control of multi-agent systems with finite time control barrier certificates and temporal logic,

    M. Srinivasan, S. Coogan, and M. Egerstedt, “Control of multi-agent systems with finite time control barrier certificates and temporal logic,” in 2018 IEEE Conference on Decision and Control (CDC) , Dec 2018, pp. 1991–1996

    2018

  6. [14]

    Barrier function certificates for forward invariance in hybrid inclusions,

    M. Maghenem and R. G. Sanfelice, “Barrier function certificates for forward invariance in hybrid inclusions,” in 2018 IEEE Conference on Decision and Control (CDC) , Dec 2018, pp. 759–764

    2018

  7. [15]

    Baier and J.-P

    C. Baier and J.-P. Katoen, Principles of model checking , 2008

    2008

  8. [16]

    Discrete abstractions of hybrid systems,

    R. Alur, T. A. Henzinger, G. Lafferriere, and G. J. Pappas, “Discrete abstractions of hybrid systems,” Proceedings of the IEEE, vol. 88, no. 7, pp. 971–984, July 2000

    2000

  9. [17]

    Controlling a class of nonlin- ear systems on rectangles,

    C. Belta and L. C. G. J. M. Habets, “Controlling a class of nonlin- ear systems on rectangles,” IEEE Transactions on Automatic Control , vol. 51, no. 11, pp. 1749–1759, Nov 2006

    2006

  10. [18]

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

    M. Kloetzer and C. Belta, “A fully automated framework for control of linear systems from temporal logic specifications,” IEEE Transactions on Automatic Control , vol. 53, no. 1, pp. 287–297, Feb 2008

    2008

  11. [19]

    Receding horizon temporal logic planning,

    T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Receding horizon temporal logic planning,” IEEE Transactions on Automatic Control , vol. 57, no. 11, pp. 2817–2830, Nov 2012

    2012

  12. [20]

    Motion planning with complex goals,

    A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y . Vardi, “Motion planning with complex goals,” IEEE Robotics Automation Magazine , vol. 18, no. 3, pp. 55–64, Sep. 2011

    2011

  13. [21]

    Temporal logic motion planning for dynamic robots,

    G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas, “Temporal logic motion planning for dynamic robots,” Automatica, vol. 45, no. 2, pp. 343–352, 2009

    2009

  14. [22]

    Control barrier functions for signal temporal logic tasks,

    L. Lindemann and D. V . Dimarogonas, “Control barrier functions for signal temporal logic tasks,” IEEE control systems letters , vol. 3, no. 1, pp. 96–101, 2019

    2019

  15. [23]

    Decentralized control barrier functions for coupled multi-agent systems under signal temporal logic tasks,

    L. Lindemann and D. V . Dimarogonas, “Decentralized control barrier functions for coupled multi-agent systems under signal temporal logic tasks,” in 2019 18th European Control Conference (ECC) , June 2019, pp. 89–94

    2019

  16. [24]

    Model predictive control with signal temporal logic specifications,

    V . Raman, A. Donz ´e, M. Maasoumy, R. M. Murray, A. Sangiovanni- Vincentelli, and S. A. Seshia, “Model predictive control with signal temporal logic specifications,” in 53rd IEEE Conference on Decision and Control, Dec 2014, pp. 81–87

    2014

  17. [25]

    Formal methods for control synthesis: An optimization perspective,

    C. Belta and S. Sadraddini, “Formal methods for control synthesis: An optimization perspective,” Annual Review of Control, Robotics, and Autonomous Systems, 2019

    2019

  18. [26]

    Distributed communication- aware motion planning for multi-agent systems from stl and spatel specifications,

    Z. Liu, B. Wu, J. Dai, and H. Lin, “Distributed communication- aware motion planning for multi-agent systems from stl and spatel specifications,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC), Dec 2017, pp. 4452–4457

    2017

  19. [27]

    Shrinking horizon model predictive control with chance-constrained signal temporal logic specifications,

    S. S. Farahani, R. Majumdar, V . S. Prabhu, and S. E. Z. Soudjani, “Shrinking horizon model predictive control with chance-constrained signal temporal logic specifications,” in 2017 American Control Confer- ence (ACC), May 2017, pp. 1740–1746

    2017

  20. [28]

    Q-learning for robust satisfaction of signal temporal logic specifications,

    D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta, “Q-learning for robust satisfaction of signal temporal logic specifications,” in 2016 IEEE 55th Conference on Decision and Control (CDC) , Dec 2016, pp. 6565–6570

    2016

  21. [29]

    Enforcing signal temporal logic specifications in multi-agent adversarial environments: A deep q-learning approach,

    D. Muniraj, K. G. Vamvoudakis, and M. Farhood, “Enforcing signal temporal logic specifications in multi-agent adversarial environments: A deep q-learning approach,” in 2018 IEEE Conference on Decision and Control (CDC). IEEE, 2018, pp. 4141–4146

    2018

  22. [30]

    Prescribed performance control guided policy improvement for satisfying signal temporal logic tasks,

    P. V ´arnai and D. V . Dimarogonas, “Prescribed performance control guided policy improvement for satisfying signal temporal logic tasks,” CoRR, vol. abs/1903.04340, 2019. [Online]. Available: http: //arxiv.org/abs/1903.04340

    1903 arXiv

  23. [31]

    Decentralized robust control of coupled multi-agent systems under local signal temporal logic tasks,

    L. Lindemann and D. V . Dimarogonas, “Decentralized robust control of coupled multi-agent systems under local signal temporal logic tasks,” in 2018 Annual American Control Conference (ACC) . IEEE, 2018, pp. 1567–1573

    2018

  24. [32]

    Fly-by-logic: Control of multi-drone fleets with temporal logic objectives,

    Y . V . Pant, H. Abbas, R. A. Quaye, and R. Mangharam, “Fly-by-logic: Control of multi-drone fleets with temporal logic objectives,” in 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS), April 2018, pp. 186–197

    2018

  25. [33]

    Exponential control barrier functions for enforcing high relative-degree safety-critical constraints,

    Q. Nguyen and K. Sreenath, “Exponential control barrier functions for enforcing high relative-degree safety-critical constraints,” in 2016 American Control Conference (ACC) , July 2016, pp. 322–328

    2016

  26. [34]

    Control barrier functions for systems with high relative degree,

    W. Xiao and C. Belta, “Control barrier functions for systems with high relative degree,” 2019

    2019

  27. [35]

    An optimal task allocation strategy for heterogeneous multi-robot systems,

    G. Notomista, S. Mayya, S. Hutchinson, and M. Egerstedt, “An optimal task allocation strategy for heterogeneous multi-robot systems,” arXiv preprint arXiv:1903.08641, 2019

    1903 arXiv

  28. [36]

    H. K. Khalil, Nonlinear systems, vol. 3

  29. [37]

    Revising motion planning under linear temporal logic specifications in partially known workspaces,

    Meng Guo, K. H. Johansson, and D. V . Dimarogonas, “Revising motion planning under linear temporal logic specifications in partially known workspaces,” in 2013 IEEE International Conference on Robotics and Automation, May 2013, pp. 5025–5032

    2013

  30. [38]

    Efficient reactive controller synthesis for a fragment of linear temporal logic,

    E. M. Wolff, U. Topcu, and R. M. Murray, “Efficient reactive controller synthesis for a fragment of linear temporal logic,” in 2013 IEEE International Conference on Robotics and Automation , May 2013, pp. 5033–5040

    2013

  31. [39]

    Temporal-logic-based reactive mission and motion planning,

    H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logic-based reactive mission and motion planning,” IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370–1381, Dec 2009

    2009

  32. [40]

    Automata theory meets barrier certificates: Temporal logic verification of nonlinear sys- tems,

    T. Wongpiromsarn, U. Topcu, and A. Lamperski, “Automata theory meets barrier certificates: Temporal logic verification of nonlinear sys- tems,” IEEE Transactions on Automatic Control , vol. 61, no. 11, pp. 3344–3355, 2016

    2016

  33. [41]

    Control barrier function based quadratic programs for safety critical systems,

    A. D. Ames, X. Xu, J. W. Grizzle, and P. Tabuada, “Control barrier function based quadratic programs for safety critical systems,” IEEE Transactions on Automatic Control, vol. 62, no. 8, pp. 3861–3876, Aug 2017

    2017

  34. [42]

    The robotarium: A remotely accessible swarm robotics research testbed,

    D. Pickem, P. Glotfelter, L. Wang, M. Mote, A. Ames, E. Feron, and M. Egerstedt, “The robotarium: A remotely accessible swarm robotics research testbed,” in 2017 IEEE International Conference on Robotics and Automation (ICRA) , May 2017, pp. 1699–1706

    2017

  35. [43]

    Hybrid nonsmooth barrier functions with applications to provably safe and composable collision avoidance for robotic systems,

    P. Glotfelter, I. Buckley, and M. Egerstedt, “Hybrid nonsmooth barrier functions with applications to provably safe and composable collision avoidance for robotic systems,” IEEE Robotics and Automation Letters , vol. 4, no. 2, pp. 1303–1310, April 2019

    2019

  36. [44]

    Near-identity diffeomorphisms and exponential ε- tracking and ε-stabilization of first-order nonholonomic SE(2) vehicles,

    R. Olfati-Saber, “Near-identity diffeomorphisms and exponential ε- tracking and ε-stabilization of first-order nonholonomic SE(2) vehicles,” in Proceedings of the 2002 American Control Conference (IEEE Cat. No.CH37301), vol. 6, May 2002, pp. 4690–4695 vol.6. Mohit Srinivasan is...

    2002

  37. [2019]

    Available: https://www.dhs.gov/science-and-technology/ trustworthy-cyber-infrastructure-power-grid-tcip-g

    [Online]. Available: https://www.dhs.gov/science-and-technology/ trustworthy-cyber-infrastructure-power-grid-tcip-g

Pith tools

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