Pith. sign in

REVIEW 2 major objections 3 minor 1 cited by

Signal Temporal Logic Motion Planning via Graphs of Convex Sets

T0 review · 2 major / 3 minor · reviewed 2026-05-25 · grok-4.3

Pith's one-line read Coupling timed automata for STL specs with convex decompositions of configuration space turns motion planning into a shortest-path problem over graphs of convex sets that yields smooth Bézier trajectories.

desk verdict The paper turns STL specs into smooth Bézier trajectories by building a timed-automaton and GCS product and solving a shortest-path problem on it, with soundness and polynomial complexity once the automaton and decomposition are already fixed. read the letter →

arxiv 2605.23240 v1 pith:J6HGKJDV submitted 2026-05-22 cs.RO cs.SYeess.SY

classification cs.ROcs.SYeess.SY
keywords signaltemporallogicmotionplanninggraphsofconvexsetstimedautomatabéziersplinesoptimizationrobottrajectories
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 develops a planning method for continuous-time robot motions that must satisfy Signal Temporal Logic formulas while obeying smoothness and velocity limits. It converts the STL requirement into a timed automaton and merges it with a convex breakdown of the robot's workspace to create a joint transition system. This system is then modeled as a graph of convex sets whose shortest path encodes both task progress and geometric feasibility. Solving the resulting convex relaxation produces a Bézier spline trajectory that meets all constraints. The approach is shown to be sound and to scale polynomially with dimension once the automaton and decomposition are given.

What carries the argument

The joint transition system obtained by coupling a timed automaton for the STL specification with a convex decomposition of the configuration space, which is then encoded as a graph of convex sets whose shortest-path solution produces the desired Bézier spline.

What would settle it

A computed shortest-path solution in the GCS that produces a Bézier trajectory violating the original STL formula or the velocity bounds.

Watch

Extended reading notes

Core claim

An STL specification is represented by a timed automaton, which is coupled with a convex decomposition of the configuration space to form a joint transition system encoding both task progress and region occupancy. Based on this joint transition system, the STL motion-planning problem is reformulated as a shortest-path problem over a GCS, whose solution induces a smooth Bézier-spline trajectory satisfying the STL specification, smoothness requirements, and velocity bounds. The formulation is sound and the convex relaxation scales polynomially with the configuration-space dimension and the Bézier degree once the timed automaton and convex decomposition are fixed.

Load-bearing premise

The timed automaton correctly captures the STL specification and the convex decomposition accurately represents the configuration space and its connectivity.

Editorial extensions

If this is right

  • The induced Bézier trajectory satisfies the STL specification, required smoothness, and velocity bounds.
  • Once the automaton and decomposition are fixed, the convex relaxation scales polynomially with configuration-space dimension and Bézier degree.
  • A compact timed-automaton construction is available for an expressive STL fragment via dedicated templates and Boolean composition.
  • The method produces executable trajectories on benchmarks, a 3-D quadrotor, a 30-DoF humanoid, and a physical UR-3 arm.

Reading between the lines

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

  • The same joint-system construction could be reused for other temporal logics that admit timed-automaton encodings.
  • If convex decompositions can be updated online, the polynomial scaling opens a route to receding-horizon STL planning.
  • The quality of the initial convex decomposition directly limits both feasibility and path optimality.
  • Hardware experiments indicate that the resulting splines are directly usable as low-level references without further smoothing.
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, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 3 minor

Summary. The paper proposes combining timed automata for STL specifications with graphs of convex sets (GCS) derived from a convex decomposition of configuration space. The STL planning problem is recast as a shortest-path problem on the resulting GCS; its solution yields a smooth Bézier-spline trajectory satisfying the STL formula, velocity bounds, and smoothness requirements. Soundness of the formulation is claimed, and computational complexity is shown to be polynomial in configuration-space dimension and Bézier degree once the timed automaton and convex decomposition are fixed. A compact timed-automaton construction for an expressive STL fragment is also given, supported by numerical experiments on low-dimensional cases, a 3-D quadrotor, a 30-DoF humanoid, and a UR-3 hardware demonstration.

