[1,4]Bettina Könighofer

1]Institute of Applied Information Processing and Communications, Graz
University of Technology, Graz, Austria 2]Institute of Software Technology,
Graz University of Technology, Graz, Austria 3]TU Graz-SAL DES Lab, Silicon
Austria Labs, Graz, Austria 4]Lamarr Security Research, Graz, Austria

# Online Shielding for Reinforcement Learning

<EMAIL_ADDRESS>Julian Rudolf
<EMAIL_ADDRESS>Alexander Palmisano
<EMAIL_ADDRESS>Martin Tappler
<EMAIL_ADDRESS>Roderick Bloem<EMAIL_ADDRESS>[
[  [  [

###### Abstract

Besides the recent impressive results on reinforcement learning (RL), safety
is still one of the major research challenges in RL. RL is a machine-learning
approach to determine near-optimal policies in Markov decision processes
(MDPs). In this paper, we consider the setting where the safety-relevant
fragment of the MDP together with a temporal logic safety specification is
given and many safety violations can be avoided by planning ahead a short time
into the future. We propose an approach for online safety shielding of RL
agents. During runtime, the shield analyses the safety of each available
action. For any action, the shield computes the maximal probability to not
violate the safety specification within the next $k$ steps when executing this
action. Based on this probability and a given threshold, the shield decides
whether to block an action from the agent.  Existing offline shielding
approaches compute exhaustively the safety of all state-action combinations
ahead of time, resulting in huge computation times and large memory
consumption.The intuition behind online shielding is to compute at runtime the
set of all states that could be reached in the near future. For each of these
states, the safety of all available actions is analysed and used for shielding
as soon as one of the considered states is reached. Our approach is well
suited for high-level planning problems where the time between decisions can
be used for safety computations and it is sustainable for the agent to wait
until these computations are finished. For our evaluation, we selected a
2-player version of the classical computer game Snake. The game represents a
high-level planning problem that requires fast decisions and the multiplayer
setting induces a large state space, which is computationally expensive to
analyse exhaustively.

###### keywords:

Shielding, Runtime Enforcement, Markov Decision Processes, Safe Reinforcement
Learning

##  1 Introduction

Reinforcement Learning (RL) has proven successful in solving complex tasks
that are difficult to solve using classic controller design, including
applications in computer games Silver et al (2016), multi-agent planning Zhang
and Bastani (2019), and robotics Wang et al (2019). RL learns high-performance
controllers by optimising objectives expressed via rewards in unknown,
stochastic environments. Although learning-enabled controllers (LECs) have the
potential to outperform classical controllers, safety concerns prevent LECs
from being widely used in real-world tasks Amodei et al (2016).

_Shielding_ Bloem et al (2015) is a runtime enforcement technique to ensure
safe decision making. By augmenting an RL agent with a _shield_ , at every
time step, unsafe actions are blocked by the shield and the learning agent can
only pick a safe action to be sent to the environment. Shields are
automatically constructed via correct-by-construction formal synthesis methods
from a model of the safety-relevant environment dynamics and a safety
specification. In the deterministic setting, shields ensure that unsafe states
specified by the safety specification are _never_ visited. Consequently, in
the absence of uncertainties, an agent augmented with a shield is guaranteed
to satisfy the safety objective as long as the shield is used.

In scenarios that incorporate uncertainties, probabilistic shields have been
used to reduce safety violations during training and execution Jansen et al
(2020). The premise of this work is that often in real-world applications,
many safety violations can be avoided by analysing the consequences of actions
in _the near future_. To compute probabilistic shields, the safety-relevant
dynamics of the environment are modelled as a Markov Decision Process (MDP)
and the specification $\varphi$ is expressed in a safety fragment of linear
temporal logic Baier and Katoen (2008). Such a specification could, for
example, forbid to reach a set of critical states in the MDP.

For each state and action, exact probabilities are computed on how likely it
is that executing the action results in violating $\varphi$ from the current
state within the next $k$ steps. At a state $s$, an actions $a$ is called
_unsafe_ if executing $a$ incurs a probability of violating $\varphi$ within
the next $k$ steps greater than a threshold $\delta$ with respect to the
optimal safety probability possible in $s$. During runtime, the probabilistic
shield then blocks any unsafe action from the agent. A probabilistic shield
can be used to shield the decisions of an agent in the training as well as in
the execution phase. In this paper, we build on the approach of Jansen et al
(2020). Hence, from here on, we simply refer to probabilistic shields as
shields.

_The problem with offline shielding._ The computation of an offline shield for
discrete-event systems requires an exhaustive, ahead-of-time safety analysis
for all possible state-action combinations. Therefore, the complexity of
offline shield synthesis grows exponentially in the state and action
dimensions, which limits the application of offline shielding to small
environments. Previous work that applied shields in complex, high-dimensional
environments relied on over-approximations of the reachable states and domain-
oriented abstractions Alshiekh et al (2018); Avni et al (2019). However, this
may result in imprecise safety computations of the shield. This way, the
shield may become over-restrictive, hindering the learning agent in properly
exploring the environment and finding its optimal policy Jansen et al (2020).

_Our solution – online shielding._ Our approach is based on the idea of
computing the safety of actions on-the-fly during run time. In many
applications, the learning agent does not have to take a decision at every
time step. Instead, the learning agent only has to make a decision when
reaching a _decision state_. As an example consider a service robot traversing
a corridor. The agent has time until the service robot reaches the end of the
corridor, i.e., the next decision state, to decide where the service robot
should go next. Online shielding uses the time between two decision states to
compute the safety of all possible actions in the next decision state. When
reaching the next decision state, this information is used to block unsafe
actions of the agent. While the online safety analysis incurs a runtime
overhead, every single computation of the safety of an action is efficient and
parallelisable. Thus, in many settings, expensive offline pre-computation and
huge shielding databases with costly lookups are not necessary. Since the
safety analysis is performed only for decision states that are actually
reached, online shielding is applicable to large, changing, or unknown
environments.

We address the problem of shielding a controllable RL agent in an environment
shared with other autonomous agents that perform tasks concurrently. For
example, some combinations of agent positions may be unsafe, as they
correspond to collisions. The specification then forbids visiting such states,
i.e., $\varphi=\mathbf{G}(\lnot\mathcal{S}_{collision})$.

In online shielding, the computation of the safety for any action in the next
decision state starts as soon as the controllable agent leaves the current
decision state. The tricky part of online shielding in the multi-agent setting
is that during the time the RL agent has between two consecutive decisions,
the other agents also change their positions. Therefore, online shielding
requires to compute the safety of actions with respect to all possible
movements of the other agents. As soon as the next decision state is reached,
the results from the safety analysis are used to block unsafe actions.

Technically, we use MDPs to formalise the dynamics of the agents operating
within the environment. At runtime, we create a sub-MDP for each action. These
sub-MDPs model the immediate future from the viewpoint of the RL agent. Via
model checking, we determine for the next $k$ steps the minimal probability of
violating $\varphi$. An action unsafe and therefore blocked by the shield, if
the action violates safety with a probability higher than a threshold
$\delta$. We generally set $\delta$ relative to the minimal probability of
violating $\varphi$ within the next $k$ steps. In some state, any available
action may impose a large risk of violating $\varphi$, while in other states
there may exists actions that guarantee to stay safe within the next $k$
steps. Using a relative threshold allows an _adaptive_ notion of shielding and
ensures deadlock freedom by always allowing at least one action.

_Requirements and Limitations._ The online shielding approach relies upon some
requirements and is affected by a few limitations that we want to briefly
summarise. The first limitation addresses the fact that the proposed approach
does not provide any worst-case computation times. Therefore the possibility
that the agent reaches the next decision state before the shield made its
decision on which action to block cannot be ruled out. Online shielding is
therefore only applicable in settings that allow an alternative course of
action such as ”waiting” if the safety analysis is not completed. In general,
we recommend to use online shielding in settings where the average time
between visiting decision states is larger than the average time used for the
safety analysis.

As a second limitation we list the possible state-space explosion of the
individual sub-MDPs. The size of the sub-MDPs depends among others on the used
finite horizon $k$, the number of agents operating within the environment and
the number of decision states within the next $k$ steps. In extreme cases
where every state is a decision state, online shielding would likely not be
applicable, because (1) there would be almost no time between the individual
decisions and (2) the state space of the constructed sub-MDPs would explode.

Third, the safety of actions is only analysed within a finite horizon $k$.
Therefore, the agent might end up in situations where any available action
induces a high probability of violating the specification. It is therefore
important to pick a finite horizon $k$ large enough to prevent such
situations. The minimal size of $k$ needed to prevent many safety violations
depends on the concrete setting and there is a natural trade-off between the
computational overhead for the safety-analysis and the number of safety
violations that can be prevented by the shield. As a reference value, we
recommend to use a finite horizon $k$ larger than the number of steps between
any two adjacent decision states.

_Contributions._ This paper is an extended version of Könighofer et al (2021),
in which we gave the formalisation of online shielding in probabilistic
environments and presented experimental results of shielding a simple tabular
Q-learning agent for a 2-player version of the classical computer game Snake
111http://www.onlineshielding.at, 20201127-1. The evaluation demonstrated that
shields can be efficiently computed at runtime, guarantee safety, and have the
potential to positively influence learning performance.

The novelty of this work with respect to Könighofer et al (2021) is an
extensive case study that focuses on the question: Can we use online shielding
to _safely learn a safe policy?_

An unshielded agent learns about the safety of actions by exploring actions
and receiving negative rewards if an action is unsafe. In case of standard
shielded learning, all unsafe actions are blocked from the agent and the agent
never gets the chance to learn the safety constraints from the negative
rewards. Since an unsafe action may look like a safe alternative to the RL
agent due to the absence of negative rewards, unsafe actions might very likely
be part of the final policy. To learn a safe policy under shielding, we
propose to apply _informed shields_. These shields update the value function
of the agent with negative rewards for any action that is blocked by the
shield, using different thresholds for the comparison of the safety values. By
investigating unshielded learning and learning with informed and uninformed
shields in our case study, we empirically assess how shields affect
convergence to an optimal and safe policy. Since learning a safe policy is
only possible if the reward structure captures all relevant safety constraints
Hunt et al (2021), uninformed shields that merely block actions may hinder
learning a safe policies.

We performed the case study on a Deep Q-learning agent for 2-Player Snake to
study the safety of the final policies in various settings. We compared the
final policies of unshielded agents and agents augmented with informed and
uninformed shields. The results show that shielding leads to a better
performance during learning in all cases. However, in most experiments, the
final policies obtained by shielded learning produce more unsafe behaviour
than the policies learned by unshielded agents. This happens with both
uninformed and informed shields that provide negative rewards for blocked
actions. These results suggest that in shielded learning, the shield is also
needed in the execution phase.

_Outline._ The rest of the paper is structured as follows. Section 1.1
discusses related work. We discuss the relevant foundations in Section 2. In
Section 3, we present the setting and formulate the problem that we address.
We present online shielding in Section 4, by defining semantics for autonomous
agents in the considered setting and defining online shield computations based
on these semantics. In Section 5, we report on the evaluation of online
shielding for the classic computer game Snake. Section 6 concludes the paper
with a summary and an outlook on future work.

###  1.1 Related Work

In reinforcement learning (RL) Sutton and Barto (1998), an agent aims to
compute an optimal policy that maximizes the expected total amount of reward
through trial-and-error via interactions with an unknown environment. While
exploring unknown state-action pairs, RL agents that are agnostic to safety
may undeliberately execute unsafe actions. Safe RL algorithms aim to guarantee
safety even during exploration, at least with high probability.

Previous approaches to safe RL include teacher advice Garcıa and Fernández
(2015), reward-shaping Hasanbeig et al (2020, 2019); Hahn et al (2019), and
policy optimisation using constraints Hunt et al (2021); Giacobbe et al
(2021).

Several recent works Hasanbeig et al (2019); Hahn et al (2019) considered
logically-constrained RL, which employs temporal logic as formal reward
shaping technique. The final policy of an agent trained with such a reward
structure maximises the probability of satisfying the specified formula. In
the context of safe RL, the formula can express a safety property and the
trained agent will minimise the risk of violating the property. In order to
ensure safety during training, logically-constrained RL has to be extended by
restricting the exploration during training Hasanbeig et al (2020).

We follow a model-based approach for safe RL. In the continuous domain, model-
based approaches have utilised Lyapunov-based methods Chow et al (2018) and
control-barrier functions Cheng et al (2019); Ohnishi et al (2019) to enable
safe learning under continuous system dynamics. Li et al. Li and Bastani
(2020) proposed model predictive shielding (MPS) for continuous systems. Given
an optimal policy and a safe policy, MPS checks online before executing the
next action of the optimal policy whether the new state would allow reaching
an invariant safe state within the next $k$ steps when executing the safe
policy. If not, MPS does not execute the action of the optimal policy and
switches to the safe policy instead. In the control community, this
architecture is also known as the simplex architecture and gave rise to
several recent applications in RL Ionescu (2021). In this architecture, a
switching logic switches from an advanced controller (the RL agent) to a
verified base controller as soon as a state would be visited that is outside
of the region where the base controller is guaranteed to satisfy an invariant
safety property. In the general shielding setting, shielding supports safety
specifications beyond invariant properties, including, for example, bounded
liveness properties. Furthermore, compared to MPS and the simplex
architecture, shielding interferes less with the agent. Instead of overwriting
an unsafe action chosen by the agent with a particular safe one, a shield lets
the agent choose any action as long as it is safe.

Fulton et al. Fulton and Platzer (2018) published the first work on verifiable
safe learning for hybrid systems. In this work, a theorem prover is used to
prove the correctness of a model with respect to a safety specification given
in differential dynamic logic. This work was extended in Fulton and Platzer
(2019) to the setting in which a single accurate model is not known at design
time. The authors propose an approach in which multiple environmental models
that are provably correct are constructed at design time. During runtime,
based on the collected data, the approach selects between the available
models. A major drawback of the approaches from Fulton and Platzer (2018,
2019) is that they only learn control policies over handcrafted symbolic state
spaces. This limitation was addressed in Hunt et al (2021). Prior to RL, an
agent is trained to detect positions of safety-critical objects from visual
data. During RL, this information is then used to enforce formal safety
constraints that take noise from the object detection systems into account.

In the discrete domain, the shielding approach is commonly used in safe RL
Alshiekh et al (2018); Könighofer et al (2020). In the deterministic setting,
shields are usually constructed offline by computing a maximally permissive
policy containing all actions that will not violate the safety specification
on the infinite horizon. Jansen et al. Jansen et al (2020) introduced offline
shielding in probabilistic environments, considering safety within a finite
horizon. Giacobbe et al. Giacobbe et al (2021) used a very similar approach to
shield safety properties in Atari games. Our work directly extends the
approach to shielding by Jansen et al. Jansen et al (2020) to the online
setting. Several resent extensions of shielding in probabilistic environments
exist, like shielding under partial observability Carr et al (2022), shielding
quantitative properties Pranger et al (2021b), or shielding multi-agent
systems Elsayed-Aly et al (2021). In 2021, the shield synthesis tool TEMPEST
was published, which is able to synthesise several different notions of
shields proposed in literature for probabilistic environments Pranger et al
(2021a).

_Novelty of our work._ All model-based safe RL approaches discussed in this
section rely on building the model (or several models) at design time and
exhaustively analysing the safety of actions within the model at design time.
Our approach builds the environmental models for a finite horizon at runtime
and performs the safety verification online. This allows our approach to be
applied on large, at design time unknown, and changing environments.

To make the safety verification at runtime possible, we are the first to
compute the safety of actions before a decision state is visited, by
considering all possible movements of adversarial agents in the computations.
By analysing the actions before a decision state is reached, we prevent delays
at runtime.

##  2 Preliminaries

_Sequence and Tuple Notation._ We denote sequences of elements by
$t=e_{0}\cdots e_{n}$ with $\epsilon$ denoting the empty sequence. The length
of $t$ is denoted as $|t|=n+1$. We use $t[i]=e_{i}$ for $0$-based indexed
access on tuples and sequences. The notation $t[i\leftarrow e_{i}^{\prime}]$
represents overwriting of the $i$th element of $t$ by $e_{i}^{\prime}$, that
is, $t[j]=t[i\leftarrow e_{i}^{\prime}][j]$ for all $j\neq i$ and
$t[i\leftarrow e_{i}^{\prime}][i]=e_{i}^{\prime}$.

A _probability distribution_ over a countable set $X$ is a function $\mu\colon
X\rightarrow[0,1]$ with $\sum_{x\in X}\mu(x)=1$. $\mathit{Distr}(X)$ denotes
all distributions on $X$. The support of $\mu\in\mathit{Distr}(X)$ is
$\mathit{supp}(\mu)=\\{x\in X\mid\mu(x){>}0\\}$.

A _Markov decision process_ (MDP)
$\mathcal{M}{}=(\mathcal{S}{},s_{0},\mathcal{A}{},\mathcal{P}{})$ is a tuple
with a finite set $\mathcal{S}$ of states, a unique initial state
$s_{0}\in\mathcal{S}$, a finite set $\mathcal{A}=\\{a_{1}\dots,a_{n}\\}$ of
actions, and a (partial) _probabilistic transition function_
$\mathcal{P}:\mathcal{S}\times\mathcal{A}\rightarrow Distr(\mathcal{S})$,
where $\mathcal{P}(s,a)=\bot$ denotes undefined behaviour. For all
$s\in\mathcal{S}$ the available actions are
$\mathcal{A}(s)=\\{a\in\mathcal{A}|\mathcal{P}(s,a)\neq\bot\\}$ and we assume
$|\mathcal{A}(s)|\geq 1$. A _path_ in an MDP $\mathcal{M}$ is a finite (or
infinite) sequence $\rho=s_{0}a_{0}s_{1}a_{1}\ldots$ with
$\mathcal{P}(s_{i},a_{i})(s_{i+1})>0$ for all $i\geq 0$ unless otherwise
noted.

Non-deterministic choices in an MDP are resolved by a so-called _policy_. For
the properties considered in this paper, memoryless deterministic policies are
sufficient Baier and Katoen (2008). These are functions
$\pi:\mathcal{S}\rightarrow\mathcal{A}$ with $\pi(s)\in\mathcal{A}(s)$. We
denote the set of all memoryless deterministic policies of an MDP by $\Pi$.
Applying a policy $\pi$ to an MDP yields an induced _Markov chain_
$\mathcal{D}{}=(\mathcal{S}{},s_{\mathit{I}}{},P{})$ with
$P:\mathcal{S}\rightarrow\mathit{Distr}(\mathcal{S})$ where all nondeterminism
is resolved. A _reward function_
${r}\colon\mathcal{S}\times\mathcal{A}\rightarrow\mathbb{R}$ for an MDP adds a
reward to every state $s$ and action $a$.

In formal methods, safety properties are often specified as _linear temporal
logic_ (LTL) formulas Pnueli (1977). For an MDP $\mathcal{M}$, probabilistic
model checking Katoen (2016); Kwiatkowska (2003) employs value iteration or
linear programming to compute the probabilities of _all states and actions of
the MDP_ to satisfy a safety property $\varphi$.

Specifically, we compute
$\eta^{\max}_{\varphi,\mathcal{M}}\colon\mathcal{S}\rightarrow[0,1]$ or
$\eta^{\min}_{\varphi,\mathcal{M}}\colon\mathcal{S}\rightarrow[0,1]$, which
yields for all states the maximal (or minimal) probability over all possible
policies to satisfy $\varphi$. For instance, for $\varphi$ encoding to reach a
set of states $T$, $\eta^{\max}_{\varphi,\mathcal{M}}(s)$ is the maximal
probability to “eventually” reach a state in $T$ from state $s\in\mathcal{S}$.

##  3 Setting and Problem Statement

##### Setting

We consider a setting similar to Jansen et al (2020), where one controllable
agent, called the _avatar_ , and multiple uncontrollable agents, called
_adversaries_ operate within an _arena_. The arena is a compact, high-level
description of the underlying model and captures the dynamics of the agents.
Any information on rewards is neglected within the arena since it is not
needed for safety computations.

From this arena, potential agent locations may be inferred. Within the arena,
the agents perform _tasks_ that are sequences of _activities_ performed
consecutively.

Formally, an _arena_ is a pair $G=(V,E)$, where $V$ is a set of nodes and $E$
is a finite set of $E\subseteq V\times V$. An agent’s _location_ is defined
via the current node $v\in V$. An edge $(v,v^{\prime})\in E$ represents an
_activity_ of an agent. By executing an activity, the agent moves to its next
location $v^{\prime}$. A _task_ is defined as a non-empty sequence
$(v_{1},v_{2})\cdot(v_{2},v_{3})\cdot(v_{3},v_{4})\cdots(v_{n-1},v_{n})\in
E^{*}$ of connected edges. To ease representation, we denote tasks also as
sequences of locations $v_{1}\cdot v_{2}\cdots v_{n}$.

The set of tasks available in a location $v\in V$ is given by the function
$\textsl{Task}(v)$. The set of all tasks of an arena $G$ is denoted by
$\textsl{Task}(G)$. The avatar is only able to select a next task at a
_decision location_ in $V_{D}\subseteq V$. To avoid deadlocks, we require for
any decision location $v\in V_{D}$ that $\textsl{Task}(v)\neq\emptyset$ and
for all $v\cdots v^{\prime}\in Task(v)$ that $v^{\prime}\in V_{D}$, i.e., any
task ends in another decision location from which the agent is able to decide
on a new task. A safety property may describe that some combinations of agent
positions are unsafe and should not be reached (or any other safety property
from the safety fragment of LTL).

1234512345AE Figure 1: Gridworld with avatar A (top right) and an adversary E
(bottom left).

######  Example 1 (Gridworld).

Figure 1 shows a simple gridworld with corridors represented by white tiles
and walls represented by black tiles. A tile is defined via its $(x,y)$
position. We model this gridworld with an arena $G=(V,E)$ by associating each
white tile with a location in $V$ and creating an edge in $E$ for each pair of
adjacent white tiles. Corners and crossings are decision locations, i.e.,
$V_{d}=\\{(1,1),(1,3),(1,5),(5,1),(5,3),(5,5)\\}$. At each decision location,
tasks define sequences of activities needed to traverse adjoining corridors,
e.g., $Task((1,3))=\\{(1,3)\cdot(2,3)\cdot(3,3)\cdot(4,3)\cdot(5,3)$,
$(1,3)\cdot(1,2)\cdot(1,1)$, $(1,3)\cdot(1,4)\cdot(1,5)\\}$.

##### Problem Statement

Consider an environment described by an arena as above and a safety
specification $\varphi$. We assume stochastic behaviours for the adversaries,
e.g, obtained using RL Sadigh et al (2018, 2016). In fact, this stochastic
behaviour determines all actions of the adversaries via probabilities. The
underlying model is then an MDP: the avatar executes an action, and upon this
execution, the next exact positions (the state of the system) are determined
stochastically. That is, the states correspond to the possible positions of
all agents including the avatar and the actions correspond to the available
tasks.

Our aim is to _shield unsafe actions_ from the avatar during training as well
as during execution. At any state $s$, an actions $a$ is called _unsafe_ if
executing $a$ incurs a probability of violating $\varphi$ within the next $k$
steps greater than a threshold $\delta$ that is defined with respect to the
optimal safety probability possible in $s$.

The safety analysis of actions is performed on-the-fly allowing the avatar to
operate within large arenas.

######  Example 2 (Gridworld).

In Figure 1, the tile labelled A denotes the location of the avatar and the
tile labelled E denotes the position of an adversary. Let $(x_{A},y_{A})$ and
$(x_{E},y_{E})$ be the positions of the avatar and the adversary,
respectively. A safety property in this scenario is
$\varphi=\mathbf{G}(\lnot(x_{A}=x_{E}\land y_{A}=y_{E}))$. The “globally”
operator $\mathbf{G}$ states that unsafe states must not be entered, i.e.,
that collisions are never allowed. The shield blocks unsafe actions that would
increase the probability of violating $\varphi$ within the next $k$ steps by
more than a relative threshold $\delta$. We give more details in Section 4.3
on how to construct a shield for this setting.

##  4 Online Shielding for MDPs

Adversary Behaviour Models Arena Runtime Information Model
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ of Next Decision
Online Shield Avatar (RL-Agent) Safety Analysis Blocking Unsafe Actions
Execution & Observation

Figure 2: Workflow of the shield construction.

In this section, we outline the workflow of online shielding in Figure 2 and
describe it below. Given an arena and behaviour models for adversaries, we
define an MDP $\mathcal{M}$ that captures all safety-relevant information. At
runtime, we use current runtime information to create sub-MDPs
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ of $\mathcal{M}$
that model the immediate future of the agents up to some finite horizon. Given
such a sub-MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and a safety
property $\varphi$, we compute via model checking the probability to violate
$\varphi$ within the finite horizon for each task available. The shield then
blocks tasks involving a too large risk from the avatar. To ensure
effectiveness, we choose the horizon large enough such that it covers the
distance between any pair of adjacent decision locations, i.e., pairs of
locations connected by a task.

###  4.1 Behaviour Models for Adversaries

The adversaries and the avatar operate within a shared environment, which is
represented by an arena $G=(V,E)$, and perform tasks independently. We assume
that we are given a stochastic behaviour model of each adversary that
determines all task choices of the respective adversary via probabilities. The
behaviour of an adversary is formally defined as follows.

######  Definition 1 (Adversary Behaviour).

For an arena $G=(V,E)$, we define the behaviour $B_{i}$ of an adversary $i$ as
a function $B_{i}\colon V_{D}\rightarrow\mathit{Distr}(\textsl{Task}(G))$ from
decision locations to distributions over tasks, with
$\mathit{supp}(B_{i}(v))\subseteq\textsl{Task}(v)$.

Behaviour models of adversaries may be derived using domain knowledge or
generalised from observations using machine learning or automata learning Mao
et al (2016); Tappler et al (2021a, b). A potential approach is to observe
adversaries in smaller arenas and transfer knowledge gained in this way to
larger arenas Jansen et al (2020). Cooperative and truly adverse behaviour of
adversaries may require considering additional aspects in the adversary
behaviour, such as the arena state at a specific point in time. Such
considerations are beyond the scope of this paper, since complex adversary
behaviour generally makes the creation of behaviour models more difficult,
whereas the online shield computations are hardly affected. For example,
history-dependent adversary behaviour would require a different definition of
sub-MDPs $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, but such
behaviour would not affect the size of sub-MDPs. Hence, it would lead to
similar computation times. The MDP size and the computation times generally
depend on the number of decision locations, the horizon, and the number of
adversaries.

###  4.2 Safety-Relevant MDP $\mathcal{M}$

In the following, we describe the safety-relevant MDP $\mathcal{M}$ underlying
the agents operating within an arena. This MDP includes non-deterministic
choices of the avatar and stochastic behaviour of the adversaries. Note that
the safety-relevant MDP $\mathcal{M}$ is never explicitly created for online
shielding, but is explored on-the-fly for the safety analysis of tasks. We
follow the presentation by Jansen et al. Jansen et al (2020) for this purpose.

Let $G=(V,E)$ be an arena, let Task be a task function for $G$, let $B_{i}$
with $i\in\\{1\ldots m\\}$ be the behaviour functions of $m$ adversaries, and
let the avatar be the zeroth agent. The safety-relevant MDP
$\mathcal{M}{}=(\mathcal{S}{},s_{0},\mathcal{A}{},\mathcal{P}{})$ models the
arena and agents’ dynamics as follows. Each agent has a _position_ and a _task
queue_ containing the activities to be performed from the last chosen task.
The agents take turns performing activities from their respective task queue.
If the task queue of an agent is empty, a new task has to be selected. Since
we control the avatar, we model its choice of tasks as non-deterministic
choice from all available tasks. Therefore, we analyse the outcomes of
carrying out all possible tasks. By Definition 1 the adversary behaviour is
probabilistic, i.e., the adversaries choose tasks according to a discrete
probability distribution.

Hence, $\mathcal{M}$ has three types of states: (1) states where the avatar’s
task queue is empty and the avatar makes a _non-deterministic_ decision on its
next task, (2) states where an adversary’s task queue is empty and the
adversary selects its next task _probabilistically_ , and (3) states where the
currently active agent has a non-empty task queue and the agent processes its
task queue _deterministically_.

Formally, the _states_
$\mathcal{S}=V^{m+1}\times(E^{*})^{m+1}\times\\{0,\ldots,m\\}$ are triples
$s=(v,q,t)$ where $v$ encodes the agent positions, $q$ encodes the task queue
states of all agents, and $t$ encodes whose turn it is. To enhance
readability, we use $\textit{pos}(s)=s[0]=v$, $\textit{task}(s)=s[1]=q$, and
$\textit{turn}(s)=s[2]=t$ to access the elements of a state $s$. We
additionally define $\textit{ava}=0$, thus $\textit{pos}(s)[\textit{ava}]$ and
$\textit{task}(s)[\textit{ava}]$ are the position and task of the avatar,
whereas $\textit{turn}(s)=\textit{ava}$ specifies that it is the turn of the
avatar. There is a unique action $\alpha_{\mathrm{adv}}$ representing
adversary decisions, there is a unique action $\alpha_{\mathrm{e}}$
representing individual activities (movement along edges), and there are
actions for each task available to the avatar, thus
$\mathcal{A}=\\{\alpha_{\mathrm{adv}},\alpha_{\mathrm{e}}\\}\cup\textsl{Task}(G)$.

######  Definition 2 (Decision State).

Given a safety-relevant MDP $\mathcal{M}$. We define the set of _decision
states_ $\mathcal{S}_{D}\subseteq\mathcal{S}$ via
$\mathcal{S}_{D}=\\{s_{D}\in\mathcal{S}\mid\textit{task}(s_{D})[\textit{ava}]=\epsilon\land\textit{turn}(s_{D})=\textit{ava}\\}$,
i.e., it is the turn of the avatar and its task queue is empty.

This implies that if $s_{D}\in\mathcal{S}_{D}$, then
$\textit{pos}(s_{D})[\textit{ava}]$ is a decision location in $V_{D}$. A
policy for $\mathcal{M}$ needs to define actions only for states in
$\mathcal{S}_{D}$, thereby defining the decisions for the avatar. All other
task decisions in states $s$, where $\textit{turn}(s)\neq\textit{ava}$, are
performed stochastically by adversaries and cannot be controlled.

At run-time, in each turn each agent performs two steps:

  1. (1)

If its task queue is empty, the agent has to select its next task and adds it
to the task queue.

  2. (2)

The agent performs the next activity of its current task queue.

##### Selecting a New Task

A new task has to be selected in all states $s$ with $\textit{turn}(s)=i$ and
$\textit{task}(s)[i]=\epsilon$, i.e, it is the turn of agent $i$ and agent
$i$’s task queue is empty.

If $i=\textit{ava}$, the avatar is in a decision state $s\in\mathcal{S}_{D}$,
with actions $\mathcal{A}(s)=\textsl{Task}(\textit{pos}(s)[\textit{ava}])$.
For each task $t\in\mathcal{A}(s)$, there is a successor state $s^{\prime}$
with $\textit{task}(s^{\prime})=\textit{task}(s)[\textit{ava}\leftarrow t]$,
$\textit{pos}(s^{\prime})=\textit{pos}(s)$,
$\textit{turn}(s^{\prime})=\textit{turn}(s)$, and
$\mathcal{P}(s,t,s^{\prime})=1$. Thus, there is a transition that updates the
avatar’s task queue with the edges of task $t$ with probability one. Other
than that, there are no changes.

If $i\neq\textit{ava}$, an adversary makes a decision, thus
$\mathcal{A}(s)=\alpha_{\mathrm{adv}}$. For each
$t\in\textsl{Task}(\textit{pos}(s)[i])$, there is a state $s^{\prime}$ with
$\textit{task}(s^{\prime})=\textit{task}(s)[i\leftarrow t]$,
$\textit{pos}(s^{\prime})=\textit{pos}(s)$,
$\textit{turn}(s^{\prime})=\textit{turn}(s)$, and
$\mathcal{P}(s,\alpha_{\mathrm{adv}},s^{\prime})=B_{i}(\textit{pos}(s)[i])(t)$.
There is a single action with a stochastic outcome determined according to the
adversary behaviour $B_{i}$.

##### Performing Activities

After potentially selecting a new task, the task queue of agent $i$ is non-
empty. We are in a state $s^{\prime}$, where
$\textit{task}(s^{\prime})[i]=t=(v_{i},v_{i}^{\prime})\cdot t^{\prime}$ with
$\textit{pos}(s^{\prime})[i]=v_{i}$. Agent $i$ moves along the edge
$(v_{i},v_{i}^{\prime})$ deterministically and we increment the turn counter
modulo $m+1$, i.e., $\mathcal{A}(s^{\prime})=\\{\alpha_{\mathrm{e}}\\}$ and
$\mathcal{P}(s^{\prime},\alpha_{\mathrm{e}},s^{\prime\prime})=1$ with
$s^{\prime\prime}[0]=\textit{pos}(s^{\prime})[i\leftarrow v_{i}^{\prime}]$,
$\textit{task}(s^{\prime\prime})=\textit{task}(s^{\prime})[i\leftarrow
t^{\prime}]$, and
$\textit{turn}(s^{\prime\prime})=\textit{turn}(s^{\prime})+1\mod m+1$.

###  4.3 Sub-MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ for Next Decision

The idea of online shielding is to compute the safety value of actions in the
decision states on the fly and block actions that are too risky. For infinite
horizon properties, the probability to violate safety, in the long run, is
often one and errors stemming from modelling uncertainties may sum up over
time Jansen et al (2020). Therefore, we consider safety relative to a _finite
horizon_ such that the action values (and consequently, a policy for the
avatar) carry guarantees for the next several steps. Explicitly constructing
an MDP $\mathcal{M}$ as outlined above yields a very large number of decision
states that may be infeasible to check. The finite horizon assumption allows
us to prune the safety-relevant MDP and construct small sub-MDPs
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ capturing the
immediate future of individual decision states.

More concretely, we consider runtime situations of being in a state $s_{t}$,
the state visited immediately after the avatar decided to perform a task $t$.
In such situations, we can use the time required to perform $t$ for shield
computations for the next decision. We create a sub-MDP
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ by determining
all states reachable within a finite horizon and use
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ to check the
safety probability of each action (task) available in the next decision and
block unsafe actions.

##### Construction of $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$

Online shielding relies on the insight that after deciding on a task $t$, the
time required to complete $t$ can be used to compute a shield for the next
decision. Thus, we start the construction of the sub-MDP
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ for the next
decision location $v_{D}^{\prime}$ from the state $s_{t}$ that immediately
follows a decision state $s_{D}$, where the avatar has chosen a task
$t\in\mathcal{A}(s_{D})$. The MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ is computed with
respect to a finite horizon $h$ for $v_{D}^{\prime}$.

By construction, the task is of the form $t=v_{D}\cdots v_{D}^{\prime}$, where
$v_{D}$ is the avatar’s current location and $v_{D}^{\prime}$ is the next
decision location. While the avatar performs $t$ to reach $v_{D}^{\prime}$,
the adversaries perform arbitrary tasks and traverse $|t|$ edges, i.e., until
$v_{D}^{\prime}$ is reached only adversaries make decisions. This leads to a
set of possible next decision states. We call these states the _first decision
states_ $S_{\mathrm{FD}}\subseteq\mathcal{S_{D}}$. After reaching
$v_{D}^{\prime}$, both avatar and adversaries decide on arbitrary tasks and
all agents traverse $h$ edges. This behaviour defines the structure of
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$.

Given a safety-relevant MDP
$\mathcal{M}{}=(\mathcal{S}{},s_{0},\mathcal{A}{},\mathcal{P}{})$, a decision
state $s_{D}$ and its successor $s_{t}$ with
$\textit{task}(s_{t})[\textit{ava}]=t$, and a finite horizon $h\in\mathbb{N}$
representing a number of turns taken by all agents following the next
decision. These turns and the (stochastic) agent behaviour leading to the next
decision are modelled by the sub-MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$.
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}=(\mathcal{S}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}},{s_{0}}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}},\mathcal{A}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}},\mathcal{P}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}})$ is formally
constructed as follows. The actions are the same as for $\mathcal{M}$, i.e.,
$\mathcal{A}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}=\mathcal{A}$. The
initial state is given by ${s_{0}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}=(s_{t},0)$. The
states of $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ are a subset of
$\mathcal{M}$’s states augmented with the distance from
${s_{0}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, i.e.,
$\mathcal{S}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\subseteq\mathcal{S}\times\mathbb{N}_{0}$.
The distance is measured in terms of the number of turns taken by all agents.

We define transitions and states inductively by:

  1. (1)

Decision Actions. If $(s,d)\in\mathcal{S}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, $d<|t|+h$, and
there is an $s^{\prime}\in\mathcal{S}$ such that
$\mathcal{P}(s,\alpha,s^{\prime})>0$ and
$\alpha\in\\{\alpha_{\mathrm{adv}}\\}\cup\textsl{Task}(G)$ then
$(s^{\prime},d)\in\mathcal{S}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and
$\mathcal{P}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}((s,d),\alpha,(s^{\prime},d))=\mathcal{P}(s,\alpha,s^{\prime})$.

  2. (2)

