STL and wSTL control synthesis: A disjunction-centric mixed-integer linear programming approach

作     者：Cardona, Gustavo A. Kamale, Disha Vasile, Cristian-Ioan 

作者机构：Lehigh Univ Dept Mech Engn & Mech Bethlehem PA 18015 USA 

出 版 物：《NONLINEAR ANALYSIS-HYBRID SYSTEMS》 (Nonlinear Anal. Hybrid Syst.)

年 卷 期：2025年第56卷

核心收录：

学科分类：08[工学] 0811[工学-控制科学与工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：MIT Lincoln Laboratory under the project Tactical Edge Reprogramming for Rapid Autonomy Adaptation (TERRAA) 

主　　题：Signal Temporal Logic Control synthesis Mixed integer linear programming Disjunction-centric encoding 

摘      要：This paper introduces an efficient optimization-based control synthesis methodology tailored for Signal Temporal Logic (STL) and its extension, weighted Signal Temporal Logic (wSTL). While STL captures Boolean and temporal operators, wSTL further allows users to express preferences and priorities over concurrent and sequential tasks denoted by weights over logical and temporal operators along with satisfaction times. The proposed approach utilizes Mixed Integer Linear Programming (MILP) for synthesis with both STL and wSTL formulae. We introduce efficient disjunction-centric encodings for STL and wSTL that capture both qualitative and quantitative semantics. This encoding minimizes the number of variables and constraints necessary to represent STL and wSTL formulae by efficiently handling conjunction operations (e.g., conjunction, always operators) and only introducing variables when disjunction operations are used (e.g., disjunction, eventually). Multiple case studies are conducted to demonstrate the proposed methodology s operation and computational efficiency for the control synthesis with STL and wSTL specifications. While non-linear dynamics and predicates can be considered using piecewise linear functions, this work focuses on linear predicates and dynamics. We show how cost functions involving potentially conflicting objectives expressed in terms of states, controls, and satisfaction robustness impact the solutions to the control synthesis problem for STL and wSTL. We conduct a sensitivity analysis of weights used in wSTL formulae, offering detailed insights into how these weights modulate solutions for given formulae. Finally, the time performance of the disjunction-centric encodings for both STL and wSTL is compared against state-of-the-art frameworks, comprehensively evaluating their efficiency and practical applicability.