大家读完觉得有帮助记得关注和点赞摘要多智能体规划问题出现在各种工程应用中如多机器人灭火和工厂中的无人机检测。一个特别的挑战是时空约束即智能体应在何时和/或何处执行何种任务和拓扑约束即智能体应如何交互的存在这些通常通过图的概念来形式化。近年来已提出了各种可以通过时空逻辑捕获此类约束的框架。我们在此关注带有图算子的时空逻辑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 编码地图几何静态或动态、障碍物和对抗特征如通信中断等属性。环境根据 wt1f(wt)wt1​f(wt​) 确定性演化其中 ff 和初始世界状态 w0w0​ 已知。因此当构建规划实例时有限轨迹 {wt}t0T{wt​}t0T​ 是固定的¹。每个智能体受一个在所有智能体间共享的转移动力学函数 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​] 分别为线速度和角速度。对于采样时间 Δt0Δt0 和单轮模型²位置和方向更新为 xt1ixtiΔt vticos⁡(θti)xt1i​xti​Δtvti​cos(θti​)yt1iytiΔt vtisin⁡(θti)yt1i​yti​Δtvti​sin(θti​)θt1iwrap[0,2π)(θtiΔt ωti)θt1i​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​) 是一个完全有向图其中 EtdV×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-GOSTL-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​∈Ne2∈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,εC0εE​,εC​0 分别为到达紧急地点和救援中心的距离容差。对于 ℓ∈Lℓ∈Lr∈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}t0T{wt​}t0T​ 是固定且已知的。令 ϕϕ 是在有界视界 T∈NT∈N 上、在诱导图集合序列 {Gt}t0T{Gt​}t0T​ 下解释于 MAS MAMA​ 的 STL-GO 公式。那么我们的目标是合成开环控制序列 {Ut}t0T−1{Ut​}t0T−1​使得根据方程2动力学得到的执行 {Xt}t0T{Xt​}t0T​ 在初始状态满足规范即 (MA,0)⊨ϕ(MA​,0)⊨ϕ。我们可以选择最小化性能目标 J({Xt}t0T,{Ut}t0T−1)J({Xt​}t0T​,{Ut​}t0T−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。令 typedtyped 表示基于距离的交互模态。Γ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}t0T{xti​}t0T​ 和 {uti}t0T−1{uti​}t0T−1​ 的决策变量(ii) 编码 ϕϕ 各子公式对每个智能体和时刻真值的辅助二元变量(iii) 在有界视界上强制执行动力学、图构造谓词以及布尔、时序和图算子的 STL-GO 语义的约束。虽然我们关注同质智能体动力学但编码可扩展到角色类型异构性如运行示例中定位器/救援者分割所用。假设。我们关注确定性环境动态下的集中式开环规划。部分可观测和局部观测下的分散规划是最终目标但我们考虑集中式、完全可观测设置作为基础步骤该设置下的可处理编码将作为分散扩展的先决条件我们将其留作未来工作。此外我们假设智能体自主执行综合的开环计划确定性环境动态让我们可以在没有概率语义的情况下推理可行性和正确性。在以下各节中我们提出一个系统性建模和综合框架将上述具有多个交互图的规划问题编译为混合整数规划或可满足性问题用于集中式规划。由于篇幅限制我们将介绍与图相关的新型编码并请读者参考附录 C 和 D 中描述的完整编码。IV 基于 MIP 的 STL-GO 规划编码IV-A 编码系统规范系统动力学。我们限制自己为确定性、同质动力学在智能体状态、智能体输入和世界状态上是仿射的以便有界综合问题允许 MIP 编码。具体地令动力学为其中 i∈Vi∈Vt0,…,T−1t0,…,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×Vi≠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,ttype1ai,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 编码对固定图类型分三步进行加上第四步在模态量词下组合按类型编码。符合条件的入边。对每个 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​。我们施加其中 δw0δw​0 是固定数值分离裕度。我们假设可行边权重与每个区间边界外部是 δwδw​-分离的低于 wmin⁡wmin​ 的权重至多为 wmin⁡−δwwmin​−δw​高于 wmax⁡wmax​ 的权重至少为 wmax⁡δwwmax​δw​。在此约定下(5) 强制计数满足 φφ 的邻居。令 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​并定义基数基数强制。首先假设 e2∞e2​∞。由于 ci,tIn,φ,typeci,tIn,φ,type​ 是整数值引入二元变量 αi,tlow,typeαi,tlow,type​ 和 αi,thigh,typeαi,thigh,type​分别指示 ci,tIn,φ,typee1ci,tIn,φ,type​e1​ 和 ci,tIn,φ,typee2ci,tIn,φ,type​e2​按类型满足变量编码为对于下界区间 [e1,∞)N[e1​,∞)N​仅需下界违规变量量化算子。存在性算子 ψInG,EW,∃φψInG,EW,∃​φ 要求至少一个图类型满足计数性质。对每个 type∈Ttype∈T上述按类型编码产生满足变量 zψ,i,ttypezψ,i,ttype​然后强制类型的析取这些约束确保 zψ,i,t1zψ,i,t​1 当且仅当某个图满足该性质。全称算子 ψInG,EW,∀φψInG,EW,∀​φ 要求 TT 中所有图类型满足计数性质。这使用合取而非图类型上的析取来编码出向算子通过在所有过程中将 (j,i)(j,i) 替换为 (i,j)(i,j) 从入向情况获得。引理6。对于由离散时间仿射差分方程描述的多智能体系统智能体局部 STL-GO 规范的规划问题可编码为 MIP使得任何满足性赋值都产生满足规范的轨迹。证明。为节省篇幅我们提供证明梗概完整证明见附录 A。我们通过结构归纳建立不变量对每个智能体局部子公式 ψψ、智能体 ii 和时间 tt 成立。动力学约束 (3) 是等式因此可行赋值对应于 FF 的有效轨迹。原子谓词、布尔连接词和 until 算子通过标准 Big-M 和展开构造编码 [stl-to-milp1, stl-to-milp2]。对于 ψInG,[e1,e2]W,#φψInG,[e1​,e2​]W,#​φ对每个 type∈Ttype∈TΓtypeΓtype 的 MIP-可编码性提供精确边指示器和 PWA 权重表达式。约束 (5) 强制 γj,i,ttype1γ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}t0T{Xt​}t0T​ 满足 ϕϕ即 (MA,0)⊨ϕ(MA​,0)⊨ϕ。证明梗概。引理6建立 (12) 对智能体局部子公式成立。我们通过结构归纳将其扩展到多智能体子公式 ψψ 为 zψ,t1 ⟺ (MA,t)⊨ψzψ,t​1⟺(MA​,t)⊨ψ联合原子谓词、嵌入 i.φi.φ、布尔连接词和 until 在多智能体变量上重用智能体局部论证EXEX 和 FAFA 编码为 {zφ,i,t}i∈V{zφ,i,t​}i∈V​ 上的析取和合取第四-C节通过智能体局部不变量匹配语义。以 zϕ,01zϕ,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​ 是 LRALIA 上的布尔公式且 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 分三步进行加上第四步在模态量词 ## 下组合按类型编码。符合条件的入边。对每个图类型 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(−∞,∞)权重比较被省略。计数满足 φφ 的邻居。令 zφ,tjzφ,tj​ 是布尔变量表示子公式 φφ 在时间 tt 被智能体 jj 满足。编码为基数。对每个图类型 type∈Ttype∈T定义整数变量 ci,ttypeci,ttype​ 计数符合条件的、满足 φφ 的入向邻居按类型满足变量受约束图类型上的量化。对于 #∃#∃ψψ 在智能体 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-可编码性确保边存在谓词和边权重是 LRALIA 表达式(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}t0T{Xt​}t0T​ 使得 (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。条件 (Condition)$\mathcal{L}$$\mathcal{R}$MIP (无目标)​MIP (线性目标)​MIP (二次目标)​SMT​时间 (s)​|Vars|​|Constr|​时间 (s)​|Vars|​|Constr|​时间 (s)​|Vars|​|Constr|​时间 (s)​|Vars|​|Constr|​STL only(仅 STL)526960k125k1862†60k126k2591†60k126k0.6621.3k23.2k73177105k146k3759†106k148k5216†106k148k1.4923.8k26.6k93277146k210k3877†147k212k5300†147k212k1.7435.2k38.5kGs​(感知)​5215174k143k1919†74k144k2659†74k144k2.1323.2k25.2k73240135k185k3846†136k187k5311†136k187k3.1527.9k30.7k93401182k257k4016†183k259k5434†183k259k2.6140.1k43.4kGs​Gc​(感知 通信)​5217581k153k2032†81k154k2635†81k154k1.2925.2k27.1k73362155k209k3940†155k211k5393†155k211k1.8032.1k34.8k93459204k284k4154†206k287k5786†206k287k4.0645.1k48.4kGs​,Gc​,Gtask​(感知 通信 任务)​5234086k161k1201†87k162k2234†86k161k3.5622.0k24.0k73775172k230k3750†173k232k5809†173k232k5.6846.9k49.8k931480225k307k4973†226k309k5997†226k309k16.5058.2k61.6k我们为上述搜索与救援示例实现了一个规划器。令 MM 表示可能发生紧急情况的固定已知集合区域集合。在规划时每个集合区域的位置已知但每个集合区域是否包含活跃紧急情况未知。定位器智能体巡逻集合区域并在进入感知范围时观察其激活状态。活跃紧急情况随后必须被通信、分配给一个或多个救援者并在有界时间内通过将被救个体运送到救援中心 CC 来解决。为考虑潜在紧急情况我们为所有可能的紧急激活场景构建计划。实验实例使用角色特定可容许控制集同时为所有智能体保留相同的运动模型结构⁹。令 Ω⊆{0,1}∣M∣Ω⊆{0,1}∣M∣ 表示场景集合其中 ωm1ωm​1 指示在场景 ωω 中集合区域 mm 包含活跃紧急情况ωm0ωm​0 指示不包含。如果考虑所有激活组合则 ∣Ω∣2∣M∣∣Ω∣2∣M∣。对每个场景 ω∈Ωω∈Ω编码包含相应的状态和控制序列。这些场景索引序列被联合求解。具有相同定位器观测历史的场景必须具有相同的控制输入即如果场景 ωω 和 ω′ω′ 在时间 tt 对智能体不可区分则 UtωUtω′Utω​Utω′​。计划仅在定位器观测区分场景后才可分支。所得解是表示为有限场景树的应急计划。在运行时智能体初始执行共同计划前缀。当定位器观测到集合区域是否活跃时选择与该观测一致的分支执行沿该分支继续。进一步的观测可能选择后续分支。以下谓词和规范对每个 ω∈Ωω∈Ω 实例化。当上下文清晰时我们省略场景上标。在场景 ωω 中φmemgφmemg​ 为真当且仅当 ωm1ω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。任务规范如下有界紧急检测。每个紧急情况必须在有界时间内被定位器群检测到检测到中继。一旦检测到紧急情况信息必须在有界时间内通信给另一个定位器或救援者检测到分配。一旦检测到紧急情况至少一个定位器必须在有界时间内分配救援者救援者响应时间。如果定位器分配救援者该救援者必须在有界时间内到达紧急情况救援与交付。到达紧急情况后救援者必须将被救个体运送到救援中心对每个场景 ω∈Ωω∈Ω令 ϕωϕω​ 表示在激活分配 ωω 下上述五个任务规范的合取。基于场景的规划问题要求 ⋀ω∈Ωϕω⋀ω∈Ω​ϕω​。所有实验使用 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) 的约束膨胀在 N10N10 时HyperLTL SMT 生成 355k 约束而 STL-GO SMT 为 2.4k。STL-GO 的图算子通过实值谓词编码相同的协调约束计数随 TT 线性增长。表 II在 N×NN×N 网格上 HyperLTL 和 STL-GO 编码的比较T4(N−1)2T4(N−1)2。NN方法Var.Constr.Time (s)5×5HyperLTL SMT388.6k0.10STL-GO SMT3958880.15HyperLTL MIP1.0k8.8k0.20STL-GO MIP1.2k12.7k0.107×7HyperLTL SMT5454.2k0.61STL-GO SMT6711.4k0.34HyperLTL MIP2.8k54.7k2.39STL-GO MIP3.0k65.3k0.3510×10HyperLTL SMT78355.1k4.26STL-GO SMT1.2k2.4k0.99HyperLTL MIP8.2k356.2k4.47STL-GO MIP8.5k387.5k1.96结论。我们提出了一个用于多智能体系统带图算子的时空逻辑规范的综合框架。STL-GO 的 MIP 和 SMT 编码支持动态交互图上的集中式规划并具有可靠性保证。我们的仿真展示了在涉及多个动态图和角色类型智能体的复杂 STL-GO 规范下的轨迹综合。局限与未来工作。我们的可靠性保证依赖于确定性的环境和智能体动力学。在随机设置中综合计划只能以一定概率保证满足规范分布式鲁棒公式的编码是一个扩展方向。由于我们综合开环控制序列将编码嵌入滚动视界循环或学习尊重 STL-GO 规范的政策是开放方向。此外部分可观测下的分散综合以及缓解图数量组合增长的分解策略留作未来工作。