pith. sign in

arxiv: 2605.23240 · v1 · pith:J6HGKJDVnew · submitted 2026-05-22 · 💻 cs.RO · cs.SY· eess.SY

Signal Temporal Logic Motion Planning via Graphs of Convex Sets

Yu Chen , Ancheng Hou , Mingyang Feng , Xiao Yu , Xiang Yin This is my paper

Pith reviewed 2026-05-25 04:32 UTC · model grok-4.3

classification 💻 cs.RO cs.SYeess.SY
keywords signal temporal logicmotion planninggraphs of convex setstimed automatabézier splinesconvex optimizationrobot trajectories
0
0 comments X

The pith

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.

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

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.

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.

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.

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.

Where Pith is reading between the lines

These are 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.

Load-bearing premise

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

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.

Figures

Figures reproduced from arXiv: 2605.23240 by Ancheng Hou, Mingyang Feng, Xiang Yin, Xiao Yu, Yu Chen.

Figure 1
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. 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 … view at source ↗
Figure 3
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 ↗
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 baseline is the MPC-based method in [2], [15], which considers STL specifications under discrete-time semantics and solves an MPC problem with… view at source ↗
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] view at source ↗
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] view at source ↗
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. Since ρ is accepting in the product, its final state belongs to S1,F ×S2,F ; hence the projected run ρ1 is accepting in A1. Moreover, ρ1 s… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

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

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.

Axiom & Free-Parameter Ledger

1 free parameters · 2 axioms · 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.
axioms (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.

pith-pipeline@v0.9.0 · 5781 in / 1359 out tokens · 35879 ms · 2026-05-25T04:32:57.967005+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

60 extracted references · 60 canonical work pages · 1 internal anchor

  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

    work page 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

    work page 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

    work page 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

    work page 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

    work page 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

    work page 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

    work page 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

    work page 2021

  9. [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

    work page 2022

  10. [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

    work page 2026

  11. [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

    work page 2025

  12. [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

    work page 2014

  13. [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

    work page 2015

  14. [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

    work page 2015

  15. [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

    work page 2022

  16. [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

    work page 2025

  17. [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

    work page 2020

  18. [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

    work page 1995

  19. [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

    work page 2024

  20. [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

    work page 2024

  21. [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

    work page 2023

  22. [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

    work page 2023

  23. [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

    work page 2015

  24. [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

    work page 2023

  25. [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

    work page 2022

  26. [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

    work page 2024

  27. [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

    work page 1994

  28. [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

    work page 1996

  29. [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

    work page 2017

  30. [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

    work page 2019

  31. [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

    work page 2015

  32. [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

    work page 2016

  33. [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

    work page 2016

  34. [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

    work page 2020

  35. [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

    work page 2001

  36. [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

    work page 2011

  37. [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

    work page 2017

  38. [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

    work page arXiv 2026

  39. [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

    work page 2026

  40. [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

    work page 2022

  41. [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

    work page 2016

  42. [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

    work page 2019

  43. [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

    work page 2020

  44. [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

    work page 2021

  45. [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

    work page 2022

  46. [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

    work page 2024

  47. [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

    work page 2023

  48. [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

    work page 2024

  49. [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

    work page 2025

  50. [50]

    DAG-STL: A Hierarchical Framework for Zero-Shot Trajectory Planning under Signal Temporal Logic Specifications

    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

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  51. [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

    work page arXiv 2025

  52. [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

    work page 1988

  53. [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, Springer, 2015

    work page 2015

  54. [54]

    Faster algorithms for growing collision-free convex polytopes 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

    work page arXiv 2024

  55. [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

    work page 2024

  56. [56]

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

    work page 2011

  57. [57]

    Nesterov and A

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

    work page 1994

  58. [58]

    ApS,The MOSEK Python Fusion API manual

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

    work page 2025

  59. [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

    work page 2011

  60. [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 A2 that inducesξ. SinceS 1 ∩S 2 =∅ and the union construction introduces no tran...

    work page 2019