pith. sign in

arxiv: 2606.06896 · v1 · pith:QGVTMAHYnew · submitted 2026-06-05 · 🧮 math.OC

Successive Convexification for Trajectory Optimization with Continuous-time Satisfaction of Signal Temporal Logic Specifications

Samet Uzun , Beh\c{c}et A\c{c}{\i}kme\c{s}e This is my paper

Pith reviewed 2026-06-27 21:31 UTC · model grok-4.3

classification 🧮 math.OC
keywords trajectory optimizationsignal temporal logicsuccessive convexificationcontinuous-time specificationsoptimal controlrobustness measuresproximal methods
0
0 comments X

The pith

Generalized mean-based robustness lets successive convexification enforce continuous-time signal temporal logic on 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 successive convexification method that incorporates continuous-time signal temporal logic specifications directly into trajectory optimization. It constructs smooth constraints by embedding temporal aggregation into augmented continuous-time dynamics using generalized mean-based robustness, then solves the resulting program with a prox-convex sequential convex programming algorithm that guarantees convergence. This approach is designed to work with time dilation for free final time, multiple-shooting discretization, and finite-dimensional control parameterization. A reader would care because it turns hard-to-handle time-based rules such as always, eventually, and until into forms that standard gradient-based solvers can manage without the locality and gradient-masking problems of ordinary quantitative semantics.

Core claim

The central claim is that generalized mean-based robustness provides a smooth and exact parameterization of discrete-time signal temporal logic that can be lifted to continuous time by embedding the required temporal aggregation into augmented system dynamics; when combined with time dilation, multiple-shooting, and the prox-convex algorithm, the resulting nonconvex optimal-control problem can be solved reliably, yielding trajectories whose continuous-time paths satisfy the original signal temporal logic formulas up to the accuracy set by a user-chosen regularization parameter.

What carries the argument

Generalized mean-based robustness (GMSR) embedded into augmented continuous-time dynamics as the logical building block for differentiable CT-STL constraints.

If this is right

  • The augmentation construction remains largely independent of the particular dynamics transcription or discretization scheme.
  • Accuracy of the resulting CT-STL parameterization is controlled by a single user-selected regularization parameter.
  • The GMSR-based constraints mitigate locality and gradient-masking behavior that appears with standard quantitative semantics.
  • The same framework applies to combined always, eventually, until, and implication specifications on both double-integrator and 6-DoF quadrotor models.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The regularization parameter creates an explicit accuracy-versus-smoothness dial that could be adapted online if computation time permits.
  • Because the construction is described as transcription-independent, it may transfer to other optimal-control toolboxes with only local changes to the state vector.
  • If the prox-convex solves remain fast, the method could support receding-horizon replanning under time-varying STL rules.

Load-bearing premise

Embedding temporal aggregation into augmented continuous-time dynamics via GMSR produces an optimization landscape in which the prox-convex method converges to trajectories that satisfy the original continuous-time STL specifications rather than only the smoothed surrogate.

What would settle it

An optimized trajectory that meets all GMSR-augmented constraints yet violates at least one original continuous-time STL formula when evaluated on the full continuous path would falsify the satisfaction guarantee.

Figures

Figures reproduced from arXiv: 2606.06896 by Beh\c{c}et A\c{c}{\i}kme\c{s}e, Samet Uzun.