Movement Actions. If $(s,d)\in\mathcal{S}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, $d<|t|+h$, and
there is an $s^{\prime}\in\mathcal{S}$ such that
$\mathcal{P}(s,\alpha_{\mathrm{e}},s^{\prime})>0$, then
$(s^{\prime},d^{\prime})\in\mathcal{S}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and
$\mathcal{P}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}((s,d),\alpha_{\mathrm{e}},(s^{\prime},d^{\prime}))=\mathcal{P}(s,\alpha_{\mathrm{e}},s^{\prime})$,
where $d^{\prime}=d+1$ if $\textit{turn}(s)=m$ and $d^{\prime}=d$ otherwise.

Movements of the last of $m+1$ agents increase the distance from the initial
state. Combined with the fact that every movement action increases the agent
index and every decision changes a task queue, we can infer that the structure
of $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ is a directed
acyclic graph. This enables an efficient probabilistic analysis.

By construction, it holds that for every state
$(s,d)\in\mathcal{S}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ with $d<|t|$, $s$
is not a decision state of $\mathcal{M}$. The set of first decision states
$S_{\mathrm{FD}}$ consists of all states $s_{\mathrm{FD}}=(s,|t|)$ such that
$s_{\mathrm{FD}}\in\mathcal{S}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ with
$\textit{task}(s)[\textit{ava}]=\epsilon$ and $\textit{turn}(s)=\textit{ava}$,
i.e., all first decision states reachable from the initial state of
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. We use
$\textsl{Task}(S_{\mathrm{FD}})=\\{t\mid s\in
S_{\mathrm{FD}},t\in\mathcal{A}(s)\\}$ to denote the tasks available in these
states. $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ does not define
actions and transitions from states
$(s,|t|+h)\in\mathcal{S}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, as their
successor states are beyond the considered horizon $h$. We have
$\mathcal{A}((s,d))\neq\emptyset$ for all states at distance $d<|t|+h$ from
the initial state.

