Mixed-Integer Programming for Signal Temporal Logic with Fewer Binary Variables

TL;DR

This paper introduces a more efficient Mixed-Integer Convex Programming encoding for Signal Temporal Logic that reduces the number of binary variables needed, improving scalability for complex control specifications.

Contribution

The authors develop a novel encoding method that encodes disjunctions with logarithmic binary variables and conjunctions without binary variables, enhancing scalability in STL trajectory synthesis.

Findings

Significantly reduces the number of binary variables in STL encoding

Outperforms existing methods on complex, long specifications

Demonstrated effectiveness through simulation examples

Abstract

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.