Significance. If the soundness result holds, the work supplies a scalable, convex-optimization-based route to continuous-time STL motion planning that produces executable smooth trajectories for high-DoF systems. The explicit conditioning on fixed automata and decompositions, together with the polynomial scaling claim for the GCS relaxation, distinguishes the contribution from prior discrete or sampling-based STL planners and could influence practical deployment in robotics tasks with temporal requirements.

major comments (2)
  1. [Abstract / complexity analysis] Abstract and § on complexity: the polynomial scaling statement is explicitly conditioned on the timed automaton and convex decomposition already being fixed; the manuscript should state the explicit dependence of GCS size (hence solve time) on the number of automaton states and regions so that the overall complexity claim is unambiguous.
  2. [Soundness section] The soundness argument rests on the product construction correctly lifting discrete transitions to continuous-time STL satisfaction via Bézier segments; the manuscript should supply the precise lemma showing that satisfaction of the timed-automaton acceptance condition plus region occupancy implies STL satisfaction over the entire continuous trajectory (including at segment boundaries).
minor comments (3)
  1. [Preliminaries / joint transition system] Notation for the joint transition system (states, transitions, labels) should be introduced with a single compact diagram or table early in the paper to aid readability.
  2. [Experiments] The hardware experiment on the UR-3 arm would benefit from a brief description of the low-level controller used to track the Bézier trajectory and any observed tracking error.
  3. [Method] Bézier degree appears as a tunable parameter; a short discussion of its effect on both feasibility and computational cost would strengthen the presentation.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The two major comments are addressed point-by-point below. Both can be resolved by targeted additions and clarifications that strengthen the presentation without altering the technical claims.

read point-by-point responses
  1. Referee: [Abstract / complexity analysis] Abstract and § on complexity: the polynomial scaling statement is explicitly conditioned on the timed automaton and convex decomposition already being fixed; the manuscript should state the explicit dependence of GCS size (hence solve time) on the number of automaton states and regions so that the overall complexity claim is unambiguous.

    Authors: We agree that an explicit statement of the dependence improves clarity. The GCS is constructed with one vertex per pair (automaton state, convex region), so its size is linear in |Q| × |R|. In the revision we will add this relation immediately after the existing conditioning sentence in both the abstract and the complexity section, making the overall scaling unambiguous while preserving the polynomial claim in dimension and degree once |Q| and |R| are fixed. revision: yes

  2. Referee: [Soundness section] The soundness argument rests on the product construction correctly lifting discrete transitions to continuous-time STL satisfaction via Bézier segments; the manuscript should supply the precise lemma showing that satisfaction of the timed-automaton acceptance condition plus region occupancy implies STL satisfaction over the entire continuous trajectory (including at segment boundaries).

    Authors: The current soundness argument sketches the lifting via the product construction and Bézier interpolation, but does not isolate the required implication as a standalone lemma. We will insert a concise lemma (with a short proof) that states: if a trajectory satisfies the timed-automaton acceptance condition and each Bézier segment lies entirely inside its assigned convex region, then the continuous-time signal satisfies the original STL formula at every time, including segment boundaries. This addition will be placed in the soundness subsection. revision: yes

Circularity Check

0 steps flagged · score 0.0 of 10

Derivation is self-contained with no circular reductions

full rationale

The paper conditions its polynomial scaling result on the timed automaton and convex decomposition already being fixed, then reformulates the planning problem as a GCS shortest-path instance whose solution induces a Bézier trajectory. Soundness follows from the standard product construction between the automaton and the decomposition. No equations or claims reduce by construction to fitted parameters, self-definitions, or load-bearing self-citations; the central claims remain independent of the paper's own inputs once the precondition is granted. This is the normal case of a compositional method built on prior automata and optimization primitives.

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

The approach rests on domain assumptions from automata theory and convex geometry without new free parameters or invented entities beyond standard choices such as Bézier degree.

free parameters (1)
  • Bézier degree
    Chosen as input to the polynomial scaling analysis; not fitted to data but affects trajectory smoothness.
assumptions (2)
  • domain assumption The configuration space admits a fixed convex decomposition.
    Invoked to form the joint transition system and enable polynomial scaling once fixed.
  • domain assumption The timed automaton faithfully encodes the STL specification.
    Central to coupling task progress with region occupancy in the transition system.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Signal Temporal Logic Motion Planning via Graphs of Convex Sets." pith.science (2026). https://pith.science/paper/J6HGKJDV

