使用 STL-GO 进行带时空与拓扑约束的多智能体规划

大家读完觉得有帮助记得关注和点赞！！！

摘要
多智能体规划问题出现在各种工程应用中，如多机器人灭火和工厂中的无人机检测。一个特别的挑战是时空约束（即智能体应在何时和/或何处执行何种任务）和拓扑约束（即智能体应如何交互）的存在，这些通常通过图的概念来形式化。近年来，已提出了各种可以通过时空逻辑捕获此类约束的框架。我们在此关注带有图算子的时空逻辑（STL-GO），这是一种支持对多智能体及其拓扑（如感知、通信和任务拓扑）进行推理的最新形式化方法。在本文中，我们考虑规划满足用 STL-GO 编写的约束的多智能体路径的问题。由于需要通过 STL-GO 固有的图算子对多个潜在时变图进行编码，这一问题尤其具有挑战性。我们提出了该问题的两种编码方法，一种基于混合整数规划（MIP），另一种基于可满足性模理论（SMT），并具有可靠性保证。我们提供了一个统一接口，用于指定智能体约束、其图拓扑和 STL-GO 规范，从而能够无缝使用这两种方法并促进它们之间的直接比较。我们在一个多无人机搜索与救援基准上评估了两种编码，对团队规模和图复杂性进行消融实验，突出了所提编码在动态多图交互下的表达能力。

I 引言
经典时序逻辑规范，如 LTL 或 STL，非常适合表达单个系统轨迹的基于时间的性质。然而，在多智能体系统（MAS）中，期望的任务行为可能不仅取决于事件发生的时间，还取决于智能体间通信、空间关系和任务依赖关系。此外，任务目标可能需要推理这些智能体间关系如何随时间演化。因此，一个有用的模型是将多智能体系统视为有向或无向图的集合，其中节点表示具有动态行为的智能体，跨多个图的时变边捕获不同类型智能体间关系。

图1：激励场景：一个异构多智能体系统在卫星地形图上协调野火响应。黄色无人机是定位器智能体，负责巡逻区域以监测火势蔓延并检测紧急情况（红色圆圈标记）。紫色无人机是救援者智能体，任务为到达幸存者并将其运送到救援中心（白色帐篷）。橙色箭头表示感知：定位器无人机检测到紧急现场。蓝色箭头表示智能体间通信链路，定位器通过它共享态势感知。红色箭头表示任务分配：检测到的紧急情况被分配给救援者。绿色箭头描绘救援路径：救援者首先导航至紧急位置，然后到达救援中心。我们的目标是综合满足编码这些协调要求的时空可达性规范、具有形式正确性保证的智能体轨迹。

近期工作集中于时空逻辑形式化方法，如 SSTL [bortolussi2014specifying, nenzi2015qualitative]、SaSTL [ma2020sastl]、SpaTeL [haghighi2015spatel]、STREL [STREL, STRELDynamicNetworks]、Census STL [xu2016census] 和 STL-GO [stlgo]。在这些形式化方法中，STL-GO 允许在多个智能体间关系结构上指定多智能体行为：它支持同时量化不同的时变智能体关系。作为一个激励示例（图1），考虑一个野火响应场景，其中：“每个紧急情况必须在有界时间内被定位器智能体感知；感知后，定位器必须将紧急情况传递给连接的智能体，并在与救援者接触后，将该救援者分配给该紧急情况。救援者必须到达紧急位置并执行救援行动，然后返回安全位置。”该规范同时推理三个不同的拓扑（感知、通信和任务分配），并约束满足期望属性的邻居数量。这类规范是形式化实际多智能体系统（如用于搜索与救援、有限通信下环境监测、不确定地形中分布式感知）行为的第一步。

STREL 在选定的动态加权空间模型上提供基于路径的可达性和逃逸算子，而 Census STL 对种群中的智能体进行计数；两者均未直接将 STL-GO 的类型化邻域基数算子与对交互图集合的显式量化相结合。超属性逻辑如 HyperLTL [hsu2025hyprl, wang2020hyperproperties, finkbeiner2023logics] 也可以表达跨智能体的关系属性，但要求将智能体级量词置于任何时序算子之外。因此，智能体集合和交互关系中的时序变化必须通过显式命题和有限域扩展来表示。我们在第七节中使用 HyperLTL 作为基于先前规划工作的关系规范比较，而非作为多智能体系统的通用基线。

在先前工作 [stlgo] 中，作者关注 STL-GO 规范的运行时监控，假设智能体的时空行为由某个给定规划器决定；如何综合此类计划未被涉及。本文考虑的主要问题是面向多智能体系统的开环、集中式、有界视界规划，受 STL-GO 规范约束，其中智能体和环境动态是确定且已知的。我们关注此情况作为基础基线：可处理的集中编码是分散扩展的先决条件，且据我们所知，尚不存在针对 STL-GO 的此类编码。

在受时序逻辑规范（如 LTL [OnlineMultiRobotLTL, SMTMultiRobotSafeLTL]、STL [FormalMethodsMultiAgent, MultiAgentSTLWaypoints]、ATL [ATL] 和 CaTL [CaTLPlus]）约束的多智能体系统规划方面已有大量工作。现有工作可大致分类如下：基于约束求解/SMT 的综合，其将时序逻辑约束符号化编码并使用 SAT/SMT 求解器推理可行性或正确性 [shoukry2016scalable, shoukry2017linear]；混合整数规划（MIP）方法，其将时序逻辑约束下的运动规划和控制综合表述为关于连续动态和二元决策变量的优化问题 [SMTMultiRobotSafeLTL, MultiAgentSTLWaypoints]；反应式综合，其关注对抗或博弈设置中的策略综合和正确性保证，常用 ATL 或相关形式化方法 [ATL]；以及基于学习的求解器 [NNSTREL, formats]。

受先前基于 SMT 和 MIP 规划工作的启发，我们提出了 STL-GO 规范下集中式规划问题的 SMT 和 MIP 编码。与先前编码方法的关键区别在于，我们显式处理由智能体和环境联合状态诱导的加权时变交互图；这需要将多图量化和邻域基数谓词编码为求解器约束。

