# Shielded Deep Reinforcement Learning for Complex Spacecraft Tasking

Robert Reed, Hanspeter Schaub, and Morteza Lahijanian This work was supported
by Air Force Research Lab (AFRL) under agreement number FA9453-22-2-0050.
Authors are with the Department of Aerospace Engineering Sciences at
University of Colorado Boulder, Boulder, Colorado, USA. {Robert.Reed-1,
Hanspeter.Schaub<EMAIL_ADDRESS>
###### Abstract

Autonomous spacecraft control via Shielded Deep Reinforcement Learning (SDRL)
has become a rapidly growing research area. However, the construction of
shields and the definition of tasking remains informal, resulting in policies
with no guarantees on safety and ambiguous goals for the RL agent. In this
paper, we first explore the use of formal languages, namely Linear Temporal
Logic (LTL), to formalize spacecraft tasks and safety requirements. We then
define a manner in which to construct a reward function from a co-safe LTL
specification _automatically_ for effective training in SDRL framework. We
also investigate methods for constructing a shield from a safe LTL
specification for spacecraft applications and propose three designs that
provide probabilistic guarantees. We show how these shields interact with
different policies and the flexibility of the reward structure through several
experiments.

##  I Introduction

The spacecraft task scheduling problem, which involves collecting data while
adhering to system constraints, traditionally relies heavily on human
intervention. This reliance is due to the inability of current autonomy
modules, often based on simplistic rules and past experiences, to ensure
compliance with spacecraft safety requirements. Due to recent technological
advancements and economical interest [1], spacecraft autonomy has become a
central research topic [2, 3, 4], and recent works show that computational
challenges such as the large dimensionality of the state space and low on-
board computation capabilities can be overcome via Reinforcement Learning (RL)
[3, 2]. Nevertheless, providing correctness and safety guarantees on the
decisions of the autonomy remains a major challenge. This work focuses on this
challenge and aims to enable safe spacecraft autonomy by combining machine
learning with formal methods.

In RL, an agent explores an unknown environment and acts to maximize a reward
function that is designed to express the desired behavior of the agent.
Typically, this reward function is hand designed. Deep RL (DRL) is an
extension of RL that utilizes the power of Neural Networks (NNs) to learn a
policy, enabling RL in high-dimensional spaces. While the optimally and data-
efficiency of DRL algorithms is well understood [5], the policies returned
from these algorithms have no guarantees on safety.

This led research in the direction of Shielded DRL (SDRL) [6, 7] with
adaptation for spacecraft autonomy [2, 3]. In SDRL, a _shield_ is designed in
order to ensure _safety_ of the system when it is deployed with a DRL policy
[7]. The shield acts as a _minimal interference_ filter on the agents action,
allowing all actions that have been pre-determined to be safe and replacing
unsafe actions with correct choices. SDRL had been shown to improve policy
performance and reduce the necessary training time for spacecraft operations
[3, 2]. Typically, shield design relies on having a description of the safety-
critical aspects of the system as a Markov Decision Process (MDP), which is
called a _Safety MDP_. Prior works [3] use a hand-designed safety MDP, where
the transition probabilities between states are chosen from expert intuition.
Such a design not only requires a domain expert with extensive knowledge, but
also limits the guarantees on safety that the shield can provide.

Formal languages, such as _linear temporal logic_ (LTL) [8], provide a manner
to rigorously define the tasks and safety requirements needed for spacecraft
deployment. Typically, the tasks that an agent should complete are composed as
a _liveness specification_ and the behaviors that should be avoided are
written as a _safety specification_. Formal specifications have been used with
great success in robotics applications [9, 10] and the effectiveness of
splitting the specifications into parts (i.e., liveness and safety) has been
well demonstrated [11]. This separation follows the idea of constructing a
shield based on a safety specification and learning a policy that satisfies a
liveness specification. When a task is defined using LTL, formal synthesis
techniques [12, 13] are often used to find a policy that is correct-by-
construction. However, such techniques are often limited by the dimensionality
of the system, hence the need for DRL in the autonomous spacecraft scenario.

This work focuses on incorporating formal methods into the SDRL framework for
the autonomous Earth imaging problem by formalizing the design of a shield for
a spacecraft system and utilizing LTL formulas to define tasking and safety
requirements. We propose to construct a safety MDP algorithmically using
physics-simulator engines and implement three different shield designs with
this MDP. Prior works in formal methods often assume the safety MDP is known a
priori [6], or restrict the RL to a set of safe policies and work to optimize
an unknown objective [14, 15], unlike our scenario. We also identify a manner
to automatically construct a reward function from an LTL specification,
removing human interpretation of a task from the process. This ensures that
DRL is optimizing a reward function that has no ambiguity from the desired
task, resulting in a policy that is optimized for the desired task. Our
evaluations show the effectiveness of the reward and shield designs and the
importance of training with safety specifications.

Our contributions are four-fold: 1) we improve the formalism of shield
construction for spacecraft SDRL, 2) we demonstrate how to incorporate
complex, formal specifications for Earth imaging tasks into a DRL framework,
3) we identify a training setup that minimizes safety violations with few
shield interventions, and 4) we illustrate the efficacy of the method on
several case studies and benchmarks.

##  II Problem Formulation

In this work, we consider autonomous spacecraft scheduling for complex Earth
observation tasks with a discrete action space. The spacecraft must select a
sequence of flight modes such that a predefined Earth observing task is
satisfied while remaining safe.

###  II-A Spacecraft Model

Spacecraft dynamics are highly complex and high dimensional, with potentially
thousands of states needed to accurately represent how each of the subsystems
on a spacecraft interact. The dynamics act over continuous space and time with
stochastic disturbances (e.g. external torques), which enhance the difficulty
of control problems. We assume that we are able to control the switching
between different modes of operation. Hence, the dynamics of the spacecraft
system can be described as a continuous-state Markov decision process (MDP).

######  Definition 1 (MDP).

A _Markov Decision Process_ (MDP) is a tuple $M=(X,x_{0},A,T,\Pi,L)$, where

  * •

$X\subseteq\mathbb{R}^{n}$ is the state space,

  * •

$x_{0}\subset X$ is a set of initial states,

  * •

$A$ is a finite set of modes or actions,

  * •

$T:X\times A\times\mathcal{B}(X)\rightarrow[0,1]$ is a transition probability
function, where $\mathcal{B}$ is a Borel set111The Borel set defines an open
set of states in $X$, hence transition probabilities can be assigned.,

  * •

$\Pi$ is a set of atomic propositions that are related to spacecraft task or
safety, and

  * •

$L:X\rightarrow 2^{\Pi}$ is a labeling function that assigns a state $x\in X$
to a subset of $\Pi$.

######  Example 1.