@misc{pith2026260523240,
  author       = {Pith},
  title        = {Pith review of: Signal Temporal Logic Motion Planning via Graphs of Convex Sets},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J6HGKJDV}},
  note         = {Machine review of arXiv:2605.23240}
}
abstract

This paper investigates continuous-time motion planning under Signal Temporal Logic (STL) specifications. The goal is to generate smooth robot trajectories that satisfy high-level logical and timing requirements while respecting low-level motion constraints. To this end, we propose an efficient framework that combines timed-automata reasoning with graphs of convex sets (GCS). An STL specification is first represented by a timed automaton, which is then coupled with a convex decomposition of the configuration space to form a joint transition system encoding both task progress and region occupancy. Based on this joint transition system, the STL motion-planning problem is reformulated as a shortest-path problem over a GCS, whose solution induces a smooth B\'ezier-spline trajectory satisfying the STL specification, smoothness requirements, and velocity bounds. We establish the soundness of the proposed formulation and analyze its computational complexity, showing that, once the timed automaton and convex decomposition are fixed, the convex relaxation scales polynomially with the configuration-space dimension and the B\'ezier degree. We further develop a compact timed-automaton construction for an expressive STL fragment using dedicated templates and Boolean composition. Numerical experiments on low-dimensional benchmarks, a $3$-D quadrotor, a $30$-DoF humanoid, and a hardware experiment on a UR-3 robot arm demonstrate that the proposed method efficiently solves complex STL motion-planning problems and produces smooth executable trajectories.

Figures

Figures reproduced from arXiv: 2605.23240 by the authors.

