STL-GO enables multi-agent planning with spatio-temporal and graph constraints

Multi-agent planning is notoriously hard when agents must satisfy constraints about when and where actions happen and how agents interact. STL-GO (Spatio-Temporal Logic with Graph Operators) addresses this by letting planners reason over graphs representing sensing, communication, and task topologies. In this paper, Sheryl Paul and colleagues propose two encodings for planning paths that meet STL-GO specifications: a mixed-integer programming (MIP) formulation and a satisfiability modulo theory (SMT) formulation. Both come with soundness guarantees, meaning any solution found is guaranteed to satisfy the constraints. The authors also provide a unified interface so users can define agent constraints, graph topologies, and STL-GO specs, and then easily switch between the two solvers for comparison.

The team evaluated both encodings on a multi-UAV search-and-rescue benchmark, ablating over team size and graph complexity. Results highlight the expressiveness of the methods under dynamic multi-graph interactions, where graphs may change over time (e.g., communication links dropping or sensing ranges shifting). While MIP and SMT each have strengths, the unified interface makes it practical for engineers to choose the best approach per scenario. This work, accepted at the Formal Methods for Computer-Aided Design (FMCAD) 2026 conference, pushes toward formal, verifiable coordination for autonomous swarms in real-world applications like wildfire fighting and industrial inspection.