AI 中文总结
针对多智能体规划中的时空与拓扑约束难题，提出基于STL-GO的混合整数规划与可满足性模理论两种编码方案，在多无人机搜索与救援基准上验证了其表达能力。
AI 中文摘要
多智能体规划问题广泛存在于各类工程应用中，如多机器人野火扑救、工厂无人机巡检等。其核心挑战在于时空约束（即智能体应在何时、何地执行何种操作）与拓扑约束（即智能体间应如何交互，通常通过图的概念形式化）的存在。近年来，已有多种框架被提出，可通过时空逻辑捕获此类约束。本文聚焦于带图算子的时空逻辑（STL-GO），这一新兴形式化方法支持对多智能体及其拓扑（如感知拓扑、通信拓扑、任务拓扑）进行推理。本文研究满足STL-GO规范的多智能体路径规划问题，该问题的核心难点在于需通过STL-GO内置的图算子对多个可能随时间变化的图进行编码。本文提出该问题的两种编码方案：基于混合整数规划（MIP）的方案与基于可满足性模理论（SMT）的方案，二者均具备可靠性保证。本文提供了统一接口，用于指定智能体约束、其图拓扑及STL-GO规范，可无缝使用两种方法并便于直接对比。本文在多无人机搜索与救援基准上对两种编码方案进行评估，针对团队规模与图复杂度开展 ablation 实验，凸显了所提编码方案在动态多图交互下的表达能力。
英文摘要
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.
CommentsAccepted at Formal Methods for Computer-Aided Design 2026
