用STL-GO逻辑统一建模多智能体时空与拓扑约束，实现可验证的协同路径规划。
Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO
- 基于MIP和SMT两种形式化方法，将STL-GO约束转化为可求解优化问题。
- 在多无人机搜救任务中验证，支持动态图交互，团队规模达10架时仍有效。
- 适合需要高可靠协同的复杂场景，如灾害救援、工厂巡检等工程应用。
多智能体规划广泛应用于多机器人灭火、工厂无人机巡检等工程场景。其核心挑战在于同时处理时空约束（何时何地执行任务）与拓扑约束（智能体间的感知、通信、任务关系），通常以图的形式建模。本文聚焦于时空逻辑带图算子（STL-GO）这一新形式化框架，支持对多智能体及其拓扑结构的联合推理。针对在STL-GO中满足路径规划约束的问题，本文提出两种编码方式：基于混合整数规划（MIP）和可满足性模理论（SMT），均具备完备性保证。设计统一接口，支持灵活指定智能体约束、图拓扑及STL-GO规范，便于两种方法的直接比较。在多无人机搜救基准上评估，通过改变团队规模与图复杂度进行消融实验，验证了该方法在动态多图交互下的表达能力与有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。