<figure><img src="image_1.png" /></figure>

HAL
open science

# Compositional shield synthesis for safe reinforcement learning in partial observability

Steven Carr, Georgios Bakirtzis, Ufuk Topcu

► To cite this version:

Steven Carr, Georgios Bakirtzis, Ufuk Topcu. Compositional shield synthesis for safe reinforcement learning in partial observability. IEEE Open Journal of Control Systems, 2025, pp.1-12. 10.1109/ojc-sys.2025.3611725. hal-05297997

HAL Id: hal-05297997

https://hal.science/hal-05297997v1

Submitted on 5 Oct 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Compositional Shield Synthesis for Safe Reinforcement Learning in Partial Observability

Steven Carr¹, Georgios Bakirtzis², Ufuk Topcu¹

¹ The University of Texas at Austin

² LTCI, Télécom Paris, Institut Polytechnique de Paris

## Abstract

Agents controlled by the output of reinforcement learning (RL) algorithms often transition to unsafe states, particularly in uncertain and partially observable environments. Partially observable Markov decision processes (POMDPs) provide a natural setting for studying such scenarios with limited sensing. Shields filter undesirable actions to ensure safe RL by preserving safety requirements in the agents' policy. However, synthesizing holistic shields is computationally expensive in complex deployment scenarios. We propose the compositional synthesis of shields by modeling safety requirements by parts, thereby improving scalability. In particular, problem formulations in the form of POMDPs using RL algorithms illustrate that an RL agent equipped with the resulting compositional shielding, beyond being safe, converges to higher values of expected reward. By using subproblem formulations, we preserve and improve the ability of shielded agents to require fewer training episodes than unshielded agents, especially in sparse-reward settings. Concretely, we find that compositional shield synthesis allows an RL agent to remain safe in environments two orders of magnitude larger than other state-of-the-art model-based approaches.

## 1 INTRODUCTION

Reinforcement learning (RL) has emerged as a promising approach for constructing controllers that can operate in uncertain and partially observable environments, often modeled as partially observable Markov decision processes (POMDPs) [1]. However, the exploratory nature of RL algorithms can lead to the execution of unsafe actions, which is particularly concerning in safety-critical domains. Shielding, a technique that restricts the action space of the learning agent to a pre-computed set of safe actions, has been shown to improve both performance and safety compared to other approaches, such as reward shaping [2, 3].

Despite its advantages, shielding in POMDPs faces a significant scalability challenge due to the exponential growth of the belief space with respect to the number of states. In a POMDP, the agent maintains a belief distribution over the possible states, and the size of this belief space is exponential in the number of states. Consequently, the memory required to track the belief support grows exponentially, making centralized shield synthesis computationally intractable for large POMDPs [4, 5], and therefore, realistic environments. Moreover, the shield synthesis problem itself is known to be EXPTIME-complete in the number of agent and belief states, further exacerbating the scalability issue [6].

To tackle this challenge, we introduce a compositional approach to shield synthesis that exploits the inherent structure present in many POMDP scenarios. By decomposing the POMDP into smaller, more manageable submodels and computing local shields for each submodel, the compositional synthesis algorithm increases the threshold of computable shields. In particular, the compositional shielding framework allows for the parallel computation of sub-shields and enables efficient belief tracking across the submodels, ultimately facilitating the application of shielding to much larger POMDPs than previously possible.

This modular safety reasoning enables the independent synthesis of local shields, each operating over a reduced state space. Recent works have shown where local shields can be computed and later
composed to form a coherent global safety mechanism [7, 8]. Our proposed framework significantly
expands the class of POMDPs for which shield synthesis is tractable, offering a scalable alterna-
tive to centralized methods [5] while maintaining formal safety guarantees. This compositional view
not only provides improvements through structure in reinforcement learning [8, 9] but also aligns
naturally with real-world systems, which are often modular by design [10].

The main contributions of this work are threefold.

1. We develop a compositional shield synthesis approach that guarantees safety both during and after learning in large-scale POMDPs, addressing the scalability limitations of centralized shielding methods.

2. We propose a mechanism for information sharing and belief tracking across the sub-shields, ensuring the coherence of the compositional shielding framework.

3. We integrate our compositional shielding approach with state-of-the-art deep RL algorithms, demonstrating its ability to calculate shields in two orders of magnitude larger than current approaches.

We design experiments that find that compositional shielding improves learning performance, sample efficiency, and scalability. Our method outperforms centralized shielding and unshielded RL baselines, while enabling the synthesis of shields for POMDPs that are two orders of magnitude larger than those feasible for existing centralized methods.

## 2 RELATED WORK

Safe RL is necessary for deploying agents in high-stakes environments such as autonomous driving and robotics, where failures can lead to significant consequences. Because RL relies on exploratory interaction to learn the effects of actions [11], it is prone to selecting unsafe behaviors that may transition the system into hazardous states. The challenge of *unsafe exploration* motivates various strategies for reducing the likelihood of dangerous behavior [12]. Safe RL can be broadly grouped into three categories:

1. **Reward shaping:** Enhancing the reward function to reflect safety preferences [13], often based on human feedback or expert demonstration.

2. **Constrained optimization:** Introducing safety through explicit cost functions or constraints [14], which penalize unsafe actions or states.

3. **Runtime shielding:** Synthesizing a safety mechanism that restricts the agent's actions during execution [3].

This work falls within the third category and extends the theory and application of shielding in reinforcement learning. In contrast to modifying reward signals or imposing soft penalties, shielding provides formal guarantees by filtering unsafe actions at runtime [2]. While shielding has been well studied in fully observable Markov decision processes [15, 16], scaling such techniques to partially observable environments remains a challenge.

POMDPs introduce an additional layer of complexity for safe RL due to uncertainty in both action outcomes and observations [17]. Effective planning in POMDPs typically requires reasoning over histories or belief states, and recent work has made progress in scaling deep POMDP solvers [18, 19]. However, these approaches do not incorporate safety constraints directly. Prior work on shielding for deep RL under partial observability [2] provides safety guarantees but encounters significant scalability limitations. In this paper, we address these limitations by proposing a compositional approach to shield synthesis for POMDPs. By decomposing the state space and safety specification into submodels, we synthesize local shields independently and combine them to form a global shield. This approach significantly improves scalability while preserving safety guarantees.
Recent work has explored compositional shielding in multi-agent systems. Melcer et al. [7] propose a decentralized shielding mechanism for multi-agent systems without requiring inter-agent communication, focusing on empirical performance. Brorholt et al. [20] apply assume-guarantee reasoning to construct independent shields for agents under a global specification. We view these works as complementary lines of research that pursue compositional safety using different methods.

In summary, this work contributes to the body of research on runtime shielding in safe RL by introducing a compositional synthesis method for POMDPs. Unlike prior work, our approach enables scalable shield synthesis while maintaining formal guarantees of safety, and is distinct from recent multi-agent compositional methods in scope and application.

# 3 THEORETICAL PRELIMINARIES

The standard model for sequential decision-making in the presence of uncertainty is the Markov decision process (MDP). MDPs traditionally model uncertainty in the form of stochasticity in the transition dynamics [21]. POMDPs are an extension of MDPs with an additional source of uncertainty: incomplete information about the system state due to noisy or partial observations. By addressing these sources of uncertainty, POMDPs are effective in modeling real-world applications like motion-planning with limited visibility [22] or sampling terrain with noisy sensors [23].

## 3.1 Partially Observable Markov Decision Processes

In this subsection, we introduce POMDPs [17] and theoretical preliminaries associated with modeling uncertain environments to train agents operating with incomplete information.

**Definition 1 (POMDP).** A (discrete) POMDP is a tuple $\mathcal{M} = (S, I, \text{Act}, O, Z, P, \mathcal{R})$ where:

* $S$ is a finite set of states.

* $I \in \Delta(S)$ is the initial state distribution, with $I(s)$ the probability of starting in state $s \in S$.

* $\text{Act}$ is a finite set of actions.

* $Z$ is a finite set of observations and $O(z|s)$ is the probability of observing $z \in Z$ in state $s \in S$.

* $P(s'|s, a)$ is the transition probability of moving to state $s' \in S$ after taking action $a \in \text{Act}$ in state $s \in S$.

* $\mathcal{R}: S \times \text{Act} \rightarrow \mathbb{R}$ is the reward function, with $\mathcal{R}(s, a)$ the reward for taking action $a$ in state $s$.

We denote the set of available actions in state $s$ by $\text{Act}(s) \subseteq \text{Act}$. In this work, we consider POMDPs with dead-ends, i.e., states from which the agent cannot obtain positive rewards in the future [24]. We do not want the agent to end up in such dead-end states because once there, it cannot achieve any positive rewards.

By defining successor states, we are essentially helping the agent understand which states are reachable or safe to transition to from a given set of states, thereby avoiding decisions that would lead it to dead-ends.

**Definition 2 (Successor States).** For a POMDP $\mathcal{M}$ and set of states $S' \subseteq S$, the successors $\text{succ}(S')$ is the set of states $s \in S$ for which there exists an action $a \in \text{Act}(s)$ with $P(s'|a, s) > 0$ for some $s' \in S'$.

## 3.2 Beliefs

A belief state $\mathfrak{b} \in \Delta(S)$ is a probability distribution over states representing the agent's belief about the likelihood of being in each state given the history of observations and actions. The support of a belief state $\mathfrak{b}$, denoted $\text{supp}(\mathfrak{b})$, is the set of states with non-zero probability under $\mathfrak{b}$, i.e., $\text{supp}(\mathfrak{b}) = \{s \in S: \mathfrak{b}(s) > 0\}$ [25].
**Definition 3 (Belief Support).** For a given belief **b**, a state **s** is in the belief support **B** if and only if $s \in \text{supp}({\bf b})$. The set of all belief supports is denoted $\mathcal{B} = \{\mathcal{B} \subseteq \mathcal{S} : \mathcal{B} \neq \emptyset\}$, i.e., the set of non-empty subsets of $\mathcal{S}$.

If the transition and observation probabilities in the POMDP are known, the agent can update its belief state using Bayes' rule after each action and observation. However, in many practical settings, these probabilities may be unknown. In such cases, we can still update the belief support **B** using only the graph structure of the POMDP, without relying on exact probability values.

**Definition 4 (Belief Support Update).** Given a current belief support **B**, action **a**, and observation **z**, the updated belief support $\mathcal{B}'$ is the set of states $s'$ such that there exists a state $s \in \mathcal{B}$ and a non-zero probability transition from **s** to **s'** under action **a**, and **z** can be observed in $s'$, meaning that updating the belief support amounts to building the set

$$ \mathcal{B}' = \{s' \in \mathcal{S} : \exists s \in \mathcal{B} \text{ s.t. } \mathcal{P}(s'|s, a) > 0 \text{ and } \mathcal{O}(z|s') > 0\}. $$

**Definition 5 (State Estimator).** A state estimator is a function $\sigma : (\mathcal{Z} \times \text{Act})^* \times \mathcal{Z} \to \mathcal{B}$ that takes as input the history of observations and actions and returns the current belief support. The estimator can be implemented by repeatedly updating the belief support using the graph structure of the POMDP, without requiring knowledge of the exact transition and observation probabilities.

A policy $\pi$ for a POMDP is a function mapping histories of observations and actions to distributions over actions, i.e., $\pi : (\mathcal{Z} \times \text{Act})^* \times \mathcal{Z} \to \Delta(\text{Act})$. This allows the choice of action to depend on the history, which is necessary for the agent to act optimally given its uncertainty about the true state. The value of a policy $\pi$ from a belief state **b** is the expected total discounted reward

$$ V^{\pi}(b) = \mathbb{E}_{\pi, \mathcal{b}} \left[ \sum_{t=0}^{\infty} \gamma^t R(s_t, a_t) \right], $$

where $\gamma \in [0, 1)$ is the discount factor, and the expectation is taken with respect to the distribution over trajectories induced by $\pi$ starting from belief state **b**.

The optimal policy $\pi^*$ maximizes the value function for all belief states

$$ \pi^* = \underset{\pi}{\operatorname{argmax}} V^{\pi}(b), \quad \forall \mathcal{b} \in \Delta(\mathcal{S}). $$

Computing the optimal policy for a POMDP is generally intractable [26], but various approximate solution methods exist, such as point-based value iteration [27] and online search methods [28].

## 3.3 Shields

In safety-critical settings, an agent must not only maximize rewards but also adhere to safety constraints. These constraints are captured using (qualitative) reach-avoid specifications, a subclass of indefinite horizon properties [29]. Such specifications require the agent to always avoid certain unsafe states, denoted by

$$ AVOID \subseteq \mathcal{S}, $$

and to reach certain states, denoted by

$$ REACH \subseteq \mathcal{S}, $$

almost surely; i.e., with probability one over an indefinite horizon. We represent these constraints as

$$ \varphi = \langle \text{REACH}, \text{AVOID} \rangle. $$

The avoid specification, denoted by $\varphi_A = \langle \text{AVOID} \rangle$, requires only the avoidance of unsafe states. The relation $\mathcal{M}(\pi) \models \varphi_A$ indicates that the agent adheres to the specification $\varphi$ under policy $\pi$. An interesting attribute of these specification is that rewards are irrelevant for computing safe sets.
For a set of states $S' \subseteq S$ in a POMDP, $Pr_b^\pi(S')$ denotes the probability of reaching $S'$ from the belief $b$ using the policy $\pi$. A policy $\pi$ is winning for $\varphi$ from belief $b$ in the POMDP $\mathcal{M}$ if and only if $Pr_b^\pi(AVOID) = 0$ and $Pr_b^\pi(REACH) = 1$. This means that the policy must reach AVOID with probability zero and REACH with probability one (almost surely) when $b$ is the initial state.

A belief $b$ is winning for $\varphi$ in $\mathcal{M}$ if there exists a winning policy from $b$. For multiple beliefs, we define winning regions (also known as safe or controllable regions). A winning region in a POMDP is a set of winning beliefs, meaning that from each belief within this region, there exists a winning policy.

The purpose of a shield is to prevent the agent from taking actions that would violate a (reach-avoid) specification. For avoid specifications, the shield ensures that the agent does not enter prede-termined avoid states or states from which it is impossible to prevent reaching an avoid state in the future. Consequently, a shield ensures that an agent stays within a winning region. To remain inside this region, the agent must select actions such that all successor states (from the current belief) also remain within the winning region.

A shield also prevents the agent from encountering dead ends in reach-avoid specifications. While a shield itself cannot force an agent to visit reach states, we can ensure that the agent eventually visits the reach state under mild assumptions [5]. Formally, we define a shield as a set of (winning) policies, often referred to as a permissive policy [30, 31].

To compute winning policies, beliefs, and regions for qualitative reach-avoid properties, we only need to consider the finite set of belief supports [25]. Constructing a finite, albeit exponential, belief-support model that suitably abstracts the belief MDP is a prerequisite to shielding. Denote the set of all belief supports by $B$. We then directly define policies on the belief support as $\pi^b: B \to Act$. This deterministic policy selects a unique action for each belief support supp($b$).