贡献：(i) 我们提出了 STL-GO 的 MIP 和 SMT 编码，支持多图存在和全称量化以及时变交互图上的邻域基数谓词，并具有可靠性保证。(ii) 我们提供了一个统一接口，用于指定智能体、交互图、STL-GO 公式和编译为 MIP/SMT 编码计划的目标函数，也使得直接实证比较成为可能。(iii) 我们使用 Gurobi 和 Z3 在一个多无人机搜索与救援基准上对编码进行了实证评估，对团队规模和交互图复杂性进行消融实验。(iv) 我们还在一个改编自 HypRL [hsu2025hyprl] 的结构不同网格世界基准上评估了编码。结果比较了 MIP 和 SMT 后端在求解时间和编码规模上的差异。我们进一步表明，相同规范编码为 HyperLTL 时会招致公式规模的线性膨胀或量词前缀的交替，从而凸显了 STL-GO 的逐点智能体级量化。

本文其余部分组织如下。第二节介绍多智能体系统模型、交互图和 STL-GO。第三节形式化受 STL-GO 规范约束的多智能体系统的有界视界规划问题。第四和第五分别介绍我们基于求解器的综合方法，描述将 STL-GO 规范转换为 MIP 和 SMT 编码的过程。我们在第六节通过仿真评估两种方法并呈现结果，并在第七节讨论相关工作与结论。

II 预备知识

II-A 多智能体系统模型
令 V={1,…,N}V={1,…,N} 为智能体集合，其时空行为在离散时间域 T⊂NT⊂N 上演化。我们考虑一个同质 MAS，其中每个智能体 i∈Vi∈V 在时间 tt 具有状态向量 xti∈Xxti​∈X，其中 XX 是共享状态空间。状态变量编码智能体本地的属性，如物理配置和内部资源。所有智能体在时间 t∈Tt∈T 的联合状态记为 Xt=(xt1,…,xtN)∈XNXt​=(xt1​,…,xtN​)∈XN。虽然为符号清晰我们关注同质设置，但编码可扩展到角色类型异构性，如下面搜索与救援示例中所用。

MAS 环境建模为具有状态 wt∈Wwt​∈W 的离散时间动力系统，其中 WW 编码地图几何（静态或动态）、障碍物和对抗特征（如通信中断）等属性。环境根据 wt+1=f(wt)wt+1​=f(wt​) 确定性演化，其中 ff 和初始世界状态 w0w0​ 已知。因此，当构建规划实例时，有限轨迹 {wt}t=0T{wt​}t=0T​ 是固定的¹。

每个智能体受一个在所有智能体间共享的转移动力学函数 FF 支配（由于 MAS 同质）。在每个时间 tt，智能体 ii 从可容许输入域 UU 中选择控制输入 uti∈Uuti​∈U，其后继状态为：

堆叠分量动力学得到联合后继状态：

其中 Ut=(ut1,…,utN)Ut​=(ut1​,…,utN​) 是联合控制输入。

示例1。考虑一个 V={1,…,N}V={1,…,N} 机器人的系统，其中智能体 i∈Vi∈V 的状态为 xti:=(pti,θti,κti)xti​:=(pti​,θti​,κti​)，其中：pti=[xti,yti]⊤∈R2pti​=[xti​,yti​]⊤∈R2 是智能体位置，θti∈[0,2π)θti​∈[0,2π) 是方向，κtiκti​ 可指代电池电量等时变资源和能力的集合。在每个时间 tt，每个智能体选择 uti:=(vti,ωti)∈Uuti​:=(vti​,ωti​)∈U，其中 vti∈[vmin⁡,vmax⁡]vti​∈[vmin​,vmax​] 和 ωti∈[ωmin⁡,ωmax⁡]ωti​∈[ωmin​,ωmax​] 分别为线速度和角速度。对于采样时间 Δt>0Δt>0 和单轮模型²，位置和方向更新为 xt+1i=xti+Δt vticos⁡(θti)xt+1i​=xti​+Δtvti​cos(θti​)，yt+1i=yti+Δt vtisin⁡(θti)yt+1i​=yti​+Δtvti​sin(θti​)，θt+1i=wrap[0,2π)(θti+Δt ωti)θt+1i​=wrap[0,2π)​(θti​+Δtωti​)。

为编码每个智能体之间丰富的交互和潜在耦合、它们对世界状态的感知以及它们对系统决策的影响，我们定义交互图的概念 [stlgo]。

定义2（交互图）。一个交互图 GttypeGttype​ 是一个有向加权图 Gttype:=(V,Ettype,wttype)Gttype​:=(V,Ettype​,wttype​)，其中 Ettype⊆V×VEttype​⊆V×V 是边集，wttype:Ettype→R≥0wttype​:Ettype​→R≥0​ 分配边属性（如距离、成本、信号质量）。不同的交互模态由不同的图类型 type∈T:={type1,…,typeM}type∈T:={type1​,…,typeM​} 建模。时间 tt 的所有交互图集合为 Gt:={Gttype∣type∈T}Gt​:={Gttype​∣type∈T}。

示例3。交互图示例包括：(i) 距离图 Gtd=(V,Etd,wtd)Gtd​=(V,Etd​,wtd​) 是一个完全有向图，其中 Etd=V×V∖{(i,i)∣i∈V}Etd​=V×V∖{(i,i)∣i∈V}（所有有序对 i≠ji=j）且 wtdwtd​ 是时间 tt 智能体 ii 和 jj 之间的距离。(ii) 感知图 Gts=(V,Ets,wts)Gts​=(V,Ets​,wts​) 编码时间 tt 智能体 ii 是否能感知智能体 jj，且 (i,j)∈Ets(i,j)∈Ets​。(iii) 通信图 Gtc=(V,Etc,wtc)Gtc​=(V,Etc​,wtc​)，其中 (i,j)∈Etc(i,j)∈Etc​ 当且仅当智能体 ii 能与智能体 jj 通信。(iv) 任务依赖图 Gttask=(V,Ettask,wttask)Gttask​=(V,Ettask​,wttask​)，指示智能体 jj 依赖智能体 ii 执行任务，其中 (i,j)∈Ettask(i,j)∈Ettask​。

II-B 带有图算子的时空逻辑（STL-GO）
STL-GO [stlgo] 扩展了信号时序逻辑（STL）[stl-dejan]，引入图算子以支持推理智能体间的时空和拓扑关系。STL-GO 的语法和语义分为智能体局部公式和多智能体组合公式。