One can consider a spacecraft with fours modes of operation
$A=\\{a_{i}\\}_{i=0}^{3}$, where $a_{0}$ is _Charging Mode_ , $a_{1}$ is
_Momentum Dumping Mode_ , $a_{2}$ is _Imaging Mode A_ , and $a_{3}$ is
_Imaging Mode B_. The Earth observation tasking can be related to the two
imaging modes. The Momentum Dumping and Charging modes are then important from
the perspective of safety.

Defining the state of the system as $x\in X$, an infinite trajectory is then
written as
$\omega_{\mathbf{x}}=x_{0}\xrightarrow{u_{0}}x_{1}\xrightarrow{u_{1}}...$
where each $u_{i}\in A$. We denote the $i$-th element of $\omega_{\mathbf{x}}$
by $\omega_{\mathbf{x}}[i]$, and the set of all finite and infinite
trajectories are $\Omega_{\mathbf{x}}^{\text{fin}}$ and $\Omega_{\mathbf{x}}$,
respectively. We are interested in controlling the trajectory through the
choice of action taken (switching modes) via a policy.

######  Definition 2 (Policy).

A policy $\pi:\Omega_{\mathbf{x}}^{\text{fin}}\rightarrow A$ is a function
that maps a finite trajectory
$\omega^{N}_{\mathbf{x}}\in\Omega_{\mathbf{x}}^{\text{fin}}$ onto the next
action in $A$. Policy $\pi$ is called stationary if it only depends on the
last element of $\omega_{\mathbf{x}}^{N}$; otherwise, it is called history
dependent.

Under a policy $\pi$, a probability measure over the paths of the MDP $M$ is
well defined [16]. We denote MDP $M$ under $\pi$ as $M^{\pi}$ and its sets of
finite and infinite trajectories as $\Omega_{\mathbf{x}}^{\text{fin},\pi}$ and
$\Omega_{\mathbf{x}}^{\pi}$, respectively.

###  II-B LTL for Earth Observing Tasks and Safety Requirements

We consider imaging tasks that can be completed in finite time and safety
requirements that must not be violated. These tasks and requirements are
related to the temporal behavior of the spacecraft system with respect to a
set of state-space regions $R=\\{r_{1},\ldots,r_{l}\\}$, where $r_{i}\subseteq
X$. To enable formal description of tasks, we associate an atomic proposition
$\mathrm{p}_{i}$ to each region $r_{i}$ such that $\mathrm{p}_{i}$ is true iff
$x\in r_{i}$. Then, the set of atomic proposition is
$\Pi=\\{\mathrm{p}_{1},\ldots,\mathrm{p}_{l}\\}$, and the labeling function
$L:X\to 2^{\Pi}$ assigns each state $x\in X$ to the set of atomic propositions
that are true at that state. Accordingly, we define an observation trace of
trajectory $\omega_{\mathbf{x}}$ to be $\rho=\rho_{0}\rho_{1}\ldots$, where
$\rho_{i}=L(\omega_{\mathbf{x}}[i])$ for all $i\geq 0$.

To formally specify spacecraft requirements, we use co-safe and safe LTL [17],
which are languages that can express the temporal behaviors of a system with a
set of Boolean connectives and temporal operators. Co-safe LTL is used to
describe tasks that the spacecraft should achieve.

######  Definition 3 (Co-safe LTL).

Given a set of atomic propositions $\Pi$, a co-safe LTL formula is recursively
defined as

$\varphi=\mathrm{p}\mid\neg\mathrm{p}\mid\varphi\land\varphi\mid\mathcal{X}\varphi\mid\varphi\mathcal{U}\varphi\mid\mathcal{F}\varphi$

where $\mathrm{p}\in\Pi$, $\neg$ (“not”) and $\land$ (“and”) are Boolean
connectives, and $\mathcal{X}$ (“next”), $\mathcal{U}$ (“until”), and
$\mathcal{F}$ (“eventually”) are temporal operators.

Safe LTL are then used to define behaviors that the spacecraft should avoid.

######  Definition 4 (Safe LTL).

Given a set of atomic propositions $\Pi$, a safe LTL formula is inductively
defined as

$\varphi=\mathrm{p}\mid\neg\mathrm{p}\mid\varphi\land\varphi\mid\mathcal{X}\varphi\mid\mathcal{G}\varphi$

where $\mathrm{p}\in\Pi$, $\neg$, $\land$, and $\mathcal{X}$ are as in
Definition 3 and $\mathcal{G}$ (“globally”) is a temporal operator.

The semantics of safe and co-safe LTL are defined over infinite traces [17].
We say an infinite trajectory $\omega_{\mathbf{x}}\in\Omega_{\mathbf{x}}$
satisfies an LTL formula $\varphi$, denoted as
$\omega_{\mathbf{x}}\models\varphi$, if its trace satisfies $\varphi$. For our
problem, we consider specifications of form

$\varphi=\varphi_{L}\land\varphi_{S},$

where $\varphi_{L}$ is a liveness specification that describes the task that
the spacecraft should achieve given as a co-safe LTL formula, and
$\varphi_{S}$ is a safety specification that identifies what the spacecraft
must avoid as a safe LTL formula. While the satisfaction of co-safe LTL
formula are defined over infinite trajectories, we can assess if a co-safe LTL
formula is satisfied with a finite trajectory. Similarly, we can only assess
satisfaction of a safe LTL formula over infinite trajectories, but the
negation of a safe LTL formula ($\lnot\varphi_{S}$) is a co-safe LTL formula,
whose satisfaction can be assessed on finite trajectories. Then, if a finite
trajectory satisfies $\lnot\varphi_{S}$, it cannot satisfy $\varphi_{S}$,
i.e., the trajectory violates $\varphi_{S}$. Hence, we say a length
$N\in\mathbb{N}$ prefix of $\omega_{\mathbf{x}}$, denoted as
$\omega_{\mathbf{x}}^{N}$, satisfies formula
$\varphi=\varphi_{L}\land\varphi_{S}$, denoted by
$\omega_{\mathbf{x}}^{N}\models\varphi$ iff $\omega_{\mathbf{x}}^{N}$ does not
violate $\varphi_{S}$ and satisfies $\varphi_{L}$, i.e.,

$\omega^{N}_{\mathbf{x}}\models\varphi_{L}\land\varphi_{S}\quad\text{iff}\quad\omega^{N}_{\mathbf{x}}\not\models\neg\varphi_{S}\land\exists
i\leq N,\,\omega^{i}_{\mathbf{x}}\models\varphi_{L}.$

The combination of safe and co-safe LTL enables the description of a wide
variety of tasks.

Recall that the trajectories of $M$ under $\pi$ have an associated probability
measure; hence, satisfaction of $\varphi$ is probabilistic. The probability of
trajectories of $M$ satisfying formula $\varphi$ under $\pi$ is defined as