###  4.4 Shield Construction

The probability of reaching a set of unsafe states $T\in\mathcal{S}$ from any
state in the safety-relevant MDP should be low. In the finite horizon setting,
we are interested in bounded reachability from decision states
$s_{D}\in\mathcal{S}_{D}$ within the finite horizon $h$. We concretely
evaluate reachability on sub-MDPs $\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and use
$T_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}=\\{(s,d)\in
S_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mid s\in T\\}$ to
denote the unsafe states that may be reached within the horizon covered by
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. The property
$\varphi=\lozenge T_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ encodes the
violation of the safety constraint, i.e., eventually reaching
$T_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ within
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. The shield needs
to limit the probability to _satisfy_ $\varphi$.

Given a sub-MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and a set of
first decision states $S_{\mathrm{FD}}$. For each task $t\in
Task(S_{\mathrm{FD}})$, we evaluate $t$ with respect to the minimal
probability to satisfy $\varphi$ from the initial state
${s_{0}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ when executing
$t$ that is given by
$\eta^{\min}_{\varphi,\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}({s_{0}}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}})$. This is
formalised with the notion of task-valuations below.

######  Definition 3 (Task-valuation).

A _task-valuation_ for a task $t$ in a sub-MDP
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ with initial
state ${s_{0}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and first
decision states $S_{\mathrm{FD}}$ is given by

$\displaystyle\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$
$\displaystyle\colon\textsl{Task}(S_{\mathrm{FD}})\rightarrow[0,1]\text{, }$
$\displaystyle\text{with }\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t)=\eta^{\min}_{\varphi,\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}({s_{0}}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}})\text{,}$
$\displaystyle\text{and }\mathcal{A}(s_{\mathrm{FD}})=\\{t\\}\text{ for each
}s_{\mathrm{FD}}\in S_{\mathrm{FD}}\text{.}$