II-B1 智能体局部公式
对于从单个智能体视角指定局部行为的公式，我们使用递归语法：

φ::=⊤∣μx∣¬φ∣φ∧φ∣φUIφ∣InG,EW,#φ∣OutG,EW,#φ.φ::=⊤∣μx​∣¬φ∣φ∧φ∣φUI​φ∣InG,EW,#​φ∣OutG,EW,#​φ.

此处，μxμx​ 表示形如 μx:X→Bμx​:X→B 的原子谓词，将智能体状态映射到布尔值；逻辑否定 ¬φ¬φ 和逻辑合取 φ∧φφ∧φ 按通常定义；UIUI​ 是 STL 中定义的区间 I=[a,b]I=[a,b] 上的 until 算子³。

STL-GO 引入了入向 InG,EW,#InG,EW,#​ 和出向 OutG,EW,#OutG,EW,#​ 图算子，其中 W=[w1,w2]⊆RW=[w1​,w2​]⊆R 约束边权重。基数约束 EE 由端点 e1∈Ne1​∈N，e2∈N∪{∞}e2​∈N∪{∞} 指定，e1≤e2e1​≤e2​，定义为 E=[e1,e2]N:={k∈N∣e1≤k≤e2}E=[e1​,e2​]N​:={k∈N∣e1​≤k≤e2​}。因此，例如 E=[1,∞)NE=[1,∞)N​ 要求至少一条符合条件的边。最后，#∈{∃,∀}#∈{∃,∀} 表示对 TT 中图类型的存有或全称量化，等价于对 GtGt​ 中图实例的量化。

令 MAMA​ 表示由多智能体系统、环境和所选控制序列诱导的有限执行。我们写 (MA,i,t)⊨φ(MA​,i,t)⊨φ 表示智能体局部公式 φφ 在智能体 ii 和时间 tt 的布尔满足性。

图算子允许智能体推理其相邻智能体的轨迹。入向算子 InG,EW,∃φInG,EW,∃​φ 断言存在至少一个图实例 Gttype∈GtGttype​∈Gt​，使得满足 wttype(j,i)∈Wwttype​(j,i)∈W 且 (MA,j,t)⊨φ(MA​,j,t)⊨φ 的指向智能体 ii 的入边 (j,i)(j,i) 的计数属于 EE。全称版本 InG,EW,∀φInG,EW,∀​φ 要求该性质对所有图实例 Gttype∈GtGttype​∈Gt​ 成立。类似地，出向算子 OutG,EW,∃φOutG,EW,∃​φ 表明存在一个图实例，使得从智能体 ii 出发满足条件的出边 (i,j)(i,j) 的计数属于 EE。如果权重不感兴趣，我们设 W:=(−∞,∞)W:=(−∞,∞) 并写简化形式 InG,E#φInG,E#​φ 和 OutG,E#φOutG,E#​φ。

形式化地，记 t⊕I:={t+τ:τ∈I}t⊕I:={t+τ:τ∈I}，我们定义如下递归语义⁴：

II-B2 多智能体公式
STL-GO 使用以下递归语法定义跨多个智能体的性质：

其中 φφ 是智能体局部公式，μμ（无下标 xx）表示形如 μ:X∣V∣×W→Bμ:X∣V∣×W→B 的原子谓词。此类谓词类似于智能体局部谓词 μxμx​，但定义在智能体和世界联合状态 (Xt,wt)(Xt​,wt​) 上。

多智能体公式允许使用逻辑连接词跨智能体指定性质，并使用时序算子跨时间指定性质。算子 i.φi.φ 将智能体局部公式嵌入多智能体公式。算子 FAFA 和 EXEX 分别表示对完整智能体集合 VV 的全称和存在量化，其中 FA φ:=⋀i∈Vi.φFAφ:=⋀i∈V​i.φ 且 EX φ:=⋁i∈Vi.φEXφ:=⋁i∈V​i.φ。

形式化地，我们写 (MA,t)⊨ϕ(MA​,t)⊨ϕ 表示 STL-GO 公式 ϕϕ 在时间 tt 被有限执行 MAMA​ 满足。其语义归纳定义如下：

在我们的示例中，考虑 UAV 被分配搜索与救援任务，智能体被分配两种角色之一：‘定位器’ L⊆VL⊆V 和‘救援者’ R⊆VR⊆V。

紧急事件可能在固定候选位置集合中的任何地点发生，必须由定位器智能体检测并分配给一个或多个救援者。救援者必须在有界时间内解决紧急情况，即到达紧急位置并将被救个体运送到救援中心。令 C⊂R2C⊂R2 表示救援中心，MM 是可能的紧急地点的固定集合，每个 m∈Mm∈M 具有位置 ptm∈R2ptm​∈R2。令 εE,εC>0εE​,εC​>0 分别为到达紧急地点和救援中心的距离容差。对于 ℓ∈Lℓ∈L，r∈Rr∈R，和 m∈Mm∈M，我们定义原子谓词 φmemg(t) ⟺ φmemg​(t)⟺ 紧急情况 mm 在 tt 活跃，φr,mnear(t) ⟺ ∥ptr−ptm∥≤εEφr,mnear​(t)⟺∥ptr​−ptm​∥≤εE​，φratC(t) ⟺ dist(ptr,C)≤εCφratC​(t)⟺dist(ptr​,C)≤εC​，φrcarry(t) ⟺ φrcarry​(t)⟺ 救援者 rr 携带被救个体。令 φℓ,r,mtask(t)φℓ,r,mtask​(t) 表示定位器 ℓℓ 在时间 tt 将救援者 rr 专门分配给紧急情况 mm。令 E≥1:=[1,∞)NE≥1​:=[1,∞)N​。紧急感知谓词是联合几何谓词，而以下其余谓词是使用 STL-GO 图算子派生的智能体局部谓词⁵：

我们编码如下规范：一旦检测到紧急情况，至少一个定位器必须在有界时间 TassignTassign​ 内分配救援者：

III 问题陈述
在本文中，我们关注多智能体系统的开环规划⁶或有界综合问题，即我们的目标是为多个同质智能体系统合成有界视界上的有限控制输入序列，使其满足形式规范。

