Multi-Agent Reinforcement Learning (MARL) discovers policies that maximize reward but do not have safety guarantees during the learning and deployment phases. Although shielding with Linear Temporal Logic (LTL) is a promising formal method to ensure safety in single-agent Reinforcement Learning (RL), it results in conservative behaviors when scaling to multi-agent scenarios. Additionally, it poses computational challenges for synthesizing shields in complex multi-agent environments. This work introduces Model-based Dynamic Shielding (MBDS) to support MARL algorithm design. Our algorithm synthesizes distributive shields, which are reactive systems running in parallel with each MARL agent, to monitor and rectify unsafe behaviors. The shields can dynamically split, merge, and recompute based on agents' states. This design enables efficient synthesis of shields to monitor agents in complex environments without coordination overheads. We also propose an algorithm to synthesize shields without prior knowledge of the dynamics model. The proposed algorithm obtains an approximate world model by interacting with the environment during the early stage of exploration, making our MBDS enjoy formal safety guarantees with high probability. We demonstrate in simulations that our framework can surpass existing baselines in terms of safety guarantees and learning performance.

翻译：多智能体强化学习（MARL）能够发现最大化奖励的策略，但在学习和部署阶段缺乏安全保障。尽管基于线性时态逻辑（LTL）的屏蔽技术是单智能体强化学习（RL）中确保安全性的有前途的形式化方法，但在扩展到多智能体场景时会导致保守行为。此外，在复杂多智能体环境中合成屏蔽器面临计算挑战。本文提出基于模型的动态屏蔽（MBDS）以支持MARL算法设计。我们的算法合成分布式屏蔽器——即与每个MARL智能体并行运行的响应式系统——用于监控和修正不安全行为。这些屏蔽器能够根据智能体状态动态分裂、合并和重新计算。该设计使得在复杂环境中无需协调开销即可高效合成屏蔽器以监控智能体。我们还提出一种无需事先了解动力学模型的屏蔽器合成算法。该算法通过在探索初期与环境交互来获取近似世界模型，使我们的MBDS能以高概率获得形式化安全保证。仿真结果表明，我们的框架在安全保证和学习性能方面均能超越现有基线方法。