$P(M^{\pi}\models\varphi)=P(\omega_{\mathbf{x}}\in\Omega_{\mathbf{x}}^{\text{fin},\pi}\mid\omega_{\mathbf{x}}\models\varphi).$

######  Example 2.

Consider the spacecraft in Example 1 with the goal of imaging a target
location on Earth with constraints on how the dynamics affect the image
quality. In natural language, this task may be written as “Image the target
successfully, and only accept images that are taken when the attitude error
($|{\sigma}_{err}|$) is less than 0.008 radians and the attitude rate
($|\dot{\sigma}|$) is less than 0.002 radians per second”. With a signal
$i\in\\{0,1\\}$ that identifies if the target is accessible for imaging, we
then define the region $r_{0}$ as a subset of state space $X$ as
$r_{0}=\\{x\in X\mid 0\leq|{\sigma}_{err}|<0.008,\hskip
2.84526pt0\leq|\dot{\sigma}|<0.002,\hskip
2.84526pta\in\\{a_{2},a_{3}\\},\hskip 2.84526pti=1\\}$. We associate the
atomic proposition $\mathrm{p}_{0}$ with region $r_{0}$ and say
$\mathrm{p}_{0}$ is true iff the state of the spacecraft $x\in r_{0}$;
otherwise $\mathrm{p}_{0}$ is false. Our task can then be written in co-safe
LTL as

$\varphi_{0L}=\mathcal{F}\mathrm{p}_{0},$ (1)

meaning eventually have the state of the spacecraft be in region $r_{0}$. A
finite trajectory of the spacecraft $\omega_{\mathbf{x}}^{N}$ can be
automatically assessed to identify if the specification is satisfied by
checking the observations associated with each state, i.e.
$\rho_{i}=L(\omega_{\mathbf{x}}^{N}(i))$. If $\mathrm{p}_{0}\in\rho_{i}$ for
some $i\leq N$, then the trajectory satisfies the specification, written as
$\omega_{\mathbf{x}}^{N}\models\varphi_{0L}$.

Consider the addition of a safety requirement to the specification as
“Additionally, never allow power to fall below 20% and never allow reaction
wheel speeds above 80% of their maximum.” The safety specification is
concerned with stored charge $\mathcal{P}$ and reaction wheel speeds $\Omega$.
We define regions $r_{1}:\\{x\in X\mid 0\leq\mathcal{P}<0.2\\}$ and
$r_{2}:\\{x\in X\mid 0.8<\Omega\leq 1\\}$ and corresponding atomic
propositions $\mathrm{p}_{1},\mathrm{p}_{2}$, resulting in a safe LTL
specification

$\varphi_{S}=\mathcal{G}(\lnot(\mathrm{p}_{1}\vee\mathrm{p}_{2})).$ (2)

The task would then only be considered satisfied if a finite trajectory
$\omega_{\mathbf{x}}^{N}\models\varphi_{L}\land\varphi_{S}$. More complex
specifications can be defined in a similar manner.

###  II-C Problem Statement

Our problem is then be defined as follows.

######  Problem 1 (Safe Control).

Given a model of the system as an MDP $M$, an Earth observation task specified
as a co-safe LTL formula $\varphi_{L}$, a safety specification as a safe LTL
formula $\varphi_{S}$, and (safety) probability threshold $p$, find a policy
$\pi^{*}$ such that the probability of satisfying
$\varphi_{L}\land\varphi_{S}$ is maximized while the probability of violating
$\varphi_{S}$ is less than or equal to $p$, i.e.,

$\pi^{*}=\operatorname*{\arg\max}_{\pi}P(M^{\pi}\models\varphi_{L}\land\varphi_{S})$

subject to

$P(M^{\pi^{*}}\models\neg\varphi_{S})\leq p.$

Note that there are several challenges in the above problem. Firstly, the
state space for a spacecraft can contain thousands of state parameters,
resulting in a dimensionality that is too large for traditional synthesis
techniques. To overcome the problem of _state explosion_ , we use DRL, with
the policy being captured as a NN which enables generalizability. This is
possible because a high-fidelity, flight-approved spacecraft physics simulator
exists, namely the Basilisk222https://hanspeterschaub.info/basilisk
astrodynamics simulation framework [18], which enables DRL for spacecraft with
its computational performance and flexible framework for integration with
common machine learning techniques [2].

However, using a NN policy that is trained via DRL introduces a new challenge:
how can the satisfaction of the safety constraint during spacecraft operation
be ensured? To address this challenge, we employ shielded DRL (SDRL) in which
a shield is constructed from $\varphi_{S}$ and deployed with the policy to
ensure the correctness of actions taken by the spacecraft. Finally, shield
design itself for a spacecraft is a challenge due to large dimensionality.
This often leads to overly conservative-shields which can interrupt task
execution unnecessarily and too frequently, significantly reducing efficiency.
We propose several methods of shield design and training that mitigate this
problem.

######  Remark 1.

While our approach is general, in this paper, we follow the observation space
setup from [2] which allows the use of DRL for the spacecraft-planning
problem, i.e., the observation space consists of canonical position and
velocity vectors, attitude error, attitude rate, wheel speeds, stored charge,
a sun access indicator, and a target access indicator.

##  III Reward and Shield Design for DRL

In this section, we discuss how to perform DRL with LTL specifications and
describe how we construct shields for the spacecraft system. In Post-Posed
SDRL, as in Figure 1, a shield acts as a monitor on the actions of the
learning agent. The shield allows any action that is safe and corrects actions
that are unsafe before returning the choice to the environment. The shield is
referred to as post-posed due to the ordering of acting after the learning
agent.

Figure 1: Post-Posed Shielded RL architecture.

###  III-A Rewards for DRL with LTL Specifications

The goal of RL is to find an optimal, or nearly-optimal, policy that maximizes
the expected value of a reward function. That is, given an MDP $M$ and a
reward function $R:X\times A\to\mathbb{R}$ find a policy
$\pi^{*}=\operatorname*{\arg\max}_{\pi}\mathbb{E}[\sum R(s,a)]$.
Traditionally, the reward function is manually constructed to define the task
that the agent is learning. The manual construction of a reward function is
prone to error, resulting in a disconnect between what the agent learns and
the desired results. To address this issue, we write the objective in (co-
safe) LTL and automatically construct a reward function from the
specification. Work [19] defines a method to construct a reward function from
an LTL specification, and provides a relation between the probability of
satisfying the specification with the expected value of the reward. To use
this method, a deterministic finite automaton (DFA) must be constructed from
the co-safe LTL specification, i.e., $\varphi_{L}$ or $\neg\varphi_{S}$, that
accepts the same traces as $\varphi$ [17].

######  Definition 5 (DFA).

A deterministic finite automaton (DFA) constructed from an LTL formula
$\varphi$ is a tuple $\mathcal{A}_{\varphi}=(Z,z_{0},2^{\Pi},\delta,Z_{f})$,
where

  * •

