Paper deep dive
Generating Local Shields for Decentralised Partially Observable Markov Decision Processes
Haoran Yang, Nobuko Yoshida
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%
Last extracted: 4/10/2026, 1:59:51 AM
Summary
The paper introduces a shield process algebra for Decentralised Partially Observable Markov Decision Processes (Dec-POMDPs) to ensure safety in multi-agent systems without requiring communication. The authors present a compilation pipeline that transforms shield process specifications into global Mealy machine filters, which are then projected into local Mealy machines for individual agents. The approach is implemented in Rust with PRISM integration and validated through a multi-agent path-finding (MAPF) case study, demonstrating effective collision avoidance and safety guarantees.
Entities (5)
Relation Signals (3)
Shield Process Algebra → compilesto → Mealy Machine
confidence 95% · From a shield process, we compile a process automaton, then a global Mealy machine as a safe joint-action filter.
PRISM → analyzes → Dec-POMDP
confidence 90% · integrate PRISM... to compute best- and worst-case safety probabilities independently of the agents' policies.
Local Mealy Machines → enforcessafetyin → MAPF
confidence 90% · A multi-agent path-finding case study demonstrates how different shield processes substantially reduce collisions.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2604.06873v1
- Canonical: https://arxiv.org/abs/2604.06873v1
Trouble viewing inline? Open PDF directly →
Full Text
29,177 characters extracted from source content.
Expand or collapse full text
Lorenzo Gheri & Kirstin Peters (Eds.): 17th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software 2026 (PLACES 2026) EPTCS 444, 2026, p. 1–10, doi:10.4204/EPTCS.444.1 © Haoran Yang, Nobuko Yoshida This work is licensed under the Creative Commons Attribution License. Generating Local Shields for Decentralised Partially Observable Markov Decision Processes Haoran Yang University of Oxford haoran.yang@balliol.ox.ac.uk Nobuko Yoshida University of Oxford nobuko.yoshida@cs.ox.ac.uk 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 Decentralised Partially Observable Markov Decision Pro- cess (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 1 and integrate PRISM, the Probabilistic Symbolic Model Checker 2 , 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 re- duce collisions compared to the unshielded baseline while exhibiting varying levels of expressiveness and conservatism. Keywords:Multi-agent systems, Dec-POMDP, Shield process algebra, Mealy machine, Deadlock- freedom, Collision-freedom, PRISM 1 Introduction Multi-agent systems are prone to encountering collisions, deadlocks, or livelocks because an individ- ual agent’s local action does not, in general, uniquely determine the resulting joint action. Consequently, ensuring that each agent selects a concrete action that is guaranteed to be safe is non-trivial. This chal- lenge is exacerbated in communication-free, Decentralised Partially Observable Markov Decision Pro- cess (Dec-POMDP) settings [10], where each agent must choose its action solely on the basis of its own local observations. One widely used approach to enforcing safety is shielding, in which a shield restricts the agents’ choices by providing, at each state, a set of safe actions. Existing approaches include temporal-logic based synthesis [1], probabilistic shields [4], learned shields [8], and decentralisation techniques [3, 6, 7] that derive local shields from a centralised safe-action set. While these methods have proved effective in many settings, they typically rely on assumptions such as access to a centralised global state, the availability of memoryless local filtering, or the sufficiency of constraints expressed purely at the action level. These assumptions limit their applicability in regimes where agents possess only local information and inter-agent communication is disallowed. 1 https://gitlab.cs.ox.ac.uk/ug23hy/shield-process-compilation-pipeline/ 2 https://w.prismmodelchecker.org 2Generating Local Shields for Decentralised Partially Observable Markov Decision Processes Although shields can sometimes be generated automatically, for example, via DFA synthesis from LTL specifications [1], such constructions tend to be rigid and conservative. Moreover, they may fail to capture the informational complexity induced by partial observations, wherein each agent’s local view reveals only a fragment of the underlying global state. To solve these problems, we propose a succinct process algebra with guarded choice and recursion. This algebra admits an automata-theoretic interpretation and can be compiled into Mealy-machine-style shields [5]. The compilation pipeline comprises three main steps. First, we translate the process algebra into a process automaton. Second, we construct a global shield Mealy machine that takes the Dec- POMDP state as input and outputs a decentralised representation of safe joint actions consistent with the process automaton. Third, we derive local shield Mealy machines by replacing the Dec-POMDP state in- put with each agent’s partial observation: the local shield Mealy machines’ states are belief-style subsets of global Mealy machine states consistent with the agent’s observation, thereby enumerating the possible individual safe action sets that remain feasible under decentralised local information. We implement this pipeline in Rust and analyse the resulting models using an integrated PRISM-based workflow. In this paper, we present the complete pipeline, from motivation to implementation details, and illustrate it through a simplified multi-agent path-finding (MAPF) [11] case study. MAPF is used here as a case study because it is easy to visualise and has simple collision rules; however, the pipeline applies more generally to communication-free Dec-POMDPs whenever the relevant safety condition can be represented using the state together with a finite counter. Contributions(1) A shield process algebra with recursion and guarded choice for decentralised, par- tially observable, communication-free settings. (2) A compilation pipeline that, given a shield process specification, generates the corresponding shield process automaton and, using transition and observa- tion descriptions, synthesises a global Mealy shield and projects it to local Mealy shields executable from local observations, which in turn export safe action sets for each agent under partial observability. (3) A Rust implementation of this pipeline with PRISM integration, enabling the computation of best- and worst-case safety probabilities without fixing a policy. 2 Pipeline Explanation This section is structured as follows. First, we introduce the preliminaries that underpin our pipeline. Second, we specify the configuration of a simplified multi-agent path-finding (MAPF) problem, which serves as a running example to illustrate the pipeline. Third, we present the process algebra used to describe a shield in terms of global states, thereby providing a global perspective on system behaviour. Fourth, we describe the pipeline itself using a special case of the MAPF problem with “blind” agents. In this final part, we construct a process automaton directly from the process algebra, derive a global shield Mealy machine from the process automaton together with the descriptions of initial states and the joint actions that induce state transitions, and subsequently synthesise a local shield Mealy machine for each agent by applying partial observation and belief-state construction to relate local observations to global states. 2.1 Preliminaries Adecentralised partially observable Markov decision process(Dec-POMDP) is a tuple [10]M= (I,S,(A i ) i∈I ,δ,(Ω i ) i∈I ,O,r,γ,ρ 0 ), whereI=1,...,nis the set of agents,Sis the global state Haoran Yang, Nobuko Yoshida3 space, andA i is the action space of agenti(with joint action spaceA:= ∏ i∈I A i ). The transition dynamics are given byδ(s ′ |s,a), the probability of transitioning from statesto states ′ under joint actiona. For each agenti,Ω i is the observation space (with joint observation spaceΩ:= ∏ i∈I Ω i ), andO(o 1 ,...,o n | s ′ ,a)denotes the probability of joint observation(o 1 ,...,o n )after executingaand reachings ′ . The shared reward function isr(s,a),γ∈(0,1]is the discount factor, andρ 0 is the initial-state distribution. Aglobal historyup to timetish t = (s 0 ,a 0 ,...,a t−1 ,s t ), and alocal historyfor agentiup to time tish t i = (o 0 i ,a 0 i ,...,a t−1 i ,o t i ). Adecentralised stochastic policyis a tupleπ:= (π 1 ,...,π n ), where each π i (a i |I t i )is a distribution overA i given the local informationI t i , typically the local historyh t i or, in the memoryless case, the current observationo t i [7]. Bounded histories can be encoded into states or obser- vations by forming the product of states or observations with actions. Consequently, in the remainder of the paper, we focus on states and observations without loss of generality. Ashieldfor an agent is a functionD:S→2 A that returns the set of safe actions at each state [1, 8, 7]. Shields can be represented, for example, as deterministic finite automata (DFAs) or as Mealy machines [3]. In this work, we considerpre-posed shieldsthat filter the available actions before the agents select them. AMealy machineis a tuple(Q,q 0 ,Σ I ,Σ O ,δ,λ), whereQis a finite set of states,q 0 ∈Qis the initial state,Σ I is the input alphabet,Σ O is the output alphabet,δ:Q×Σ I →Qis the transition function, and λ:Q×Σ I →Σ O is the output function. In this paper, Mealy machines represent shields whose inputs are either global states or local observations, and whose outputs are safe action sets. 2.2 A (Simplified) Multi-Agent Path-Finding Problem We consider a simplified multi-agent path-finding (MAPF) problem [11]. The environment is a fixed H×Wgrid populated bynagents. Each grid cell is either an obstacle or a free cell. A free cell may be empty, occupied by an agent, or designated as an agent’s target. Each agent can perform one of five actions:←,→,↑,↓,·, which correspond to moving left, right, up, down, or remaining stationary. Agents operate under partial observability; each agent’s observation Ω i includes its local neighbourhood within radiusRand a coarse direction-to-target signal in−1,0,1× −1,0,1. For simplicity, we consider onlyvertex conflicts, meaning that no two agents may occupy the same cell after a transition. Figure 1(a) shows a representative grid configuration with two agents, their tar- gets, obstacles, and an example observation radius and direction-to-target-signal. Figure 1(b) depicts the action space for each agent, and Figure 1(c) illustrates a vertex conflict. A 1 A 2 T 1 T 2 R=1 (a) Grid with agents (filled cells), obstacles (grey cells), targets (bordered cells), and the current observation re- gion ofA 1 forR=1. up downleft right · stay (b) Agent action space. A 1 A 2 (c) Vertex conflict example. Figure 1: Example MAPF grids. 4Generating Local Shields for Decentralised Partially Observable Markov Decision Processes 2.3 Shield Process Algebra Shield ProcessWe define aglobal state shieldas a set of statesSh⊆Sthat are considered safe to move next. We also define ashield processusing the following grammar: P::=idle|fail|μX.P|X|Sh.P|P 1 ∥ g P 2 , whereidledenotes successful termination of the shield process, andfaildenotes unsuccessful termi- nation. The constructionμX.Pintroduces recursion (which is assumed to be guarded), withXas the corresponding recursion variable. The termSh.Pdenotes a continuation process that asserts that the next state lies in the global state shieldSh⊆Sand then continues asP. For a guarded choiceP 1 ∥ g P 2 with g⊆S, the process behaves asP 1 when the current states∈g, and asP 2 otherwise. 2.4 Vertex Conflict Avoidance Example with the Pipeline An interesting motivating example arises when the agents are blind (R=0), a scenario we refer to as the “Blind Agents”, in the environment shown in Figure 2. A 1 A 2 T 1 T 2 Figure 2: Initial state for the “Blind Agents” (R=0). Since each agent’s local observation remains constant over time, it is impossible to construct a shield that depends solely on local observations [7]. Likewise, DFA-based constructions that attempt to avoid unsafe states [3] are ineffective in this setting, because no action available to any agent can be guaranteed to lead, in combination, to a safe joint action. By contrast, our method enriches the available information through the process syntax, hence it is able to address this problem using the pipeline as shown below: Pipeline InitiationTo instantiate the pipeline, we provide a transition descriptionSAS:S×S→2 A , an observation descriptionO ′ i :S→2 Ω i , and an initial set descriptionS 0 ⊆S. These descriptions may be instantiated as the supports ofδ,Oandρ 0 , or as conservative abstractions thereof. Shield Process DescriptionWe begin with the following process specification: P= (Sh 1 .Sh 2 .Sh 3 .idle)∥ g fail whereg= A 1 A 2 T 1 T 2 T 2 ,Sh 1 = A 1 A 2 T 1 T 2 ,Sh 2 = A 1 A 2 T 2 ,Sh 3 = A 1 A 2 demonstrates a sequence of safe states that ensures both agents eventually reach their respective targets without encountering vertex conflicts. Haoran Yang, Nobuko Yoshida5 Shield Process AutomatonWe generate a shield process automaton from the process specification, obtaining a deterministic automaton that interprets the shield process: A P 0 = (Q P ,Σ,δ P ,q 0 ),Σ:=S,q 0 :=start Its states are eitheridle,fail, a continuation process (e.g.,Sh 2 .Sh 3 .idle), or the dummy initial statestart. Transitions follow the guard setgand consume the global state shieldShin sequence. The resulting automaton for the “Blind Agents” is shown in Figure 3. start Sh 1 .Sh 2 .Sh 3 .idleSh 2 .Sh 3 .idleSh 3 .idle idle fail g S S 1 Sh 1 S 2 Sh 2 S 3 Sh 3 S S Figure 3: Shield process automaton for the “Blind Agents”. Global Shield Mealy MachineWe construct the global shield Mealy machine G= (Q G ,q G 0 ,Σ G I ,Σ G O ,δ G ,λ G ), whereQ G :=idle,fail ∪(2 S ×(Q P \idle,fail)),q G 0 := (S 0 ,start),Σ G I :=S, andΣ G O := ∏ n i=1 2 A i ∪ ⊥. Here, the distinguished output symbol⊥denotes shield failure: no safe action set can be provided for the current situation. Each global Mealy state thus records the current set of reachable Dec-POMDP states together with the current state of the process automaton. To compute outputs, we fix a deterministic decompositionDec: 2 A → ∏ n i=1 2 A i that turns a joint action set into one safe local action set per agent. ForDec( ˆ A) = (U 1 ,...,U n ), where ˆ A⊆Ais a set of joint actions, we require ∏ n i=1 U i ⊆ ˆ Aand ∏ n i=1 U i =/0⇐⇒ ˆ A=/0. Thus, if each agent independently chooses an action from its local set, the resulting joint action remains in ˆ A. In this paper, we instantiate Decby selecting, in a deterministic manner, a maximum-cardinality product set ∏ n i=1 U i ⊆ ˆ A. For a transition from(S cur ,q)to(S next ,q ′ ), we compute ˆ Aby intersecting, over alls∈S cur ∩g, with q g −→q ′ , the joint actions that can move fromsinto any state inS next usingSAS, and outputDec( ˆ A). For the “Blind Agents”, the resulting global shield Mealy machine is shown in Figure 4. (g,start)(Sh 1 ,Sh 1 .Sh 2 .Sh 3 .idle)(Sh 2 ,Sh 2 .Sh 3 .idle)(Sh 3 ,Sh 3 .idle) idlefail g/[↓ A 1 ,· A 2 ] S /⊥ S 1 /⊥ Sh 1 /[↓ A 1 ,→ A 2 ] S 2 /⊥ Sh 2 /[· A 1 ,→ A 2 ] S 3 /⊥ Sh 3 /[· A 1 ,· A 2 ] ⊥ S Figure 4: Global shield Mealy machine for the “Blind Agents”. 6Generating Local Shields for Decentralised Partially Observable Markov Decision Processes Local Shield Mealy MachineThe local shield for agentiis a Mealy machine L i = (Q L i ,q L i 0 ,Σ L i I ,Σ L i O ,δ L i ,λ L i ), whereQ L i :=2 Q G ,q L i 0 :=(S 0 ,start),Σ L i I :=Ω i , andΣ L i O :=2 A i ∪⊥. Each local Mealy state is a belief subset over global Mealy states consistent with agenti’s current observation, as determined by the observation descriptionO ′ i . The transition function is defined byδ L i (q L i ,o i ):= S ( ˆ S,q)∈q L i δ G (( ˆ S,q),s)| s∈ ˆ S,o i ∈O ′ i (s), whereq L i ⊆Q G is the current local Mealy state ando i ∈Ω i is the observation. The local Mealy output is obtained by intersecting theith components of the global Mealy outputs over the global Mealy states represented by the current local Mealy state. We treatfailas contributing all actions unless every state in the belief isfail, in which case the output is⊥, indicating a shield failure: the shield cannot provide any action set that is guaranteed to be safe for the agent to choose from. In the “Blind Agents”, all observations are identical, so the belief state remains maximal and all process branches are treated as possible. The resulting local shields are shown in Figure 5. (g,start)(Sh 1 ,Sh 1 .Sh 2 .Sh 3 .idle),fail (Sh 2 ,Sh 2 .Sh 3 .idle),fail(Sh 3 ,Sh 3 .idle),fail idle,fail ·/↓ ·/↓ ·/· ·/· ·/· (a) Local shield forA 1 . (g,start)(Sh 1 ,Sh 1 .Sh 2 .Sh 3 .idle),fail (Sh 2 ,Sh 2 .Sh 3 .idle),fail(Sh 3 ,Sh 3 .idle),fail idle,fail ·/· ·/→ ·/→ ·/· ·/· (b) Local shield forA 2 . Figure 5: Local shield Mealy machines in the "Blind Agents". PRISM analysisWe analyse the shielded model using PRISM model checker, treating the agents’ policies as nondeterministic. PRISM computes lower and upper bounds on both the probability of shield failure and the probability of reaching unsafe states; in this instance,shield failurehas lower and upper bounds of 0.000000, andreaching unsafe stateshas lower and upper bounds of 0.000000, indicating that our shield ends correctly with no shield failure or reaching unsafe states. 3 Case Study In this case study, we compare multiple shield process specifications in a more general MAPF setting, using the unshielded case as the baseline. We evaluate random instances withn=2 andn=3 agents on 3×3, 4×4, and 5×5 grids, using the following shield process specifications: P 1 =μX.S sa f e .X P 2 =μX.(S sa f e .X∥ g o 1 (S sa f e .X∥ g o 2 (·(S sa f e .X∥ g o · fail)))) Haoran Yang, Nobuko Yoshida7 whereS safe ranges over safe states, andg o enumerates all global states consistent with each joint obser- vationo∈Ω. ProcessP 1 is a conservative shield that primarily aims to keep the system in safe states; to this end, it often forces each agent to remain in its original position. ProcessP 2 is the least conservative shield obtainable under our current pipeline. It minimises the loss of actions due to intersections introduced by the branch structure (i.e., it avoids disallowing multiple partial observations whenever possible) and, conversely, admits the largest possible set of next safe states. In addition to the number of agents and the grid size, our case study also varies several environ- mental and evaluation parameters. Specifically, for each configuration we keep the number of obstacles fixed, since obstacle density is associated with the probability of vertex conflicts. We then evaluate each run along three dimensions:collision(vertex conflicts),shield failure(⊥outputs from the local Mealy machines), andreached(all agents reaching their targets). gridnRobstaclesshieldcollisionshield failurereached 4×42−9/0.7270.0000.273 4×4229P 1 0.0000.0000.051 4×4229P 2 0.0000.0000.929 4×4219P 1 0.0000.0000.055 4×4219P 2 0.0000.0000.906 4×4209P 1 0.0000.0000.046 4×4209P 2 0.0000.3250.295 3×33−3/0.9860.0000.015 3×3313P 1 0.0000.0000.017 3×3313P 2 0.0000.3630.292 4×43−9/0.9690.0000.031 4×4319P 1 0.0000.0000.006 4×4319P 2 0.0000.4140.256 4×4329P 1 0.0000.0000.009 4×4329P 2 0.0000.0220.533 Table 1: MAPF experiments under a random policy. We first benchmark the different shield process specifications under a random policy across some MAPF configurations (Table 1). Here, a random policy means that each agent samples uniformly from its currently available actions; in the shielded cases, this uniform sampling is taken over the action set returned by the shield. In Table 1, across all configurations, the unshielded random policy yields highcollision, as it does not discriminate between colliding and non-colliding actions. In contrast, both shields eliminate vertex conflicts in all configurations, providing a strict safety improvement over the unshielded baseline. Among the shielded,P 2 consistently attains a higherreachedthan bothP 1 and the unshielded model. P 2 removes colliding joint actions while still admitting many safe moves, so agents can explore more states and execute more actions under a random policy. By comparison, the conservatism ofP 1 over- suppresses many potential safe actions. Varying the observation radiusRshows that a larger observation radius improves the performance of P 2 . AsRincreases,P 2 achieves higher reachability, since richer observations enable more precise belief updates and thus larger safe action sets.shield failureoccurs in configurations where (e.g.,n=3,R=1 with dense obstacles), limited observability prevents the shield from always proposing a non-empty safe joint action. AsRincreases,shield failuredecreases rapidly. 8Generating Local Shields for Decentralised Partially Observable Markov Decision Processes We next evaluate four policies trained using Q-learning with Q-tables [12] in a 3×3 MAPF con- figuration with uniformly random obstacle numbers across training and test environments (Figure 6). Q-learning is a reinforcement-learning algorithm that updates action values from sampled transitions, and a Q-table is the finite table storing those state-action values. The policies are:Q reach , trained to max- imise the probability of reaching targets only;Q safe , trained to maximise target reach while explicitly penalising vertex conflicts in the reward function;Q reach withP 1 , trained to maximise reach, with shield processP 1 enforced during interaction; andQ reach withP 2 , trained to maximise reach, with shield process P 2 enforced. Figure 6: Evaluation curves under training for learned policies with shields under 3×3,n=2,R=1 configuration For comparison, the figure also includes random policies (unshielded, shielded byP 1 , and shielded by P 2 ) as baselines, as well as the post-hoc shielding ofQ reach byP 1 and byP 2 .shield failuredoes not occur in this configuration and is therefore omitted from the plots. Black dots indicate the random baselines. The learning curves show that bothQ reach andQ safe exhibit non-zerocollision, but these rates decrease over training.collisiondeclines faster forQ safe , as expected, due to the explicit vertex conflicts penalty. All shielded variants maintain zerocollisionthroughout, demonstrating that the shields enforce safety regardless of the underlying policy. In terms ofreached,Q safe attains slightly lower success rates than Q reach , reflecting the trade-off introduced by the vertex conflicts penalty in learning. The best performance inreachedis obtained byQ reach withP 2 and by shieldingQ reach withP 2 . These combinations achieve highreachedwhile maintaining zerocollision, showing thatP 2 provides strong safety guarantees without unduly restricting actions. In contrast, policies trained withP 1 or evaluated underP 1 perform only slightly better than the random policy withP 1 : the over-conservatism ofP 1 severely limits movement, so even a trained policy cannot substantially exceed the baseline, though it may still Haoran Yang, Nobuko Yoshida9 discover narrow paths to some targets. Overall, these results reinforce the earlier findings:P 2 delivers a more favourable safety-performance trade-off thanP 1 , and all shielding can strictly improve safety relative to the unshielded while preserving, or even enhancing, task performance across environments. 4 Related Work Bloem et al. [2] establish reactive-synthesis and temporal-logic foundations that underpin many runtime-enforcement and shield-style artefacts. Alshiekh et al. [1] propose temporal-logic shields for safe reinforcement learning by synthesising an online action filter that blocks unsafe actions during learning and execution. Jansen et al. [4] propose probabilistic shields that use probabilistic model check- ing to restrict actions so that safety objectives hold with explicit probability guarantees. Elsayed-Aly et al. [3] extend shielding to multi-agent reinforcement learning by enforcing safety properties in settings where multiple agents jointly determine outcomes. Melcer et al. [6] introduce shield decentralisation by decomposing a centralised safe-action filter into per-agent filters suitable for decentralised execution. Melcer et al. [7] study decentralisation under general partial observability via a SAT-based formulation that decides whether local action sets can be chosen so that their product remains within the centralised safe joint-action set. Melcer et al. [8] explore learned shields for multi-agent reinforcement learning by training shield policies when explicit models or specifications are unavailable or costly to engineer. El Mqirmi et al. [9] propose abstraction-based post-hoc checking for deep multi-agent reinforcement learning, verifying learned behaviours against desired properties rather than filtering actions online. 5 Conclusion and Future Work This paper presents a shield process algebra for specifying safe global behaviour under Dec-POMDP, together with a compilation pipeline that produces local Mealy shields executable from local observa- tions. The resulting local Mealy shields enforce safety without communication or shared global states and are implemented in Rust with PRISM integration for model analysis. Our case study illustrates how the algebra and pipeline can eliminate collisions while preserving task performance. Future work includes optimising the decentralised joint-action decomposition (Dec), for example by integrating SAT-based decentralisation methods [7]; combining our approach with learned shields [8] to reduce manual specification effort; and improving robustness through probabilistic shield design [4]. Another direction is to extend the algebra with compositional constructs, such as combinations of shield processes, to improve both semantic clarity and pipeline efficiency. Acknowledgements The first author received travel support to attend PLACES 2026 from Balliol College, University of Oxford, through the Donald Michie Scholarship Fund. The second author is partially supported by EPSRC grants EP/T006544/2, EP/T014709/2, EP/Y005244/1, EP/V000462/1, EP/X015955/1, EP/Z0005801/1; Horizon EU TaRDIS 101093006 (UKRI No. 10066667); and ARIA. 10Generating Local Shields for Decentralised Partially Observable Markov Decision Processes References [1] Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum & Ufuk Topcu (2018):Safe Reinforcement Learning via Shielding.Proceedings of the AAAI Conference on Artificial In- telligence32(1), doi:10.1609/aaai.v32i1.11797. Available athttps://ojs.aaai.org/index.php/AAAI/ article/view/11797. [2] Roderick Bloem, Bettina Koenighofer, Robert Koenighofer & Chao Wang (2015):Shield Synthesis: Runtime Enforcement for Reactive Systems, doi:10.48550/arXiv.1501.02573. arXiv:1501.02573. [3] Ingy Elsayed-Aly, Suda Bharadwaj, Christopher Amato, Rüdiger Ehlers, Ufuk Topcu & Lu Feng (2021):Safe Multi-Agent Reinforcement Learning via Shielding, doi:10.48550/arXiv.2101.11196. arXiv:2101.11196. [4] Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban & Roderick Bloem (2020):Safe Reinforce- ment Learning Using Probabilistic Shields. In Igor Konnov & Laura Kovacs, editors:31st International Conference on Concurrency Theory, CONCUR 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, p. 31–316, doi:10.4230/LIPIcs.CONCUR.2020.3. 31st International Conference on Concurrency Theory, CONCUR 2020 ; Conference date: 01-09-2020 Through 04-09-2020. [5] George H. Mealy (1955):A method for synthesizing sequential circuits.The Bell System Technical Journal 34(5), p. 1045–1079, doi:10.1002/j.1538-7305.1955.tb03788.x. [6] Daniel Melcer, Christopher Amato & Stavros Tripakis (2022):Shield Decentralization for Safe Multi- Agent Reinforcement Learning.In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho & A. Oh, editors:Advances in Neural Information Processing Systems, 35, Curran Associates, Inc., p. 13367–13379.Available athttps://proceedings.neurips.c/paper_files/paper/2022/file/ 57444e14ecd9e2c8f603b4f012ce3811-Paper-Conference.pdf. [7] Daniel Melcer, Christopher Amato & Stavros Tripakis (2024):Shield Decentralization for Safe Re- inforcement Learning in General Partially Observable Multi-Agent Environments.p. 2384–2386, doi:10.65109/VAAR1124. [8] Daniel Melcer, Stavros Tripakis & Christopher Amato (2025):Learned Shields for Multi-Agent Rein- forcement Learning. In:The Seventeenth Workshop on Adaptive and Learning Agents. Available at https://openreview.net/forum?id=DXHxmyq5kO. [9] Pierre El Mqirmi,Francesco Belardinelli & Borja G. León (2021):An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours.CoRRabs/2102.01434, doi:10.48550/arXiv.2102.01434. arXiv:2102.01434. [10] Frans Oliehoek & Christopher Amato (2016):A Concise Introduction to Decentralized POMDPs. doi:10.1007/978-3-319-28929-8. [11] Roni Stern, Nathan R. Sturtevant, Ariel Felner, Sven Koenig, Hang Ma, Thayne T. Walker, Jiaoyang Li, Dor Atzmon, Liron Cohen, T. K. Satish Kumar, Eli Boyarski & Roman Barták (2019):Multi-Agent Pathfind- ing: Definitions, Variants, and Benchmarks.CoRRabs/1906.08291, doi:10.48550/arXiv.1906.08291. arXiv:1906.08291. [12] Christopher J. C. H. Watkins & Peter Dayan (1992):Technical Note: Q -Learning.Mach. Learn.8(3–4), p. 279–292, doi:10.1007/BF00992698.