**Definition 6 (Shield).** A permissive policy for a POMDP $\mathcal{M}$ is given by the function $v: b \to 2^{Act}$. A policy $\pi$ is admissible for $v$ if for all beliefs $b$ it holds that $\pi(b) \in v(b)$. A permissive policy is a $\varphi$-shield for $\mathcal{M}$ if all its admissible policies are winning.

We present the general problem for enforcing an agent to remain safe in POMDPs [5].

**Problem 1 (Ensured safety in POMDPs).** Given a POMDP $\mathcal{M}$, a safety constraint $\varphi$, and a sequence of policies employed by an agent $\pi_1, \dots, \pi_n$, ensure that for all policies $\pi_i$ it holds that $\mathcal{M}(\pi_i) \models \varphi$ with $1 \le i \le n$.

Precise, accurate models of uncertain systems are expensive to obtain, requiring the collection of large amounts of data or expert domain knowledge [32]. However, the system's limitations that give rise to those uncertainties are often known. This tension motivates the use of a partial model. We assume the agent only has access to a partial model $\mathcal{M}' = (S, I, Act, O, Z, P')$ where the transition model $P'$ yields unknown but positive probabilities. Essentially, $P'$ defines a set of possible transitions.

A POMDP $\mathcal{M} = (S, I, Act, O, Z, P)$ and a partial model $\mathcal{M}' = (S, I, Act, O, Z, P')$ have coinciding transitions if and only if for all states $s, s' \in S$ and actions $a \in Act$, $P(s' | s, a) > 0$. The partial model defines exactly the graph of the original POMDP. Similarly, $\mathcal{M}'$ overapproximates the transition model of $\mathcal{M}$ if for all states $s, s' \in S$ and actions $a \in Act$, $P(s' | s, a) > 0$ if $P'(s' | s, a) > 0$. The original POMDP has no transitions that are not present in the partial model.

The provable guarantees produced by a shield depend on the partiality of the model. Knowing the exact set of transitions with arbitrary positive probability for a POMDP is sufficient to compute a $\varphi$-shield [2].

# 4 COMPOSITIONAL SHIELD SYNTHESIS

We first outline decomposition of a POMDP $\mathcal{M}$ into a set of submodels $\{\mathcal{M}_1, \dots, \mathcal{M}_n\}$ and describe properties that make a composition admissible. Then we describe shielding and the guarantees computed on the submodels. We present a working example in the domain *Obstacle(8)* (example 1):
<figure><img src="image_3.png" /><figcaption>(a) Environment with an overlay of the $\varphi_1$-shield.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>(c) Submodel composition</figcaption></figure>

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /><figcaption>(b) $\varphi_{2,3,4}$-shields</figcaption></figure>

Figure 1: *Obstacle(8)* equipped with a compositional shield, comprising four sub-shields that cover the entire state space using distinct sets of states and form connections using the set of potential successor states (highlighted in yellow). The reach-avoid specification $\varphi$ can be composed as $\bigcup_{i \in \{1...4\}} \varphi_i$, where each $\varphi_i$ represents the reach-avoid specification applied to its distinct set of states. The connected submodels form a composition graph, which helps us to define winning regions when the reach states are outside of the submodel’s set of states (section 4.3).

**Example 1.** Consider the environment *Obstacle(8)* (Figure 1), which is a single-agent gridworld with four initial locations and five “dead zones” from which the agent cannot exit. The agent has three observations {white, red, green} where white is an unlabelled state, red is a dead zone, and green is the target state. At each state, the agent may select one of four actions {left, right, up, down}, upon selecting the agent, the agent may move one or two spaces depending on the probability of slip $p = 0.1$. In such an environment, there is a natural segmentation into smaller grids as quadrants (dashed lines of Figure 1).

## 4.1 POMDP (De)composition

When decomposing the POMDP model $\mathcal{M}$ into submodels $\{M_1, ..., M_n\}$, there are multiple approaches to achieving a compositional abstraction. Some examples include:

* distinguishing the location of an agent from the location of a moving obstacle,

* splitting a large area into smaller areas, and

* separating the tracking of the fuel reserves from the avoiding of collisions.

While each corresponds to different features in the problem formulation, all decompositions have the following in common: The subproblems are all performed on smaller state spaces than their precursor models. After decomposing and computing the behavior induced within the submodels, we must preserve some properties to compose.
**Definition 7 (State-based POMDP decomposition).** Let $\mathcal{M} = (S, I, \text{Act}, O, Z, \mathcal{P}, \mathcal{R})$ be a POMDP. Given a subset of states $S_i \subseteq S$, we define the corresponding submodel POMDP as

$$ \mathcal{M}_i = (\hat{S}_i, I_i, \text{Act}, O_i, Z, \mathcal{P}_i, \mathcal{R}_i), $$

where:

* The submodel state space is $\hat{S}_i = S_i \cup \text{succ}(S_i)$, where

$$ \text{succ}(S_i) = \{s' \in S \mid \exists s \in S_i, a \in \text{Act}, \mathcal{P}(s' \mid s, a) > 0\}. $$

* The transition function $\mathcal{P}_i$ is defined as:

$$ \mathcal{P}_i(s' \mid s, a) = \begin{cases} \mathcal{P}(s' \mid s, a) & \text{if } s \in S_i \text{ and } s' \in \hat{S}_i, \\ 1 & \text{if } s \in \hat{S}_i \setminus S_i \text{ and } s' = s, \\ 0 & \text{otherwise.} \end{cases} $$

That is, states in $\hat{S}_i \setminus S_i$ are treated as absorbing states with self-loops for all actions. We emphasize that while interface states $\hat{S}_i \setminus S_i$ are included to model successors and enable belief tracking, they are not controllable in $\mathcal{M}_i$ and are never initial. These “absorbing” interface states are a conservative overapproximation to handle belief updates at submodel boundaries and capture the condition when the agent leaves the domain of that submodel. They serve solely to close the dynamics of a given submodel upon exit (guaranteed local safety) and preserve successor structure without underestimating risk transiting from one submodel to another.

* The observation function $O_i$ is the restriction of $O$ to $\hat{S}_i$, i.e.,

$$ O_i(z \mid s) = O(z \mid s) \quad \text{for all } s \in \hat{S}_i, z \in Z. $$

* The reward function $\mathcal{R}_i$ is the restriction of $\mathcal{R}$ to core states:

$$ \mathcal{R}_i(s, a) = \begin{cases} \mathcal{R}(s, a) & \text{if } s \in S_i, \\ 0 & \text{otherwise.} \end{cases} $$

* The initial distribution $I_i$ must satisfy:

$$ \text{supp}(I) \cap S_i \subseteq \text{supp}(I_i) \text{ and } I_i(s) = 0 \text{ for all } s \in \hat{S}_i \setminus S_i. $$

**Example 1. cont.** Returning to Example 1, for an agent that may be at the top-right corner (state $s \in S_1$) of submodel $\mathcal{M}_1$. The action right would lead to $s' \in \hat{S}_i \setminus S_i$. It is important that this successor $s$ is included in the states modelled by the submodel $\mathcal{M}_1$ as we want to ensure a safe transition out of the submodel. By then making this state $s'$ absorbing, we reflect that $\mathcal{M}_1$ does not have control over what happens after the agent $s'$, which is the responsibility of submodel $\mathcal{M}_2$. This design ensures that each submodel operates only within its assigned domain and handles transitions conservatively at the edges. The absorbing behavior prevents circular dependencies between submodels and makes shield computation tractable by enforcing a clear boundary.

We describe the conditions on the initial distribution $I_i$ (definition 8) but at a minimum we preserve any initial states in $I(s)$ to the submodel initial states $I_i(s)$ by restricting the domain to $S_i$.

**Definition 8 (Admissible composition).** A set of submodels $\{\mathcal{M}_1, \dots, \mathcal{M}_n\}$ is an admissible composition of a POMDP $\mathcal{M} = (S, I, \text{Act}, O, Z, \mathcal{P}, \mathcal{R})$ if the following conditions hold:

P1 State cover: Every state in $S$ is included in at least one submodel, i.e.,

$$ S = \bigcup_{i=1}^{n} S_i, $$

where $S_i$ is the set of core states in submodel $\mathcal{M}_i$.
P2 Initialization consistency: For each submodel $\mathcal{M}_i$ with initial distribution $I_i$, the support of the global initial distribution $I$ restricted to $S_i$ must be contained in the support of $I_i$, i.e.,

$$ \mathrm{supp}(I) \cap S_i \subseteq \mathrm{supp}(I_i). $$

To ensure that all transitions coincide we must include the successor states $\mathrm{succ}(S_i) \subseteq S$. However, it is important to distinguish that while submodel $\mathcal{M}_i$ may contain states $s \in \mathrm{succ}(S_i) \setminus S_i$ that are $s \notin S_i$ we do not use the submodel $\mathcal{M}_i$ to model the behavior in these states. We use these states to describe endpoints for the model $\mathcal{M}_i$. In this work, unless otherwise described, we refer to set of states inside of model $\mathcal{M}_i$ as $S_i$ rather the $\hat{S}_i$ that they contain.

A set of submodels may have overlapping states. A submodel may, also, include more states in their initial distribution $I_i$ compared to the original model $\mathcal{M}$, i.e., $|\mathrm{supp}(I(s))| < |\mathrm{supp}(I_i(s))|$, to allow for an overapproximated composition.

## 4.2 Compositional Avoid Shield

To form a composition, we consider the features of the problem and attempt to capitalize on symmetries. In Example 1, a standard gridworld, While state estimation (tracking of the belief support $B$, see right-hand side of Figure 2) may still be conducted on the full model $\mathcal{M}_i$, we require an interface for estimating the belief support inside the submodels to compute a shield.

**Definition 9 (Submodel state estimator).** Let $\mathcal{M}_i = (\hat{S}_i, I_i, \mathrm{Act}, O_i, Z, P_i, R_i)$ be a submodel defined over core state set $S_i \subseteq S$ and extended state set $\hat{S}_i \supseteq S_i$.

Let $b_i: Z \times \mathrm{Act} \times Z \to \Delta(S_i)$ denote the submodel belief distribution over $S_i$, and let the corresponding belief support be defined as:

$$ B_i = \mathrm{supp}(b_i) \subseteq S_i. $$

Let $B_i$ denote the set of all possible belief supports over $S_i$.

Then, a submodel state estimator is a function

$$ \sigma_i : (Z \times \mathrm{Act})^* \to B_i $$

that, given a sequence of observation-action pairs, computes the updated belief support $B_i$ over $S_i$, using the transition relation $P_i$ and observation function $O_i$.

Specifically, $\sigma_i$ maintains a sound overapproximation of reachable states in $S_i$ given the agent's history $h \in (Z \times \mathrm{Act})^*$, based on the POMDP graph structure of the submodel.

**CONSISTENCY OF BELIEF SUPPORT.** We assume that the agent interacts with the environment by producing a trace of observations and actions. Let $h = (z_0, a_0, z_1, a_1, \dots, z_t) \in (Z \times \mathrm{Act})^*$ denote such a trace. The belief support $B \subseteq S$ of the global POMDP $\mathcal{M}$ at time $t$ is computed using a state estimator $\sigma: (Z \times \mathrm{Act})^* \to 2^S$, which maps the agent's trace to a set of states consistent with the observations and transitions in $\mathcal{M}$. That is,

$$ B = \sigma(h). $$

For each submodel $\mathcal{M}_i$, we define a corresponding *submodel state estimator*

$$ \sigma_i : (Z \times \mathrm{Act})^* \to 2^{S_i}, $$

which tracks the belief support $B_i = \sigma_i(h) \subseteq S_i$ based only on the submodel's transition graph and observation function.

The compositional belief support is then given by the union of the submodel belief supports:

$$ \hat{B} = \bigcup_{i=1}^{n} B_i. $$
<figure><img src="image_8.png" /><figcaption>Figure 2: Feature-based compositional shield synthesis.</figcaption></figure>
We say that the belief support is *consistent under composition* if the global estimator and the union of submodel estimators yield the same result, i.e.,

$$ \sigma(h) = \bigcup_{i=1}^{n} \sigma_i(h) \quad \text{for all } h \in (Z \times Act)^*. $$

Under this consistency condition, belief updates also align: if $a \in Act$ and $z \in Z$ are the latest action and observation, then

$$ B' = \sigma(h \cdot (a, z)) = \bigcup_{i=1}^{n} \sigma_i(h \cdot (a, z)) = \hat{B}'. $$

There are two sufficient conditions for consistency, both of which come by construction in Definitions 7-9: 1.) a shared trace input, where all submodels process a common trace h and 2.) consistent graph interfaces, i.e. the transition and observation functions used by $\sigma_i$ are faithful restrictions or projections of the global model. Importantly, belief consistency does not require exact agreement on belief distributions across submodels. Because all estimators process the same trace h, and use deterministic updates based on the known graph-structure of their respective submodels, the union of their outputs naturally conserves the reachable set as computed globally.

