⚡ electrical engineering

Security-Aware Planning and Control of Multi-Agent Systems with LTL Tasks

本文提出了一种面向多智能体系统的“构建即安全”框架，该框架将针对被动入侵者的安全约束直接集成到线性时序逻辑（LTL）综合中，以形式化地确保任务满足性，并保护有关任务执行和智能体身份敏感信息的安全。

原作者： Georgios Mitsos, Dimos V. Dimarogonas, Siyuan Liu

发布于 2026-05-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Georgios Mitsos, Dimos V. Dimarogonas, Siyuan Liu

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一支无人机编队在城市上空飞行，执行一项复杂任务：一架需要扫描空中，另一架需要发送数据，第三架需要前往一个安全的维修站。它们必须按特定顺序无限循环地执行这些任务，同时避开恶劣天气区域。

现在，想象有一位“间谍”在监视它们。这位间谍无法看到无人机内部的计算机或其精确的 GPS 坐标。间谍只能看到无人机位于哪个大致区域（例如“北区”或“南区”）。间谍试图弄清楚两件事：

是否有无人机访问了秘密、敏感的位置？（例如高安全级别的维修站）。
具体是哪一架无人机做的？

本文提出了一种“设计即安全”的框架。作者不是先规划飞行路径再试图事后掩盖痕迹，而是将安全规则直接构建在规划过程中。他们确保无论间谍看到什么，都永远无法 100% 确定是否发生了秘密任务，或者无法确定是谁执行的。

以下是他们如何实现这一点的简单类比：

1. 两种类型的“掩护故事”

作者提出了两种保护无人机的方法，分别称为A 型和B 型安全。

A 型安全（“幽灵”策略）：
想象间谍看到一架无人机进入了秘密的红色区域。为了满足 A 型安全，系统必须能够声称：“实际上，那架无人机在同一时间完全可能处于一个普通的蓝色区域，而间谍看到的情况会完全一样。”
- 类比： 这就像魔术师让兔子消失。观众（间谍）看到魔术师的手在移动，但他们无法判断兔子是真的消失了，还是只是藏在了另一个从外面看起来完全相同的口袋里。系统创建了一条“复制路径”（一个虚假的历史轨迹），对间谍来说看起来完全一样，但其中不包含任何秘密访问。
B 型安全（“混淆”策略）：
想象间谍看到一架无人机在秘密区域。为了满足 B 型安全，系统确保另一架无人机也处于一个对间谍来说看起来完全相同的区域。
- 类比： 这就像一群人戴着相同的面具。如果间谍看到“人物 A"在做可疑的事情，他们无法确定是人物 A 还是人物 B，因为两人在同一时间都处在同一个“戴面具”的区域。间谍看到了行动，但无法识别肇事者。

2. “数字孪生”游戏

为了实现这一点，计算机不仅仅规划一条飞行路径。它同时规划两条路径：

真实路径： 无人机实际执行的操作。
复制路径： 一个虚假的任务版本，对间谍来说看起来与真实路径完全相同，但避开了秘密（或者交换了执行者）。

系统检查每一个可能的动作。如果某个动作让间谍能够说：“啊哈！我确切知道无人机 1 在秘密区域，因为没有其他无人机可能在那里”，那么该动作就会被删除。系统只保留那些让间谍始终处于困惑状态的动作。

3. 从数学到实际飞行

本文描述了一个三步过程，将这些复杂的数学规则转化为实际飞行的无人机：

步骤 1：地图（抽象化）： 现实世界是一个连续空间（无限个点）。计算机将其分解为“房间”（多面体）的网格。它将复杂的飞行物理转化为一个简单的棋盘游戏，你只需从房间 A 移动到房间 B。
步骤 2：安全过滤器： 计算机构建一个“安全棋盘游戏”。它删除任何违反 A 型或 B 型规则的动作。它还检查无人机是否能在不坠毁或耗尽电池的情况下在房间之间物理跳跃（使用称为“控制障碍函数”的工具，它们就像看不见的墙壁，将无人机限制在当前房间内，直到它们准备好切换）。
步骤 3：任务规划器： 计算机使用逻辑工具（线性时序逻辑，简称 LTL）在安全棋盘游戏中找到最佳路径，以完成任务（扫描、编码、传输），同时保持安全和保密。

4. 结果：双无人机测试

作者用两架无人机测试了这种方法：

无人机 1 扫描空气质量并编码数据。
无人机 2 传输数据并访问安全诊断站。

秘密： “安全诊断站”和“敏感数据区”是保密的。
间谍： 只能看到无人机是在天空的“北半部”还是“南半部”。

结果：
当无人机 1 飞入秘密区域进行数据编码时，系统同时生成一条“复制路径”，其中无人机 1 处于一个对间谍来说看起来相同的非秘密区域。与此同时，无人机 2 也处于一个符合间谍视角的区域。

结果： 间谍看到无人机在移动，但他们永远无法证明无人机 1 访问了秘密地点，也无法确定具体是哪一架无人机执行的。无人机成功完成任务，避开障碍物，并保守了它们的秘密。

总结

本文是关于如何教导机器人在执行任务的同时与间谍玩“捉迷藏”。通过从一开始就同时规划“虚假”故事和“真实”故事，系统保证了间谍始终处于困惑之中，从而确保敏感任务以及执行这些任务的代理身份保持隐蔽。

技术摘要：具有 LTL 任务的多智能体系统的安全感知规划与控制

问题陈述

本文解决了在连续工作空间内、在线性时序逻辑（LTL）规范下规划与控制多智能体系统（MAS），同时确保信息免受被动入侵者侵害的挑战。

