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

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.