屏蔽强化学习通常表现为一种运行时安全机制，它将时间逻辑规范编译成限制代理的动作的自动机。我们认为这是错误的产品。相同的自动机理论机制——规范编译,产品游戏构建,吸引子计算,和获胜区域提取——最好理解为设计时分析工具，其输出是有关系统的结构见解，而不是对已部署代理的运行时约束。我们通过用于网络防御的受限两人安全游戏来实例化这一点。这两个规范是不对称执行的:，防御者规范定义了游戏的不安全区域,，而攻击者规范则限制对手'在吸引子计算期间的合法行动。解决游戏会产生可防御性判决——拓扑规范对是否可防御的正式证书——以及相关的获胜区域和盾牌。除了二元判决,之外，我们从吸引子结构中得出拓扑级度量，并将它们与屏蔽约束对抗性多智能体强化学习的收敛后行为相结合。这些共同形成了防御性指纹，捕获网络'的形式安全属性及其在自适应游戏下的操作行为。假设分析表明，正式的防御性和运营有效性捕获了安全性的不同方面%3微小的架构变化可以在运营结果方面产生巨大的变化，同时使正式的安全裕度几乎保持不变。因此，护盾合成最有价值的不是作为安全代理,的部署机制，而是作为回答有关是否,在哪里,以及如何防御系统的架构问题的框架。可防御性判决是输出,，而不是安全策略。
Shielded reinforcement learning is typically presented as a runtime safety mechanism that compiles temporal-logic specifications into automata restricting an agent的 actions. We argue this is the wrong product. The same automata-theoretic machinery -- specification compilation, product game construction, attractor computation, and winning-region extraction -- is better read as a design-time analytical instrument whose outputs are structural insights about a system rather than runtime constraints on a deployed agent. We instantiate this through a constrained two-player safety game for network defense. The two specifications are enforced asymmetrically: the defender specification defines the unsafe region of the game, whereas the attacker specification restricts the adversary的 legal actions during attractor computation. Solving the game yields a defensibility verdict -- a formal certificate that a topology-specification pair is or is not defensible -- with the associated winning region and shield. Beyond the binary verdict, we derive topology-level metrics from the attractor structure and combine them with post-convergence behavior from shield-constrained adversarial multi-agent reinforcement learning. Together these form a defensibility fingerprint capturing both a network的 formal safety properties and its operational behavior under adaptive play. A what-if analysis shows that formal defensibility and operational effectiveness capture distinct aspects of security: small architectural changes can produce large shifts in operational outcomes while leaving formal safety margins nearly unchanged. Shield synthesis is thus most valuable not as a deployment mechanism for safe agents, but as a framework for answering architectural questions about whether, where, and how a system can be defended. The defensibility verdict is the output, not the safe policy.
科目: 人工智能 (cs.AI); 密码学和安全 (cs.CR); 计算机科学和游戏理论 (cs.GT); 机器学习 (cs.LG); 多代理系统 (cs.MA)
Subjects: Artificial Intelligence (cs.AI); Cryptography and Security (cs.CR); Computer Science and Game Theory (cs.GT); Machine Learning (cs.LG); Multiagent Systems (cs.MA)