Figure 1
Figure 1. Figure 1: shows the optimized trajectory for the always obstacle-avoidance example. The vehicle departs from the straight start-to-goal path, bends around the two implication-type forbidden regions, and passes through the admissible corridor before reaching the terminal state. The color-coded speed profile along the trajectory also indicates a smooth acceleration and deceleration pattern, with no abrupt maneuvers re… view at source ↗
Figure 2
Figure 2. Figure 2: Obstacle-clearance histories for the always example. Both clearance signals remain in the safe region throughout the maneuver, confirming continuous-time satisfaction of the two obstacle-avoidance constraints. confirms this behavior quantitatively. The obstacle￾clearance signals remain in the safe region for the entire horizon, so the trajectory never enters either for￾bidden set. The common continuous-tim… view at source ↗
Figure 3
Figure 3. Figure 3: Optimized trajectory for the three-waypoint [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Distances from the vehicle to the three waypoint cen [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Optimized trajectory for the charging-station [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Speed profile for the charging-station until example. The speed remains below the pre-charging threshold vsa f e until the charging event occurs, while also remaining below the global speed bound throughout the maneuver. maximize x φunt(·),u(·) − wηηp(tf ) + Γbunt subject to . r(t) = v(t), . v(t) = u(t) − g0e3, . ηp (t) = χθ (u(t)) + χT(u(t)) + χv(v(t)), . y(t) = 1 tf h v 2 sa f e − ∥v(t)∥ 2 2 i2 − , . z(t… view at source ↗
Figure 7
Figure 7. Figure 7: Signed charging-station margin for the until exam￾ple. The margin is negative outside the charging region, zero on its boundary, and positive inside. The first zero crossing marks the witness time for the charging event. 4.2 Free-final-time 6-DoF quadrotor example For the main example, the physical quadrotor state and control are xq := (r, v, ϕ, θ, ψ, pb , qb ,rb ) ∈ R12 , uq := (τϕ, τθ , τψ, T) ∈ R4 , whe… view at source ↗
Figure 8
Figure 8. Figure 8: Optimized 3D trajectory for the free-final-time 6-DoF [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Representative state and input histories for the [PITH_FULL_IMAGE:figures/full_fig_p017_9.png] view at source ↗
read the original abstract

This paper presents a successive convexification framework for trajectory optimization under continuous-time Signal Temporal Logic (CT-STL) specifications. The framework employs generalized mean-based robustness (GMSR), a smooth and exact parameterization of discrete-time STL, as a logical building block for constructing differentiable CT-STL constraints in optimal control. It is integrated with time-dilation for free-final-time problems, finite-dimensional control parameterization, multiple-shooting discretization of the dynamics, and a convergence-guaranteed sequential convex programming method, prox-convex, to solve the nonconvex program. The main CT-STL realization embeds temporal aggregation into augmented continuous-time dynamics. This augmentation-based construction is largely transcription-independent, can be incorporated into existing optimal-control pipelines with minimal structural changes, and enables smooth CT-STL parameterizations with accuracy controlled by a user-selected regularization parameter. We also discuss a complementary dense-time realization that evaluates CT-STL formulas directly on the integration subnodes used for dynamics discretization, yielding a smooth and exact parameterization on the numerical trajectory representation, up to the accuracy of the integration scheme. The proposed GMSR-based formulations mitigate the locality and gradient-masking behavior of standard quantitative semantics and therefore provide a favorable landscape for gradient-based trajectory optimization. The framework is demonstrated through trajectory-optimization examples for a double-integrator system with continuous-time \always{}, \eventually{}, and \until{} specifications, and a 6-DoF quadrotor flight problem with combined \always{}, \implication{}, and \eventually{}-type specifications. The implementation is available at https://github.com/UW-ACL/TrajOpt_CT-STL.

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 / 1 minor

Summary. This paper presents a successive convexification framework for trajectory optimization subject to continuous-time Signal Temporal Logic (CT-STL) specifications. It employs generalized mean-based robustness (GMSR) as a smooth parameterization of STL, embedding temporal aggregation into augmented continuous-time dynamics for differentiable constraints. The approach integrates time-dilation for free-final-time problems, finite-dimensional control parameterization, multiple-shooting discretization, and the prox-convex sequential convex programming solver. Complementary dense-time and augmentation-based realizations are discussed, with demonstrations on double-integrator systems (always, eventually, until) and a 6-DoF quadrotor (combined always, implication, eventually), and code released on GitHub.

Significance. If the central claims hold, the work provides a largely transcription-independent method to incorporate CT-STL into existing optimal-control pipelines while mitigating locality and gradient-masking issues of standard quantitative semantics. The reproducible implementation and concrete examples on standard benchmark systems strengthen its potential utility for robotics applications requiring temporal logic constraints.

major comments (2)
  1. [Abstract] Abstract: The central claim that the GMSR-augmented dynamics yield an 'exact' parameterization (up to integration accuracy) whose solutions satisfy the original continuous-time STL specifications rests on the regularization parameter controlling accuracy. No analysis is supplied showing that solutions of the regularized problem converge to exact satisfaction of the unsmoothed CT-STL semantics in the limit as the regularization parameter tends to zero, nor that prox-convex SCP on the surrogate avoids local minima that violate the original specification.
  2. [Abstract] Abstract and § on GMSR-based formulations: The assertion that the augmentation-based construction mitigates gradient-masking and provides a favorable landscape for gradient-based optimization is load-bearing for the framework's advantage over standard quantitative semantics, yet the manuscript provides no supporting error bounds, landscape analysis, or comparison of convergence rates to the original (non-surrogate) problem.
minor comments (1)
  1. The GitHub repository link is a positive feature for reproducibility; ensure the released code includes the exact regularization values and integration tolerances used in the reported quadrotor and double-integrator examples.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments on our manuscript. We address the major comments point by point below, acknowledging the points where the manuscript lacks supporting analysis and outlining planned revisions.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that the GMSR-augmented dynamics yield an 'exact' parameterization (up to integration accuracy) whose solutions satisfy the original continuous-time STL specifications rests on the regularization parameter controlling accuracy. No analysis is supplied showing that solutions of the regularized problem converge to exact satisfaction of the unsmoothed CT-STL semantics in the limit as the regularization parameter tends to zero, nor that prox-convex SCP on the surrogate avoids local minima that violate the original specification.

    Authors: The referee correctly notes that the manuscript does not supply a formal analysis of convergence of the regularized solutions to the original CT-STL semantics as the regularization parameter approaches zero. The GMSR is presented as an exact smooth parameterization for discrete-time STL, with the continuous-time embedding relying on this property and the regularization for smoothness. The prox-convex SCP guarantees convergence to a stationary point of the surrogate problem, but not necessarily to a solution satisfying the unsmoothed specification. We will revise the abstract and the relevant sections to qualify the 'exact' claim as holding up to the regularization and integration accuracy, and add a discussion noting the lack of convergence guarantees to the original semantics as an open question. revision: yes

  2. Referee: [Abstract] Abstract and § on GMSR-based formulations: The assertion that the augmentation-based construction mitigates gradient-masking and provides a favorable landscape for gradient-based optimization is load-bearing for the framework's advantage over standard quantitative semantics, yet the manuscript provides no supporting error bounds, landscape analysis, or comparison of convergence rates to the original (non-surrogate) problem.

    Authors: We agree that no quantitative error bounds, landscape analysis, or convergence rate comparisons are included in the manuscript. The claim is motivated by the fact that GMSR replaces the min and max operators of standard quantitative semantics with generalized means, which are differentiable and do not exhibit the same gradient masking in regions where the robustness is large. The augmentation embeds this into the dynamics for a transcription-independent approach. We will revise the abstract and the GMSR section to provide a more detailed qualitative explanation of the expected benefits and acknowledge that a rigorous landscape analysis is beyond the scope of the current work. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper introduces an augmentation-based embedding of GMSR into continuous-time dynamics for CT-STL constraints, combined with standard successive convexification (prox-convex SCP), time-dilation, and multiple-shooting. No load-bearing step reduces by definition or self-citation to its own inputs; GMSR is presented as a building block with explicit regularization parameter, and claims are supported by external quadrotor/double-integrator examples plus public code. Self-citations on SCP (if present) are not invoked as uniqueness theorems or to close the central argument. The framework remains transcription-independent by construction and does not rename known results or smuggle ansatzes.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 0 invented entities

The framework relies on a user-selected regularization parameter for smoothing accuracy and standard assumptions from optimal control (convexity of subproblems, differentiability after smoothing). No new invented entities are introduced.

free parameters (1)
  • regularization parameter
    Controls accuracy of the smooth CT-STL parameterization; user-selected and affects the approximation quality.
axioms (1)
  • domain assumption prox-convex sequential convex programming guarantees convergence for the formulated nonconvex program
    Invoked to solve the resulting program after GMSR embedding and discretization.

pith-pipeline@v0.9.1-grok · 5837 in / 1213 out tokens · 18447 ms · 2026-06-27T21:31:51.779503+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

75 extracted references · 58 canonical work pages · 1 internal anchor

  1. [1]

    Principles of Model Checking

    Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT press, 2008. URL: https://mitpress.mit.edu/ 9780262026499/principles-of-model-checking/, doi:10.5555/ 1373322

    2008

  2. [2]

    Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming

    Yunus Emre Sahin, Rien Quirynen, and Stefano Di Cairano. Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming. In 2020 American Control Conference (ACC), pages 454–459. IEEE,

    2020

  3. [3]

    URL: https://doi.org/10.23919/ACC45564.2020.9147917, doi:10.23919/acc45564.2020.9147917

    work page doi:10.23919/acc45564.2020.9147917 2020

  4. [4]

    Trajectory optimization for high- dimensional nonlinear systems under STL specifications

    Vince Kurtz and Hai Lin. Trajectory optimization for high- dimensional nonlinear systems under STL specifications. IEEE Control Systems Letters, 5(4):1429–1434, 2020. URL: https://doi. org/10.1109/LCSYS.2020.3038640, doi:10.1109/lcsys.2020. 3038640

    work page doi:10.1109/lcsys.2020.3038640 2020

  5. [5]

    Probabilistic control of heterogeneous swarms subject to graph temporal logic specifications: A decentralized and scalable approach

    Franck Djeumou, Zhe Xu, Murat Cubuktepe, and Ufuk Topcu. Probabilistic control of heterogeneous swarms subject to graph temporal logic specifications: A decentralized and scalable approach. IEEE Transactions on Automatic Control, 68(4):2245– 2260, 2022. URL: https://doi.org/10.1109/TAC.2022.3176797, doi:10.1109/tac.2022.3176797

    work page doi:10.1109/tac.2022.3176797 2022

  6. [6]

    Multirobot coordination with counting temporal logics

    Yunus Emre Sahin, Petter Nilsson, and Necmiye Ozay. Multirobot coordination with counting temporal logics. IEEE Transactions on Robotics, 36(4):1189–1206, 2019. URL: https://doi.org/10.1109/TRO.2019.2957669, doi:10.1109/ tro.2019.2957669. 0.0 2.5 5.0 0 5 10 15Thrust, T [N] 0.0 2.5 5.0 0 5 10 15 20Speed, v [m s □1] 0.0 2.5 5.0 −4 −2 0 2 Altitude, rz [m] 0....

    work page doi:10.1109/tro.2019.2957669 2019

  7. [7]

    Planning of heterogeneous multi-agent systems under signal temporal logic specifications with integral predicates

    Ali Tevfik Buyukkocak, Derya Aksaray, and Yasin Yazıcıo˘ glu. Planning of heterogeneous multi-agent systems under signal temporal logic specifications with integral predicates. IEEE Robotics and Automation Letters, 6(2):1375–1382, 2021. URL: https://doi.org/10.1109/LRA.2021.3057049, doi:10.1109/ lra.2021.3057049

    work page doi:10.1109/lra.2021.3057049 2021

  8. [8]

    Planning for heterogeneous teams of robots with temporal logic, capability, and resource constraints

    Gustavo A Cardona and Cristian-Ioan Vasile. Planning for heterogeneous teams of robots with temporal logic, capability, and resource constraints. The International Journal of Robotics Research, page 02783649241247285, 2024. doi: 10.1177/02783649241247285

    work page doi:10.1177/02783649241247285 2024

  9. [9]

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

    Yash Vardhan Pant, Houssam Abbas, Rhudii A Quaye, and Rahul 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), pages 186–197. IEEE, 2018. URL: https://doi.org/10.1109/ ICCPS.2018.00026, doi:10.1109/iccps.2018.00026

    work page doi:10.1109/iccps.2018.00026 2018

  10. [10]

    Mission planning and control of multi-aircraft systems with signal temporal logic specifications

    Barı¸ s Ba¸ spınar, Hamsa Balakrishnan, and Emre Koyuncu. Mission planning and control of multi-aircraft systems with signal temporal logic specifications. IEEE Access, 7:155941– 155950, 2019. URL: https://doi.org/10.1109/ACCESS.2019. 2949426, doi:10.1109/access.2019.2949426

    work page doi:10.1109/access.2019 2019

  11. [11]

    A decision tree approach to data classification using signal temporal logic

    Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, pages 1–10, 2016. doi: 10.1145/2883817.2883843. 17

    work page doi:10.1145/2883817.2883843 2016

  12. [12]

    A safe preference learning approach for personalization with applications to autonomous vehicles

    Ruya Karagulle, Nikos Aréchiga, Andrew Best, Jonathan DeCastro, and Necmiye Ozay. A safe preference learning approach for personalization with applications to autonomous vehicles. IEEE Robotics and Automation Letters, 9(5):4226–4233,

  13. [13]

    URL: https://doi.org/10.1109/LRA.2024.3375626, doi:10.1109/lra.2024.3375626

    work page doi:10.1109/lra.2024.3375626 2024

  14. [14]

    STLnet: Signal temporal logic enforced multivariate recurrent neural networks

    Meiyi Ma, Ji Gao, Lu Feng, and John Stankovic. STLnet: Signal temporal logic enforced multivariate recurrent neural networks. Advances in Neural Information Processing Systems, 33:14604–14614, 2020. URL: https://dl.acm.org/doi/abs/10. 5555/3495724.3496948, doi:10.5555/3495724.3496948

    work page doi:10.5555/3495724.3496948 2020

  15. [15]

    Q-learning for robust satisfaction of signal temporal logic specifications

    Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), pages 6565–6570. IEEE, 2016. URL: https://doi.org/10.1109/CDC.2016.7799279, doi:10.1109/ cdc.2016.7799279

    work page doi:10.1109/cdc.2016.7799279 2016

  16. [16]

    Alshiekh, R

    Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.11797, doi: 10.1609/aaai.v32i1.11797

    work page doi:10.1609/aaai.v32i1.11797 2018

  17. [17]

    Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods

    Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods. The International Journal of Robotics Research, 42(6):356–370, 2023. doi:10.1177/02783649221082115

    work page doi:10.1177/02783649221082115 2023

  18. [18]

    2003.1238204

    Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pages 46–57. IEEE, 1977. URL: https://doi.org/10.1109/SFCS. 1977.32, doi:10.1109/sfcs.1977.32

    work page doi:10.1109/sfcs 1977

  19. [19]

    A theory of timed automata

    Rajeev Alur and David L Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994. doi:10. 1016/0304-3975(94)90010-8

    1994

  20. [20]

    Receding horizon temporal logic planning

    Tichakorn Wongpiromsarn, Ufuk Topcu, and Richard M Murray. Receding horizon temporal logic planning. IEEE Transactions on Automatic Control, 57(11):2817–2830, 2012. URL: https://doi.org/10.1109/TAC.2012.2195811, doi: 10.1109/tac.2012.2195811

    work page doi:10.1109/tac.2012.2195811 2012

  21. [21]

    TuLiP: a software toolbox for receding horizon temporal logic planning

    Tichakorn Wongpiromsarn, Ufuk Topcu, Necmiye Ozay, Huan Xu, and Richard M Murray. TuLiP: a software toolbox for receding horizon temporal logic planning. In Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, pages 313–314, 2011. doi:10.1145/1967701.1967747

    work page doi:10.1145/1967701.1967747 2011

  22. [22]

    Optimal control of mixed logical dynamical systems with linear temporal logic specifications

    Sertac Karaman, Ricardo G Sanfelice, and Emilio Frazzoli. Optimal control of mixed logical dynamical systems with linear temporal logic specifications. In 2008 47th IEEE Conference on Decision and Control, pages 2117–2122. IEEE,

    2008

  23. [23]

    URL: https://doi.org/10.1109/CDC.2008.4739370, doi:10.1109/cdc.2008.4739370

    work page doi:10.1109/cdc.2008.4739370 2008

  24. [24]

    Specifying real-time properties with metric temporal logic

    Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255–299, 1990. URL: https://doi.org/10.1007/BF01995674, doi:10.1007/ bf01995674

    work page doi:10.1007/bf01995674 1990

  25. [25]

    The benefits of relaxing punctuality

    Rajeev Alur, Tomás Feder, and Thomas A Henzinger. The benefits of relaxing punctuality. Journal of the ACM (JACM), 43(1):116–146, 1996. doi:10.1145/227595.227602

    work page doi:10.1145/227595.227602 1996

  26. [26]

    Monitoring temporal properties of continuous signals

    Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 152–166. Springer, 2004. doi:10.1007/978-3-540-30206-3_ 12

    work page doi:10.1007/978-3-540-30206-3_ 2004

  27. [27]

    Robustness of temporal logic specifications for continuous-time signals

    Georgios E Fainekos and George J Pappas. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42):4262–4291, 2009. doi: 10.1016/j.tcs.2009.06.021

    work page doi:10.1016/j.tcs.2009.06.021 2009

  28. [28]

    Robust satisfaction of temporal logic over real-valued signals

    Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 92–106. Springer, 2010. doi:10.1007/ 978-3-642-15297-9_9

    2010

  29. [29]

    Control barrier functions for signal temporal logic tasks

    Lars Lindemann and Dimos V Dimarogonas. Control barrier functions for signal temporal logic tasks. IEEE Control Systems Letters, 3(1):96–101, 2018. URL: https://doi.org/10.1109/ LCSYS.2018.2853182, doi:10.1109/lcsys.2018.2853182

    work page doi:10.1109/lcsys.2018.2853182 2018

  30. [30]

    Formal methods for control synthesis: An optimization perspective

    Calin Belta and Sadra Sadraddini. Formal methods for control synthesis: An optimization perspective. Annual Review of Control, Robotics, and Autonomous Systems, 2:115–140, 2019. doi:10.1146/annurev-control-053018-023717

    work page doi:10.1146/annurev-control-053018-023717 2019

  31. [31]

    Model predictive control with signal temporal logic specifications

    Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A Seshia. Model predictive control with signal temporal logic specifications. In 53rd IEEE Conference on Decision and Control, pages 81–87. IEEE, 2014. URL: https://doi.org/10. 1109/CDC.2014.7039363, doi:10.1109/cdc.2014.7039363

    work page doi:10.1109/cdc.2014.7039363 2014

  32. [32]

    Robust temporal logic model predictive control

    Sadra Sadraddini and Calin Belta. Robust temporal logic model predictive control. In 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 772–779. IEEE, 2015. URL: https://doi.org/10.1109/ ALLERTON.2015.7447084, doi:10.1109/allerton.2015. 7447084

    work page doi:10.1109/allerton.2015 2015

  33. [33]

    Neural network training as an optimal control problem : — an augmented lagrangian approach —

    Alëna Rodionova, Lars Lindemann, Manfred Morari, and George J Pappas. Time-robust control for STL specifications. In 2021 60th IEEE Conference on Decision and Control (CDC), pages 572–579. IEEE, 2021. URL: https://doi.org/10.1109/ CDC45484.2021.9683477, doi:10.1109/cdc45484.2021. 9683477

    work page doi:10.1109/cdc45484.2021 2021

  34. [34]

    Combined left and right temporal robustness for control under STL specifications

    Alëna Rodionova, Lars Lindemann, Manfred Morari, and George J Pappas. Combined left and right temporal robustness for control under STL specifications. IEEE Control Systems Letters, 7:619–624, 2022. URL: https://doi.org/10.1109/LCSYS. 2022.3209928, doi:10.1109/lcsys.2022.3209928

    work page doi:10.1109/lcsys 2022

  35. [35]

    Smooth operator: Control using the smooth robustness of temporal logic

    Yash Vardhan Pant, Houssam Abbas, and Rahul Mangharam. Smooth operator: Control using the smooth robustness of temporal logic. In 2017 IEEE Conference on Control Technology and Applications (CCTA), pages 1235–1240. IEEE, 2017. URL: https://doi.org/10.1109/CCTA.2017.8062628, doi:10.1109/ ccta.2017.8062628

    work page doi:10.1109/ccta.2017.8062628 2017

  36. [37]

    A smooth robustness measure of signal temporal logic for symbolic control

    Yann Gilpin, Vince Kurtz, and Hai Lin. A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Systems Letters, 5(1):241–246, 2020. URL: https://doi. org/10.1109/LCSYS.2020.3001875, doi:10.1109/lcsys.2020. 3001875

    work page doi:10.1109/lcsys.2020.3001875 2020

  37. [38]

    Successive convexification for optimal control with signal temporal logic specifications

    Yuanqi Mao, Behçet Açıkme¸ se, Pierre-Loic Garoche, and Alexandre Chapoutot. Successive convexification for optimal control with signal temporal logic specifications. In Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control, pages 1–7, 2022. doi:10.1145/3501710.3519518

    work page doi:10.1145/3501710.3519518 2022

  38. [39]

    Robust control for signal temporal logic specifications using discrete average 18 space robustness

    Lars Lindemann and Dimos V Dimarogonas. Robust control for signal temporal logic specifications using discrete average 18 space robustness. Automatica, 101:377–387, 2019. doi:10.1016/ j.automatica.2018.12.022

    2019

  39. [40]

    Arithmetic-geometric mean robustness for control from signal temporal logic specifications

    Noushin Mehdipour, Cristian-Ioan Vasile, and Calin Belta. Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In 2019 American Control Conference (ACC), pages 1690–1695. IEEE, 2019. URL: https://doi.org/10.23919/ACC.2019.8814487, doi:10.23919/ acc.2019.8814487

    work page doi:10.23919/acc.2019.8814487 2019

  40. [41]

    Mixed integer linear programming approach for control synthesis with weighted signal temporal logic

    Gustavo A Cardona, Disha Kamale, and Cristian-Ioan Vasile. Mixed integer linear programming approach for control synthesis with weighted signal temporal logic. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pages 1–12, 2023. doi:10.1145/ 3575870.3587120

    arXiv 2023

  41. [42]

    Specifying user preferences using weighted signal temporal logic

    Noushin Mehdipour, Cristian-Ioan Vasile, and Calin Belta. Specifying user preferences using weighted signal temporal logic. IEEE Control Systems Letters, 5(6):2006–2011, 2020. URL: https://doi.org/10.1109/LCSYS.2020.3047362, doi:10.1109/ lcsys.2020.3047362

    work page doi:10.1109/lcsys.2020.3047362 2006

  42. [43]

    Continuous-time signal temporal logic planning with control barrier functions

    Peter Varnai and Dimos V Dimarogonas. On robustness metrics for learning STL tasks. In 2020 American Control Conference (ACC), pages 5394–5399. IEEE, 2020. URL: https://doi.org/10.23919/ACC45564.2020.9147692, doi: 10.23919/acc45564.2020.9147692

    work page doi:10.23919/acc45564.2020.9147692 2020

  43. [44]

    and Shamma, Jeff S

    Noushin Mehdipour, Cristian-Ioan Vasile, and Calin Belta. Average-based robustness for continuous-time signal temporal logic. In 2019 IEEE 58th Conference on Decision and Control (CDC), pages 5312–5317. IEEE, 2019. URL: https://doi.org/10. 1109/CDC40024.2019.9029989, doi:10.1109/cdc40024.2019. 9029989

    work page doi:10.1109/cdc40024.2019 2019

  44. [45]

    Time robustness in MTL and expressivity in hybrid system falsification

    Takumi Akazaki and Ichiro Hasuo. Time robustness in MTL and expressivity in hybrid system falsification. In International Conference on Computer Aided Verification, pages 356–374. Springer, 2015. doi:10.1007/978-3-319-21668-3_21

    work page doi:10.1007/978-3-319-21668-3_21 2015

  45. [46]

    Optimization with temporal and logical specifications via generalized mean-based smooth robustness measures

    Samet Uzun, Purnanand Elango, Pierre-Loic Garoche, and Behçet Açıkme¸ se. Optimization with temporal and logical specifications via generalized mean-based smooth robustness measures. arXiv preprint arXiv:2405.10996, 2024. URL: https: //doi.org/10.48550/arXiv.2405.10996, arXiv:2405.10996, doi:10.48550/arxiv.2405.10996

    work page doi:10.48550/arxiv.2405.10996 2024

  46. [47]

    Barrier function- based model predictive control under signal temporal logic specifications

    Maria Charitidou and Dimos V Dimarogonas. Barrier function- based model predictive control under signal temporal logic specifications. In 2021 European Control Conference (ECC), pages 734–739. IEEE, 2021. doi:10.23919/ecc54610.2021.9655231

    work page doi:10.23919/ecc54610.2021.9655231 2021

  47. [48]

    Control barrier functions with actuation constraints under signal temporal logic specifications

    Ali Tevfik Buyukkocak, Derya Aksaray, and Yasin Yazıcıo˘ glu. Control barrier functions with actuation constraints under signal temporal logic specifications. In 2022 European Control Conference (ECC), pages 162–168, 2022. doi:10.23919/ ecc55457.2022.9838028

    arXiv 2022

  48. [49]

    Continuous- time control synthesis under nested signal temporal logic specifications

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

  49. [50]

    doi:10.1109/tro.2024.3353081

    work page doi:10.1109/tro.2024.3353081 2024

  50. [51]

    Continuous-time signal temporal logic planning with control barrier functions

    Guang Yang, Calin Belta, and Roberto Tron. Continuous-time signal temporal logic planning with control barrier functions. In 2020 American Control Conference (ACC), pages 4612–4618. IEEE, 2020. doi:10.23919/acc45564.2020.9147387

    work page doi:10.23919/acc45564.2020.9147387 2020

  51. [52]

    Temporally robust multi-agent stl motion planning in continuous time

    Joris Verhagen, Lars Lindemann, and Jana Tumova. Temporally robust multi-agent stl motion planning in continuous time. arXiv preprint arXiv:2310.10585, pages 251– 258, 2024. arXiv:2310.10585, doi:10.23919/acc60939.2024. 10644216

    work page doi:10.23919/acc60939.2024 2024

  52. [53]

    Signal temporal logic planning with time-varying robustness

    Yating Yuan, Thanin Quartz, and Jun Liu. Signal temporal logic planning with time-varying robustness. IEEE Control Systems Letters, 8:3015–3020, 2024. doi:10.1109/lcsys.2024. 3520152

    work page doi:10.1109/lcsys.2024 2024

  53. [54]

    Continuous-time control synthesis for multiple quadrotors under signal temporal logic specifications

    Yating Yuan. Continuous-time control synthesis for multiple quadrotors under signal temporal logic specifications. CoRR, abs/2505.07240, 2025. URL: https://arxiv.org/abs/2505.07240, arXiv:2505.07240, doi:10.48550/arXiv.2505.07240

    work page doi:10.48550/arxiv.2505.07240 2025

  54. [55]

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

    Gregorio Marchesini, Siyuan Liu, Lars Lindemann, and Dimos V . Dimarogonas. Sampling-based planning under stl specifications: A forward invariance approach. CoRR, abs/2506.10739, 2025. URL: https://arxiv.org/abs/2506.10739, arXiv:2506.10739, doi:10.48550/arXiv.2506.10739

    work page doi:10.48550/arxiv.2506.10739 2025

  55. [56]

    G., Naranjo, S., Rideout, W

    Purnanand Elango, Dayou Luo, Abhinav G Kamath, Samet Uzun, Taewan Kim, and Behçet Açıkme¸ se. Continuous- time successive convexification for constrained trajectory optimization. Automatica, 180:112464, 2025. doi:10.1016/j. automatica.2025.112464

    work page doi:10.1016/j 2025

  56. [57]

    Chari, Abhinav G

    Govind M. Chari, Abhinav G. Kamath, Purnanand Elango, and Behçet Açıkme¸ se. Fast monte carlo analysis for 6-DoF powered-descent guidance via GPU-accelerated sequential convex programming. In AIAA SciTech 2024 Forum, page 1762. AIAA, jan 2024. doi:10.2514/6.2024-1762

    work page doi:10.2514/6.2024-1762 2024

  57. [58]

    Successive convexification for nonlinear model predictive control with continuous-time constraint satisfaction

    Samet Uzun, Purnanand Elango, Abhinav G Kamath, Taewan Kim, and Behçet Açıkme¸ se. Successive convexification for nonlinear model predictive control with continuous-time constraint satisfaction. IFAC-PapersOnLine, 58(18):421–429, aug

  58. [59]

    doi:10.1016/j.ifacol.2024.09.062

    work page doi:10.1016/j.ifacol.2024.09.062 2024

  59. [60]

    Potential of Diffractive Sail’s Sun-Earth Equilibria for Continuous Polar Observation,

    Taewan Kim, Abhinav G Kamath, Niyousha Rahimi, Behçet Açıkme¸ se, Mehran Mesbahi, and Jasper Corleis. Six-degree- of-freedom aircraft landing trajectory planning with runway alignment. Journal of Guidance, Control, and Dynamics, 48(10):2225–2242, 2025. URL: https://doi.org/10.2514/1. G008521, doi:10.2514/1.g008521

    work page doi:10.2514/1 2025

  60. [61]

    Low Lunar Orbit Design via Graphical Manipulation of Eccentricity Vector Evolution

    Samet Uzun, Behçet Açıkme¸ se, and John M Carson. Sequential convex programming for 6-dof powered descent guidance with continuous-time compound state-triggered constraints. In AIAA SCITECH 2025 Forum, page 1895. American Institute of Aeronautics and Astronautics, jan 2025. doi:10.2514/6. 2025-1895

    work page doi:10.2514/6 2025

  61. [62]

    Motion planning for information acquisition via continuous- time successive convexification

    Samet Uzun, Behçet Açıkme¸ se, and Stefano Di Cairano. Motion planning for information acquisition via continuous- time successive convexification. IEEE Control Systems Letters,

  62. [63]

    URL: https://doi.org/10.1109/LCSYS.2025.3576066, doi:10.1109/lcsys.2025.3576066

    work page doi:10.1109/lcsys.2025.3576066 2025

  63. [64]

    Auto-tuned primal-dual successive convexification for powered descent guidance

    Skye Mceowen, Carlos M Morales, Daniel J Calderone, Samet Uzun, Edgerton M Cook, and Behcet Acikmese. Auto-tuned primal-dual successive convexification for powered descent guidance. In AIAA SCITECH 2026 Forum, page 0972, 2026. doi:10.2514/6.2026-0972

    work page doi:10.2514/6.2026-0972 2026

  64. [65]

    Kamath, Samet Uzun, Govind M

    Abhinav G. Kamath, Samet Uzun, Govind M. Chari, Behçet Açıkme¸ se, Purnanand Elango, and Michael Szmuk. SCvxGEN: Successive convexification with automatic custom code generation for fast and embedded general-purpose trajectory optimization, 2025. Software documentation. URL: https: //scvxgen.com

    2025

  65. [66]

    Smooth and Exact Parameterization of Continuous-time Signal Temporal Logic Specifications for Trajectory Optimization

    Samet Uzun and Behçet Açıkme¸ se. Smooth and exact parameterization of continuous-time signal temporal logic specifications for trajectory optimization. arXiv preprint arXiv:2604.04245, 2026. doi:10.48550/arXiv.2604.04245

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2604.04245 2026

  66. [67]

    A multiplicative calculus

    Dick Stanley. A multiplicative calculus. Problems, Resources, and Issues in Mathematics Undergraduate Studies, 9(4):310–326, 1999. doi:10.1080/10511979908965937

    work page doi:10.1080/10511979908965937 1999

  67. [68]

    Multiplicative calculus and its applications

    Agamirza E Bashirov, Emine Mısırlı Kurpınar, and Ali Özyapıcı. Multiplicative calculus and its applications. Journal 19 of mathematical analysis and applications, 337(1):36–48, 2008. doi:10.1016/j.jmaa.2007.03.081

    work page doi:10.1016/j.jmaa.2007.03.081 2008

  68. [69]

    Kamath, Purnanand Elango, Yue Yu, Skye Mceowen, Govind M

    Abhinav G. Kamath, Purnanand Elango, Yue Yu, Skye Mceowen, Govind M. Chari, John M. Carson, III, and Behçet Açıkme¸ se. Real-time sequential conic optimization for multi- phase rocket landing guidance. IFAC-PapersOnLine, 56(2):3118– 3125, 2023. doi:10.1016/j.ifacol.2023.10.1444

    work page doi:10.1016/j.ifacol.2023.10.1444 2023

  69. [70]

    A multiple shooting algorithm for direct solution of optimal control problems

    H G Bock and K J Plitt. A multiple shooting algorithm for direct solution of optimal control problems. IFAC Proceedings Volumes, 17(2):1603–1608, jul 1984. 9th IFAC World Congress: A Bridge Between Control Science and Technology, Budapest, Hungary, 2-6 July 1984. doi:10.1016/s1474-6670(17) 61205-9

    work page doi:10.1016/s1474-6670(17 1984

  70. [71]

    A proximal method for composite optimization with smooth and convex components

    Samet Uzun, Dayou Luo, Behçet Açıkme¸ se, and Aleksandr Y Aravkin. A proximal method for composite optimization with smooth and convex components. arXiv preprint arXiv:2512.20602, 2025. URL: https://arxiv.org/abs/2512. 20602, arXiv:2512.20602, doi:10.48550/arXiv.2512.20602

    work page doi:10.48550/arxiv.2512.20602 2025

  71. [72]

    JAX: composable transformations of Python+ NumPy programs, 2018

    James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, et al. JAX: composable transformations of Python+ NumPy programs, 2018. URL: https://github.com/jax-ml/jax

    2018

  72. [73]

    Cvxpy: A python- embedded modeling language for convex optimization

    Steven Diamond and Stephen Boyd. Cvxpy: A python- embedded modeling language for convex optimization. The Journal of Machine Learning Research, 17(1):2909–2913, 2016. URL: https://www.cvxpy.org/,doi:10.5555/2946645. 3007036

    work page doi:10.5555/2946645 2016

  73. [74]

    QOCO: A quadratic objective conic optimizer with custom solver generation

    Govind M Chari and Behçet Açıkme¸ se. QOCO: A quadratic objective conic optimizer with custom solver generation. arXiv preprint arXiv:2503.12658, 2025. URL: https://doi.org/10. 48550/arXiv.2503.12658, arXiv:2503.12658, doi:10.48550/ arxiv.2503.12658

    arXiv 2025

  74. [75]

    Modelling and control of quadcopter,

    Teppo Luukkonen. Modelling and control of quadcopter,

  75. [76]

    URL: https://sal.aalto.fi/publications/pdf-files/eluu11_ public.pdf. 6 Appendix 6.1 Feasibility of an FOH parameterization of the dilation factor Proposition 7 (Why ZOH is used for s(τ)) If the dila- tion factor were parameterized by FOH, then the physical interval lengths would satisfy ∆tk = 1 2 (sk + sk+1)∆τ. As a result, the normalized interval-length ...