FlagThis

Abstract

Shielded reinforcement learning is typically presented as a runtime safety mechanism: temporallogic specifications are compiled into automata that restrict an agents actions to guarantee safe behavior. We argue that this is the wrong product. The same automata-theoretic machineryspecification compilation, product game construction, attractor computation, and winning-region extractionis more naturally viewed 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 perspective through a constrained two-player safety game for network defense. A defender safety specification defines the set of unacceptable outcomes, while an attacker specification imposes operational constraints on the adversary. The two specifications are enforced asymmetrically: the defender specification defines the unsafe region of the game, whereas the attacker specification restricts the adversarys legal actions during attractor computation. Solving the resulting game produces a _defensibility verdict_ a formal certificate that a topology-specification pair is or is not defensibleas well as the associated winning region and shield. To move beyond a binary verdict, we derive a set of topology-level defensibility metrics from the attractor structure and combine them with post-convergence behavior from shieldconstrained adversarial multi-agent reinforcement learning. Together, these form a _defensibility fingerprint_ that characterizes both the formal safety properties of a network and its operational behavior under adaptive attack and defense. A what-if analysis across topology and specification perturbations demonstrates that formal defensibility and operational effectiveness capture distinct aspects of security. In particular, small architectural changes can produce large shifts in operational outcomes while leaving formal safety margins nearly unchanged. The results suggest that shield synthesis is 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.