Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO
06:00 · August 3, 2026 · arXiv cs.AI RSS
Multi-agent planning problems arise in a variety of engineering applications, such as multi-robot wildfire fighting and unmanned aerial inspection in factories. A particular challenge is the existence of spatio-temporal (i.e., when and/or where an agent should do what) and topological constraints (i.e., how agents should interact), as typically formalized via the notion of graphs. Over the last years, various frameworks have been proposed that can capture such constraints via spatio-temporal logics. We focus here on spatio-temporal logic with graph operators (STL-GO), a recent formalism that supports reasoning about multiple agents and their topologies, such as sensing, communication, and task topologies. In this paper, we consider the problem of planning multi-agent paths that satisfy constraints written in STL-GO. This problem is particularly challenging due to the need of encoding multiple, potentially time-varying graphs via the graph operators inherent to STL-GO. We present two encodings of this problem, one based on mixed-integer programming (MIP) and another based on satisfiability modulo theory (SMT), with soundness guarantees. We provide a unified interface for specifying agent constraints, their graph topologies, and the STL-GO specification, enabling seamless use of both methods and facilitating direct comparison between them. We evaluate both encodings on a multi-UAV search-and-rescue benchmark, ablating over team size and graph complexity, highlighting the expressiveness of the proposed encodings under dynamic multi- graph interactions.
Summary
Multi-agent planning often requires satisfying both spatio-temporal requirements, such as when and where each agent must act, and topological constraints that govern how agents interact through sensing, communication, or task-assignment relations. These interactions are naturally modeled as multiple directed or undirected graphs whose edges can change over time. Spatio-Temporal Logic with Graph Operators (STL-GO) provides a compact way to express such specifications by combining standard signal-temporal operators with explicit quantification over neighborhoods in several distinct, time-varying graphs.
The paper introduces two sound encodings that translate STL-GO specifications into centralized, bounded-horizon planning problems. One formulation uses mixed-integer programming (MIP) while the other relies on satisfiability modulo theories (SMT). Both encodings explicitly represent the joint state of the agents, the evolution of multiple weighted interaction graphs, and the neighborhood-cardinality predicates that appear in STL-GO formulas. A single interface accepts agent dynamics, graph definitions, and the STL-GO specification, allowing the same problem to be solved with either backend and enabling direct comparison of their performance.
The approach is demonstrated on a multi-UAV search-and-rescue scenario in which locator and rescuer agents must coordinate over sensing, communication, and task-assignment graphs. Experiments vary team size and graph complexity, measuring solve time and encoding size with Gurobi for MIP and Z3 for SMT. An additional grid-world benchmark adapted from prior hyperproperty work further illustrates how STL-GO avoids the quantifier alternation or formula blow-up that arises when the same relational requirements are expressed in HyperLTL.
Why it matters
This paper provides foundational research in formal methods for multi-agent systems, highly applicable to the Dutch robotics, logistics, and agri-tech sectors. It offers advanced readers rigorous mathematical frameworks to guarantee the safety and coordination of autonomous swarms.
