A More Scalable Mixed-Integer Encoding for Metric Temporal Logic

TL;DR

This paper introduces a new mixed-integer encoding for Metric Temporal Logic that enhances scalability and solver performance, enabling efficient control synthesis for complex specifications in robotics.

Contribution

A novel MICP encoding for finite transition systems that improves scalability to complex MTL specifications by focusing on tight convex relaxation rather than variable reduction.

Findings

Reduces computation times by several orders of magnitude in simulations.

Improves branch-and-bound solver efficiency for long and complex specifications.

Demonstrates scalability in mobile robot grid-world scenarios.

Abstract

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 MICP approach is sound and complete, but struggles to scale to long and complex specifications. Drawing on recent advances in trajectory optimization for piecewise-affine systems, we propose a new MICP encoding for finite transition systems that significantly improves scalability to long and complex MTL specifications. Rather than seeking to reduce the number of variables in the MICP, we focus instead on designing an encoding with a tight convex relaxation. This leads to a larger optimization problem, but significantly improves branch-and-bound solver performance. In simulation experiments involving a mobile robot in a grid-world, the proposed encoding can reduce computation times by several orders of magnitude.