更具体地，我们考虑智能体集合 V={1,…,N}V={1,…,N}，状态空间 XX 和联合输入 Ut=(ut1,…,utN)∈UNUt​=(ut1​,…,utN​)∈UN，在世界状态空间 WW 中运行。每个智能体在离散时间中根据已知、确定性、同质动力学函数 F:X×U×W→XF:X×U×W→X 演化。对于本文呈现的编码，我们将 FF 限制为在智能体状态、控制输入和世界状态上是仿射的。我们假设当构建规划实例时，初始联合状态 X0X0​ 和有限世界轨迹 {wt}t=0T{wt​}t=0T​ 是固定且已知的。

令 ϕϕ 是在有界视界 T∈NT∈N 上、在诱导图集合序列 {Gt}t=0T{Gt​}t=0T​ 下解释于 MAS MAMA​ 的 STL-GO 公式。那么，我们的目标是合成开环控制序列 {Ut}t=0T−1{Ut​}t=0T−1​，使得根据方程2动力学得到的执行 {Xt}t=0T{Xt​}t=0T​ 在初始状态满足规范，即 (MA,0)⊨ϕ(MA​,0)⊨ϕ。我们可以选择最小化性能目标 J({Xt}t=0T,{Ut}t=0T−1)J({Xt​}t=0T​,{Ut​}t=0T−1​)（例如控制努力、总路径长度等），得到最优有界综合问题。

我们识别一类具有状态依赖交互图的多智能体系统，其特征为图构造函数，对于这些系统，有界综合可以在不对问题编码本身做重大改变的情况下表述为基于优化或满足性问题。

定义4（图构造函数）。对于给定交互模态 type∈Ttype∈T，图构造函数 ΓtypeΓtype 将 X∣V∣×WX∣V∣×W 的元素映射到 VV 上的一个有向加权图。在时间 tt，我们写 Gttype=Γtype(Xt,wt)=(V,Ettype,wttype)Gttype​=Γtype(Xt​,wt​)=(V,Ettype​,wttype​)。因此，对于每个有序对 (i,j)(i,j)，构造函数确定 (i,j)∈Ettype(i,j)∈Ettype​ 是否成立，以及当边存在时其权重 wttype(i,j)wttype​(i,j)。

示例5。令 type=dtype=d 表示基于距离的交互模态。Γd(Xt,wt)Γd(Xt​,wt​) 映射到函数 (i,j)↦d1(xti,xtj)(i,j)↦d1​(xti​,xtj​)，其中 xtixti​ 和 xtjxtj​ 表示智能体 ii 和 jj 的 2D（或 3D）坐标，d1d1​ 是 ℓ1ℓ1​ 距离⁷。

在如上确定性和同质性假设下，并将 ΓtypeΓtype 限制为可编码类（在第四和第五节中明确），有界综合问题可通过引入以下内容转换为适合可满足性检查（如 SMT）或优化（如 MIP）的有限约束集：(i) {xti}t=0T{xti​}t=0T​ 和 {uti}t=0T−1{uti​}t=0T−1​ 的决策变量；(ii) 编码 ϕϕ 各子公式对每个智能体和时刻真值的辅助二元变量；(iii) 在有界视界上强制执行动力学、图构造谓词以及布尔、时序和图算子的 STL-GO 语义的约束。虽然我们关注同质智能体动力学，但编码可扩展到角色类型异构性，如运行示例中定位器/救援者分割所用。

假设。我们关注确定性环境动态下的集中式开环规划。部分可观测和局部观测下的分散规划是最终目标，但我们考虑集中式、完全可观测设置作为基础步骤；该设置下的可处理编码将作为分散扩展的先决条件，我们将其留作未来工作。此外，我们假设智能体自主执行综合的开环计划，确定性环境动态让我们可以在没有概率语义的情况下推理可行性和正确性。

在以下各节中，我们提出一个系统性建模和综合框架，将上述具有多个交互图的规划问题编译为混合整数规划或可满足性问题，用于集中式规划。由于篇幅限制，我们将介绍与图相关的新型编码，并请读者参考附录 C 和 D 中描述的完整编码。

IV 基于 MIP 的 STL-GO 规划编码

IV-A 编码系统规范

系统动力学。我们限制自己为确定性、同质动力学，在智能体状态、智能体输入和世界状态上是仿射的，以便有界综合问题允许 MIP 编码。具体地，令动力学为：

其中 i∈Vi∈V，t=0,…,T−1t=0,…,T−1，且 A,B,EA,B,E 和 cc 具有适当维度。

状态和输入约束。我们假设智能体状态和控制输入位于超矩形集合内，因此它们分量有界为：

交互图。在每个时间 tt，交互图通过定义4的图构造函数 ΓtypeΓtype 从联合智能体状态 Xt∈XNXt​∈XN 和世界状态 wt∈Wwt​∈W 构造。对于每个有序对 (i,j)∈V×V(i,j)∈V×V，i≠ji=j，有向边 (i,j)(i,j) 的存在性由布尔变量表示，而边权重为实值。具体地，写 ηi,jtype:X∣V∣×W→Bηi,jtype​:X∣V∣×W→B 为边存在谓词，ei,jtype:X∣V∣×W→R≥0ei,jtype​:X∣V∣×W→R≥0​ 为边权重表达式。则 (i,j)∈Ettype(i,j)∈Ettype​ 当且仅当 ηi,jtype(Xt,wt)ηi,jtype​(Xt​,wt​) 成立，且存在的边权重为 wttype(i,j)=ei,jtype(Xt,wt)wttype​(i,j)=ei,jtype​(Xt​,wt​)。

为确保与基于求解器的综合兼容，我们将注意力限制在边存在谓词允许精确混合整数编码、边权重函数为 (Xt,wt)(Xt​,wt​) 的分片仿射函数的图构造函数上。令 PWA(X∣V∣×W)PWA(X∣V∣×W) 表示联合智能体和世界状态上的分片仿射函数集合。我们说图构造函数 ΓtypeΓtype 是 MIP-可编码的，如果对于每个有序对 (i,j)(i,j)，ηi,jtypeηi,jtype​ 是具有精确混合整数表示的仿射比较的布尔组合，且 ei,jtype∈PWA(X∣V∣×W)ei,jtype​∈PWA(X∣V∣×W)。编码引入 ai,j,ttype∈{0,1}ai,j,ttype​∈{0,1}，其中 ai,j,ttype=1ai,j,ttype​=1 当且仅当 ηi,jtype(Xt,wt)ηi,jtype​(Xt​,wt​) 成立。原子仿射比较使用具有有效界和所需数值分离裕度的双边 Big-M 约束编码；布尔连接词转换为二元变量上的线性约束。

