Compositional Shielding and Reinforcement Learning for Multi-Agent Systems

Summary

This partial ingest is based on the extracted full PDF text. Brorholt, Larsen, and Schilling propose a compositional shielding framework for multi-agent systems. Instead of synthesizing one global shield over the full state space, they synthesize local shields in each agent’s projection and use assume-guarantee reasoning to prove that their composition enforces a global safety property. They also introduce cascading shielded learning for acyclic dependency structures and evaluate the approach on car-platoon and chemical-production case studies.

Key Claims

• Classical shield synthesis provides hard safety guarantees but scales exponentially in the number of state variables, making centralized multi-agent shields impractical.
• Independent local shields are not enough when the global safety property requires coordination; assumptions about other agents’ guaranteed behavior are needed.
• Assume-guarantee reasoning can decompose a global safety property into ordered local obligations so shields coordinate at synthesis time without online communication.
• The resulting distributed shield provides absolute safety guarantees when the local shields are compatible.
• Cascading shielded learning trains agents in dependency order for acyclic systems; the paper proves in-distribution training and Pareto optimality under local optimality/uniqueness assumptions.
• Case studies report large synthesis-time gains, reducing centralized shield computations that take hours or become infeasible to distributed shields computed in seconds or less.

Methods / Formalism

• The paper abstracts an MDP into an induced LTS by replacing positive transition probabilities with possible transitions.
• A safety property is a set of safe states phi; a shield nabla[phi] is a nondeterministic strategy whose outcomes from winning states remain in phi.
• A shielded MDP removes transitions whose actions are disallowed by the shield; every policy over the shielded MDP has safe outcomes.
• Multi-agent systems use projections prj_i:S -> O_i from the global state to each agent’s observation space.
• A local shield nabla_i operates over the projected LTS for agent i; its extension permits exactly those global actions whose local component is allowed by nabla_i.
• Distributed Shield Synthesis records the projection-based and assume-guarantee proof rules, including the ordered condition that agent i may rely only on guarantees from agents j < i.
• Cascading shielded learning builds a dependency graph over agents, trains an agent with no outgoing dependencies, instantiates that policy, removes the node, and repeats until all policies are trained.

Evidence / Experiments

• Car platoon: centralized shield synthesis for a small reduced model takes 78 minutes, while a corresponding distributed shield takes 3 seconds; a single-agent shield for the full safety property takes 6.5 seconds and is reused across a 10-car platoon.
• In the platoon learning comparison, shielded cascading learning converges quickly with no observed safety violations. MAPPO sometimes finds lower-cost but risky policies and retains safety violations because it is not safe by construction.
• Chemical production plant: distributed shielding is computed in less than 1 second, while centralized shielding is treated as infeasible; cascading learning obtains the lowest reported cost among the compared methods.
• The experiments support scalability and safety claims, but the authors manually provide the useful local guarantees.

Connections

• Extends Shielding from centralized action filtering to decentralized, communication-free multi-agent shielding.
• Builds on the safe-MARL shielding line after ElSayed-Aly2021 - Safe Multi-Agent Reinforcement Learning via Shielding, but replaces factored online join/leave coordination with assume-guarantee local obligations.
• Adds a formal-methods route into Safe Multi-Agent Reinforcement Learning that is complementary to equilibrium-constrained learning in Alatur2024 - Provably Learning Nash Policies in Constrained Markov Potential Games.
• Connects to Control Theory through safe feedback/action filtering in dynamical multi-agent domains.
• Connects to Temporal Logic and Runtime Verification through safety properties interpreted over transition-system executions.
• The assume-guarantee decomposition is a reusable artifact in Distributed Shield Synthesis.

Open Questions

• The paper assumes useful local guarantees are given manually; automatically discovering them is left as future work.
• Cascading shielded learning requires an acyclic dependency graph; cyclic dependencies remain outside the method.
• Local shields may be more conservative than a centralized shield that can coordinate online, even though the centralized version may be computationally infeasible.
• The case studies use finite-state abstractions; scaling the guarantee to learned continuous abstractions or neural perception is an open bridge.

Citation

Brorholt, A. H., Larsen, K. G., and Schilling, C. (2025). Compositional Shielding and Reinforcement Learning for Multi-Agent Systems. arXiv:2410.10460v2.