现有的基于 LTL 的规划方法通常将连续动力学抽象为有限状态模型以综合离散计划，随后将其细化为连续轨迹。然而，这些方法通常忽视信息安全。在无人机群或智能交通系统等关键应用中，必须在任务正确性与机密性之间取得平衡。具体问题是：为具有线性仿射动力学的智能体综合控制器，使得生成的连续轨迹满足全局 LTL 任务，同时防止恶意观测者（仅能部分观测智能体位置）推断出：

是否执行了“秘密”任务（访问指定的秘密区域）。
具体是哪个智能体负责执行该秘密任务。

作者指出，虽然基于不透明性（opacity）的安全机制已在单智能体系统和部分离散多智能体系统中得到探索，但在同时处理具有连续动力学、输入约束和复杂 LTL 规范的系统方面仍存在空白。

方法论

所提出的框架遵循“构建即安全”（secure-by-construction）的方法，将安全约束直接集成到综合过程中。方法论分为四个主要阶段：

1. 抽象与安全建模

系统模型：工作空间被划分为互不重叠的多胞形。智能体动力学被抽象为加权转换系统（WTS）。通过个体智能体 WTS 的同步积形成全局 WTS（gWTS）。
安全定义：基于入侵者的观测能力（ $H_i$ $H_{i}$ ）引入了两种互补的安全概念：
- A 类安全：防止入侵者推断是否有任意智能体访问了秘密状态。这是通过确保对于每条发生秘密访问的“真实”路径，都存在一条不可区分的“副本”路径，其中智能体访问了具有相同观测的非秘密状态来实现的。
- B 类安全：防止入侵者识别哪个智能体访问了秘密状态。这要求如果智能体 $i$ 访问了秘密状态，则在该时间步至少存在另一个智能体 $k$ 产生相同的观测。
安全抽象：为了强制执行这些属性，作者构建了：
- 双子 gWTS（Twin-gWTS）：一个捕获成对不可区分全局状态的积系统。
- 安全双子 gWTS（Secure Twin-gWTS）：对双子 gWTS 的细化，移除了真实智能体和副本智能体同时处于秘密状态的状态对。
- B 类 gWTS：对全局状态空间的限制，确保秘密访问被其他智能体的观测所“掩盖”。

2. 转换可行性验证

在应用 LTL 综合之前，该框架验证安全抽象中的离散转换在连续工作空间中是否具有动力学可行性。

控制障碍函数（CBFs）：作者使用 CBF 来保证智能体保持在分配的多胞形内（前向不变性）并在特定时间跨越边界。
二次规划（QP）：对于每个离散转换，求解一个集中式 QP，以找到驱动智能体在多胞形质心之间移动的控制输入，同时满足动力学、输入界限和 CBF 约束。如果无解，则该转换将从抽象模型中剔除。

3. LTL 综合

积 Büchi 自动机（PBA）：将安全 gWTS 与由 LTL 规范导出的非确定性 Büchi 自动机（NBA）进行同步。
路径搜索：算法在 PBA 中搜索前缀 - 后缀路径，以最小化成本函数（平衡前缀和后缀成本）。该路径代表了一个同时满足 LTL 任务和安全约束的离散计划。

4. 连续轨迹生成

通过连接 QP 阶段计算出的可行轨迹段，将最优离散路径细化为连续轨迹。提供了形式化保证，证明生成的连续轨迹满足 LTL 公式和安全属性。

主要贡献

本文声称具有以下贡献：

新的安全概念：引入了适用于多智能体系统的 A 类和 B 类安全，放宽了现有的不透明性定义以提高可扩展性，同时保持强大的安全保证（合理的可否认性和智能体匿名性）。
连续动力学框架：一个直接适用于具有连续仿射动力学和输入约束的多智能体系统的规划框架。作者指出，据其所知，这是首个处理一般 LTL 任务及此类安全约束的框架，而先前的工作主要集中在有限状态模型上。
复杂度降低：所提出的离散规划算法实现了比现有安全感知多智能体方法显著更低的计算复杂度（具体引用将搜索空间从 $(2|Q|)^{2M^2+M}$ 个状态减少到 $|Q|^{2M}$ 个状态）。

结果与案例研究

该框架通过涉及两架无人机的案例研究进行了验证：

场景：无人机 1 扫描空气质量并编码数据；无人机 2 中继数据并访问诊断站。两者都必须避开障碍物区域。
任务：一个 LTL 公式，要求重复执行扫描、编码和传输序列，并最终进行检查，同时避开障碍物。
安全：两个区域被指定为秘密（敏感数据收集和诊断站）。系统必须针对观测无人机大致位置（北/南区域）的入侵者满足 A 类/B 类安全。
结果：算法成功综合出一条轨迹，其中：
- 当无人机 1 访问秘密区域时，一条“副本”路径显示其处于具有相同观测的非秘密区域（满足 A 类安全）。
- 无人机 2 被定位在使得其在秘密访问期间产生与无人机 1 相同观测的位置，从而防止入侵者识别负责的智能体（满足 B 类安全）。
性能：完整算法（包括抽象、QP 求解和路径搜索）在 MacBook Air M2 上运行时间约为 70 秒。

意义与主张

本文将其工作定位为迈向自主网络物理系统构建即安全策略的重要一步。作者声称，通过将安全约束直接集成到 LTL 综合过程中，他们提供了形式化保证，确保生成的行为既满足全局任务规范，又满足机密性要求。

其意义在于以安全感知的方式弥合了高层逻辑规划与底层连续控制之间的差距。作者强调，他们的方法是首个在此安全感知 LTL 综合上下文中直接处理连续动力学和输入约束的方法，提供了一种可扩展的解决方案，在计算复杂度方面优于现有的仅离散方法。

本文结论较为谦逊，指出未来的工作可以将该框架扩展到非线性动力学，并研究分层架构，以进一步提高大规模多智能体系统的可扩展性。