Motion Planning with Metric Temporal Logic Using Reachability Analysis and Hybrid Zonotopes

TL;DR

This paper tackles motion planning for autonomous systems subject to time-dependent mission specifications expressed in Metric Temporal Logic (MTL). It introduces a framework that encodes MTL specifications into forward reachable sets using hybrid zonotopes, enabling a mixed-integer quadratic program (MIQP) with significantly fewer binary variables than big-M-based methods. Key innovations include compact encoding of the Until operator, a map representation that ties state regions to propositions via augmented binary factors, and a sparsity-friendly reachability construction. The approach is demonstrated through numerical benchmarks and a ROS2 experimental application with multi-agent coordination and region-dependent disturbances, highlighting improved computational efficiency and scalability in time-varying environments. The work advances practical, real-time capable planning under complex temporal logic constraints in dynamic, possibly multi-agent settings.

Abstract

Metric temporal logic (MTL) provides a formal framework for defining time-dependent mission requirements on autonomous vehicles. However, optimizing control decisions subject to these constraints is often computationally expensive. This article presents a method that uses reachability analysis to implicitly express the set of states satisfying an MTL specification and then optimizes to find a motion plan. The hybrid zonotope set representation is used to efficiently and conveniently encode MTL specifications into reachable sets. A numerical benchmark highlights the proposed method's computational advantages as compared to existing methods in the literature. Further numerical examples and an experimental application demonstrate the ability to address time-varying environments, region-dependent disturbances, and multi-agent coordination.

Figures (7)

• Figure 1: Example of a rectangular environment with a single region of interest, $\mathcal{X}_{\pi,1}$, created using (a) a disjoint convex partition and (b) a non-disjoint convex partition.
• Figure 2: Door-key problem where the agent must reach the goal region, $\mathcal{G}$. However, the two door regions, $\mathcal{D}_1$ and $\mathcal{D}_2$, cannot bet entered until the agent visits the corresponding key regions, $\mathcal{K}_1$ and $\mathcal{K}_2$. The hatched regions show the polytopic partition and the gray regions represent obstacles.
• Figure 3: Comparison of problem sizes for the door-key problem.
• Figure 4: Modified traveling salesperson problem where the agent must visit at least one region of each color. The colored regions are moving with constant velocity but rebound off the boundaries of the map. The agent visits a purple region at $k=8$, a red region at $k=13$, a green region at $k=18$, a yellow region at $k=24$, and a blue region at $k=25$.
• Figure 5: Energy-aware problem where the agent must visit three goal regions, $\mathcal{G}_i$. In (a), with no timing constraints on when regions are visited, the agent first visits $\mathcal{G}_2$, recharges, visits $\mathcal{G}_3$, recharges again, and then visits $\mathcal{G}_1$. In (b), the agent must visit $\mathcal{G}_3$ within the first 12 time steps and does not have enough time to visit $\mathcal{G}_2$ on its way to $\mathcal{G}_3$, so it must circle back.

Theorems & Definitions (18)

• Proposition 1
• proof
• Proposition 2
• proof
• Proposition 3
• proof
• Proposition 4
• proof
• Proposition 5
• proof