$Z$ is a finite set of states,

  * •

$z_{0}\in Z$ is an initial state,

  * •

$2^{\Pi}$ is a finite set of input symbols,

  * •

$\delta:Z\times 2^{\Pi}\rightarrow Z$ is a transition function, and

  * •

$Z_{f}\subseteq Z$ is the set of final (accepting) states.

A finite run on $\mathcal{A}_{\varphi}$ is a sequence of states
$\mathbf{z}=z_{0}z_{1}...z_{n+1}$ induced by a trace
$\rho=\rho_{0}\rho_{1}...\rho_{n}$ where $\rho_{i}\in 2^{\Pi}$ and
$z_{i+1}=\delta(z_{i},\rho_{i})$. A finite run is accepting if, for some
$i\leq n$, $z_{i}\in Z_{f}$. If a run is accepting, its associated trace is
accepted by $\mathcal{A}_{\varphi}$. The set of all traces that are accepted
by $\mathcal{A}_{\varphi}$ is called the language of $\mathcal{A}_{\varphi}$.
The language of $\mathcal{A}_{\varphi}$ is equal to the language of $\varphi$,
i.e., trace $\rho$ is accepted by $\mathcal{A}_{\varphi}$ iff
$\rho\models\varphi$.

To perform DRL given $\mathcal{A}_{\varphi}$ and MDP $M$, the product
$M_{\mathcal{A}_{\varphi}}=M\times\mathcal{A}_{\varphi}$, which captures both
the dynamics of $M$ and the constraints of $\varphi$, is necessary.

######  Definition 6 (Product MDP).