IV-B 编码智能体局部算子

逻辑与时序算子。原子谓词、逻辑运算符和时序运算符的编码紧密遵循文献中的已有公式 [stl-to-milp1, stl-to-milp2]。为完整性和正确性，它们包含在附录 C 中。

图算子编码。对于智能体 ii 在时间 tt，入向算子 ψ=InG,[e1,e2]W,#φψ=InG,[e1​,e2​]W,#​φ 对每个图类型 type∈Ttype∈T 进行评估。其按类型计数包含入向邻居 j≠ij=i，使得智能体 jj 满足 φφ 且图构造函数权重 Γtype(Xt,wt)(j,i)Γtype(Xt​,wt​)(j,i) 位于可容许区间 W=[wmin⁡,wmax⁡]W=[wmin​,wmax​] 内；计数必须位于 [e1,e2][e1​,e2​] 内。符号 #∈{∃,∀}#∈{∃,∀} 表示对 type∈Ttype∈T 的存在或全称量化。InIn 的 MIP 编码对固定图类型分三步进行，加上第四步在模态量词下组合按类型编码。

1. 符合条件的入边。对每个 j∈V∖{i}j∈V∖{i}，引入二元变量 λj,i,tlow,typeλj,i,tlow,type​ 和 λj,i,thigh,typeλj,i,thigh,type​，分别指示上下权重界的满足，以及一个合格变量 γj,i,ttypeγj,i,ttype​。我们施加：

其中 δw>0δw​>0 是固定数值分离裕度。我们假设可行边权重与每个区间边界外部是 δwδw​-分离的：低于 wmin⁡wmin​ 的权重至多为 wmin⁡−δwwmin​−δw​，高于 wmax⁡wmax​ 的权重至少为 wmax⁡+δwwmax​+δw​。在此约定下，(5) 强制：

1. 计数满足 φφ 的邻居。令 zφ,j,t∈{0,1}zφ,j,t​∈{0,1} 表示子公式 φφ 在时间 tt 被智能体 jj 满足。引入 yj,i,tφ,type∈{0,1}yj,i,tφ,type​∈{0,1} 编码 γj,i,ttype∧zφ,j,tγj,i,ttype​∧zφ,j,t​：

并定义基数

1. 基数强制。首先假设 e2<∞e2​<∞。由于 ci,tIn,φ,typeci,tIn,φ,type​ 是整数值，引入二元变量 αi,tlow,typeαi,tlow,type​ 和 αi,thigh,typeαi,thigh,type​，分别指示 ci,tIn,φ,type<e1ci,tIn,φ,type​<e1​ 和 ci,tIn,φ,type>e2ci,tIn,φ,type​>e2​：

按类型满足变量编码为：

对于下界区间 [e1,∞)N[e1​,∞)N​，仅需下界违规变量：

1. 量化算子。存在性算子 ψ=InG,EW,∃φψ=InG,EW,∃​φ 要求至少一个图类型满足计数性质。对每个 type∈Ttype∈T，上述按类型编码产生满足变量 zψ,i,ttypezψ,i,ttype​；然后强制类型的析取：

这些约束确保 zψ,i,t=1zψ,i,t​=1 当且仅当某个图满足该性质。

全称算子 ψ=InG,EW,∀φψ=InG,EW,∀​φ 要求 TT 中所有图类型满足计数性质。这使用合取而非图类型上的析取来编码：

出向算子通过在所有过程中将 (j,i)(j,i) 替换为 (i,j)(i,j) 从入向情况获得。

引理6。对于由离散时间仿射差分方程描述的多智能体系统，智能体局部 STL-GO 规范的规划问题可编码为 MIP，使得任何满足性赋值都产生满足规范的轨迹。

证明。为节省篇幅，我们提供证明梗概，完整证明见附录 A。我们通过结构归纳建立不变量：

对每个智能体局部子公式 ψψ、智能体 ii 和时间 tt 成立。

1. 动力学约束 (3) 是等式，因此可行赋值对应于 FF 的有效轨迹。

2. 原子谓词、布尔连接词和 until 算子通过标准 Big-M 和展开构造编码 [stl-to-milp1, stl-to-milp2]。

3. 对于 ψ=InG,[e1,e2]W,#φψ=InG,[e1​,e2​]W,#​φ，对每个 type∈Ttype∈T，ΓtypeΓtype 的 MIP-可编码性提供精确边指示器和 PWA 权重表达式。约束 (5) 强制 γj,i,ttype=1γj,i,ttype​=1 当且仅当 (j,i)∈Ettype(j,i)∈Ettype​ 且其权重位于 WW 内。约束 (6) 精确计数那些满足 φφ 的合格邻居。方程 (7)-(8) 编码有限基数区间，而 (9) 编码 [e1,∞)N[e1​,∞)N​。最后，(10)-(11) 编码图类型上的存在或全称量化。出向情况对称。

合取所有约束，智能体局部 STL-GO 规范的规划问题是 MIP 的可行性问题，其决策变量包括每步动作。∎

IV-C 编码多智能体量词

智能体上的存在量化。存在量词 EX φEXφ 在至少一个智能体 i∈Vi∈V 满足 φφ 时成立。令 ψ:=EX φψ:=EXφ。我们将 ψψ 编码为：

智能体上的全称量化。全称量词 FA φFAφ 在 φφ 对所有智能体 i∈Vi∈V 成立时成立。令 ψ:=FA φψ:=FAφ。我们将 ψψ 编码为：

定理7。对于 STL-GO 规范 ϕϕ 和视界 TT，如果多智能体系统动力学和图构造函数如上所述是 MIP-可编码的，且相应的 MIP 编码可行，则所得状态轨迹 {Xt}t=0T{Xt​}t=0T​ 满足 ϕϕ，即 (MA,0)⊨ϕ(MA​,0)⊨ϕ。

