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

TL;DR

This paper introduces a smooth, dense-time parameterization of CT-STL specifications for trajectory optimization, ensuring continuous satisfaction and improving solver performance.

Contribution

It develops a dense-time, smooth parameterization method for CT-STL that guarantees specification satisfaction and enhances gradient-based optimization.

Findings

Enables continuous-time satisfaction of path constraints like obstacle avoidance.

Reduces nonconvex program dimension, lowering computational cost.

Demonstrates effectiveness on a quadrotor flight with complex specifications.

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