Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exact Smooth Reformulations for Trajectory Optimization Under Signal Temporal Logic Specifications

Shaohang Han, Joris Verhagen, Jana Tumova

TL;DR

This work tackles trajectory optimization under Signal Temporal Logic by embedding the STL robustness into a differentiable, exact smooth reformulation. By constructing an STL robustness tree and applying node-wise reformulation rules, the authors replace non-smooth max/min operators with exact, differentiable constraints, enabling a smooth NLP that preserves the original feasible set and objective. They demonstrate that the approach yields superior or competitive results compared to smooth under-approximations and MICP on both linear and nonlinear problems, while remaining scalable through DFS-based embedding and warm-start techniques. The method provides practical, open-source tooling for STL-based planning with nonlinear dynamics and predicates, reducing the need for tuning and enabling reliable optimization-based planning under complex temporal specifications.

Abstract

We study motion planning under Signal Temporal Logic (STL), a useful formalism for specifying spatial-temporal requirements. We pose STL synthesis as a trajectory optimization problem leveraging the STL robustness semantics. To obtain a differentiable problem without approximation error, we introduce an exact reformulation of the max and min operators. The resulting method is exact, smooth, and sound. We validate it in numerical simulations, demonstrating its practical performance.

Exact Smooth Reformulations for Trajectory Optimization Under Signal Temporal Logic Specifications

TL;DR

This work tackles trajectory optimization under Signal Temporal Logic by embedding the STL robustness into a differentiable, exact smooth reformulation. By constructing an STL robustness tree and applying node-wise reformulation rules, the authors replace non-smooth max/min operators with exact, differentiable constraints, enabling a smooth NLP that preserves the original feasible set and objective. They demonstrate that the approach yields superior or competitive results compared to smooth under-approximations and MICP on both linear and nonlinear problems, while remaining scalable through DFS-based embedding and warm-start techniques. The method provides practical, open-source tooling for STL-based planning with nonlinear dynamics and predicates, reducing the need for tuning and enabling reliable optimization-based planning under complex temporal specifications.

Abstract

We study motion planning under Signal Temporal Logic (STL), a useful formalism for specifying spatial-temporal requirements. We pose STL synthesis as a trajectory optimization problem leveraging the STL robustness semantics. To obtain a differentiable problem without approximation error, we introduce an exact reformulation of the max and min operators. The resulting method is exact, smooth, and sound. We validate it in numerical simulations, demonstrating its practical performance.

Paper Structure

This paper contains 14 sections, 6 theorems, 17 equations, 2 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries And Problem Formulation
  3. Signal Temporal Logic
  4. STL Robustness Tree
  5. Problem Formulation
  6. Analysis of the Smooth Approximations
  7. Exact Smooth Reformulation
  8. Node-wise Reformulation Rules
  9. Recursive Reformulation on the Robustness Tree
  10. Final Smooth NLP
  11. Numerical Experiments
  12. Linear Benchmarks
  13. Nonlinear Case Study
  14. Conclusion

Key Result

Lemma 1

Given $k>0$ and a vector $\bm{a}=[a_1, \ldots, a_m]^\top$. Without loss of generality, we may assume that $m \geq 2$ and $\bm{a}$ is ordered so that ${a_1\ge\cdots\ge a_m}$, since $\max$, $\min$ and eq:smooth_op are invariant under permutations of the entries. Let $r$ be the number of entries attain

Figures (2)

  • Figure 1: Building blocks used to construct a robustness tree.
  • Figure 2: Comparison of trajectories generated by the baseline method gilpin2020smooth (left) and our approach (right). The color bar indicates the time steps along each trajectory.

Theorems & Definitions (16)

  • Definition 1: Time-bounded STL
  • Definition 2: STL Robustness Semantics
  • Definition 3: STL Robustness Tree
  • Remark 1
  • Lemma 1
  • proof
  • Lemma 2
  • Lemma 3
  • proof
  • Lemma 4
  • ...and 6 more