Optimization with Temporal and Logical Specifications via Generalized Mean-based Smooth Robustness Measures
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
Cite
@article{arxiv.2405.10996,
title = {Optimization with Temporal and Logical Specifications via Generalized Mean-based Smooth Robustness Measures},
author = {Samet Uzun and Purnanand Elango and Pierre-Loic Garoche and Behcet Acikmese},
journal= {arXiv preprint arXiv:2405.10996},
year = {2024}
}