证明梗概。引理6建立 (12) 对智能体局部子公式成立。我们通过结构归纳将其扩展到多智能体子公式 ψψ 为 zψ,t=1 ⟺ (MA,t)⊨ψzψ,t​=1⟺(MA​,t)⊨ψ：联合原子谓词、嵌入 i.φi.φ、布尔连接词和 until 在多智能体变量上重用智能体局部论证；EXEX 和 FAFA 编码为 {zφ,i,t}i∈V{zφ,i,t​}i∈V​ 上的析取和合取（第四-C节），通过智能体局部不变量匹配语义。以 zϕ,0=1zϕ,0​=1 为约束的可行性得到 (MA,0)⊨ϕ(MA​,0)⊨ϕ。完整证明见附录 A。∎

V 基于 SMT 的 STL-GO 规划编码

我们将多智能体规划问题编码为线性实数算术与整数（LRA + LIA）理论中的无量词 SMT 实例，其中满足性赋值产生其执行满足 STL-GO 规范的控制序列。

V-A 编码系统规范

状态和控制约束。为确保物理和操作可行性，智能体状态被约束到超矩形工作空间 Xws⊂RnxXws​⊂Rnx​ 并具有分量界，控制输入分量受执行器限制（如最大速度、推力、转向角）有界：

系统动力学。我们假设系统遵循确定性离散时间仿射动力学⁸：

交互图。我们关注结构依赖于图构造函数 ΓtypeΓtype 的交互图。对每个时间 tt 和有序对 (i,j)(i,j)，令 ηi,jtype(Xt,wt)ηi,jtype​(Xt​,wt​) 为边存在谓词，令 ei,jtype(Xt,wt)ei,jtype​(Xt​,wt​) 计算相应边权重。我们说 ΓtypeΓtype 是 SMT-可编码的，如果对每个 (i,j)(i,j)，ηi,jtypeηi,jtype​ 是 LRA+LIA 上的布尔公式，且 ei,jtypeei,jtype​ 是 LRA 项。两者都可直接在无量词 SMT 实例中编码。

V-B 编码智能体局部算子

对每个子公式 ψψ of 规范 φφ、智能体 i∈Vi∈V 和时间 t∈Tt∈T，我们引入布尔变量 zψ,ti∈{⊤,⊥}zψ,ti​∈{⊤,⊥}，意图语义为：

原子谓词、逻辑运算符和时序运算符的编码紧密遵循文献中的已有公式 [momtaz2023monitoring, prabhakar2018automatic]。为完整性和正确性，它们包含在附录 D 中。

图算子。

对于 ψ=InG,[e1,e2]W,#φψ=InG,[e1​,e2​]W,#​φ，SMT 编码对每个固定图类型 type∈Ttype∈T 分三步进行，加上第四步在模态量词 ## 下组合按类型编码。

1. 符合条件的入边。对每个图类型 type∈Ttype∈T、智能体 i,j∈Vi,j∈V 且 i≠ji=j，以及时间 tt，引入布尔变量 bj,i,ttypebj,i,ttype​，指示 (j,i)(j,i) 是图实例 GttypeGttype​ 中的边且其权重位于 WW 内：

其中 ηj,itypeηj,itype​ 是边存在谓词，ej,itype(Xt,wt)ej,itype​(Xt​,wt​) 是图构造函数提供的边权重。如果权重不感兴趣且 W=(−∞,∞)W=(−∞,∞)，权重比较被省略。

1. 计数满足 φφ 的邻居。令 zφ,tjzφ,tj​ 是布尔变量，表示子公式 φφ 在时间 tt 被智能体 jj 满足。编码为：

1. 基数。对每个图类型 type∈Ttype∈T，定义整数变量 ci,ttypeci,ttype​ 计数符合条件的、满足 φφ 的入向邻居：

按类型满足变量受约束：

1. 图类型上的量化。对于 #=∃#=∃，ψψ 在智能体 ii 的满足性是按类型满足性的析取：

对于 #=∀#=∀，使用合取而非析取。OutG,[e1,e2]W,#φOutG,[e1​,e2​]W,#​φ 算子的编码通过将入向情况中的 (j,i)(j,i) 替换为 (i,j)(i,j) 获得。

引理8。对于由离散时间仿射差分方程描述、图构造函数 SMT-可编码的多智能体系统，智能体局部 STL-GO 规范的规划问题可编码为无量词 SMT 实例，使得任何满足性赋值都产生满足规范的轨迹。

证明梗概。我们通过结构归纳建立不变量：

对每个智能体局部子公式 ψψ、智能体 ii 和时间 tt 成立。动力学约束 (16) 是 SMT 变量中的等式，因此任何满足性赋值对应于 FF 的有效轨迹。原子谓词、布尔连接词和 until 算子通过直接 LRA 约束和有界视界上的有限展开编码 [momtaz2023monitoring, prabhakar2018automatic]。对于 ψ=InG,[e1,e2]W,#φψ=InG,[e1​,e2​]W,#​φ，对每个 type∈Ttype∈T，ΓtypeΓtype 的 SMT-可编码性确保边存在谓词和边权重是 LRA+LIA 表达式；(18)-(21) 强制 zψ,ti,type=⊤zψ,ti,type​=⊤ 当且仅当符合条件的满足 φφ 的邻居计数位于 [e1,e2][e1​,e2​] 内，且 (22) 将其提升为图类型上的 ##-量化。出向情况对称。完整证明见附录 B。∎

V-C 编码多智能体量词

存在量词 EX φEXφ 表示至少存在一个智能体 i∈Vi∈V 使得 φφ 成立。对于公式 ψ:=EX φψ:=EXφ，我们将 ψψ 编码为 zψ,t=⋁i∈Vzφ,tizψ,t​=⋁i∈V​zφ,ti​。全称量词 FA φFAφ 类似地使用 ⋀i∈V⋀i∈V​ 而非 ⋁i∈V⋁i∈V​。

定理9。对于 STL-GO 规范 ϕϕ 和视界 TT，如果多智能体系统动力学和图构造函数如上所述是 SMT-可编码的，且 SMT 实例可满足，则任何满足性赋值产生轨迹 {Xt}t=0T{Xt​}t=0T​ 使得 (MA,0)⊨ϕ(MA​,0)⊨ϕ。

