Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Signal Temporal Logic Meets Convex-Concave Programming: A Structure-Exploiting SQP Algorithm for STL Specifications

Yoshinari Takayama, Kazumune Hashimoto, Toshiyuki Ohtsuka

TL;DR

This work tackles trajectory synthesis for discrete-time linear systems under Signal Temporal Logic (STL) specifications, addressing the nonconvexity and local minima issues that plague traditional smoothing-based SQP approaches. It introduces a CCP-based SQP framework that selectively linearizes concave parts of the robustness expression, preserving convex information and yielding more robust trajectories with faster convergence. A robustness decomposition strategy transforms the STL robustness into a difference-of-convex (DC) program by recursing through the STL tree and introducing slack variables to handle max/min constructs, enabling subproblems to be solved as linear or quadratic programs. Empirical results on a two-target STL task show superior robustness and computational efficiency compared to MIP-based and naive NLP methods, confirming the practical impact of exploiting STL structure within an SQP-like solver.

Abstract

This study considers the control problem with signal temporal logic (STL) specifications. Prior works have adopted smoothing techniques to address this problem within a feasible time frame and solve the problem by applying sequential quadratic programming (SQP) methods naively. However, one of the drawbacks of this approach is that solutions can easily become trapped in local minima that do not satisfy the specification. In this study, we propose a new optimization method, termed CCP-based SQP, based on the convex-concave procedure (CCP). Our framework includes a new robustness decomposition method that decomposes the robustness function into a set of constraints, resulting in a form of difference of convex (DC) program that can be solved efficiently. We solve this DC program sequentially as a quadratic program by only approximating the disjunctive parts of the specifications. Our experimental results demonstrate that our method has a superior performance compared to the state-of-the-art SQP methods in terms of both robustness and computational time.

Signal Temporal Logic Meets Convex-Concave Programming: A Structure-Exploiting SQP Algorithm for STL Specifications

TL;DR

This work tackles trajectory synthesis for discrete-time linear systems under Signal Temporal Logic (STL) specifications, addressing the nonconvexity and local minima issues that plague traditional smoothing-based SQP approaches. It introduces a CCP-based SQP framework that selectively linearizes concave parts of the robustness expression, preserving convex information and yielding more robust trajectories with faster convergence. A robustness decomposition strategy transforms the STL robustness into a difference-of-convex (DC) program by recursing through the STL tree and introducing slack variables to handle max/min constructs, enabling subproblems to be solved as linear or quadratic programs. Empirical results on a two-target STL task show superior robustness and computational efficiency compared to MIP-based and naive NLP methods, confirming the practical impact of exploiting STL structure within an SQP-like solver.

Abstract

This study considers the control problem with signal temporal logic (STL) specifications. Prior works have adopted smoothing techniques to address this problem within a feasible time frame and solve the problem by applying sequential quadratic programming (SQP) methods naively. However, one of the drawbacks of this approach is that solutions can easily become trapped in local minima that do not satisfy the specification. In this study, we propose a new optimization method, termed CCP-based SQP, based on the convex-concave procedure (CCP). Our framework includes a new robustness decomposition method that decomposes the robustness function into a set of constraints, resulting in a form of difference of convex (DC) program that can be solved efficiently. We solve this DC program sequentially as a quadratic program by only approximating the disjunctive parts of the specifications. Our experimental results demonstrate that our method has a superior performance compared to the state-of-the-art SQP methods in terms of both robustness and computational time.
Paper Structure (15 sections, 10 theorems, 23 equations, 5 figures)

This paper contains 15 sections, 10 theorems, 23 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. System description
  4. Specification by Signal temporal logic
  5. Smooth approximation
  6. Problem statement
  7. A structure-aware decomposition of STL formulae
  8. Convex-concave procedure (CCP)
  9. Robustness decomposition
  10. Properties of the subproblem
  11. Numerical Experiments
  12. Conclusion
  13. Equivalence between the two programs: \ref{['eq:moto']} and \ref{['eq:max_trans']}
  14. Proof of Proposition \ref{['lem:robust_vs_slack']}
  15. Proof of Theorem \ref{['theo:global']}

Key Result

Proposition 1

Let $\boldsymbol{z}'=(\boldsymbol{x}', \boldsymbol{u}',s'_\xi,\boldsymbol{s}'_{\max},\boldsymbol{s}'_{\min})$ denote a feasible solution for program eq:final. Then, $\overline{\rho}_{\text{rev}}^{\varphi}(\boldsymbol{x}')\leq 0$ holds.

Figures (5)

  • Figure 1: Two-target scenario
  • Figure 2: A tree description of the two-target formula with $T=1$ and $T_d=1$
  • Figure 3: Computational times
  • Figure 4: Robustness scores
  • Figure 6: Example of trajectories generated by the proposed method with 5 random initial values for $T=50$.

Theorems & Definitions (24)

  • Definition 1
  • Example 1
  • Definition 2
  • Definition 3
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Theorem 1
  • proof
  • ...and 14 more