**COMPOSITIONAL AVOID PROCEDURE.** Given a global avoid specification $\varphi' = \langle AVOID \rangle$, each submodel $M_i$ defined over core states $S_i$ and extended state space $\hat{S}_i$ inherits a local avoid specification $\varphi'_i = \langle AVOID_i \rangle$, where

$$ AVOID_i = AVOID \cap \hat{S}_i. $$

That is, all avoid states from the global specification that are present in submodel $M_i$—whether in its core or interface states—must also be treated as avoid in the submodel specification. This ensures that any shield synthesized for $M_i$ prevents transitions into states that violate the global avoid specification, maintaining soundness under composition.

**Theorem 1 (Compositional AVOID-shield).** Let $M' = (S, I, Act, O, Z, P', R)$ be a POMDP with avoid set $AVOID \subseteq S$. Let $\{M'_1, \dots, M'_n\}$ be submodels forming an admissible composition of $M'$ (Definition 8). For each $i \in \{1, \dots, n\}$, define $AVOID_i = AVOID \cap \hat{S}_i$, $\varphi'_i = \langle AVOID_i \rangle$, and let $v_i$ be a $\varphi'_i$-shield for $M'_i$ (i.e., no trace allowed by $v_i$ in $M'_i$ can visit a state in $AVOID_i$). Define the global shield

$$ v(b) = \bigcap_{i=1}^{n} v_i(B_i(b)), $$

where $B_i(b)$ is the submodel-i belief support computed by the submodel state estimator $\sigma_i$ (Definition 9). Then $v$ is a $\varphi'$-shield for $M'$: no trace allowed by $v$ in $M'$ can ever visit a state in $AVOID$.

*Proof.* We prove the claim by induction on the length $t$ of the observation-action trace

$$ h_t = (z_0, a_0, z_1, \dots, a_{t-1}, z_t). $$

**BASE CASE ($t=0$)** The agent starts in some state $s_0 \sim I$. By admissible composition (Definition 8, property P2), every $s_0 \in \text{supp}(I)$ lies in at least one submodel $M'_i$ and hence in $S_i \subseteq \hat{S}_i$. Since $AVOID_i = AVOID \cap \hat{S}_i$, we know $s_0 \notin AVOID_i$ and hence $s_0 \notin AVOID$. Thus the base case holds.

**INDUCTIVE STEP** Assume that after trace $h_t$ of length $t$, the agent's belief support $B(h_t) \subseteq S$ satisfies $B(h_t) \cap AVOID = \emptyset$.

Let $a_t$ be an action allowed by the shield $v$, i.e.,

$$ a_t \in v(B(h_t)) = \bigcap_{i=1}^{n} v_i(B_i(h_t)), $$

where $B_i(h_t) = \sigma_i(h_t)$ is the belief support tracked within submodel $M'_i$ using its own estimator.
Since $a_t$ is allowed by every submodel shield on its local belief support, and each $v_i$ is a $\phi_i$-shield, it follows that for all $s \in B_i(h_t)$, no successor state

$$s' \in \mathrm{succ}(s, a_t) \cap \mathrm{AVOID}_i$$

is reachable in $M_i'$.

By admissible composition (Definition 8, property P1) and the construction of each submodel (Definition 7), every successor state

$$s' \in \mathrm{succ}(B(h_t), a_t)$$

in the global model $M'$ lies in at least one $\hat{S}_i$ and hence is subject to some local shield that prevents entry into $AVOID_i$. Because $AVOID_i = AVOID \cap \hat{S}_i$, we conclude $s' \notin AVOID$. Thus the updated belief support $B(h_{t+1}) = \sigma(h_{t+1})$ satisfies

$$B(h_{t+1}) \cap AVOID = \emptyset.$$

By induction, no trace permitted by the global shield $v$ can reach a state in $AVOID$.

**ONLY IF** If the set $\{M'_1, \dots, M'_n\}$ does not form an admissible composition of $M'$, then either some state $s \in S$ is not covered by any $S_i$ (violating P1), or some $s \in \mathrm{supp}(I)$ is not included in any $\mathrm{supp}(I_i)$ (violating P2), in which case no set of local shields can guarantee global avoidance of $s \in AVOID$; i.e., shielding is unsound or incomplete. $\square$

## 4.3 Compositional Reach-Avoid Shield

While the avoid shield from the previous section restricts actions that could enter $AVOID$ states, it is necessary to construct shields that also allow reaching the target.

**Definition 10** (Winning submodel). Let $\mathcal{M} = (S, I, \mathrm{Act}, O, Z, P, \mathcal{R})$ be a POMDP with a reach set $REACH \subseteq S$. A submodel $\mathcal{M}_i$ with core state set $S_i$ is called a winning submodel if $REACH \cap S_i \neq \emptyset$.

**STATE SPACE SEGMENTATION AND CONNECTORS** We examine the possible transitions between the subsets of states for each submodel to determine which submodels are connected. Submodel $\mathcal{M}_i$ connects to submodel $\mathcal{M}_j$ if and only if there exists a state $s \in S_j$ that is a successor state of $s \in \mathrm{succ}(S_i)$. We define the connection graph as a directed graph formed by connected submodels. In the presented example, one may move from the top-left quadrant to the top-right or the bottom-left but not the bottom right (see Figure 1c for the connection graph of the submodels). We must form this connection graph to give the submodels a REACH specification. Then we form a path from the directed graph created by the connected submodels (dark gray lines in Figure 1c).

**COMPOSITIONAL REACH-AVOID PROCEDURE** Consider the non-covered successor states in sub-model $\mathrm{succ}(S_i) \setminus S_i$, if connected submodel $\mathcal{M}_j$ has a direct path to a winning submodel. Then we label $REACH_i = (\mathrm{succ}(S_i) \setminus S_i) \cap S_j \subseteq \hat{S}_i$. Any $AVOID \subseteq S$ state will remain an $AVOID_i \subseteq S_i$ in the submodel $\mathcal{M}_i$. The reach-avoid specification for submodel $\mathcal{M}_i$ is then given by $\phi_i = \langle REACH_i, AVOID_i \rangle$.

**REACHABLE SPACES** In example 1, it is insufficient for the reach-avoid shield to synthesize a strategy for the states within the quadrants. For instance, if we consider the set of states inside the dashed lines of the top-left quadrant (covered by $\mathrm{shield}_{\phi_1}$ in Figure 1), there is no winning state for the agent to enforce a reach-avoid specification. For the spaces with a subset of states without a winning condition, we modify the winning region to move the agent outside these spaces. This modification includes adding all possible successor states into the set of states covered by the shield.

**INITIAL BELIEF SUPPORT** Similarly, if there is no initial state within the set of states, such as the top-right quadrant ($\mathrm{shield}_{\phi_2}$ in Figure 1), then there is no input for the synthesis approach to tracking belief support. To initialize such belief support, we overapproximate the input belief support for $\mathcal{M}_2$. We extend the state space of the submodel to include any precursor states for the region (yellow states in figure 1b). We then include any states from precursor models (backward along the dark gray line in
**Algorithm 1** Compositional Shield Synthesis for POMDPs

**Require:** For POMDP $\mathcal{M}$, a partial model of the structure $\mathcal{M}' = (S, I, Act, O, Z, P')$

**Require:** Safety specification $\varphi = \langle \text{REACH}, \text{AVOID} \rangle$

**Require:** Decomposition strategy ▷ e.g., feature- or location-based

**Ensure:** Global shield $v$ enforcing $\varphi$ across $\mathcal{M}$

1: **// Step 1: Decompose Global Model**

2: Construct a set of submodels $\{\mathcal{M}'_1, \dots, \mathcal{M}'_n\}$ with core states $S_i$ and extended states $\hat{S}_i = S_i \cup \text{succ}(S_i)$

3: **for** each submodel $\mathcal{M}_i$ **do**

4: $\mathcal{M}'_i \leftarrow (\hat{S}_i, I_i, Act, O_i, Z, P'_i)$

