Optimization with Temporal and Logical Specifications via Generalized Mean-based Smooth Robustness Measures

TL;DR

This paper presents a novel smooth robustness measure for signal temporal logic that improves numerical optimization for trajectory planning in robotics, demonstrated on quadrotor and rocket landing tasks.

Contribution

It introduces a generalized mean-based C1-smooth robustness measure for STL, enabling efficient optimization with theoretical guarantees.

Findings

The proposed measure is sound and complete.

It improves gradient properties for optimization.

Successful application to quadrotor and rocket landing trajectories.

Abstract

This paper introduces a generalized mean-based C^1-smooth robustness measure over discrete-time signals (D-GMSR) for signal temporal logic (STL) specifications. In conjunction with its C1-smoothness, D-GMSR is proven to be both sound and complete. Furthermore, it demonstrates favorable gradient properties and addresses locality and masking problems, which are critical for numerical optimization. The C^1-smoothness of the proposed formulations enables the implementation of robust and efficient numerical optimization algorithms to solve problems with STL specifications while preserving their theoretical guarantees. The practical utility of the proposed robustness measure is demonstrated on two real-world trajectory optimization problems: i) quadrotor flight, and ii) autonomous rocket landing. A sequential convex programming (SCP) framework, incorporating a convergence-guaranteed optimization algorithm (the prox-linear method) is used to solve inherently non-convex trajectory optimization problems with STL specifications. The implementation is available at https://github.com/UW-ACL/D-GMSR