Distributed Shield Synthesis

Context

Brorholt2025 - Compositional Shielding and Reinforcement Learning for Multi-Agent Systems scales Shielding to multi-agent systems by synthesizing local shields in agent observation projections and composing them with an assume-guarantee proof rule. It is a later compositional route than ElSayed-Aly2021 - Safe Multi-Agent Reinforcement Learning via Shielding, whose factored shields rely on state-space factors and online join/leave coordination.

Formal Statement

A safety property is a set of safe states phi subseteq S. A shield nabla[phi] is a nondeterministic strategy whose outcomes from winning states remain in phi.

Given an MDP M=(S,Act,P), the induced LTS keeps exactly the transitions with positive probability. A shielded MDP removes actions disallowed by the shield, so every policy over the shielded MDP has safe outcomes.

For an n-agent system, agent i has a projection

$$pr{j}_i:S\to O_i$$

and a local shield nabla_i over the projected LTS. Its extension permits global actions whose i-th component is locally allowed:

$$\uparrow ({\nabla }_i)(s)=\{a\in Act\mid a[i]\in {\nabla }_i(pr{j}_i(s))\}.$$

If the composition

$$\nabla =\bigcap _i\uparrow ({\nabla }_i)$$

exists and the local shields satisfy the projection-based proof condition, then nabla is a global shield.

The assume-guarantee rule strengthens this with an ordered dependency condition: agent i may rely only on guarantees from agents j<i. If each local shield guarantees phi_i under the previous guarantees, then the composed distributed shield guarantees phi = cap_i phi_i.

Derivation / Construction

• Project the global transition system into each agent’s observation space.
• Choose local safety obligations phi_i whose conjunction implies the desired global property.
• Synthesize a shield in each projected LTS, optionally after restricting the local model by guarantees already established for lower-index agents.
• Extend each local shield back to the global action space.
• Intersect the extended shields. Compatibility is required so at least one joint action remains enabled in every relevant state.
• Apply the assume-guarantee theorem to conclude that all outcomes of the shielded global system remain in the global safety property.

Implications

• Distributed shields coordinate at synthesis time through guarantees, not through online communication.
• The method can turn an infeasible centralized shield-synthesis problem into several lower-dimensional local ones.
• The result may be more conservative than a centralized shield with full communication, but it provides a hard safety guarantee for decentralized agents.
• Compared with Centralized and Factored MARL Shielding, this annex emphasizes assume-guarantee obligations and communication-free local shield composition rather than boundary-crossing coordination between factored shields.
• The guarantee search is still a design problem: the paper supplies local obligations manually.

Links

• Sources: ElSayed-Aly2021 - Safe Multi-Agent Reinforcement Learning via Shielding, Brorholt2025 - Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
• Concepts: Shielding, Safe Reinforcement Learning