5: $P_i(s, a, s)' \leftarrow 1 \quad \forall a \in Act, \forall s \in \hat{S}_i \setminus S_i \quad \triangleright \text{Treat all interface states as absorbing (see Definition 7)}$

6: **end for**

7: **// Step 2: Assign Local Specifications**

8: **for** each $\mathcal{M}'_i$ **do**

9: $\text{AVOID}_i \leftarrow \text{AVOID} \cap \hat{S}_i$

10: **if** $\text{REACH} \cap S_i \neq \emptyset$ **then**

11: $\text{REACH}_i \leftarrow \text{REACH} \cap S_i$

12: **else**

13: $\text{REACH}_i \leftarrow \text{succ}(S_i) \quad \triangleright \text{use connection graph to assign proxy through successors}$

14: **end if**

15: $\varphi_i \leftarrow \langle \text{REACH}_i, \text{AVOID}_i \rangle \quad \triangleright \text{Define local spec}$

16: **end for**

17: **// Step 3: Compute Local Shields**

18: **for** each $\mathcal{M}'_i$ **do**

19: $v_i \leftarrow \text{compute}(\mathcal{M}'_i, \varphi_i) \quad \triangleright \text{Synthesize local permissive policy (shield) [5]}$

20: **end for**

21: **// Step 4: Compose Global Shield**

22: **function** GLOBALSHIELD($h$)

23: **for** each $i \in \{1, \dots, n\}$ **do**

24: $B_i \leftarrow \sigma_i(h) \quad \triangleright \text{Use submodel estimator on current trace}$

25: $Act_i \leftarrow v_i(B_i) \quad \triangleright \text{Actions allowed by shield } i$

26: **end for**

27: **return** $v(h) = \bigcap_{i=1}^n a_i$ \quad ▷ Intersection of local shields

28: **end function**

29: **// RL Integration**

30: Use $v(h)$ to mask actions in RL training (see Figure 3)
<figure><img src="image_9.png" /><figcaption>Figure 3: RL with a compositional shield.</figcaption></figure>

Figure 1c) into the initial distribution $I_2(s)$ of the submodel $\mathcal{M}_2$. This modification makes it possible to synthesize a shield from this overapproximation on the belief support.

