Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Samet Uzun, Behçet Açıkmeşe

Abstract

This paper presents a smooth parameterization of continuous-time Signal Temporal Logic (CT-STL) specifications for nonconvex trajectory optimization that is sound and complete up to the accuracy of the underlying numerical integration scheme. CT-STL provides a natural framework for encoding rich temporal and logical task requirements, but existing trajectory-optimization formulations typically enforce such specifications only at discrete sampling nodes. In contrast, the proposed method evaluates specifications in dense time, thereby guaranteeing continuous-time satisfaction of always predicates, which is critical for path constraints such as obstacle avoidance, while eliminating the node-induced conservatism of eventually predicates by allowing satisfaction at any time within the prescribed interval. These two dense-time constructions also serve as the main building blocks for handling more general CT-STL formulas, including complex until specifications. Furthermore, the proposed parameterization resolves the locality and gradient-masking issues inherent in standard quantitative semantics, yielding a more favorable landscape for gradient-based solvers. Although dense-time evaluation introduces additional function evaluations during discretization, it also permits substantially coarser temporal grids without sacrificing safety or logical fidelity. This, in turn, reduces the dimension of the resulting nonconvex program, which is often the dominant factor in trajectory-generation cost. The numerical effectiveness and semantic exactness of the proposed framework are demonstrated on an agile quadrotor flight problem subject to a complex continuous-time until specification. The implementation is available at https:// github.com/UW-ACL/TrajOpt_CT-STL

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

Abstract

This paper presents a smooth parameterization of continuous-time Signal Temporal Logic (CT-STL) specifications for nonconvex trajectory optimization that is sound and complete up to the accuracy of the underlying numerical integration scheme. CT-STL provides a natural framework for encoding rich temporal and logical task requirements, but existing trajectory-optimization formulations typically enforce such specifications only at discrete sampling nodes. In contrast, the proposed method evaluates specifications in dense time, thereby guaranteeing continuous-time satisfaction of always predicates, which is critical for path constraints such as obstacle avoidance, while eliminating the node-induced conservatism of eventually predicates by allowing satisfaction at any time within the prescribed interval. These two dense-time constructions also serve as the main building blocks for handling more general CT-STL formulas, including complex until specifications. Furthermore, the proposed parameterization resolves the locality and gradient-masking issues inherent in standard quantitative semantics, yielding a more favorable landscape for gradient-based solvers. Although dense-time evaluation introduces additional function evaluations during discretization, it also permits substantially coarser temporal grids without sacrificing safety or logical fidelity. This, in turn, reduces the dimension of the resulting nonconvex program, which is often the dominant factor in trajectory-generation cost. The numerical effectiveness and semantic exactness of the proposed framework are demonstrated on an agile quadrotor flight problem subject to a complex continuous-time until specification. The implementation is available at https:// github.com/UW-ACL/TrajOpt_CT-STL

Paper Structure

This paper contains 14 sections, 45 equations, 3 figures, 3 tables.

Table of Contents

  1. INTRODUCTION
  2. Preliminaries
  3. Trajectory Optimization with CT-STL Specifications
  4. Control Input Parameterization
  5. Discretization and Multiple Shooting
  6. Parameterization of the CT-STL specifications via GMSR
  7. Parameterization of the logical operators
  8. Parameterization of the temporal operators
  9. Gradient behavior and optimization relevance
  10. Numerical Example
  11. Problem setup
  12. Penalized discretization and prox-convex for solution
  13. Results
  14. CONCLUSIONS AND FUTURE DIRECTIONS

Figures (3)

  • Figure D1: Optimized point-mass quadrotor trajectory together with the charging station. The vehicle reaches the charging region before proceeding to the terminal state, consistent with the continuous-time until specification.
  • Figure D2: Speed profile along the optimized trajectory. The speed remains below the threshold $v_{\mathrm safe}$ until the charging station is reached, and always remains below the global bound $v_{\max}$.
  • Figure D3: Signed charging-station margin $m_{\mathrm c}(t)=d_{\mathrm c}-\|r(t)-r_{\mathrm c}\|_2$. The margin is negative outside the station, zero on the boundary, and positive inside. The first zero crossing marks the witness time for the until specification.

Theorems & Definitions (4)

  • Definition 1: Continuous-time STL semantics donze2010robust
  • Remark 1
  • Remark 2: Smoothing parameter and GMSR extensions
  • Remark 3