证明梗概。引理8建立 (23) 对智能体局部子公式成立。我们通过结构归纳将其扩展到多智能体子公式 ψψ 为 zψ,t=⊤ ⟺ (MA,t)⊨ψzψ,t​=⊤⟺(MA​,t)⊨ψ：联合原子谓词、嵌入 i.φi.φ、布尔连接词和 until 在多智能体变量上重用智能体局部论证；EXEX 和 FAFA 如上编码，通过智能体局部不变量匹配语义。以 zϕ,0=⊤zϕ,0​=⊤ 为约束的 SMT 实例可满足性得到 (MA,0)⊨ϕ(MA​,0)⊨ϕ。完整证明见附录 B。∎

VI 实验与结果

无目标函数（a）

线性目标（b）

二次目标（c）

图2：目标函数对智能体轨迹的影响（5个定位器，2个救援者）。无目标函数（a）时，MIP 返回任意可行解。线性目标（b）和二次目标（c）逐步引导救援者走向更直接的到达紧急地点的路径。

图3：线性目标下跨团队规模的可扩展性。增加定位器数量改善了对监视区域的覆盖，同时救援者根据更密集的检测紧急情况调整路径。

表 I 翻译：消融实验与可扩展性结果

说明：该表格展示了在 SwarmLab 搜救应急规划模拟中，采用 MIP（混合整数规划）和 SMT（可满足性模理论）两种编码方式下的求解时间、变量数量和约束数量。

• ∣L∣ 和 ∣R∣ 分别表示定位器（locator）和救援机器人（rescuer）的数量。

• 报告的时间是场景扫描的总耗时（当 ∣L∣=5 时场景数 ∣Ω∣=4，否则 ∣Ω∣=8）。

• 报告的模型大小是每个场景中最大程序的数据。

• † 表示达到了单场景时间限制，报告的是当前找到的最优解。

• SMT 仅进行可行性求解；目标函数的消融实验仅适用于 MIP。

我们为上述搜索与救援示例实现了一个规划器。令 MM 表示可能发生紧急情况的固定已知集合区域集合。在规划时，每个集合区域的位置已知，但每个集合区域是否包含活跃紧急情况未知。定位器智能体巡逻集合区域，并在进入感知范围时观察其激活状态。活跃紧急情况随后必须被通信、分配给一个或多个救援者，并在有界时间内通过将被救个体运送到救援中心 CC 来解决。为考虑潜在紧急情况，我们为所有可能的紧急激活场景构建计划。

实验实例使用角色特定可容许控制集，同时为所有智能体保留相同的运动模型结构⁹。

令 Ω⊆{0,1}∣M∣Ω⊆{0,1}∣M∣ 表示场景集合，其中 ωm=1ωm​=1 指示在场景 ωω 中集合区域 mm 包含活跃紧急情况，ωm=0ωm​=0 指示不包含。如果考虑所有激活组合，则 ∣Ω∣=2∣M∣∣Ω∣=2∣M∣。

对每个场景 ω∈Ωω∈Ω，编码包含相应的状态和控制序列。这些场景索引序列被联合求解。具有相同定位器观测历史的场景必须具有相同的控制输入，即如果场景 ωω 和 ω′ω′ 在时间 tt 对智能体不可区分，则 Utω=Utω′Utω​=Utω′​。计划仅在定位器观测区分场景后才可分支。

所得解是表示为有限场景树的应急计划。在运行时，智能体初始执行共同计划前缀。当定位器观测到集合区域是否活跃时，选择与该观测一致的分支，执行沿该分支继续。进一步的观测可能选择后续分支。

以下谓词和规范对每个 ω∈Ωω∈Ω 实例化。当上下文清晰时我们省略场景上标。在场景 ωω 中，φmemgφmemg​ 为真当且仅当 ωm=1ωm​=1。

我们引入以下原子谓词：φmemgφmemg​（紧急活跃）、φr,mnearφr,mnear​（救援者靠近紧急情况）、φratCφratC​（救援者在救援中心）和 φrcarryφrcarry​（救援者携带个体）。联合几何谓词 φmsenseφmsense​ 表明至少一个定位器位于紧急情况 mm 的感知范围内。图派生谓词捕获剩余的集体和关系条件：φℓLLφℓLL​（定位器-定位器通信）和 φℓLRφℓLR​（定位器-救援者通信）。令 φℓ,r,mtaskφℓ,r,mtask​ 表示定位器 ℓℓ 在当前时间已将救援者 rr 专门分配给紧急情况 mm 的谓词。其真值意味着相应的任务边 (ℓ,r)∈Ettask(ℓ,r)∈Ettask​ 是活跃的。

我们固定视界 Tdet,Tassign,Trelay,Treach,Tdeliver∈NTdet​,Tassign​,Trelay​,Treach​,Tdeliver​∈N。任务规范如下：

1. 有界紧急检测。每个紧急情况必须在有界时间内被定位器群检测到：

1. 检测到中继。一旦检测到紧急情况，信息必须在有界时间内通信给另一个定位器或救援者：

1. 检测到分配。一旦检测到紧急情况，至少一个定位器必须在有界时间内分配救援者：

1. 救援者响应时间。如果定位器分配救援者，该救援者必须在有界时间内到达紧急情况：

1. 救援与交付。到达紧急情况后，救援者必须将被救个体运送到救援中心：

对每个场景 ω∈Ωω∈Ω，令 ϕωϕω​ 表示在激活分配 ωω 下上述五个任务规范的合取。基于场景的规划问题要求 ⋀ω∈Ωϕω⋀ω∈Ω​ϕω​。所有实验使用 Gurobi [gurobi]（用于 MIP）和 Z3 [z3]（用于 SMT），在配备16 CPU核心和64 GB内存的计算集群上执行。仿真使用定制化的 SwarmLab [swarmlab] 框架进行，该框架扩展以纳入我们的环境和动力学，并执行综合轨迹¹⁰。

目标函数的影响。图2显示了目标函数对5个定位器和2个救援者救援者轨迹的影响。无目标函数（a）时，MIP 返回任意可行计划；线性目标（b）和二次目标（c）逐步塑造救援者走向更直接的路径¹¹。由于 SMT 仅满足性，此比较特定于 MIP 编码，并激励尽管编码规模较大仍保留 MIP 用于目标驱动规划。