**SHIELD SYNTHESIS** We can now compute shields for each submodel. This synthesis procedure can be performed in parallel (Figure 2 and Algorithm 1). For the partial submodel $\mathcal{M}'_i$ and reach-avoid specification $\varphi_i$, we can compute the permissive policy $v_i$, which ensures that an agent with belief support $B_i$ will almost-surely satisfy $\varphi_i$.

# 5 SAFE RL VIA COMPOSITIONAL SHIELDS

We present the problem of safe learning in POMDPs.

**Problem 2 (Safety-critical RL).** Given a POMDP $\mathcal{M}$, a safety constraint $\varphi$, and let $\pi_1, \dots, \pi_n$ be the (training) sequence of policies employed by an agent. The problem is to ensure that for all policies $\pi_i$ it holds that $\mathcal{M}(\pi_i) \models \varphi$ with $1 \le i \le n$ and the final policy $\pi_n$ maximizes $\mathbb{E}[\sum_{t=0}^{\infty} \gamma^t R_t]$.

An optimal solution to problem 2 may induce a lower reward than unconstrained learning, as the agent has to strictly adhere to the safety constraint while collecting rewards.

A shielded agent augments the reinforcement learning loop [33] (Figure 3). In particular, at each decision step, the RL agent selects an action $a$ from the set of available actions $Act(s)$. The shielded RL agent selects from the subset of these actions $Act'(s)$ created by the permissive policy $v$. Additionally, the RL agent uses the graph knowledge to track the belief support.

## 5.1 Shields and RL in POMDPs

Enforcing shielding for safe RL is useful for environments with sparse reward and incomplete information [2]. However, one limitation is that the size of the potential belief supports $B$ increases exponentially with the number of aliased observations.

In this work, we formulate a procedure that allows an RL agent to compute a shield by parts from a set of connected sub-shields with two benefits. First, the sub-shield upper bounds the size of belief support, ensuring a computable and tractable shield. Second, it provides the learner with additional information about the features of the environment as it learns, which allows for warm-start learning [34] in sparse reward settings.
## 5.2 Shield Properties

First we describe the important properties that are preserved when deploying shielding in deep RL. In particular, we motivate the use of a partial model, which represents an overapproximation of the POMDP graph.

**USING THE PARTIAL MODEL** The *belief-support state estimator* $\sigma$ provides a light-weight, interface to track the possible system states at every loop of Figure 3. This estimator also provides the input for the shield (definition 6).

**USING THE PARTIAL MODEL VIA A SHIELD** We assume the availability of a shield that ensures reach-avoid specifications as outlined above (definition 6). Using the state estimator, we can synthesize a shield $v$: $\text{supp}(b) \rightarrow 2^{Act}$ that operates directly on the belief support. For the specification $\varphi$, this shield yields for every belief the set of *safe actions*. We restrict the available actions for the agent to these safe actions. For the specification $\varphi$, this shield yields for every belief the set of *safe actions*. We restrict the available actions for the agent to these safe actions.

## 5.3 Learning Outcomes

Shielded RL agents can enforce safe decisions during learning. Without a shield, the agent must take action to record that it may transition to an unsafe state. While a shield ensures that the agent visits the reach states eventually (with probability one), there is no upper bound on the number of steps required to visit these states. The shielded agent may violate the specification if the partial model is not faithful – it has a different graph structure – to the true POMDP. Moreover, state estimators themselves do not directly enforce safe exploration. However, precise tracking of the belief support augments the learning agent with structured information.

**SAFETY AFTER LEARNING** Even after the RL agent has finished learning, agents who keep exploring may violate safety. Furthermore, reward objectives and safety constraints may not coincide, e.g., a car driving to a location. A reward structure may only focus on a particular feature, such as arriving with enough fuel, while a safety constraint only enforces collision avoidance. In such cases, there is a risk-reward consideration where the RL may accept a small but non-zero risk to avoid a significant and expensive re-route.

**RL CONVERGENCE SPEED** Learning in partially observable settings remains challenging beyond providing safety guarantees, especially when rewards are sparse. The availability of a partial model can accelerate the learning process. In particular, the availability of a state estimator allows enriching the observation with a signal that compresses the history and the shield induces longer episodes that improve learning in sparse-reward environments [2].

## 5.4 Compositional Shield Execution

After computing a shield, we can filter and apply the belief support relevant to the states covered in its submodel (dashed segment in Figure 2). For example, if the agent's belief support contains two states: one in the top-left quadrant and one in the top-right quadrant, then the input belief support $B$ is filtered to a single state for shield $v_1$ and a single state for $v_2$. Finally, we constrain the RL agent with the intersect of the sets of allowed actions $Act' = \bigcap_{i=1}^{n} Act'_i$, eliminating any possible violating actions for all states in the belief support $B$.

## 5.5 Parallel Training

One advantage of the decomposition and its corresponding shields is that we can use a learning method that is compatible and operable with compositional RL frameworks [34]. We may deploy each RL subsystem and subtask, initializing a subtask learning problem for each subtask and submodel, thereby emphasizing relevant regions and ignoring low-value subsystems. While a deep exploration of the various compositional RL frameworks is beyond the scope of this paper, we demonstrate that this approach to shielding is compatible with higher abstraction levels.
<table><caption>Table 1: Individual sizes and total compute times for shield and sub-shield synthesis.</caption><thead><tr><th rowspan="2">Domain (param)</th><th colspan="2">Shield Synthesis</th><th colspan="2">Compositional</th></tr><tr><th>States</th><th>Time (s)</th><th>States</th><th>Time (s)</th></tr></thead><tbody><tr><td><em>Obstacle</em>(6)</td><td>37</td><td>1</td><td>26</td><td>2</td></tr><tr><td><em>Obstacle</em>(8)</td><td>65</td><td>18</td><td>37</td><td>5</td></tr><tr><td><em>Obstacle</em>(10)</td><td>101</td><td>598</td><td>50</td><td>55</td></tr><tr><td><em>Obstacle</em>(16)</td><td>257</td><td>6314</td><td>101</td><td>1504</td></tr><tr><td><em>Obstacle</em>(20)</td><td>401</td><td>TO</td><td>145</td><td>1605</td></tr><tr><td><em>Refuel</em>(6,8)</td><td>270</td><td>6</td><td>101</td><td>6</td></tr><tr><td><em>Refuel</em>(8,10)</td><td>641</td><td>109</td><td>270</td><td>24</td></tr><tr><td><em>Refuel</em>(10,12)</td><td>1201</td><td>816</td><td>651</td><td>150</td></tr><tr><td><em>Refuel</em>(16,18)</td><td>4609</td><td>TO</td><td>1235</td><td>860</td></tr><tr><td><em>Evade</em>(6,2)</td><td>4232</td><td>142</td><td>1833</td><td>120</td></tr><tr><td><em>Evade</em>(8,2)</td><td>10368</td><td>1510</td><td>2501</td><td>213</td></tr><tr><td><em>Evade</em>(10,2)</td><td>16391</td><td>TO</td><td>7121</td><td>1609</td></tr><tr><td><em>Evade</em>(16,2)</td><td>TO</td><td>TO</td><td>14501</td><td>9601</td></tr><tr><td><em>Intercept</em>(7,1)</td><td>4705</td><td>116</td><td>2501</td><td>32</td></tr><tr><td><em>Intercept</em>(10,1)</td><td>9690</td><td>1861</td><td>4705</td><td>450</td></tr><tr><td><em>Intercept</em>(16,1)</td><td>49235</td><td>TO</td><td>10032</td><td>4601</td></tr></tbody></table>

# 6 EMPIRICAL ANALYSIS

