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 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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Neural Networks for Encoding Dynamic Security-Constrained Optimal Power Flow
This paper introduces a framework to capture previously intractable optimization constraints and transform them to a mixed-integer linear program, through the use of neural networks. We encode the feasible space of optim…
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 P…
Encoding Linear Constraints into SAT
Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of …
Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications
We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encoding of the STL semantics; it follows the…
Exact Graph Learning via Integer Programming
Learning the dependence structure among variables in complex systems is a central problem across medical, natural, and social sciences. These structures can be naturally represented by graphs, and the task of inferring s…
Graph Learning