Mixed-Integer Programming for Signal Temporal Logic with Fewer Binary Variables
Signal Temporal Logic (STL) provides a convenient way of encoding complex control objectives for robotic and cyber-physical systems. The state-of-the-art in trajectory synthesis for STL is based on Mixed-Integer Convex Programming (MICP). The MICP approach is sound and complete, but has limited scalability due to exponential complexity in the number of binary variables. In this letter, we propose a more efficient MICP encoding for STL. Our new encoding is based on the insight that disjunction can be encoded using a logarithmic number of binary variables and conjunction can be encoded without binary variables. We demonstrate in simulation examples that our proposed approach significantly outperforms the state-of-the-art for long and complex specifications. Open-source software is available at https://stlpy.readthedocs.io.
Code (1)
Similar Papers 제목 키워드 기반
A More Scalable Mixed-Integer Encoding for Metric Temporal Logic
The state-of-the-art in optimal control from timed temporal logic specifications, including Metric Temporal Logic (MTL) and Signal Temporal Logic (STL), is based on Mixed-Integer Convex Programming (MICP). The standard M…
Direct data-driven control with signal temporal logic specifications
Most control synthesis methods under temporal logic properties require a model of the system, however, identifying such a model can be a challenging task. In this work, we develop a direct data-driven control synthesis m…
Control Synthesis using Signal Temporal Logic Specifications with Integral and Derivative Predicates
In many applications, the integrals and derivatives of signals carry valuable information (e.g., cumulative success over a time window, the rate of change) regarding the behavior of the underlying system. In this paper, …
Multi-Agent Control Synthesis from Global Temporal Logic Tasks with Synchronous Satisfaction Requirements
This paper addresses the multi-agent control problem under global temporal logic tasks, considering agents with heterogeneous capabilities. These global tasks involve not only absolute and relative temporal and spatial c…
Motion PlanningSTLCCP: Efficient Convex Optimization-based Framework for Signal Temporal Logic Specifications
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 …
Motion Planning