The _optimal task-value_ for $\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ is
$\textsl{optval}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}=\min_{t^{\prime}\in\textsl{Task}(S_{\mathrm{FD}})}\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t^{\prime})$.

A task-valuation is the minimal probability to reach an unsafe state in $T$
from each immediately reachable decision state $s_{\mathrm{FD}}\in
S_{\mathrm{FD}}$ weighted by the probability to reach $s_{\mathrm{FD}}$. When
the avatar chooses an optimal task $t$ (with
$\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t)=\textsl{optval}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$) as next task in
a state $s_{\mathrm{FD}}$,
$\textsl{optval}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$ can be achieved
if all subsequent decisions are optimal as well.

We now define a shield for the decision states $S_{\mathrm{FD}}$ in a sub-MDP
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ using the task-
valuations. Specifically, a _shield_ for a threshold $\delta\in[0,1]$
determines a set of tasks available in $S_{\mathrm{FD}}$ that are
$\delta$-optimal for the specification $\varphi$. All other tasks are
“shielded” or “blocked”.

######  Definition 4 (Shield).

For task-valuation $\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$ and a threshold
$\delta\in[0,1]$, a _shield for $S_{\mathrm{FD}}$ in
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$_ is given by

$\displaystyle\textsl{shield\,}_{\delta}^{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$
$\displaystyle\in 2^{\textsl{Task}(S_{\mathrm{FD}})}\text{ with }$
$\displaystyle\textsl{shield\,}_{\delta}^{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$
$\displaystyle=\\{t\in\textsl{Task}(S_{\mathrm{FD}})\mid$
$\displaystyle\qquad\delta\cdot\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t)\leq\textsl{optval}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Intuitively, $\delta$ enforces a constraint on tasks that are acceptable
w.r.t. the optimal probability. The shield is _adaptive_ with respect to
$\delta$, as a high value for $\delta$ yields a stricter shield, a smaller
value a more permissive shield. In particularly critical situations, the
shield can enforce the decision maker to resort to (only) the optimal actions
w.r.t. the safety objective. This can be achieved by temporarily setting
$\delta=1$. Online shielding creates shields on-the-fly by constructing sub-
MDPs $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and computing
task-valuations for all available tasks.

Through online shielding, we transform the safety-relevant MDP $\mathcal{M}$
into a _shielded MDP_ with which the avatar interacts (which is never
explicitly created) that is obtained from the composition of all sub-
MDP$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. Due to the
assumption on the task functions that requires a non-empty set of available
tasks in all decision locations and due to the fact that every decision for
shielding is defined w.r.t. an optimal task, the shielded MDP is deadlock-
free. The deadlock-freedom follows from using a relative threshold ensuring
that the safest action never gets blocked, thus at least one action is always
available. Using task valuations as a basis, our notion of online shielding
guarantees optimality with respect to safety.

By using the minimal probability as task valuation
$\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t)$, we assume
that the avatar performs optimally with respect to safety in upcoming
decisions. This means that to compute task valuations we assume that the agent
always chooses the safest action that is available. Alternative definitions
that are less optimistic would be possible as well. Defining task valuations
as the maximal probability to violate safety would yield stricter guarantees.
The corresponding shield would block each action $a$ if there exists any
future behaviour following $a$ that violates safety with a too large
probability.

Instead of a relative threshold,  we may use a fixed absolute threshold
$\lambda\in[0,1]$ such that only tasks $t$ with
$\textsl{val}_{\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to3.63pt{\vbox to4.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{3.76735pt}\pgfsys@lineto{0.0pt}{1.61458pt}\pgfsys@curveto{0.0pt}{0.72287pt}{0.72287pt}{0.0pt}{1.61458pt}{0.0pt}\pgfsys@curveto{2.50629pt}{0.0pt}{3.22916pt}{0.72287pt}{3.22916pt}{1.61458pt}\pgfsys@lineto{3.22916pt}{3.76735pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}(t)\leq\lambda$
are allowed. Since this may induce deadlocks in case there are no sufficiently
safe actions, we fall back to shielding with $\delta=1$, which defines the
threshold as the valuation of the safest action. That is, if there are no
$\lambda$-safe actions, we use the safest action available. Hence, we either
enforce a limit on unsafe behaviour or use the safest option available, which
avoids deadlocks.

###  4.5 Optimisation – Updating Shields after Adversary Decisions

After the avatar decides on a task, we use the time to complete the task to
compute shields based on task-valuations (see Definition 3 and Definition 4).
Such shield computations are inherently affected by uncertainties stemming
from stochastic adversary behaviour. These uncertainties consequently decrease
whenever we observe a concrete decision from an adversary that we considered
stochastic in the initial shield computation.

An optimisation of the online shielding approach is to compute a new shield
after any decision of an adversary, if there is enough remaining time until
the next decision location. Suppose that after visiting a decision state, we
computed a shield based on $\mathcal{M}_{\text{\raisebox{-1.5pt}{
\leavevmode\hbox to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. While moving to
the next decision state, an adversary decides on a new task and we observe the
concrete state $s$. We can now construct a new sub-MDP
$\mathcal{M}^{\prime}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ using
${s_{0}^{\prime}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}=s$ as initial
state, thereby resolving a stochastic decision between the original initial
state ${s_{0}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and
${s_{0}^{\prime}}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$. Using
$\mathcal{M}^{\prime}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox
to4.92pt{\vbox to5.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$, we compute a new
shield for the next decision location.

The facts that the probabilistic transition function of
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ does not change
during updates and that we consider safety properties enable a very efficient
implementation of updates. For instance, if value iteration is used to compute
task-valuations, we can simply change the initial state and reuse computations
from the initial shield computation. Note that if a task is completely safe,
i.e., tasks with a valuation of zero, the value of this task will not change
under a re-computation, since the task is safe under any sequence of adversary
decisions.

##  5 Implementation and Experiments

We consider several experiments of shielded reinforcement learning for a
2-player version of the classic game Snake. We picked this game because it
requires fast decision making during runtime, and provides an intuitive and
fun setting to show the potential of shielding such that it can potentially be
used for teaching formal methods. Furthermore the game is interesting for
shielding, since the agent has to experience risky situations in order to win
the game. This allows us to evaluate the ability of the shield in protecting
the agent from entering unsafe states, to study the influence of the shield on
the learning performance, and to evaluate the safety of the final learned
policy.

In this section, we start by giving details on the computation of the shield.
In this context, we examine the runtime of shield computations. Afterwards, we
discuss several experiments of shielding learning agents in tabular Q-learning
and deep Q-learning.

The source code can be found at http://onlineshielding.at along with videos,
evaluation data, and a Docker image that enables easy experimentation.

###  5.1 2-Player Snake

Figure 3: A screenshot of the Snake game using Map 1 with colour-coded shield
display.

In the game of 2-player Snake, each player controls a snake of a different
colour. A player wins, if it is either able to eat all randomly positioned
apples of their own colour before the adversary snake collects all apples in
its colour, or if it is able to cut off the other player. In the case that the
heads of both snakes collide, the game ends in a tie.

We provide an open-source implementation of the 2-player Snake game. The game
can be played on 6 different maps, one of which is shown in Figure 3. The game
settings allow varying the lengths of the snakes and their speed, allowing the
user to set different levels of difficulty. For both snakes, shielding can be
activated and deactivated. The game can be played in the following player
modes: (1) double player (two human players compete), (2) player against agent
(human player plays against a trained learning agent), or (3) agent against
agent. The third mode is used for reinforcement learning. One snake is
controlled by the avatar (the RL-agent), and the adversary snake is controlled
by a trained agent.

Implementation. The game’s interface and logic was implemented using the
pygame222https://www.pygame.org/, 20201127-1 library.

###  5.2 Shield Computation

Figure 4: Screenshots from the Snake game using a simple map to demonstrate
recalculation.
$10$$12$$14$$16$$18$$20$$22$$24$$26$$28$$30$$10^{-1}$$10^{0}$$10^{1}$$10^{2}$Horizon
$h$Time [s]$l=10$, mean$l=15$, mean$l=10$, maximum$l=15$, maximum Figure 5:
Shield computation time for varying horizon values and snake lengths.

The task of the shield is to protect its snake from collisions with the
adversary snake and with its own body.

In the safety-relevant MDP $\mathcal{M}$, the avatar snake can make a decision
at every crossing, thus the crossings define the decision locations. The
states in $\mathcal{M}$ store the positions of the bodies of both snakes.
Therefore, we store for each snake the location of the head, the tail, and all
crossings that are covered by the body of the snake. The locations of the
corridors covered by the bodies are then implicitly defined. The safety
specification $\varphi$ defines that the heads of the snake should not collide
and that the head of the avatar snake should not crash into the body of the
adversary snake or its own body.  This results in a safety specification
$\varphi=\mathbf{G}(\neg\texttt{Collision\\_Heads}(\texttt{head\\_s1},\texttt{head\\_s2})$
$\wedge\neg\texttt{Collision\\_Bodies}(\texttt{head\\_s1},\\{\texttt{body\\_s1}\\},$
$\texttt{tail\\_s1},$ $\\{\texttt{body\\_s2}\\}$, $\texttt{tail\\_s2}))$,
where the predicates Collision_Bodies and Collision_Heads compare the
locations of the snakes and check for collisions. Each time the avatar snake
enters a corridor, the shielding approach creates sub-MDPs
$\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ for the next
crossing and possible future positions for the adversary snake. Given such a
sub-MDP $\mathcal{M}_{\text{\raisebox{-1.5pt}{ \leavevmode\hbox to4.92pt{\vbox
to5.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}}{{}}{}
{{}{}}{}{}{{{{}{}{}{}}} {{}{}{}{}}}{} {} {}{} {}{}
{}{}\pgfsys@moveto{0.0pt}{5.2743pt}\pgfsys@lineto{0.0pt}{2.26042pt}\pgfsys@curveto{0.0pt}{1.01202pt}{1.01202pt}{0.0pt}{2.26042pt}{0.0pt}\pgfsys@curveto{3.50882pt}{0.0pt}{4.52084pt}{1.01202pt}{4.52084pt}{2.26042pt}\pgfsys@lineto{4.52083pt}{5.2743pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}$ and the safety
property $\varphi$, we compute the minimal probability to violate $\varphi$
within the next $h$ steps. When the avatar snake arrives at the next crossing,
_the shield allows only the corridors with the highest safety value_. The
game, as shown in Figure 3, indicates the risk of taking a corridor from low
to high by the colours green, yellow, orange, red.

We also implemented the optimisation to recalculate the shield after a
decision of the adversary snake. Figure 4 contains two screenshots of the game
on a simple map to demonstrate the effect of a shield update. In the left