We evaluate the effectiveness of compositionally shielded reinforcement learning (RL) in four partially observable domains with sparse reward functions. These domains, adapted from [5] and [2], present unique challenges for RL agents:

1. *Obstacle*: An agent navigates a maze (movement reward: -1) with static traps, uncertain initial state, and noisy movement distance. The agent only observes whether its current position is a trap (-10³ reward) or the exit (+10³ reward).

2. *Refuel*: A rover traverses from one corner to another (+10 reward), avoiding a diagonal obstacle. Movement consumes energy, and the rover can recharge at designated stations to full capacity without rewards or costs. The rover has noisy sensors for position and battery level. Collisions and battery depletion terminate the episode.

3. *Evade*: An agent must reach an escape door (+10 reward) while evading a faster robot. The agent has a limited vision range (Radius), but can scan the entire grid instead of moving.

4. *Intercept*: Compared to *Evade*, the agent aims to intercept (+10³ reward) a robot before it exits the grid (-10³ reward). The agent has a view radius and observes a central corridor. Movements incur a -1 reward.

We employ five deep RL methods: DQN [35], DDQN [36], PPO [37], discrete SAC [38], and REINFORCE [39]. Episodes are limited to 100 steps, and average rewards are calculated across 10 evaluation episodes. To improve readability, we apply smoothing to all figures using a five-interval window.

For both the complete model and the submodels, we use the *Storm* framework [40] to interface the model, shield, and state estimator. We use the same tool for both approaches to the problem
<figure><img src="image_10.png" /><figcaption>Figure 4: Learning agents with different shield types on a reward normalized across the set of small domains.</figcaption></figure>

(composition vs. no composition) for a fair comparison with the state-of-the-art. Bindings to Tens-
sorflow's *TF-Agents* package [41] are deployed, and its masking function is used to implement the
precomputed shield [2]. Experiments are conducted on an 8 × 3.2 GHz Intel Xeon Platinum 8000
series processor with 32 GB of RAM. Computations exceeding 10⁵ seconds are marked as timed
out (TO).

**6.1 Shield Synthesis through Subproblem Composition**

**DOMAIN DECOMPOSITIONS** We employ quadrant-based decompositions for the *Obstacle* and *Re-fuel* domains. For *Evade* and *Intercept*, we use a dual quadrant-based decomposition (16 submodels) to represent agent and adversary locations in each region.

**SCALABILITY IMPROVEMENTS** Traditional shield synthesis [5, 2] often fails to scale beyond 10⁴ states (Table 1). Our compositional approach computes shields for these and larger domains, achieving a two-order-of-magnitude scalability improvement over centralized methods.

**LEARNING PERFORMANCE** We normalize RL agent performance to [0, 1], with 1 representing the highest achievable value. In small domains, compositional shields require slightly more data to converge than centralized shields (Figure 4). However, the compositional RL framework improves data efficiency, with faster convergence than initializing RL only in initial states (Figure 5).

**SAFETY AND PERFORMANCE IN LARGE DOMAINS** In large domains where centralized shield synthesis is infeasible, agents with compositional shields significantly outperform unshielded agents (Figure 5). Shielding ensures safety throughout learning, with sub-shields maintaining this property (Table 2). Although sub-shields may converge slower in small domains, compositional shielding is crucial for safe and efficient learning in complex environments.

For ease of comparison across domains and learning methods, we normalized the RL agent perfor-
mance across all domains. We modify the reward such that the agent will take a value between 0 and
1, where 1 is the known highest possible value that the RL agent can achieve.

**EQUIVALENT PERFORMANCE TO CENTRALIZED SHIELD IN SMALL DOMAINS** When comparing the
<figure><img src="image_11.png" /><figcaption>Figure 5: Learning agents with different shield types on a reward normalized across the set of domains too large for a centralized shield.</figcaption></figure>

<table><caption>Table 2: Average violation and positive rewards during and after reinforcement learning.</caption><thead><tr><th rowspan="2">Learning Setting</th><th colspan="2">No. violations</th><th colspan="2">% successful runs</th></tr><tr><th>During</th><th>After</th><th>During</th><th>After</th></tr></thead><tbody><tr><td>No shield</td><td>3153</td><td>1023</td><td>25%</td><td>40%</td></tr><tr><td>Shield</td><td>0</td><td>0</td><td>90%</td><td>95%</td></tr><tr><td>Sub-shields</td><td>0</td><td>0</td><td>75%</td><td>95%</td></tr></tbody></table>

learning performance for the shield with the compositional shield, we observe that the compositional shield needs slightly more data to converge (dark gray line compared to the yellow line in Figure 4).

**IMPROVED PERFORMANCE COMPARED TO UNSHIELDED AGENTS IN LARGER DOMAINS** When we compare the shielded agent to that of an unshielded agent in very large domains that we are unable to synthesize shields for (dark gray outperforms light gray in Figure 5).

**IMPROVED DATA EFFICIENCY USING COMPOSITIONAL RL** When we deploy a compositional RL framework, the RL converges faster than a simple problem where we perform RL initialized only in initial states (yellow line in Figure 5 converges around 2000 episode while the dark gray line converges around 3500). Here, the RL agent may initialize the belief support on the sub-models that are not inside the set of initial distribution, which allows the RL to better explore regions of interest without relying on repetitive trajectories.

**ENFORCING SAFETY WHILE LEARNING** Shielding ensures that the agent is safe while learning, i.e., it will never violate the safety specification $\varphi$ (table 2). We demonstrate that the sub-shields maintain this property but it does not as easily enforce that the RL agent will reach the goal during the learning process. This condition leads to the sub-shields taking slightly longer to converge in smaller domains when compared to overall shield. However, the RL agent employing a compositional shield still significantly outperforms an unshielded agent in larger domains.

**AUTOMATED APPROACHES TO DECOMPOSITION** While the decompositions used in our experiments (e.g., quadrant-based or feature-partitioned) are manually chosen to match domain symmetries, we acknowledge the need for more systematic methods. One potential direction is to leverage the sparsity structure of the transition graph associated with the POMDP $\mathcal{M}$. Specifically, we can
treat the POMDP's transition kernel $P'$ as a sparse adjacency matrix and apply graph partitioning or
sparse matrix decomposition techniques such as spectral clustering [42] to identify weakly connected
subgraphs. These subgraphs correspond to regions of the state space with limited interconnectivity,
making them ideal candidates for submodels. Such an approach not only reduces cross-submodel de-
pendencies (and hence conservatism in the shield) but also provides a data-driven, automated method
for selecting a “good” decomposition that scales with the topology of the environment. We consider
the design and analysis of such structured decomposition strategies a valuable direction for future
work.

# 7 CONCLUSION

Shield synthesis is an effective method for ensuring safety requirements in systems that operate within an intrinsic uncertainty. However, shielding needs to scale more efficiently with the size of the problem formulation. Exploiting compositionality in the POMDP problem formulation parallelizes shield synthesis, making it more efficient without sacrificing effectiveness. In particular, compositional shield synthesis relies on connecting state and action spaces between submodel formations via information sharing. We demonstrate this increase in efficiency and preservation of shield properties using compositional synthesis with state-of-the-art deep RL algorithms in sparse-reward and partially observable environments.

# ACKNOWLEDGMENTS

S. Carr and U. Topcu are partially supported by the US DoD Air Force Office of Scientific Research under award number AFOSR FA9550-22-1-0403 and the National Science Foundation (NSF) under award number NSF 2409535.

G. Bakirtzis is partially supported by the academic and research chair *Architecture des Systèmes Complexes* through the following partners: Dassault Aviation, Naval Group, Dassault Systèmes, KNDS France, Agence de l'Innovation de Défense, and Institut Polytechnique de Paris.

