Generating Local Shields for Decentralised Partially Observable Markov Decision Processes

AI summary

Overview

• Research area: Multi-agent systems safety, formal methods, decentralised planning (Dec-POMDPs), runtime shielding, and probabilistic model checking.
• Technical level: Advanced. The paper is built on process algebra, automata theory, Mealy machines, belief-state construction, and PRISM model checking, though the pipeline itself is described step by step.
• Scope: The paper presents a process-algebra-to-shield compilation pipeline that turns a compact global safety specification into per-agent local shields usable in communication-free, partially observable multi-agent settings, and illustrates it on a simplified multi-agent path-finding (MAPF) case study.

What This Paper Is About

In decentralised, partially observable settings where agents cannot communicate, one agent's locally chosen action does not by itself determine the resulting joint action, so guaranteeing safety is hard. Existing shielding techniques usually assume a centralised global state, or use memoryless local filters that ignore interaction history. This paper's goal is a pipeline that compiles a succinct global shield specification into local, memory-equipped filters that each agent can run using only its own observations and that output safe action sets.

Key Contributions

1. A shield process algebra with recursion and guarded choice, designed for decentralised, partially observable, communication-free settings. The grammar includes idle, fail, recursion μX.P, a global-state shield prefix Sh.P, and guarded choice P₁ ∥_g P₂ that behaves as P₁ when the current state is in the guard set g and as P₂ otherwise.
2. A compilation pipeline that turns a shield process specification into a shield process automaton, then into a global Mealy machine acting as a safe joint-action filter, and finally projects it into local Mealy machines whose states are belief-style subsets of the global Mealy machine states consistent with an agent's observations. The local machines output per-agent safe action sets under partial observability.
3. A Rust implementation with PRISM integration, which lets the researchers compute best-case and worst-case safety probabilities without fixing the agents' policies, using PRISM (the Probabilistic Symbolic Model Checker).
4. A MAPF case study showing that different shield process specifications reduce collisions relative to an unshielded baseline, with the specifications exhibiting varying levels of expressiveness and conservatism.

Main Findings

• A demonstrated impossibility case for existing methods: In the "Blind Agents" example with observation radius R = 0 and two agents (A₁, A₂) with targets (T₁, T₂), each agent's local observation stays constant over time. The paper states it is impossible to construct a shield depending solely on local observations in this setting, and that DFA-based constructions that try to avoid unsafe states are ineffective because no available action combination is guaranteed to reach a safe joint action.
• The process syntax supplies the missing information: Because the shield process encodes a sequence of global-state shields (Sh₁.Sh₂.Sh₃.idle guarded by a set g), the pipeline still produces usable local shields for the blind-agents case. All observations being identical, each local belief state stays maximal and all process branches are treated as possible.
• Concrete local outputs in the blind-agents case: The local shield for A₁ outputs the action sets {↓}, {↓}, {⋅}, {⋅}, {⋅} across its states, while the local shield for A₂ outputs {⋅}, {→}, {→}, {⋅}, {⋅}.
• Verification results for the blind-agents instance: Using PRISM with the agents' policies treated as nondeterministic, the lower and upper bounds on the probability of shield failure are both 0.000000, and the lower and upper bounds on the probability of reaching unsafe states are also both 0.000000, indicating the shield terminates correctly with no shield failure and no unsafe states in that instance.
• Case-study setup: The authors evaluate random instances with n = 2 and n = 3 agents on 3 × 3, 4 × 4, and 5 × 5 grids, comparing shield process specifications P₁ (recursive μX.S_safe.X) and P₂ (a nested guarded-choice variant over S_safe and g_{o₁}, g_{o₂}, … with a fail fallback) against the unshielded baseline.
• Reported outcome vs. baseline: The abstract states the shield processes substantially reduce collisions compared to the unshielded baseline. Specific collision counts, percentages, or per-instance tables are not reported in the provided content, which is truncated partway through the description of P₂.
• Only vertex conflicts are modelled: The simplification restricts the safety condition to vertex conflicts, meaning no two agents may occupy the same cell after a transition.

Methodology in Plain English