The product MDP $M_{\mathcal{A}_{\varphi}}=M\times\mathcal{A}_{\varphi}$ is a
tuple $M_{\mathcal{A}_{\varphi}}=(S,A,\Delta,S_{f},S_{v})$, where $S=X\times
Z$ is the set of product states, $A$ is as in Def. 1, $\Delta:S\times
A\times(\mathcal{B}(X)\times Z)\rightarrow[0,1]$ is the transition function
such that
$\Delta((x,z),a,(\mathcal{B}(x^{\prime}),z^{\prime})=T(x,a,\mathcal{B}(x^{\prime}))$
if $z^{\prime}=\delta(z,L(x))$ and is 0 otherwise, and $S_{f}=X\times Z_{f}$
is the set of final states.

With product construction in Def. 6, the states of $M_{\mathcal{A}_{\varphi}}$
encode the history of trajectories of $M$ with respect to $\varphi$, i.e.,
runs $\mathbf{z}$ on $\mathcal{\mathcal{A}_{\varphi}}$. Let $Z_{v}\subseteq
Z\setminus Z_{f}$ be the set of DFA sink states, i.e., $\forall z\in Z_{v}$
and $\forall\sigma\in 2^{\Pi}$, $z=\delta(z,\sigma)$. We adapt the method
proposed in [19] to our environment, and define the reward $R:S\to[-1,1]$,
discount function $\Gamma\in(0,1)$, and cumulative reward function $V_{F}$ as:

$\displaystyle
R((x,z),(x^{\prime},z^{\prime}))=\begin{cases}1-\gamma_{F}&\text{if
$z^{\prime}\in Z_{f}$}\\\ -1&\text{if $z^{\prime}\in Z_{v}$}\\\
1-\gamma_{T}&\text{if $z\neq z^{\prime}$}\\\ 0&\text{otherwise}\\\
\end{cases},$ (3)
$\displaystyle\Gamma((x,z),(x^{\prime},z^{\prime}))=\begin{cases}\gamma_{F}&\text{if
$z^{\prime}\in Z_{f}$}\\\ \gamma_{T}&\text{if $z\neq z^{\prime}$}\\\
\gamma&\text{otherwise}\\\ \end{cases},$ (4)
$V_{F}(\omega_{\mathbf{x}},\mathbf{z},n)=\sum_{i=0}^{n}R((\omega_{\mathbf{x}}[i],\mathbf{z}[i]),(\omega_{\mathbf{x}}[i+1],\mathbf{z}[i+1]))\\\
\prod_{j=0}^{i-1}\Gamma((\omega_{\mathbf{x}}[j],\mathbf{z}[j]),(\omega_{\mathbf{x}}[j+1],\mathbf{z}[j+1])),$
(5)

where $\gamma,\gamma_{T},\gamma_{F}\in(0,1)$ are hyper-parameters, and
$\mathbf{z}[i]$ is the $i$-th element of run $\mathbf{z}$. While this reward
is defined over the product states, the product does not need to be
constructed explicitly; it is sufficient to implicitly construct it for reward
evaluation.

Training with this reward is not conditioned on the presence of a shield and
is then applicable for generic DRL tasks. As we train with co-safe LTL
specifications which can be satisfied in finite time, it would be natural to
terminate a training episode once an accepting state of the DFA is reached. In
order to expand the search space, we instead reset to the initial state of the
DFA if we reach an accepting state and allow the agent to continue training.
Intuitively, this means a trajectory is more valuable if it can satisfy a
specification quickly and frequently. This can result in rewards much larger
than 1 in the event a specification can be satisfied multiple times in an
episode. If we reach a sink state in $Z_{v}$ of the DFA, we cannot satisfy
$\varphi$, and hence the episode is terminated and the reward is reduced by 1.

We note that the reward construction proposed in [19] produces a direct
relation between the probability of satisfying a specification and the
cumulative reward received. However, reward is only received when reaching an
accepting state of the DFA which can result in extremely sparse reward as the
number of states in the DFA grows. The alterations from the original design we
propose in (3)-(5), in particular, the additional reward in $R$ when $z\neq
z^{\prime}$, encourage transitions along the states of the DFA. However, they
also limit the direct relation between reward and the probability of
satisfying the specification. As noted in our case studies, a correlation
between reward and satisfaction rate is retained.

For example, the DFA constructed from $\varphi_{0L}$ in Example 2 consists of
only two states; an initial state and the accepting state. Here the reward
formulation in [19] performs identically to our modified version. However, if
the specification is more complex, the resulting DFA is likely to have more
states. In a specification that requires five images with alternating imaging
modes and an inclusion of safety, the DFA has seven states. In our
experiments, training to satisfy this specification with the original reward
results in 38.9% of trajectories ending with spacecraft failure, whereas our
formulation results in only 1.4% of trajectories failing; further discussion
on these benchmarks can be seen in Section IV. This difference is almost
entirely due to the sparsity of reward, resulting in a sub-optimal policy when
trained under the same number of epochs.

Lastly, we note that a policy $\pi:S\to A$ trained on product MDP
$M_{\mathcal{A}_{\varphi}}$ is stationary. This policy however becomes history
dependent on $M$, i.e., since $S=X\times\mathcal{A}_{\varphi}$, the history is
captured by the states of $\mathcal{A}_{\varphi}$.

###  III-B Shield Design

Shield design is typically based on having an MDP that describes the evolution
of the safety aspects of the system in question. In our problem, the MDP that
describes the evolution of the spacecraft is unknown _a priori_. This poses a
major challenge for designing a shield. To that end, we abstract $M$ to a
finite MDP that fully captures the behavior of the spacecraft w.r.t.
$\varphi_{S}$ and refer to it as the Safety MDP. We obtain this abstraction by
partitioning state space $X$ such that the partition respects the regions of
interest that correspond to $\varphi_{S}$. Let $R_{S}\subseteq R$ be the set
of safety regions. Then, the Safety MDP is defined as follows.

######  Definition 7 (Safety MDP).

Given a partition of $X$ that respects the regions of interest in
$R_{S}\subseteq R$, the _safety_ MDP is a finite-state MDP
$\bar{M}=(Q,A,P,\bar{\Pi},\bar{L})$, where $A$ is as in Def. 1,

  * •

$Q=\\{q_{1},\ldots,q_{m}\\}$ is a finite set of states obtained from the
partition of $X$, i.e., $q_{i}\subseteq X$,

  * •

$P:Q\times A\times Q\rightarrow[0,1]$ is a transition probability function
such that, for every $q,q^{\prime}\in Q$ and $a\in A$,
$P(q,a,q^{\prime})=\mathbb{E}_{x\sim D(q)}[T(x,a,q^{\prime})]$, where $D(q)$
is a probability distribution over region $q$,

  * •

$\bar{\Pi}\subseteq\Pi$ is a set of (safety) atomic propositions that are
associated with the regions in $R_{S}$,

  * •

$\bar{L}:Q\rightarrow 2^{\bar{\Pi}}$ is a labeling function such that
$\bar{L}(q)=L(x)\cap\bar{\Pi}$ for all $x\in q$.

In general, the Safety MDP $\bar{M}$ does not require the full dimensionality
of the MDP $M$. This dimensionality reduction enables rigorous safety analysis
while maintaining computational tractability when constructing a shield.
Specifically, for the spacecraft in Example 1, we are interested in regulating
body rates $|\dot{\sigma}|$, reaction wheel speeds $\Omega$, and stored charge
$\mathcal{P}$. As in RL, identifying an appropriate state space for the
spacecraft is challenging, as the true state space may include thousands of
states [3] and the problem must remain Markovian [20] in a lower
dimensionality. We propose a reduction of the state space to just the values
of interest: $|\dot{\sigma}|,\Omega,\mathcal{P}$. These states on their own
are not Markovian. For instance, the attitude rate in the next time step
cannot be predicted just from the current attitude rate as it also depends on
states such as the attitude error. We approach this problem by identifying the
transition probabilities between states of the safety MDP through simulation.

We first define a domain $\bar{X}\subset X$ in which the spacecraft can safely
operate, e.g., $|\dot{\sigma}|\leq 0.01$ , $\Omega\leq 1$ , and
$0<\mathcal{P}\leq 1$. We then discretize $\bar{X}$ into a set non-overlapping
regions, defining the states $Q$ of $\bar{M}$. Due to the complexity of the
dynamics, we compute the transition probabilities $P$ through simulation of
$M$ using Basilisk [18]. For each state $q\in Q$ of the MDP, we initialize the
spacecraft simulation with randomized parameters (e.g. orientation) and limit
the three states of interest to the values described by the discretization
(e.g. $0\leq\Omega<0.2$) and simulate the evolution of the system $N_{P}$
times, where $N_{P}$ is a large number ($N_{P}=10,000$ in our case studies)
under each action. This allows the identified transition probabilities to no
longer be conditioned on aspects such as orientation, allowing the abstraction
of the safety MDP to remain Markovian.

Shield Algorithms. With the safety MDP constructed above, shield synthesis is
enabled. Given $\bar{M}$, the goal is to find the set of _all_ safe policies
that guarantee no violation to $\varphi_{S}$ with at least probability $1-p$.
As the policies can be history dependent, finding the set of all policies can
lead to combinatorial problems and computational intractability. Hence, we
focus on finding a set of stationary policies on the product MDP with the DFA
corresponding to $\varphi_{S}$.

Since $\varphi_{S}$ is a safe LTL formula, $\neg\varphi_{S}$ is a co-safe
formula. Then, DFA $\mathcal{A}_{\neg\varphi_{S}}$ can be constructed that
precisely accepts all the safety-violating traces. The product
$\bar{M}_{\neg\varphi_{S}}=\bar{M}\times\mathcal{A}_{\neg\varphi_{S}}$ can be
constructed per Def. 6 with the set of states $\bar{S}:Q\times Z$, transition
probability function $\bar{\Delta}:\bar{S}\times A\times\bar{S}\to[0,1]$, and
set of final states $\bar{S}_{f}$. Note that the paths of
$\bar{M}_{\neg\varphi_{S}}$ that reach $\bar{S}_{f}$ violate $\varphi_{S}$.
Hence, our aim becomes to find the set of stationary policies on
$\bar{M}_{\neg\varphi_{S}}$, under which the probability of the paths that
reach $\bar{S}_{f}$ is at most $p$.

We note that the traditional shield construction methods as in [6] are based
on game formulation. Those approaches strictly require all the paths of the
MDP to remain safe all the time, which is analogous to requiring a violation
probability threshold of $p=0$, which result in very conservative design. For
example, in our case studies, those approaches never produced a safe action.
Therefore, we relax such strong requirement and focus on probabilistic
shields, i.e., allowing a small violation probability up to a threshold $p$,
and propose three different shield designs that result in safe actions for our
MDP, each design providing a different guarantee on safety.

####  III-B1 One-Step Safety

The first shield we investigate is a one-time step safety shield, i.e., we
find actions that enable transition to the safe set
$\bar{S}\setminus\bar{S}_{f}$ with high probability. This shield is the
simplest to implement, as actions that are safe on the product
$\bar{M}\times\mathcal{A}_{\neg\varphi_{S1}}$ can be directly assessed from
the transition probabilities of the MDP $\bar{M}$ given a state and action.
This design provides a guarantee that the system remains safe with probability
$1-p$ for at least one time step; however, there are no guarantees on long
term safety. We allow any action that transitions to a safe state, even if the
next states have no safe actions themselves. Then the shield is defined as,
for every $s\in\bar{S}$,

$\displaystyle\pi_{\textrm{\it shield}}^{1}(s)=\\{a\in
A\mid\sum_{s^{\prime}\in\bar{S_{f}}}\bar{\Delta}(s,a,s^{\prime})<p\\}.$

####  III-B2 Two-Step Safety

As the first design has no long term safety guarantees, we design a shield
that only allows actions that have a high probability of transitioning to safe
states, where a safe state is recursively defined as a state where there is a
safe action. This translates into finding actions that have a high probability
of remaining safe for two time steps. This guarantees the system will remain
safe for two consecutive time steps with probability $\geq 1-p$ at each step.
Two steps are considered sufficient as transition probabilities in MDPs are
not history dependent; hence, this guarantee holds for each time step the
system begins in a safe state. We call the set of unsafe states $U$ and
initialize it with $U=\bar{S_{f}}$. Then, states are recursively added to $U$
when no safe action is available. The process repeats until we reach a fixed
point ($U$ gains no more states). The algorithm is as follows.

$\displaystyle U=\bar{S}_{f}$ $\displaystyle\texttt{While }U\neq U^{\prime}$
$\displaystyle\qquad U^{\prime}=U$ $\displaystyle\qquad\forall
s\in\bar{S},\;\pi_{\textrm{\it shield}}^{2}(s)=\\{a\in
A\mid\Sigma_{s^{\prime}\in U}\bar{\Delta}(s,a,s^{\prime})<p\\}$
$\displaystyle\qquad U=U\cup\\{s\in\bar{S}\mid\pi_{\textrm{\it
shield}}^{2}(s)=\emptyset\\}$ $\displaystyle\texttt{Return }\bar{S}\setminus
U,\;\pi_{\textrm{\it shield}}^{2}$

In the event that the system transitions into the unsafe states ($U$ for
$\pi_{\textrm{\it shield}}^{2}$ or $\bar{S}_{f}$ for $\pi_{\textrm{\it
shield}}^{1}$), we select the action with the highest probability of returning
to the safe set.

####  III-B3 Q-optimal Safety

The final shield design we assess is based on dynamic programming, which
results in the strongest guarantees for safety. We consider safety horizon
$N\in\mathbb{N}\cup\\{\infty\\}$ and use a dynamic programming approach to
compute the policy that minimizes probability of reaching unsafe set
$\bar{S}_{f}$ in $N$ steps, resulting in optimal policy $\pi^{*}_{S}$ and
value function $V^{*}_{S}$, i.e.,

$\displaystyle
V^{\pi}_{S}(s)=P(\omega_{\mathbf{x}}^{N}\in\Omega_{\mathbf{x}}^{\text{fin},\pi}\mid\omega_{\mathbf{x}}^{N}[0]\in
s,$ $\displaystyle\hskip
108.12047pt\omega_{\mathbf{x}}^{N}[i]\in\bar{S}_{f}\text{ for some
}i\in\mathbb{N}),$

and $\pi^{*}_{S}=\operatorname*{\arg\min}_{\pi}V^{\pi}_{S}$ and
$V^{*}_{S}=V^{\pi_{S}^{*}}_{S}$. When the shield is used, we assess the
Q-value of each action and only allow actions that have a (unsafety
probability) value below threshold $p$. Then, the shield is defined as

$\displaystyle\pi_{\textrm{\it shield}}^{\text{Q}}(s)=\\{a\in
A\mid\sum_{s^{\prime}\in\bar{S}}\bar{\Delta}(s,a,s^{\prime})V^{*}_{S}(s^{\prime})<p\\}.$

In the event no action satisfies the bound $p$, the shield uses the optimal
policy $\pi_{S}^{*}$, i.e., if for a $s\in\bar{S}$, $\pi_{\textrm{\it
shield}}^{\text{Q}}(s)=\emptyset$, then $\pi_{\textrm{\it
shield}}^{\text{Q}}(s)=\pi_{S}^{*}(s)$.

######  Remark 2.

During learning and deployment, we use post-posed shielding shown in Figure 1.
Here the shield receives the observations of the environment and the action of
the agent and returns a safe action to the environment. As in [7], there is no
penalty (reward) associated with the shield changing the action.

##  IV Case Studies

Figure 2: Action history and reaction wheel speeds when deploying under policy
$\pi_{0}$ (top) and $\pi_{1}$ (bottom) from a fixed initial condition. The red
highlight shows when the spacecraft has access to the target, the blue
highlights show when the spacecraft is in Momentum Dumping (RW Desat) Mode.
Note that policy $\pi_{1}$ (trained in $\varphi_{0L}\land\varphi_{S}$) keeps
the spacecraft safe after imaging the target whereas policy $\pi_{0}$ (trained
on only $\varphi_{0L}$) prioritizes imaging over spacecraft survival.

We evaluate the efficacy of our LTL-SDRL framework on the spacecraft in
Example 1. We first show the importance of training with safety specification
on a simple task scenario. Then, we consider a complex scenario for
benchmarking (comparing) the three shield designs. The shields are each
designed to prevent the spacecraft from having less than 20% power and wheel
speeds above 80%. We also assess training with the shield and training without
the shield.

In all the case studies, the Basilisk [18] simulator is used to create an
environment for implementation of PPO2 [21]. The agent is trained with a
learning rate $\alpha=3\times 10^{-4}$ with a fully-connected network composed
of two hidden layers of width 10 with a hyperbolic tangent activation
function. The network is trained for $4.6\times 10^{5}$ time steps on an Intel
Core i7-12700K CPU at 3.60GHz with 32 GB of RAM limited to 8 threads. The
input space of the network contains information on 19 states, composed as 13
states with 12 as in [2] and the addition of the DFA state. The Safety MDP
consists of 100 discrete states. All of our validations are computed from 1000
deployment simulations, where the dynamics are propagated with 0.5 second
integration steps. Each flight mode is executed with and observations are
received at three minute intervals.

###  IV-A Simple Task: Importance of $\varphi_{S}$ in Training

We first demonstrate the effect of learning with and without a safety
specification in (unshielded) DRL. We use the formula $\varphi_{0L}$ and
$\varphi_{S}$ in (1)-(2) from Example 2 and train for a fixed orbit and fixed
target location. We compare the frequency of satisfying the specifications and
the frequency of spacecraft failures over 300 minutes (100 time steps), which
is longer than the time needed for one orbit (271 minutes). Here, we expect to
see a high satisfaction rate of $\varphi_{0L}$ and some violations of
$\varphi_{S}$. Results are shown in Table I.

We first train on a DFA constructed from $\varphi_{0L}$ and refer to the
policy returned from DRL as $\pi_{0}$. The large average $V_{F}$ suggests
frequent satisfaction of the specification during training under $\pi_{0}$.
When we deploy with $\pi_{0}$, we see a high satisfaction rate of
$\varphi_{0}$, but we also find frequent violations of $\varphi_{S}$ (i.e.,
either power falls below 20% or reaction wheel speeds exceed 80%) and even
some spacecraft failures. This is expected, as without shielding and with no
information in the reward structure about safety the policy never learns to
avoid unsafe behavior.

TABLE I: Training results for a simple task. Reported values are average value $V_{F}$ during training, rates of satisfaction of $\varphi_{0L}$ and violation of $\varphi_{S}$, and spacecraft (SC) failure rate. Spec. | Avg. $V_{F}$ | % Sat. $\varphi_{0L}$ | % Violate $\varphi_{S}$ | SC Failure
---|---|---|---|---
$\varphi_{0L}$ | 3.295 | 99.6 | 27.1 | 3.4
$\varphi_{0L}\wedge\varphi_{S}$ | 3.1 | 99.0 | 3.5 | 0

When we train on a DFA constructed from
$\varphi=\varphi_{0L}\wedge\varphi_{S}$, which implicitly incorporates the
safety requirements into the reward structure, we find a policy $\pi_{1}$. We
see a similarly high satisfaction rate of $\varphi_{0L}$; however, very few
runs violate $\varphi_{S}$ and no runs end with spacecraft failure. This
demonstrates the power of incorporating safety into the training
specification. We show a sample trajectory under both strategies in Figure 2,
where each sample is initialized with the same parameters.

###  IV-B Complex Tasks and Shielding

We consider a more complex imaging task, to highlight the flexibility provided
by training with LTL specifications and demonstrate the effects of shielding.
Here we train to satisfy a task for a random LEO and random target locations.
Our task is given as “Image targets at least five times, alternating imaging
modes starting from Imaging mode A. Only accept images that are taken when the
attitude error ($|{\sigma}_{err}|$) is less than 0.008 radians and the
attitude rate ($|\dot{\sigma}|$) is less than 0.002 radians per second.” This
is translated into the co-safe LTL formula

$\varphi_{1L}=\mathcal{F}(\mathrm{p}_{3}\wedge\mathcal{X}\mathcal{F}(\mathrm{p}_{4}\wedge\mathcal{X}\mathcal{F}(\mathrm{p}_{3}\wedge\mathcal{X}\mathcal{F}(\mathrm{p}_{4}\wedge\mathcal{X}\mathcal{F}\mathrm{p}_{3}))))$

where $\mathrm{p}_{3}$ and $\mathrm{p}_{4}$ are similar to $\mathrm{p}_{0}$
from Example 2, but the corresponding regions only include one imaging mode.
Note that in traditional reward design a finite state machine would need to be
constructed to account for mode switching; however, in our formulation the
switching is automatically captured through the specification. The safety
specification is the same $\varphi_{S}$ in (2) as above, and probability
threshold is $p=0.05$.

For this scenario, each episode consists of 90 actions which corresponds to
three orbits. We assess the average value $V_{F}$ during training, the
satisfaction rate of specification with and without the shield after the agent
has been trained, the average number of shield interventions, and the
frequency of unsafe behavior. Results are shown in Table II.

TABLE II: Results for the complex specification $\varphi_{1L}$. We report average value $V_{F}$ of trajectories during training, liveness specification satisfaction rate (% Sat. $\varphi_{1L}$), safety specification violation rate (% Violate $\varphi_{S}$), spacecraft failure rate (SC Failure, % of tests), and the average number of shield interventions (over 90 time steps) when $\varphi_{1L}$ was satisfied and not satisfied. ∗1 and ∗2 denote that the same policy was used for these experiments, i.e., they were trained without a shield.  Shield Type | Trained | Spec. | Avg. $V_{F}$ | % Sat. | % Violate | SC Failure |  Avg. # of Interventions
---|---|---|---|---|---|---|---
w/ Shield | $\varphi_{1L}$ | $\varphi_{S}$ | Sat. $\varphi_{1L}$ | Not Sat. $\varphi_{1L}$
No Shield | No∗1 | $\varphi_{1L}$ | 3.39∗1 | 92.7 | 55.3 | 10.9 | – | –
No∗2 | $\varphi_{1L}\wedge\varphi_{S}$ | 2.47∗2 | 90.9 | 11.7 | 1.4 | – | –
One Step ($\pi_{\textrm{\it shield}}^{1}$) | No∗1 | $\varphi_{1L}$ | 3.39∗1 | 79.2 | 0.4 | 0 | 13.6 | 29.2
No∗2 | $\varphi_{1L}\wedge\varphi_{S}$ | 2.47∗2 | 85.9 | 0.6 | 0 |  3.7 | 11.1
Yes | $\varphi_{1L}$ | 1.88 | 64.8 | 0.8 | 0 | 44.0 | 60.6
Yes | $\varphi_{1L}\wedge\varphi_{S}$ | 1.93 | 74.9 | 0.6 | 0 | 48.6 | 66.8
Two Step ($\pi_{\textrm{\it shield}}^{2}$) | No∗1 | $\varphi_{1L}$ | 3.39∗1 | 82.0 | 0.6 | 0 | 13.2 | 28.5
No∗2 | $\varphi_{1L}\wedge\varphi_{S}$ | 2.47∗2 | 86.2 | 0.9 | 0 |  3.9 | 10.9
Yes | $\varphi_{1L}$ | 1.84 | 61.6 | 1.0 | 0 | 41.4 | 59.9
Yes | $\varphi_{1L}\wedge\varphi_{S}$ | 1.86 | 72.6 | 1.2 | 0 | 47.1 | 64.0
Q-optimal ($\pi_{\textrm{\it shield}}^{\text{Q}}$) | No∗1 | $\varphi_{1L}$ | 3.39∗1 | 79.9 | 0.2 | 0 | 14.2 | 28.9
No∗2 | $\varphi_{1L}\wedge\varphi_{S}$ | 2.47∗2 | 85.2 | 0.4 | 0 |  3.8 | 11.2
Yes | $\varphi_{1L}$ | 1.70 | 63.2 | 0.5 | 0 | 44.2 | 61.0
Yes | $\varphi_{1L}\wedge\varphi_{S}$ | 2.23 | 73.4 | 0.2 | 0 | 49.1 | 66.9

####  IV-B1 Trained and Deployed without Shielding

We see a similar trend as with the simple specification, where training with
the safety specification included results in a lower reward, fewer spacecraft
failures, and fewer safety violations. Due to the more stressing environment,
we see more safety violations during training which results in the large gap
in value $V_{F}$ between the two policies. As noted earlier, we still see a
correlation between the average value $V_{F}$ of trajectories and the
probability of satisfying the liveness specification, a higher $V_{F}$ means
the policy is more likely to result in satisfaction when deployed.

####  IV-B2 Trained without Shielding and Deployed with Shielding

We first note that in each case a shield is deployed, there are no instances
of spacecraft failure and the frequency of violations of $\varphi_{S}$ fall
below 5%, which is the threshold we allow for choosing safe actions. When we
train with just $\varphi_{1L}$, we see a significant reduction in satisfaction
rate and a high frequency of shield interventions. This follows intuition, as
over 50% of trajectories would violate $\varphi_{S}$ without shielding.
Contrarily, when we train on $\varphi_{1L}\wedge\varphi_{S}$, we see far fewer
shield interventions and a higher rate of satisfaction of $\varphi_{1L}$. This
demonstrates that the policy learned from the safety specification acts in a
more flexible manner when shielded. In all cases, we see that far more shield
interventions occur when a trajectory does not satisfy $\varphi_{1L}$ as
actions must be repeatedly corrected to maintain guarantees.

####  IV-B3 Trained and Deployed with Shielding

Minor differences are seen between our shield designs when we train with them
in the loop. As noted in [7], the policy learns to rely on the shield
interventions. In each case, over half of all actions the DRL policy chooses
are rejected by the shield in place of a safe action which results in far
fewer trajectories satisfying $\varphi_{1L}$. Here, the improvements seen when
training with a safety specification are more noticeable, despite the same
number of shield interventions occurring. This, again, shows the correlation
between $V_{F}$ and the satisfaction rate.

######  Remark 3.

Despite the differences in guarantees provided by each shield, we see that
they perform very similarly when deployed. This suggests that the safety MDP
we constructed contains overly conservative transition probabilities,
resulting in similar policies among the shields. The states chosen to
represent safety likely increase conservatism, as these states have highly
non-deterministic transitions which requires the shield to select actions for
worst case orientations (e.g. The norm of the wheel speed vector contains no
information about direction).

##  V Conclusion

In this work, we provide a method to enable autonomous decision making for the
satisfaction of complex Earth imaging tasks through SDRL. Safety is ensured
through the designs of three shield algorithms, which are based on a simulated
safety MDP. We identify that training on composed liveness and safety
specifications without a shield results in the best interaction of policy and
shield, i.e., a high rate of satisfaction of liveness, few violations of
safety, and few shield interventions. The shields we produced are far less
restrictive than prior designs. However, while safety guarantees hold for the
safety MDP, the transition probabilities are computed based on empirical
evaluation (physics simulator). Numerical simulations suggest the shields
provide stronger guarantees than necessary. We hope to further formalize the
safety MDP in future work and reduce the associated conservatism seen by the
shielding.

## References

  * [1] C. Frost, A. Butt, and D. Silva, “Challenges and opportunities for autonomous systems in space,” in _Frontiers of Engineering: Reports on Leading-Edge Engineering from the 2010 Symposium_ , 2010.
  * [2] A. T. Harris and H. Schaub, “Spacecraft command and control with safety guarantees using shielded deep reinforcement learning,” in _AIAA Scitech 2020 Forum_ , 2020, p. 0386.
  * [3] I. Nazmy, A. Harris, M. Lahijanian, and H. Schaub, “Shielded deep reinforcement learning for multi-sensor spacecraft imaging,” in _2022 American Control Conference (ACC)_. IEEE, 2022, pp. 1808–1813.
  * [4] C. Adams, B. Kempa, M. Iatauro, J. Frank, and W. Vaughan, “An overview of distributed spacecraft autonomy at nasa ames,” in _Proceedings of the Small Satellite Conference_ , no. 37. Utah State University, 2023.
  * [5] K. Arulkumaran, M. P. Deisenroth, M. Brundage, and A. A. Bharath, “Deep reinforcement learning: A brief survey,” _IEEE Signal Processing Magazine_ , vol. 34, no. 6, pp. 26–38, 2017.
  * [6] R. Bloem, B. Könighofer, R. Könighofer, and C. Wang, “Shield synthesis: Runtime enforcement for reactive systems,” in _International conference on tools and algorithms for the construction and analysis of systems_. Springer, 2015, pp. 533–548.
  * [7] M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu, “Safe reinforcement learning via shielding,” in _Proceedings of the AAAI conference on artificial intelligence_ , vol. 32, no. 1, 2018.
  * [8] A. Pnueli, “The temporal logic of programs,” in _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. ieee, 1977, pp. 46–57.
  * [9] A. Bhatia, L. E. Kavraki, and M. Y. Vardi, “Sampling-based motion planning with temporal goals,” in _2010 IEEE International Conference on Robotics and Automation_. IEEE, 2010, pp. 2689–2696.
  * [10] A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi, “Motion planning with complex goals,” _IEEE Robotics & Automation Magazine_, vol. 18, no. 3, pp. 55–64, 2011.
  * [11] M. Lahijanian, M. R. Maly, D. Fried, L. E. Kavraki, H. Kress-Gazit, and M. Y. Vardi, “Iterative temporal planning in uncertain environments with partial satisfaction guarantees,” _IEEE Transactions on Robotics_ , vol. 32, no. 3, pp. 583–599, 2016.
  * [12] H. Kress-Gazit, M. Lahijanian, and V. Raman, “Synthesis for robots: Guarantees and feedback for robot behavior,” _Annual Review of Control, Robotics, and Autonomous Systems_ , vol. 1, pp. 211–236, 2018.
  * [13] M. Lahijanian, S. B. Andersson, and C. Belta, “Formal verification and synthesis for discrete-time stochastic systems,” _IEEE Transactions on Automatic Control_ , vol. 60, no. 8, pp. 2031–2045, 2015.
  * [14] M. Wen, R. Ehlers, and U. Topcu, “Correct-by-synthesis reinforcement learning with temporal logic constraints,” in _2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)_. IEEE, 2015, pp. 4983–4990.
  * [15] S. Junges, N. Jansen, C. Dehnert, U. Topcu, and J.-P. Katoen, “Safety-constrained reinforcement learning for mdps,” in _International conference on tools and algorithms for the construction and analysis of systems_. Springer, 2016, pp. 130–146.
  * [16] M. Lahijanian, S. Andersson, and C. Belta, “Control of markov decision processes from pctl specifications,” in _Proceedings of the 2011 American Control Conference_. IEEE, 2011, pp. 311–316.
  * [17] O. Kupferman and M. Y. Vardi, “Model checking of safety properties,” _Formal methods in system design_ , vol. 19, pp. 291–314, 2001.
  * [18] P. W. Kenneally, S. Piggott, and H. Schaub, “Basilisk: A flexible, scalable and modular astrodynamics simulation framework,” _Journal of aerospace information systems_ , vol. 17, no. 9, pp. 496–507, 2020.
  * [19] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Mungojerrie: Linear-time objectives in model-free reinforcement learning,” in _International Conference on Tools and Algorithms for the Construction and Analysis of Systems_. Springer, 2023, pp. 527–545.
  * [20] R. S. Sutton and A. G. Barto, _Reinforcement learning: An introduction_. MIT press, 2018.
  * [21] J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov, “Proximal policy optimization algorithms,” _arXiv preprint arXiv:1707.06347_ , 2017\.