STL-GO를 이용한 시공간 및 위상적 제약 조건 하에서의 다중 에이전트 계획

Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO

다중 에이전트 계획 문제는 다중 로봇 소방 활동이나 공장 내 무인 항공기 검사 등 다양한 엔지니어링 응용 분야에서 발생합니다. 특히, 시공간 제약(즉, 각 에이전트가 언제, 어디서 어떤 작업을 수행해야 하는지)과 위상적 제약(즉, 에이전트들이 어떻게 상호 작용해야 하는지)의 존재는 중요한 과제이며, 이는 일반적으로 그래프 개념을 통해 형식화됩니다. 최근 몇 년 동안 이러한 제약을 시공간 논리를 사용하여 표현할 수 있는 다양한 프레임워크가 제안되었습니다. 본 연구에서는 그래프 연산자를 포함하는 시공간 논리(STL-GO)에 초점을 맞춥니다. STL-GO는 센싱, 통신 및 작업 위상과 같은 다중 에이전트와 그들의 상호 작용에 대한 추론을 지원하는 비교적 새로운 형식입니다. 본 논문에서는 STL-GO로 표현된 제약을 만족하는 다중 에이전트 경로 계획 문제를 다룹니다. 이 문제는 STL-GO의 그래프 연산자에 내재된 여러 개의, 잠재적으로 시간 변화하는 그래프를 인코딩해야 하므로 특히 어렵습니다. 우리는 이 문제를 두 가지 방식으로 인코딩했습니다. 하나는 혼합 정수 프로그래밍(MIP)을 기반으로 하고 다른 하나는 만족 가능성 모듈로 이론(SMT)을 기반으로 하며, 모두 정확성을 보장합니다. 우리는 에이전트 제약 조건, 그래프 위상 및 STL-GO 사양을 지정하기 위한 통합 인터페이스를 제공하여 두 방법 모두를 원활하게 사용할 수 있도록 하고 직접적인 비교를 용이하게 합니다. 우리는 다양한 팀 크기와 그래프 복잡도를 고려하여 다중 UAV 탐색 및 구조 구출 벤치마크에서 제안된 두 인코딩 방식을 평가했습니다. 이를 통해 동적 다중 그래프 상호 작용 환경에서 제안된 인코딩 방식의 표현력을 강조합니다.

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.