增加图复杂性和团队规模的可扩展性评估。我们通过逐步增加规范复杂性（同时保持环境、动力学和目标固定）来评估图依赖约束对规划复杂性的增量影响。从 STL 谓词基线（无图算子）开始，我们添加 (i) 时变感知图的感知邻域约束，(ii) 时变通信图的通信邻域约束，(iii) 时变任务图的任务约束。对每种情况，我们进一步变化定位器和救援者智能体数量（见图3）。

结果。结果见表 I，比较了两种方法在所有消融下的变量数和约束数以及找到解的时间。无图算子的 STL 规范在两个求解器上都扩展得相对较好，并作为清晰基线。添加感知图通过耦合连续智能体状态与逻辑满足性增加了复杂性；通信图通过强制需要联合推理智能体配置的成对邻近约束放大了这一效应；具有决策依赖分配的任务图在两个求解器上都导致求解时间和问题规模的大幅增加。定量上，SMT 编码产生更少的变量和约束并表现出更快的求解时间。MIP 编码尽管规模更大、求解时间更长，但对于目标驱动规划是必需的（图2）；对于最难配置（∣L∣=9,∣R∣=3∣L∣=9,∣R∣=3，所有图，二次目标），在达到最优性之前达到时间限制，表 I 报告最佳当前解。

VII 讨论

相关工作。STL 已通过基于优化的综合广泛用于多智能体控制和规划，包括鲁棒性感知反馈公式 [FormalMethodsMultiAgent, PPCSTL] 和带有时序航点等抽象的 MIP 编码 [MultiAgentSTLWaypoints]。这些方法关注个体智能体轨迹和连续动力学，不显式捕获基于图的空间关系或集体约束。为纳入空间结构，STREL 等时空逻辑引入了基于图的可达性和逃逸算子 [STREL, STRELDynamicNetworks]，使得能够指定和监控集体行为。STREL 的基于学习和综合方法也已被探索 [NNSTREL]，但这些工作未涉及通过 MIP 或 SMT 的基于优化的规划。

有几项工作使用 SMT 或 SAT 编码进行时序逻辑约束下的多智能体规划。使用 SMT 从安全 LTL 片段进行组合综合提高了可扩展性和正确性保证 [SMTMultiRobotSafeLTL]，LTL 下的在线或增量规划也被研究 [OnlineMultiRobotLTL]。通过惰性 SMT 和 MIP 公式进一步探索了基于优化的规划 [shoukry2016scalable, SMTMultiRobotSafeLTL]，以及基于 SAT 的凸优化 [shoukry2017linear]，而基于 MIP 的航点公式实现了长视界多智能体 STL 规划 [MultiAgentSTLWaypoints]。能力时序逻辑（CaTL）将时序逻辑与任务分配、路由和异构团队的资源约束相结合 [ProbabilisticCaTLCoordination, CaTLResourceConstraints]，通常将规划表述为分配和时间表上的组合优化问题。虽然 CaTL 采用与我们类似的集中式规划视角，但其算子关注能力和任务满足性，而非交互图上的时空推理。

与 HyperLTL 的比较。超属性也被用于描述多智能体系统的规范 [hsu2025hyprl, wang2020hyperproperties, finkbeiner2023logics]。最接近我们设置的是 [wang2020hyperproperties] 的工作，其使用 HyperLTL 规划具有关系目标的多个机器人系统，以及 HypRL [hsu2025hyprl]，其在分散无模型设置中（我们是集中式基于模型的）从超属性规范学习控制策略。

除此之外，HyperLTL 是命题逻辑：它仅允许布尔原子命题，且跨多个智能体的联合谓词被简化为离散、网格状环境中单智能体谓词析取的语法糖。将我们的规范编码为 HyperLTL 还需要具体化出现在时序算子内的每个逐点智能体选择，因为 HyperLTL 仅在最外层前缀允许迹线量词。例如，分配规范 ϕassignϕassign​ 中的定位器和救援者选择被展开为固定集合 LL 和 RR 上的析取：

或一种 Skolemization 将存在量词提升到前缀，代价是一次交替，产生一个落在无交替片段之外的 ∀∃∀∃ 公式。相比之下，到达和交付公式使用固定全称前缀，但需要联合谓词如 φℓ,r,mtaskφℓ,r,mtask​ 和 φr,mnearφr,mnear​ 被表示为多迹线原子命题。STL-GO 逐点评估这些有限智能体选择并直接支持联合谓词；完整具体化延迟到附录 E。

此外，为了实证比较 HyperLTL 和 STL-GO 的编码，我们改编了 HypRL [hsu2025hyprl] 的野火救援网格世界基准，其中作者考虑 N×NN×N 网格，3≤N≤103≤N≤10。一个消防员智能体必须扑灭所有火单元，同时一个医疗智能体救援所有受害者单元；两个智能体必须保持在有界通信范围内，且医疗智能体在消防员扑灭之前不能进入任何火单元。我们将任务编码为 HyperLTL 和 STL-GO，并在 MIP 和 SMT 后端下分别求解；完整规范和编码细节见附录 E。表 II 的结果显示，随着网格增长，HyperLTL 编码因通信范围约束所需的成对单元枚举而招致 O(T⋅N4)O(T⋅N4) 的约束膨胀：在 N=10N=10 时，HyperLTL + SMT 生成 355k 约束，而 STL-GO + SMT 为 2.4k。STL-GO 的图算子通过实值谓词编码相同的协调，约束计数随 TT 线性增长。

表 II：在 N×NN×N 网格上 HyperLTL 和 STL-GO 编码的比较（T=4(N−1)+2T=4(N−1)+2）。

结论。我们提出了一个用于多智能体系统带图算子的时空逻辑规范的综合框架。STL-GO 的 MIP 和 SMT 编码支持动态交互图上的集中式规划，并具有可靠性保证。我们的仿真展示了在涉及多个动态图和角色类型智能体的复杂 STL-GO 规范下的轨迹综合。

局限与未来工作。我们的可靠性保证依赖于确定性的环境和智能体动力学。在随机设置中，综合计划只能以一定概率保证满足规范，分布式鲁棒公式的编码是一个扩展方向。由于我们综合开环控制序列，将编码嵌入滚动视界循环或学习尊重 STL-GO 规范的政策是开放方向。此外，部分可观测下的分散综合，以及缓解图数量组合增长的分解策略，留作未来工作。