The authors would like to thank Sebastian Junges and Nils Jansen for input at the early stages of
this research.

# References

[1] E. Even-Dar, S. M. Kakade, and Y. Mansour, “Reinforcement learning in POMDPs without resets,” in *IJCAI*, 2005. [Online]. Available: http://ijcai.org/Proceedings/05/Papers/0685.pdf

[2] S. Carr, N. Jansen, S. Junges, and U. Topcu, “Safe reinforcement learning via shielding under partial observability,” in *AAAI*, 2023.

[3] M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu, “Safe reinforcement learning via shielding,” in *AAAI*, 2018.

[4] S. Chatterjee and A. S. Hadi, *Sensitivity analysis in linear regression*. John Wiley & Sons, 2009.

[5] S. Junges, N. Jansen, and S. A. Seshia, “Enforcing almost-sure reachability in POMDPs,” in *CAV*, 2021.

[6] K. Chatterjee, M. Chmelík, R. Gupta, and A. Kanodia, “Qualitative analysis of pomdps with temporal logic specifications for robotics applications,” in *ICRA*. IEEE, 2015, pp. 325–330.

[7] D. Melcer, C. Amato, and S. Tripakis, “Shield decentralization for safe reinforcement learning in general partially observable multi-agent environments,” in *AAMAS*, 2024.

[8] C. Neary, A. S. Samyal, C. Verginis, M. Cubuktepe, and U. Topcu, “Verifiable reinforcement learning systems via compositionality,” *arXiv preprint arXiv:2309.06420*, 2023.
[9] C. Simpkins and C. Isbell, "Composable modular reinforcement learning," in *Proceedings of the AAAI conference on artificial intelligence*, vol. 33, no. 01, 2019, pp. 4975-4982.

[10] U. Rosolia, A. Singletary, and A. D. Ames, "Unified multi-rate control: from low level actuation to high level planning," *CoRR*, vol. abs/2012.06558, 2020.

[11] J. Peters and S. Schaal, "Policy gradient methods for robotics," in *IROS*. IEEE, 2006.

[12] J. García and F. Fernández, "A comprehensive survey on safe reinforcement learning," *J. Mach. Learn. Res.*, 2015.

[13] A. Laud and G. DeJong, "The influence of reward on the speed of reinforcement learning: An analysis of shaping," in *ICML*, 2003.

[14] T. M. Moldovan and P. Abbeel, "Safe exploration in Markov decision processes," in *ICML*, 2012. [Online]. Available: http://icml.cc/2012/papers/838.pdf

[15] N. Fulton and A. Platzer, "Safe reinforcement learning via formal methods: Toward safe control through proof and learning," in *AAAI*, 2018.

[16] M. Bouton, J. Karlsson, A. Nakhaei, K. Fujimura, M. J. Kochenderfer, and J. Tumova, "Reinforcement learning with probabilistic guarantees for autonomous driving," in *Workshop on Safety Risk and Uncertainty in Reinforcement Learning*, 2018.

[17] L. P. Kaelbling, M. L. Littman, and A. R. Cassandra, "Planning and acting in partially observable stochastic domains," *Artificial Intelligence*, 1998.

[18] M. J. Hausknecht and P. Stone, "Deep recurrent Q-learning for partially observable MDPs," in *AAAI Fall Symposia*, 2015.

[19] V. Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wierstra, and M. A. Riedmiller, "Playing Atari with deep reinforcement learning," arXiv:1312.5602 [cs.LG], 2013.

[20] A. H. Brorholt, K. G. Larsen, and C. Schilling, "Compositional shielding and reinforcement learning for multi-agent systems," arXiv:2410.10460 [cs.LO], 2024.

[21] C. Baier and J. Katoen, *Principles of model checking*. MIT Press, 2008.

[22] S. Thrun, W. Burgard, and D. Fox, *Probabilistic Robotics*. The MIT Press, 2005.

[23] T. Smith and R. Simmons, "Heuristic search value iteration for POMDPs," in *UAI*, 2004.

[24] A. Kolobov, Mausam, and D. S. Weld, "A theory of goal-oriented MDPs with dead ends," in *UAI*, 2012.

[25] J. Raskin, K. Chatterjee, L. Doyen, and T. A. Henzinger, "Algorithms for omega-regular games with imperfect information," *Log. Methods Comput. Sci.*, 2007.

[26] C. H. Papadimitriou and J. N. Tsitsiklis, "The complexity of Markov decision processes," *Math. Oper. Res.*, 1987.

[27] J. Pineau, G. J. Gordon, and S. Thrun, "Point-based value iteration: An anytime algorithm for POMDPs," in *IJCAI*, 2003. [Online]. Available: http://ijcai.org/Proceedings/03/Papers/147.pdf

[28] S. Ross, J. Pineau, S. Paquet, and B. Chaib-draa, "Online planning algorithms for POMDPs," *J. Artif. Intell. Res.*, 2008.

[29] M. L. Puterman, *Markov Decision Processes*. John Wiley and Sons, 1994.

[30] K. Dräger, V. Forejt, M. Z. Kwiatkowska, D. Parker, and M. Ujma, "Permissive controller synthesis for probabilistic systems," *Log. Methods Comput. Sci.*, 2015.
[31] S. Junges, N. Jansen, C. Dehnert, U. Topcu, and J. Katoen, “Safety-constrained reinforcement learning for MDPs,” in *TACAS*, 2016.

[32] C. Baier, H. Hermanns, and J.-P. Katoen, “The 10,000 facets of MDP model checking,” *Computing and Software Science*, 2019.

[33] R. S. Sutton and A. G. Barto, *Reinforcement Learning: An Introduction*. MIT Press, 1998.

[34] C. Neary, C. Verginis, M. Cubuktepe, and U. Topcu, “Verifiable and compositional reinforcement learning systems,” in *ICAPS*, 2022. [Online]. Available: https://ojs.aaai.org/index.php/ICAPS/article/view/19849

[35] V. Mnih, K. Kavukcuoglu, D. Silver, A. A. Rusu, J. Veness, M. G. Bellemare, A. Graves, M. A. Riedmiller, A. Fidjeland, G. Ostrovski, S. Petersen, C. Beattie, A. Sadik, I. Antonoglou, H. King, D. Kumaran, D. Wierstra, S. Legg, and D. Hassabis, “Human-level control through deep reinforcement learning,” *Nature*, 2015.

[36] H. van Hasselt, A. Guez, and D. Silver, “Deep reinforcement learning with double Q-learning,” in *AAAI*, 2016.

[37] J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov, “Proximal policy optimization algorithms,” arXiv:1707.06347 [cs.LG], 2017.

[38] P. Christodoulou, “Soft actor-critic for discrete action settings,” arXiv:1910.07207 [cs.LG], 2019.

[39] R. J. Williams, “Simple statistical gradient-following algorithms for connectionist reinforcement learning,” *Mach. Learn.*, 1992.

[40] C. Hensel, S. Junges, J. Katoen, T. Quatmann, and M. Volk, “The probabilistic model checker Storm,” *Int. J. Softw. Tools Technol. Transf.*, 2022.

[41] S. Guadarrama, A. Korattikara, O. Ramirez, P. Castro, E. Holly, S. Fishman, K. Wang, E. Go-nina, N. Wu, E. Kokiopoulou, L. Sbaiz, J. Smith, G. Bartók, J. Berent, C. Harris, V. Van-houcke, and E. Brevdo, “TF-Agents: A library for reinforcement learning in tensorflow,” https://github.com/tensorflow/agents, 2018.

[42] K. Azizzadenesheli, A. Lazaric, and A. Anandkumar, “Reinforcement learning of pomdps using spectral methods,” in *Conference on Learning Theory*. PMLR, 2016, pp. 193–256.