STLCCP: Efficient Convex Optimization-based Framework for Signal Temporal Logic Specifications

TL;DR

This paper tackles robust controller synthesis under Signal Temporal Logic (STL) specifications for long-horizon dynamical systems, where traditional MIP and NLP approaches struggle with scalability and global optimality. It introduces STLCCP, a structure-aware framework that reformulates the STL robustness into a difference-of-convex (DC) program and solves it via an improved convex-concave procedure (CCP), augmented by a mellowmin smoothing to enable gradient-based optimization. The authors develop a robust robustness-decomposition process, a Tree-Weighted Penalty CCP (TWP-CCP) to leverage the STL hierarchy, and prove equivalence and convergence guarantees alongside soundness and asymptotic completeness for the smoothing approach. Numerical experiments on motion-planning benchmarks show STLCCP outperforms MIP and naive NLP in both robustness and computation time, with the TWP-CCP and mellowmin smoothing further improving stability and scalability in challenging long-horizon tasks.

Abstract

Signal temporal logic (STL) is a powerful formalism for specifying various temporal properties in dynamical systems. However, existing methods, such as mixed-integer programming and nonlinear programming, often struggle to efficiently solve control problems with complex, long-horizon STL specifications. This study introduces \textit{STLCCP}, a novel convex optimization-based framework that leverages key structural properties of STL: monotonicity of the robustness function, its hierarchical tree structure, and correspondence between convexity/concavity in optimizations and conjunctiveness/disjunctiveness in specifications. The framework begins with a structure-aware decomposition of STL formulas, transforming the problem into an equivalent difference of convex (DC) programs. This is then solved sequentially as a convex quadratic program using an improved version of the convex-concave procedure (CCP). To further enhance efficiency, we develop a smooth approximation of the robustness function using a function termed the \textit{mellowmin} function, specifically tailored to the proposed framework. Numerical experiments on motion planning benchmarks demonstrate that \textit{STLCCP} can efficiently handle complex scenarios over long horizons, outperforming existing methods.

Figures (17)

• Figure 1: An example of the robustness tree for formula $\varphi=((A\vee\Diamond_{[1, T]}B)\wedge \square_{[1, T]}C) \wedge((D\wedge E)\vee F)$, where $A,B_1,...,B_T,C_1,...,C_T,D,E,F$ denote predicates. The grey circles represent the $\max$ operators, whereas the white circles represent the $\min$ operators. The square boxes represent predicate functions $g^A,...,g^F:\mathbb{R}^{n}\rightarrow\mathbb{R}$ associated with each predicate.
• Figure 2: The simplified version of the robustness tree in Fig. \ref{['fig:robustnesstree']}.
• Figure 3: two-target
• Figure 4: narrow-passage
• Figure 5: many-target

Theorems & Definitions (49)

• Definition 1
• Remark 1
• Definition 2
• Example 1
• Remark 2
• Definition 3
• Definition 4
• Example 2
• Remark 3
• Remark 4