Figure 1
Figure 1. Timed automata for φ1U[a,b]φ2 and G[a,b]φ. Dashed states are accepting states. Here R1 = Rφ1 , R2 = Rφ1∧φ2 . (a) Case of F[a,b]G[c,d]φ. (b) Case of G[a,b]F[c,d]φ [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗
Figure 2
Figure 2. Timed automata for F[a,b]G[c,d]φ and G[a,b]F[c,d]φ. Dashed states are accepting states. Here R1 = Rφ, R2 = R¬φ The intuition behind these templates is as follows. For F[a,b]φ, the automaton enters a φ-enforcing state at some time within [a, b]. For G[a,b]φ, the automaton enters the φ￾enforcing state no later than a and leaves it no earlier than b. For φ1U[a,b]φ2, the state s0 enforces φ1 until a switching time in [a… view at source ↗
Figure 3
Figure 3. Benchmarks and computed trajectories of each method for a [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Results for the 3-D quadrotor experiment. motion planning. The first baseline is the piecewise-linear (PWL) method in [25], which computes a piecewise-linear path satisfying the STL task and assumes the availability of a tracking controller for execution. The second ba…
Figure 5
Figure 5. Figure 5: Visualization of the humanoid STL task. The left panel shows the annotated target regions, and the right panel shows [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Visualization of the hardware experiment under the STL task. The left panel shows the hardware setup, where the green [PITH_FULL_IMAGE:figures/full_fig_p017_6.png]
Figure 7
Figure 7. Figure 7: The TA for Φˆ a run ρ1 of A1. Indeed, right transitions do not change the first component and, because C1 ∩ C2 = ∅, they do not reset any clock in C1. Therefore, the clock valuations and guards along the remaining left transitions are exactly those of a valid run of A1…

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

  1. STL-GCS: A Planner-Controller Framework for Signal Temporal Logic via Graphs of Time-varying Convex Sets

    eess.SY 2026-07 conditional novelty 6.0 of 10

    A GCS-based planner plus control-barrier controller satisfies a disjunctive-convex fragment of STL by keeping the system inside time-varying convex sets in configuration space.

Reference graph

Works this paper leans on

60 extracted references · 60 canonical work pages · cited by 1 Pith paper

  1. [1]

    Synthesis for robots: Guarantees and feedback for robot behavior,

    H. Kress-Gazit, M. Lahijanian, and V . Raman, “Synthesis for robots: Guarantees and feedback for robot behavior,”Annual Review of Control, Robotics, and Autonomous Systems, vol. 1, pp. 211–236, 2018

  2. [2]

    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, vol. 2, no. 1, pp. 115–140, 2019

  3. [3]

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

    X. Yin, B. Gao, and X. Yu, “Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,”Annual Reviews in Control, vol. 57, p. 100940, 2024

  4. [4]

    Monitoring temporal properties of con- tinuous signals,

    O. Maler and D. Nickovic, “Monitoring temporal properties of con- tinuous signals,” inInternational Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 152–166, Springer, 2004

  5. [5]

    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

  6. [6]

    Power line inspection tasks with multi-aerial robot systems via signal temporal logic specifications,

    G. Silano, T. Baca, R. Penicka, D. Liuzza, and M. Saska, “Power line inspection tasks with multi-aerial robot systems via signal temporal logic specifications,”IEEE Robotics and Automation Letters, vol. 6, no. 2, pp. 4169–4176, 2021

  7. [7]

    STLGame: Signal temporal logic games in adversarial multi-agent systems,

    S. Yang, H. Zheng, C.-I. Vasile, G. Pappas, and R. Mangharam, “STLGame: Signal temporal logic games in adversarial multi-agent systems,” in7th Annual Learning for Dynamics & Control Conference, pp. 181–196, PMLR, 2025

  8. [8]

    Learning from demonstra- tions using signal temporal logic,

    A. Puranic, J. Deshmukh, and S. Nikolaidis, “Learning from demonstra- tions using signal temporal logic,” inConference on Robot Learning, pp. 2228–2242, 2021

Show all 60 references
  1. [9]

    Cooperative object manipulation under signal temporal logic tasks and uncertain dynamics,

    M. Sewlia, C. K. Verginis, and D. V . Dimarogonas, “Cooperative object manipulation under signal temporal logic tasks and uncertain dynamics,” IEEE Robotics and Automation Letters, vol. 7, no. 4, pp. 11561–11568, 2022

  2. [10]

    Neuro-symbolic generation of explanations for robot policies with weighted signal temporal logic,

    M. Yuasa, R. S. Sreenivas, and H. T. Tran, “Neuro-symbolic generation of explanations for robot policies with weighted signal temporal logic,” IEEE Robotics and Automation Letters, 2026

  3. [11]

    Robust-locomotion-by-logic: Perturbation-resilient bipedal locomotion via signal temporal logic guided model predictive control,

    Z. Gu, Y . Zhao, Y . Chen, R. Guo, J. K. Leestma, G. S. Sawicki, and Y . Zhao, “Robust-locomotion-by-logic: Perturbation-resilient bipedal locomotion via signal temporal logic guided model predictive control,” IEEE Transactions on Robotics, 2025

  4. [12]

    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,” in53rd IEEE Conference on Decision and Control, pp. 81–87, IEEE, 2014

  5. [13]

    Robust temporal logic model predictive control,

    S. Sadraddini and C. Belta, “Robust temporal logic model predictive control,” in2015 53rd Annual Allerton Conference on Communication, Control, and Computing, pp. 772–779, IEEE, 2015

  6. [14]

    Robust model predic- tive control for signal temporal logic synthesis,

    S. S. Farahani, V . Raman, and R. M. Murray, “Robust model predic- tive control for signal temporal logic synthesis,”IFAC-PapersOnLine, vol. 48, no. 27, pp. 323–328, 2015

  7. [15]

    Mixed-integer programming for signal temporal logic with fewer binary variables,

    V . Kurtz and H. Lin, “Mixed-integer programming for signal temporal logic with fewer binary variables,”IEEE Control Systems Letters, 2022

  8. [16]

    STL and wSTL control synthesis: A disjunction-centric mixed-integer linear programming ap- proach,

    G. A. Cardona, D. Kamale, and C.-I. Vasile, “STL and wSTL control synthesis: A disjunction-centric mixed-integer linear programming ap- proach,”Nonlinear Analysis: Hybrid Systems, vol. 56, p. 101576, 2025

  9. [17]

    Trajectory optimization for high-dimensional non- linear systems under stl specifications,

    V . Kurtz and H. Lin, “Trajectory optimization for high-dimensional non- linear systems under stl specifications,”IEEE Control Systems Letters, vol. 5, no. 4, pp. 1429–1434, 2020

  10. [18]

    Differential flatness of mechanical control systems: A catalog of prototype systems,

    R. M. Murray, M. Rathinam, and W. Sluis, “Differential flatness of mechanical control systems: A catalog of prototype systems,” inASME international mechanical engineering congress and exposition, pp. 349– 357, Citeseer, 1995

  11. [19]

    Marcucci,Graphs of Convex Sets with Applications to Optimal Control and Motion Planning

    T. Marcucci,Graphs of Convex Sets with Applications to Optimal Control and Motion Planning. PhD thesis, Massachusetts Institute of Technology, 2024

  12. [20]

    Shortest paths in graphs of convex sets,

    T. Marcucci, J. Umenberger, P. Parrilo, and R. Tedrake, “Shortest paths in graphs of convex sets,”SIAM Journal on Optimization, vol. 34, no. 1, pp. 507–532, 2024

  13. [21]

    Motion planning around obstacles with convex optimization,

    T. Marcucci, M. Petersen, D. von Wrangel, and R. Tedrake, “Motion planning around obstacles with convex optimization,”Science robotics, vol. 8, no. 84, p. eadf7843, 2023

  14. [22]

    Temporal logic motion planning with convex optimization via graphs of convex sets,

    V . Kurtz and H. Lin, “Temporal logic motion planning with convex optimization via graphs of convex sets,”IEEE Transactions on Robotics, vol. 39, no. 5, pp. 3791–3804, 2023

  15. [23]

    Reac- tive synthesis from signal temporal logic specifications,

    V . Raman, A. Donz´e, D. Sadigh, R. M. Murray, and S. A. Seshia, “Reac- tive synthesis from signal temporal logic specifications,” inProceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 239–248, 2015

  16. [24]

    Mixed integer linear pro- gramming approach for control synthesis with weighted signal temporal logic,

    G. A. Cardona, D. Kamale, and C.-I. Vasile, “Mixed integer linear pro- gramming approach for control synthesis with weighted signal temporal logic,” inProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1–12, 2023

  17. [25]

    Multi-agent motion planning from signal temporal logic specifications,

    D. Sun, J. Chen, S. Mitra, and C. Fan, “Multi-agent motion planning from signal temporal logic specifications,”IEEE Robotics and Automa- tion Letters, vol. 7, no. 2, pp. 3451–3458, 2022

  18. [26]

    Optimization-based model checking and trace synthesis for complex stl specifications,

    S. Sato, J. An, Z. Zhang, and I. Hasuo, “Optimization-based model checking and trace synthesis for complex stl specifications,” inComputer Aided Verification–36th International Conference, CAV 2024, Proceed- ings, pp. 282–306, Springer, 2024

  19. [27]

    A theory of timed automata,

    R. Alur and D. L. Dill, “A theory of timed automata,”Theoretical computer science, vol. 126, no. 2, pp. 183–235, 1994

  20. [28]

    The benefits of relaxing punctuality,

    R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,”Journal of the ACM (JACM), vol. 43, no. 1, pp. 116–146, 1996

  21. [29]

    MightyL: A compositional translation from MITL to timed automata,

    T. Brihaye, G. Geeraerts, H.-H. Ho, and B. Monmege, “MightyL: A compositional translation from MITL to timed automata,” inIn- ternational Conference on Computer Aided Verification, pp. 421–440, Springer, 2017

  22. [30]

    From real-time logic to timed automata,

    T. Ferrere, O. Maler, D. Ni ˇckovi´c, and A. Pnueli, “From real-time logic to timed automata,”Journal of the ACM (JACM), vol. 66, no. 3, pp. 1– 31, 2019

  23. [31]

    Computational methods for stochastic control with metric interval temporal logic specifications,

    J. Fu and U. Topcu, “Computational methods for stochastic control with metric interval temporal logic specifications,” in2015 54th IEEE Conference on Decision and Control (CDC), pp. 7440–7447, IEEE, 2015

  24. [32]

    Timed automata approach for motion planning using metric interval temporal logic,

    Y . Zhou, D. Maity, and J. S. Baras, “Timed automata approach for motion planning using metric interval temporal logic,” inProceedings of the European Control Conference, pp. 690–695, 2016

  25. [33]

    Cooperative task planning of multi-agent systems under timed temporal specifications,

    A. Nikou, J. Tumova, and D. V . Dimarogonas, “Cooperative task planning of multi-agent systems under timed temporal specifications,” in Proceedings of the American Control Conference, pp. 7104–7109, 2016

  26. [34]

    Efficient automata-based plan- ning and control under spatio-temporal logic specifications,

    L. Lindemann and D. V . Dimarogonas, “Efficient automata-based plan- ning and control under spatio-temporal logic specifications,” in2020 American Control Conference (ACC), pp. 4707–4714, IEEE, 2020

  27. [35]

    Randomized kinodynamic planning,

    S. M. LaValle and J. J. Kuffner Jr, “Randomized kinodynamic planning,” The international journal of robotics research, vol. 20, no. 5, pp. 378– 400, 2001

  28. [36]

    Sampling-based algorithms for optimal motion planning,

    S. Karaman and E. Frazzoli, “Sampling-based algorithms for optimal motion planning,”The international journal of robotics research, vol. 30, no. 7, pp. 846–894, 2011

  29. [37]

    Sampling-based synthesis of maximally-satisfying controllers for temporal logic specifications,

    C.-I. Vasile, V . Raman, and S. Karaman, “Sampling-based synthesis of maximally-satisfying controllers for temporal logic specifications,” in2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3840–3847, IEEE, 2017

  30. [38]

    RRT η: Sampling-based motion planning and control from stl specifications using arithmetic- geometric mean robustness,

    A. Ahmad, S. Liu, R. Tron, and C. Belta, “RRT η: Sampling-based motion planning and control from stl specifications using arithmetic- geometric mean robustness,”arXiv preprint arXiv:2602.16825, 2026

  31. [39]

    Sampling-based planning under stl specifications: A forward invariance approach,

    G. Marchesini, S. Liu, L. Lindemann, and D. V . Dimarogonas, “Sampling-based planning under stl specifications: A forward invariance approach,”IEEE Transactions on Automatic Control, 2026

  32. [40]

    Automaton- guided control synthesis for signal temporal logic specifications,

    Q. H. Ho, R. B. Ilyes, Z. N. Sunberg, and M. Lahijanian, “Automaton- guided control synthesis for signal temporal logic specifications,” in 2022 IEEE 61st Conference on Decision and Control (CDC), pp. 3243– 3249, IEEE, 2022

  33. [41]

    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,” in2016 IEEE 55th Conference on Decision and Control, pp. 6565–6570, IEEE, 2016

  34. [42]

    Structured reward functions using stl,

    A. Balakrishnan and J. V . Deshmukh, “Structured reward functions using stl,” inProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 270–271, 2019

  35. [43]

    Tractable reinforcement learning of signal temporal logic objectives,

    H. Venkataraman, D. Aksaray, and P. Seiler, “Tractable reinforcement learning of signal temporal logic objectives,” inLearning for Dynamics and Control, pp. 308–317, PMLR, 2020

  36. [44]

    Model-free reinforcement learning for optimal control of markov decision processes under sig- nal temporal logic specifications,

    K. C. Kalagarla, R. Jain, and P. Nuzzo, “Model-free reinforcement learning for optimal control of markov decision processes under sig- nal temporal logic specifications,” in2021 60th IEEE Conference on Decision and Control, pp. 2252–2257, IEEE, 2021

  37. [45]

    Deep reinforcement learning under signal temporal logic constraints using lagrangian relaxation,

    J. Ikemoto and T. Ushio, “Deep reinforcement learning under signal temporal logic constraints using lagrangian relaxation,”IEEE Access, vol. 10, pp. 114814–114828, 2022

  38. [46]

    Synthesis of temporally-robust policies for signal temporal logic tasks using reinforcement learning,

    S. Wang, S. Li, L. Yin, and X. Yin, “Synthesis of temporally-robust policies for signal temporal logic tasks using reinforcement learning,” in2024 IEEE International Conference on Robotics and Automation, pp. 10503–10509, IEEE, 2024

  39. [47]

    Guided conditional diffusion for controllable traffic simulation,

    Z. Zhong, D. Rempe, D. Xu, Y . Chen, S. Veer, T. Che, B. Ray, and M. Pavone, “Guided conditional diffusion for controllable traffic simulation,” in2023 IEEE International Conference on Robotics and Automation, pp. 3560–3566, IEEE, 2023

  40. [48]

    Diverse controllable diffusion policy with signal temporal logic,

    Y . Meng and C. Fan, “Diverse controllable diffusion policy with signal temporal logic,”IEEE Robotics and Automation Letters, vol. 9, no. 10, pp. 8354–8361, 2024

  41. [49]

    Zero-shot trajectory planning for signal temporal logic tasks,

    R. Liu, A. Hou, X. Yu, and X. Yin, “Zero-shot trajectory planning for signal temporal logic tasks,” inThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025

  42. [50]

    Dag-stl: A hierarchical framework for zero-shot trajectory planning under signal temporal logic specifica- tions,

    R. Liu, A. Hou, X. Yu, and X. Yin, “Dag-stl: A hierarchical framework for zero-shot trajectory planning under signal temporal logic specifica- tions,”arXiv preprint arXiv:2604.18343, 2026

  43. [51]

    Towards tighter convex relaxation of mixed-integer programs: Leveraging logic network flow for task and motion planning,

    X. Lin, J. Ren, Y . Luo, W. Xie, and Y . Zhao, “Towards tighter convex relaxation of mixed-integer programs: Leveraging logic network flow for task and motion planning,”arXiv preprint arXiv:2509.24235, 2025

  44. [52]

    Algorithms for polynomials in bernstein form,

    R. T. Farouki and V . Rajan, “Algorithms for polynomials in bernstein form,”Computer Aided Geometric Design, vol. 5, no. 1, pp. 1–26, 1988

  45. [53]

    Computing large convex regions of obstacle- free space through semidefinite programming,

    R. Deits and R. Tedrake, “Computing large convex regions of obstacle- free space through semidefinite programming,” inAlgorithmic Founda- tions of Robotics XI: Selected Contributions of the Eleventh International Workshop on the Algorithmic Foundations of Robotics, pp. 109–124...

  46. [54]

    Faster algorithms for growing collision-free convex poly- topes in robot configuration space,

    P. Werner, T. Cohn, R. H. Jiang, T. Seyde, M. Simchowitz, R. Tedrake, and D. Rus, “Faster algorithms for growing collision-free convex poly- topes in robot configuration space,”arXiv preprint arXiv:2410.12649, 2024

  47. [55]

    Certified polyhedral decompositions of collision-free configuration space,

    H. Dai, A. Amice, P. Werner, A. Zhang, and R. Tedrake, “Certified polyhedral decompositions of collision-free configuration space,”The International Journal of Robotics Research, vol. 43, no. 9, pp. 1322– 1341, 2024

  48. [56]

    R. E. Kass and P. W. V os,Geometrical foundations of asymptotic inference. John Wiley & Sons, 2011

  49. [57]

    Nesterov and A

    Y . Nesterov and A. Nemirovskii,Interior-point polynomial algorithms in convex programming. SIAM, 1994

  50. [58]

    ApS,The MOSEK Python Fusion API manual

    M. ApS,The MOSEK Python Fusion API manual. Version 11.0., 2025

  51. [59]

    Minimum snap trajectory generation and control for quadrotors,

    D. Mellinger and V . Kumar, “Minimum snap trajectory generation and control for quadrotors,” in2011 IEEE international conference on robotics and automation, pp. 2520–2525, IEEE, 2011

  52. [60]

    Drake: Model-based design and verification for robotics,

    R. Tedrake and the Drake Development Team, “Drake: Model-based design and verification for robotics,” 2019. APPENDIX A. Proof of Proposition 3 Proof of Proposition 3.We first prove 1). For the “=⇒” direction, suppose thatξ|=A 1 F A2. Then there exists an accepting runρofA 1 F ...

Pith tools

Reviewed May 25, 2026 · model on record in the stance chip above.