1. Set up the model. The system is a Dec-POMDP: a set of agents, a global state space, per-agent action spaces, a transition function, per-agent observation spaces, an observation function, a shared reward, a discount factor, and an initial-state distribution. A shield is a function returning safe actions; the paper focuses on pre-posed shields that filter actions before agents choose.
2. Choose a running example. A simplified MAPF problem on a fixed H × W grid where each cell is an obstacle or free, and each agent picks from five actions (←, →, ↑, ↓, ⋅ for stay). Observations comprise the neighbourhood within radius R plus a coarse direction-to-target signal in {-1, 0, 1} × {-1, 0, 1}.
3. Write the safety requirement as a process. The user writes a shield process using the algebra (recursion, guarded choice, global-state shield prefixes). Guards pick which branch applies based on the current state.
4. Compile to a process automaton. The process is translated into a deterministic automaton whose states are idle, fail, continuation processes, or a dummy start state, and whose transitions consume global-state shields in sequence under the guard sets.
5. Build the global Mealy shield. Given a transition description SAS : S × S → 2^A, an observation description O′ᵢ : S → 2^{Ωᵢ}, and an initial set S₀, the pipeline constructs a global Mealy machine whose states pair a set of reachable Dec-POMDP states with a process automaton state. Outputs are per-agent safe action sets produced by a fixed deterministic decomposition of the safe joint-action set into one local action set per agent, with a distinguished ⊥ symbol marking shield failure.
6. Project to local shields. Each local Mealy machine's states are belief subsets over global Mealy states consistent with the agent's current observation. Its transition function unions the global transitions over states consistent with the observation, and its output intersects the relevant component of the global outputs — treating fail as contributing all actions unless every state in the belief is fail, in which case the output is ⊥.
7. Verify with PRISM. The shielded model is analysed with PRISM, with agent policies nondeterministic, to obtain lower and upper bounds on shield-failure probability and on the probability of reaching unsafe states — bounds that hold regardless of which policy the agents follow.

Why This Matters

• Research impact: The work connects formal specification languages (process algebra) with decentralised runtime enforcement, showing how memory and interaction history can be encoded into a shield even when agents never communicate. It also provides a way to reason about safety bounds without committing to a particular decentralised policy, which is unusual in the multi-agent safety literature.
• Warehouse and logistics robotics: Fleets of robots moving goods on shared grids face exactly the vertex-conflict problem modelled here; local shields would let each robot decide safely from onboard sensing alone.
• Autonomous vehicle intersections and merging: Vehicles with only local perception and no inter-vehicle negotiation could use local shields to filter manoeuvres that risk collisions.
• Drone delivery corridors and airspace management: Swarms or delivery drones operating under limited local sensing need decentralised filters that account for history, not just instantaneous position.
• Multi-robot inspection and assembly cells: Teams of coordinated arms or mobile manipulators need provably safe action sets under partial observability and without a central controller.
• Industry relevance: The Rust-plus-PRISM toolchain targets practitioners in robotics and autonomous systems who need verifiable safety layers, and the code is released at https://gitlab.cs.ox.ac.uk/ug23hy/shield-process-compilation-pipeline/, with PRISM at https://www.prismmodelchecker.org.

Future Directions

• Scaling the evaluation: The reported case study covers n = 2 and n = 3 agents on grids up to 5 × 5; whether the pipeline remains tractable for larger teams and larger state spaces is left open.
• Richer conflict models: The paper restricts the MAPF study to vertex conflicts. Edge conflicts, deadlocks, and livelocks — named in the keywords as deadlock-freedom and collision-freedom — are natural extensions.
• Generalising the decomposition step: Dec, the function that splits a safe joint-action set into per-agent sets, is instantiated here as a deterministic maximum-cardinality product set. Alternative decompositions and their effect on conservatism are unexplored.
• Broadening beyond MAPF: The authors state the pipeline applies generally to communication-free Dec-POMDPs whenever the safety condition can be represented using the state together with a finite counter; demonstrating that claim outside the grid-world example remains future work.
• Loosening the communication-free assumption: Because the whole construction targets settings where inter-agent communication is disallowed, any relaxation toward limited communication would require rethinking the belief-state projection.

Target Audience

Researchers and graduate students working on safe multi-agent reinforcement learning, Dec-POMDP planning, formal methods for robotics, and runtime verification; robotics and autonomous-systems engineers who need guaranteed safe action filtering on decentralised platforms; and tooling developers interested in how model checkers such as PRISM can be coupled to specification-compilation pipelines. Some familiarity with automata, process calculi, or probabilistic model checking is needed to follow the compilation steps in detail.

Authors’ abstract

Multi-agent systems under partial observation often struggle to maintain safety because each agent's locally chosen action does not, in general, determine the resulting joint action. Shielding addresses this by filtering actions based on the current state, but most existing techniques either assume access to a shared centralised global state or employ memoryless local filters that cannot consider interaction history. We introduce a shield process algebra with guarded choice and recursion for specifying safe global behaviour in communication-free Dec-POMDP settings. From a shield process, we compile a process automaton, then a global Mealy machine as a safe joint-action filter, and finally project it to local Mealy machines whose states are belief-style subsets of the global Mealy machine states consistent with each agent's observations, and which output per-agent safe action sets. We implement the pipeline in Rust and integrate PRISM, the Probabilistic Symbolic Model Checker, to compute best- and worst-case safety probabilities independently of the agents' policies. A multi-agent path-finding case study demonstrates how different shield processes substantially reduce collisions compared to the unshielded baseline while exhibiting varying levels of expressiveness and conservatism.