# Optimality Principles in Spacecraft Neural Guidance and Control

Dario Izzo,1∗ Emmanuel Blazquez,1 Robin Ferede2
Sebastien Origer2, Christophe De Wagter2, Guido C.H.E. de Croon2
1Advanced Concepts Team of the European Space Research & Technology Centre
Keplerlaan 1, 2200 AG Noordwijk, NL.
2Micro Air Vehicle Lab of the Faculty of Aerospace Engineering
Delft University of Technology, 2629 HS Delft, NL.

∗To whom correspondence should be addressed; E-mail<EMAIL_ADDRESS>
> Spacecraft and drones aimed at exploring our solar system are designed to
> operate in conditions where the smart use of onboard resources is vital to
> the success or failure of the mission. Sensorimotor actions are thus often
> derived from high-level, quantifiable, optimality principles assigned to
> each task, utilizing consolidated tools in optimal control theory. The
> planned actions are derived on the ground and transferred onboard where
> controllers have the task of tracking the uploaded guidance profile. Here we
> argue that end-to-end neural guidance and control architectures (here called
> G&CNets) allow transferring onboard the burden of acting upon these
> optimality principles. In this way, the sensor information is transformed in
> real time into optimal plans thus increasing the mission autonomy and
> robustness. We discuss the main results obtained in training such neural
> architectures in simulation for interplanetary transfers, landings and close
> proximity operations, highlighting the successful learning of optimality
> principles by the neural model. We then suggest drone racing as an ideal gym
> environment to test these architectures on real robotic platforms, thus
> increasing confidence in their utilization on future space exploration
> missions. Drone racing shares with spacecraft missions both limited onboard
> computational capabilities and similar control structures induced from the
> optimality principle sought, but it also entails different levels of
> uncertainties and unmodelled effects. Furthermore, the success of G&CNets on
> extremely resource-restricted drones illustrates their potential to bring
> real-time optimal control within reach of a wider variety of robotic
> systems, both in space and on Earth.

## Introduction

The design of a space exploration mission heavily relies on optimality
principles. Given the absence of a safe harbor in space, every onboard
resource, including propellant mass, available energy, and computing
capabilities, must be utilized parsimoniously to ensure the highest possible
mission return. Even with safety margins built into the mission plan,
executing sub-optimal plans can result in the failure of the entire mission.
To address this challenge, optimal control models have been developed that
capture the optimality principles relevant to different mission phases and
translate them into elaborate system behaviours. In practice, the optimal
guidance profile that follows the application of abstract optimality
principles is carefully derived on the ground, well ahead of the mission
launch, for most flown and planned missions. The plan is then uploaded onboard
and acted upon by the dedicated control system that, using the specific
actuators available, tracks the planned profile continuously canceling
incurred deviations. This approach is common to interplanetary trajectory
phases, landing phases, surface exploration phases, formation flying missions
and more (see Figure 1), thanks to the abstract nature of the well-established
optimal control theory which allows to capture different dynamics, actuator
models and timescales well. It also has the advantage of being a well-tested
and validated approach with a history of successfully embedding optimality
principles in the on-board control system allowing missions to meet their
requirements.

This common approach is, however, known to be sub-optimal. It violates a
‘minimal intervention’ principle, well described by _Todorov_ and _Jordan_
(?): efforts in correcting deviations from an average path should be only made
when interfering with the task performance. In our context, in case of a
deviation from the pre-planned trajectory, the onboard controller should not
try to steer back the system to it as the new situation may require other
actions for optimality. The approach also carries higher risks in missions
where significant unmodeled effects, noise, uncertainties, and unforeseen
events are present, which could result in strong deviations from the original
plan. In such cases, a new optimal guidance profile may need to be developed
on the ground and uploaded to the spacecraft, greatly hindering its autonomy.

This raises the question of why space missions do not continuously re-plan and
compute the optimal guidance profile onboard, for example, by employing Model
Predictive Control (MPC). Recent efforts have been made to develop MPC
approaches for various mission profiles, aiming to overcome these limitations.
MPC has been studied in the last decades as a promising control approach for
aerospace systems (see _Eren et al._ (?) for a review of MPC in this context)
allowing to automate on-board the task of transforming high-level optimality
principles into actions. It relies on the availability of numerical methods to
solve reliably some form of an optimal control problem, starting from the
information on the current system state and the time. This online optimization
returns an optimal sequence of open-loop predicted actions, the first of which
is considered the best current control action. Despite great advances in the
associated numerical techniques and theory (?), the uptake of modern MPC
approaches in space missions remains limited by the available on-board
computational capabilities and the reliability of the existing numerical
solvers.

A different, albeit related, approach appeared more recently in the robotics
as well as in the aerospace field. It is loosely inspired by models that
interpret sensorimotor action in humans in terms of optimal control theory
(?), thus suggesting how optimality principles, in the mathematical sense, are
deeply embedded directly in the neuro-musculo-skeletal system. The new
approach attempts to mimic this structure in the guidance and control
architecture of space systems and thus to train a deep artificial neural
network (DNN) to represent directly the relation between the system state and
its action under some predefined task and optimality principle. In this
context, the network depth refers to the use of multilayer perceptrons that
are capable, already with a few layers, of a high representativity (?, ?).
Following this approach, the guidance and control blocks of a typical space
mission control architecture are substituted with one, end-to-end, DNN which
does not need any form of a reference trajectory and is thus also called a
Guidance and Control Net or G&CNet (?, ?). In comparison to the MPC approach,
the step of having to solve on-board an instance of the optimal control
problem is bypassed and substituted by a single, computationally less
expensive, neural inference (see Figure 2). Most of the desirable properties
of MPC (?) are instead retained, while the new architecture requires orders of
magnitude fewer on-board computational resources. Ongoing research in this
emerging approach is focused on designing an efficient procedure to train the
weights of artificial neural networks to accurately represent the desired task
execution.

In this review, we discuss the use of G&CNets as a viable and promising path
towards achieving on-board optimal decision-making in different space mission
scenarios. We then discuss two main avenues available for training such
networks in the context of space missions: (a) imitation learning, also known
as behavioral cloning (essentially supervised learning) and (b) reinforcement
learning. After evaluating the current state-of-the-art for both approaches,
we conclude by proposing drone flight racing as a safe stepping stone towards
the on-board implementation of such networks for real missions. We finally
present concrete examples of the capabilities of embedded G&CNet
implementations using drones as a model system.

## Optimality in guidance and control of space systems

Space systems are typically well characterized and tested extensively on the
ground prior to launch. Their mass, inertia tensor, flexibility, and thrusters
are all subject to thorough testing, and precise models of the entire system
behavior are developed well in advance of the mission launch. However, in some
cases, the development of the control system of a space system still requires
the consideration of stochastic terms in its dynamics. Uncertainties can arise
from unmodelable (or difficult to model) effects originating either from the
system itself or from the environment in which it is designed to operate.
Examples of the former include fuel sloshing (?, ?), mis-thrust events (?, ?,
?), or corrupted sensor measurements (?). Uncertainties coming from the
environment arise, for example, in deep space missions to asteroids where the
body shape is known only to a limited extent during most mission phases (?,
?), or in situations where the atmosphere of some celestial body plays a role
such as re-entry, aero-capture or exploratory drone flights (?, ?, ?).
Uncertainties about solar activity or other space environment quantities also
result in unmodeled effects.

In any case, ignoring the stochastic contribution and using the sophisticated
mathematical framework for deterministic optimal control emerged from the work
of _Pontryagin_ (?) offers a starting point in understanding the underlying
structure rising from chosen optimality principles. Under this framework, it
is well known how the optimal feedback is a discontinuous and non-linear
function of the system state already for most simple low-dimensional and
linear systems (?). An informing example is that of the time optimal
precession angle control of a spinning satellite (?) where the analytical
solution is available and allows exceptionally, to observe the optimal control
switching structure in the full state space, revealing the extremely nonlinear
and discontinuous nature of such a function (see Figure 3). This is the case
for time optimality, but also and to a larger extent for higher dimensional
cases and propellant mass optimality: the primary optimality principle for
most deep-space mission phases. In deep-space missions, thrust is mostly
achieved through the ejection of propellant mass which causes the spacecraft
to lose mass and accelerate in the opposite direction. This specific form of
control for mass varying systems creates a distinct structure of the resulting
optimal actions which is the subject of a large body of works from the
aerospace community (see for example (?)). Thrust is also often modeled as a
sequence of impulsive velocity changes rather than as a continuous action, and
dedicated concepts such as the primer vector introduced by _Lawden_ (?) have
been used to expand upon Pontryagin work and help to answer complex questions
on the resulting intricate structure of the optimal sequence of impulsive
maneuvers (?, ?, ?, ?).

When stochastic terms are considered in the system dynamics, the mathematical
structure of the optimal control problem undergoes a significant change. As a
result, Pontryagin theory is no longer applicable, and Bellman’s dynamic
programming methods (?) offer a more appropriate tool based on the concept of
the optimal cost-to-go or value function (?). This added complexity is
captured by a set of nonlinear, second-order, partial differential equations
known as the Hamilton-Jacobi-Bellman equations (?). Finding a solution to
these equations yields the value function and thus the optimal policy, but
even in the simplest cases, it can be challenging, particularly for problems
of interest in this context.

Most importantly, Belmann’s mathematical framework allows for demonstrating
the existence and uniqueness of solutions in terms of the value function, and
thus the existence (outside of singular corner cases) of optimal feedback in
the form $\mathbf{u}^{*}(\mathbf{x})$ where $\mathbf{u}^{*}$ denotes the
optimal feedback and $\mathbf{x}$ denotes the system state. In summary, for
any (deterministic or stochastic) task, the current system state and an
associated optimality principle are sufficient to decide upon the action to be
taken. However, such an optimal state-action mapping is nonlinear,
discontinuous, and has an extremely intricate differential structure.

## Embedding optimality principles into neural models

Artificial neural networks are highly versatile in their ability to
approximate complex and discontinuous functions, even in their simplest
shallow feed-forward architecture, as recently re-discussed in depth by
_Calin_ (?). They have been demonstrated to represent the optical
characteristics of complex 3D scenes with remarkable detail, as evidenced by
the work of Mildenhall et al. (?), as well as to model the gravitational field
of irregular bodies in the solar system with a precision exceeding that of
classical methods, such as spherical harmonics expansions (?). Therefore, DNNs
are an obvious choice for representing the complex structure of the optimal
policies $\mathbf{u}^{*}$ (or the value function $v$) often needed in space
missions. A DNN (here denoted generically with $\mathcal{N}_{\theta}$) can
formally approximate, within some tolerance $\epsilon$, a parametric optimal
feedback of the form
$\mathbf{u}^{*}(\mathbf{x},\mathbf{p})=\mathcal{N}_{\theta}(\mathbf{x},\mathbf{p})+\epsilon$,
where the parameters $\mathbf{p}$ may capture different tasks, objectives and
environmental properties, such as constraints and unknown gravitational
effects. As a result, the biases and weights $\theta$ of the neural model
incorporate multiple optimality principles, which are subsequently converted
into control commands through onboard inference. This inference process is
becoming increasingly efficient due to the development of dedicated AI
accelerators for on-the-edge space systems, leading to the creation of new
dedicated hardware (?). AI-focused processors were embarked in the
${\Phi}$-Sat-1 (?) mission, field-programmable gate arrays (FPGAs) on OPS-SAT
(?) and HYPSO-1 (?, ?), and graphics processing units (GPUs) are being
considered for future non-mission-critical applications (?, ?). The use of
DNNs for onboard systems with limited computational resources, such as
spacecraft, cubesats, and planetary drones, has been only recently proposed in
the context of space missions and is attracting the attention of a growing
number of scientists. The term G&CNets (guidance and control network) (?, ?),
introduced in early studies at European Space Agency, is here used to indicate
such DNNs promising to replace traditional control and guidance architectures
in future space missions. G&CNets main attractiveness stems from their promise
to bypass problems connected to the onboard solution of optimal control
problems, typical for example of classic MPC schemes (?), at the cost of
introducing the need of pre-training robust neural models on the ground.
Trivially, in the limit case in which both an MPC and a G&CNets are able to
compute the actual true optimal-feedback $\mathbf{u}^{*}$ without errors and
with similar computational complexity, they are equivalent. Two main
approaches are mostly being studied in the context of G&CNets training:
supervised learning and reinforcement learning.

### Approaches based on Supervised Learning

The model parameters $\theta$ of the DNN approximating the parametric optimal
feedback $\mathcal{N}_{\theta}(\mathbf{x},\mathbf{p})$ can be learned via a
supervised learning approach provided some dataset
$\mathcal{D}:=\left\\{(\mathbf{x},\mathbf{p}),\mathbf{u}^{*}\right\\}$ is
available containing optimal state-action pairs for one or more tasks
represented by $\mathbf{p}$. This approach can also be referred to as
imitation learning (?) or behavioral cloning (?) to highlight the control
aspect of the dataset to be learned. After the successful demonstration over a
range of simulated landing tasks (?), a large number of works independently
tested the capabilities of imitating the optimal control in diverse space
contexts such as lunar and Mars landing (?, ?), irregular asteroid landings
(?), low-thrust missions and orbital transfers (?, ?, ?), solar sailing (?),
proximity operations (?), drone flights (?) and mis-thrust problems (?). While
achieving convincing results in many of the cases reported, much research
still needs to be done to tackle the issues connected to the imitation
learning approach: the efficient creation of a dataset $\mathcal{D}$, the
verification of requirements on the resulting onboard control system (?), and
the inclusion of mechanisms able to cope with unmodeled components (?).

The creation of a dataset $\mathcal{D}$ requires running numerical optimal
control solvers over a large set of initial states. This demanding
computational effort can be alleviated by the use of techniques leveraging the
proximity to previous solutions found (such as homotopy or continuation (?)),
but remains a limiting factor, although not one burdening the on-board
inference speed. As a consequence, the number of optimal trajectories needed
to build $\mathcal{D}$ and test the capabilities of an imitation learning
approach to G&CNets, have been, so far, mostly limited to the order of tens of
thousands (?, ?, ?, ?). Small datasets are unable to harness the full
potentials of a deep supervised learning pipeline and only allow for partial
investigations of the potentials of G&CNets, restricting possible results to
only small portions of the state space. In cases where Pontryagin’s theory can
be used to derive necessary conditions for optimality via the introduction of
a two-point boundary value problem defined on the augmented dynamics (indirect
methods) a technique called Backward Generation of Optimal Examples - or BGOE
- (see Figure 4) has been recently introduced to allow the creations of
datasets $\mathcal{D}$ orders of magnitude larger than what is otherwise
possible. BGOE has been used in the context of studies on Earth-Venus mass
optimal interplanetary transfers (?), as well as time-optimal asteroid belt
mining missions (?), showing promising results and allowing the creation of
public datasets containing millions of optimal trajectories rather than only a
few thousand.

Studies on the use of BGOE are still preliminar, and the technique cannot be
used in general, for example in contexts where indirect optimization methods
fail. As a consequence, most of the past works on imitation learning for
G&CNets suffer from an insufficient representativity of the trained network,
resulting in the system state propagating outside the training set and thus
the onboard closed-loop becoming unstable. In the presence of strong
perturbations and uncertainties, this can be the case even if the dataset size
is appropriate. To tackle this issue, approaches of data augmentation
implementing different variations of the DAGGER (?) technique have been
proposed and used (?, ?, ?, ?), but also criticized as they increase the
burden of generating additional optimal state-action pairs.

Finally, the question of how many different tasks and optimality principles
can be embedded in a single DNN via imitation learning remains open as work
addressing the issue has only been carried out preliminarily for
interplanetary trajectories (?) and drones (?, ?). These early results show
how the introduction of multiple tasks and environment variables encoded in
the extra parameters $\mathbf{p}$ seem to help in regularizing the
discontinuous behavior resulting from aggressive optimality principles as well
as in coping with unforeseen unmodeled external perturbations (see the later
section on onboard drone flight implementation).

### Approaches based on Deep Reinforcement Learning

A second approach suitable to learn the parameters $\theta$ of a G&CNet is
deep reinforcement learning (DRL). DRL captures a large variety of approaches
and numerical methods concerned with the problem of an agent learning from
experience, and not from expert demonstrations, a policy to perform a
specified task in its environment. The policy – often indicated with the
symbol $\pi_{\theta}(\mathbf{u}|\mathbf{x})$ – is represented by a DNN and
returns the probability to choose the control $\mathbf{u}$ given the agent
state $\mathbf{x}$. In a deterministic setting such a policy, when optimal,
must correspond to the solution of the related optimal control problem so that
one can formally write
$\pi^{*}_{\theta}(\mathbf{u}|\mathbf{x})=\delta(\mathbf{u}-\mathbf{u}^{*}(\mathbf{x}))$
where the Dirac delta has been employed to indicate certainty over choosing
the optimal feedback $\mathbf{u}^{*}$. In a stochastic setting, the DNN
typically outputs some statistical property of the policy, most commonly its
mean value – the variance being often considered constant. In order to use DRL
to train the parameters of a G&CNET, the continuous control problem has to be
modeled as an agent that learns through a sequential decision-making process,
a Markov Decision Problem (MDP), where the simulated environment includes all
types of uncertainties relevant to the particular mission phase considered.
Early works (?, ?), for example, applied this approach to the problem of
controlling a spacecraft hovering over an asteroid with an uncertain gravity
field and considering a stochastic dynamics perturbed by solar radiation
pressure acceleration as well as accounting for sensor noise. The approach was
later extended and refined to interplanetary transfers (?, ?), rendezvous and
docking (?, ?), planetary landing problems (?) as well as drone flights (?,
?). In all these cases the trained DNN is suitable for on-board utilization
and proved to be robust to different levels and types of stochastic effects.
While very promising, the DRL approach has much to prove in terms of actual
optimality. Optimality principles as well as terminal and path constraints are
all encapsulated in the so-called reward function driving most of the agent
learning. Engineering an appropriate reward function turns out to be
problematic in most cases and, when successful, it is unclear to what
optimality principle it corresponds to. This is not necessarily an issue when
optimality with respect to an assigned objective is not of primary concern,
but it is nevertheless something to be well aware of in most scenarios of
interest to space missions. Not surprisingly, the sub-optimality resulting
from the DRL approach is noted and quantified by the authors of successful
implementations (?, ?, ?). In this context, it may be argued how modern DRL
efforts do not seek to optimize a given objective function better than methods
based on optimal control theory, but that instead they intrinsically define a
better objective. We agree that this may be indeed the case, but only for
systems where uncertainties are prevailing and approaches grounded on the
underlying optimal control theory (i.e. Bellman equations) fail to provide
sufficient performances. A common criticism toward the DRL approach derives
from its intense computational requirements that can result in three orders of
magnitude larger computational times to find a policy with respect to, for
example, running one single optimal control solver (?). Finally, to the best
of our knowledge, there are no attempts to include in the DRL framework the
possibility to learn a class of policies and thus embed in the same deep
network multiple space tasks, objectives and constraints.

## Testing on Flying drones

The field of onboard guidance and control of space systems using deep neural
networks (DNNs), specifically the G&CNet architecture, is in its infancy. To
gain acceptance within the aerospace community as a potential improvement over
current guidance and control (G&C) schemes, convincing evidence of its
embedded capabilities is necessary, as well as of the possibility to offer
guarantees on the resulting system behavior. With much of the current research
on G&CNets focused on simulations, concerns are raised that the reality gap
may be overlooked.

Drone racing platforms share similarities with space systems, as they too have
limited onboard resources and require careful optimization of their
utilization. The time optimality principle in drone racing, coupled with the
complex dynamics of the drones, provides a valuable comparison to the mass
optimality principles preeminent in space missions. An ongoing effort is
underway to integrate G&CNets into quadcopter flight control systems, aiming
to achieve end-to-end control with optimal flight time and to increase the
trust in the use on-board spacecraft. Building upon research that employed
simplified quadcopter models in simulations (?, ?) and performed real-world
flight tests where G&CNets were utilized for longitudinal control (?), tests
have been conducted where a high-dimensional quadcopter model with sixteen
degrees of freedom was employed to compute the optimal-feedback for the
networks to imitate. The networks were then trained for end-to-end control,
which involved sending motor commands directly without any intermediate
controllers (?, ?). This approach granted the network complete control
authority, allowing it to handle actuator saturation directly and without
being constrained by an inner-loop controller as in previous attempts.
However, this also posed new challenges, as the time optimality principle
pursued resulted in aggressive maneuvers that were highly dependent on the
network’s ability to accurately replicate the ground truth optimal actions.
Due to the short dynamical timescale of the quadcopter flights considered (on
the order of seconds), even minor discrepancies in the network’s performance
significantly impacted the overall control accuracy. In hover-to-hover
flights, unmodeled moments caused the drone to take a sub-optimal path, diving
down and overshooting its target. Additionally, modeling errors accumulated
and caused deviations from the optimal plan, which destabilized the trajectory
(?).

Despite the difficulty in modeling the system dynamics, sensor measurements
onboard can be used to detect discrepancies between predicted and actual
forces and moments. This suggests to modify the G&CNet adding to its inputs
estimated unmodeled effects. A modified network
$\mathcal{N}_{\theta}(\mathbf{x},\mathbf{p})$ can then trained to approximate
the solution of a parametric optimal control problem where $\mathbf{p}$
represents the discrepancy between the modeled dynamics and the observed
behavior. By comparing the predicted and measured moments onboard and using
their difference as input to the network (?), G&CNets have been shown to adapt
to unexpected moments delivering a significant improvement in stability and
optimality, as illustrated during real flights of a Parrot™ AR 2.0 drone in
Figure 5a.

In (?), a similar approach was adopted, where the G&CNet was modified to
instead handle unexpected actuator saturations. It was demonstrated that the
knowledge of the actuator’s limits was crucial to remain on the optimal path
during high-speed successive waypoint flights. By estimating a model parameter
onboard (in this case, the maximum motor revolutions per minute) and feeding
it back into an additional neural network input, G&CNets can thus cope with
unmodeled effects, as shown in Figure 5b.

Additional parameters fed into a G&CNet can also represent different tasks.
For instance, in (?), a G&CNet is also trained to fly through two waypoints,
where the waypoint positions in space, boundary conditions to the optimal
control problem, can vary. When computing the state-action pairs to use in the
training dataset, different distances between waypoints are used, and the
network thus learns to represent the solution of the optimal control problem
specific to the parametric geometry it receives as additional input. During
flight, the network can then optimally plan a path through two waypoints,
where the second waypoint position is displaced, as illustrated in Figure 6.

G&CNets face significant challenges when highly aggressive or acrobatic
maneuvers are pursued on drones. The G&CNets here showcased during in real
flights were trained to imitate energy optimal control (?) or a mixture of
energy and time optimal control (?). Energy optimality was preferred as it
resulted in smoother trajectories, which were simpler to learn and execute.
However, moving towards more time-optimal trajectories also creates a
challenge as the optimal solution approaches a bang-bang profile, which is
increasingly difficult to learn (see Figure 3c), particularly for the small
networks used (?). Moreover, the aggressive commands will steer the drone
toward the edge of its flight envelope where the dynamics are most
unpredictable. Therefore the reality gap problem remains the biggest obstacle
to this approach in the context of aggressive maneuvering. Although the
adaptive networks have shown significant robustness improvement, additional
alterations are necessary to guarantee more general robustness for modeling
errors, sensor noise and delays.

These findings demonstrate that relatively small G&CNets, in this case a feed-
forward neural network with three hidden layers consisting of 120 neurons
each, are capable of representing a broad range of optimal control problems
and tasks effectively. The resulting G&CNets are able to cancel out, rather
than accumulate the errors made in-flight, both in simulation and on the real
quadcopter. This is in part possible because they can be made adaptive, but
also because they can be inferred at a high rate ($450$Hz) in real-time,
onboard of the drone (as measured on the Parrot P7 dual-core Cortex A9 CPU). A
Dual-core 800 MHz ARM Cortex-A9 processor is also currently orbiting on-board
the European Space Agency’s OPS-SAT satellite (?), thus making the results
achieved of particular interest here as they map closely to the space systems
with similar computational capabilities.

## Future works

Small neural networks have demonstrated, in several scenarios relevant to
space exploration, their ability to capture optimality principles and perform
various guidance and control tasks requiring significant levels of autonomy.
As the development of specialized accelerators for on-board inference
continues to grow (?), there is increasing interest in exploring which
additional capabilities can be integrated into larger networks. However, due
to the data-intensive nature of deep architectures, the efficient generation
of training examples is imperative for realizing the potential of larger
networks. End-to-end training of large models, when performed on-board
spacecraft, remains an open question, subject to availability of on-board
acceleration and the development of distributed learning systems as a key
enabling technology. (?) This could result in significant autonomy benefits
for future deep space missions, and recent interest in satellite swarms and
constellations may rapidly lead to new developments in this field.

The question of whether the training procedure of G&CNets should imitate
optimal examples or utilize a reinforcement learning paradigm remains open and
can today only be answered on a case-per-case basis, based on on the user’s
desired trade-off between computational efficiency, robustness, quest for
optimality and interpretability. While exploring the synergies between these
two approaches may lead to innovative, hybrid solutions, it is clear that this
topic will continue to fuel scientific discussions in the years to come.

Unresolved challenges remain regarding the complete qualification and
validation of artificial neural networks when embedded into mission-critical
systems like the guidance, navigation and control subsystem. To achieve
certification, end-to-end neural guidance and control implementations need to
demonstrate robustness to stochastic parametric and dynamic system
uncertainties, as well as compatibility with modern fault detection, isolation
and recovery (FDIR) routines that require both significant explainability and
adaptability. It is crucial to ensure that neural systems perform as intended
under a range of operating conditions and environments while meeting safety
and performance requirements comparable with modern day control solutions.
This involves rigorous testing and validation of the underlying models and
algorithms, as well as ensuring that the system can operate reliably in the
presence of uncertainties such as sensor noise, communication delays, and
other disturbances commonly faced in space applications. Fortunately, recent
developments in explainable artificial intelligence (XAI) offer new
possibilities for developing more comprehensive deep neural models that can
provide greater transparency and understanding of their capabilities and
limitations, which could ultimately unlock mission-critical certifications.
(?)

Neuromorphic technologies have recently emerged as promising enablers for on-
board edge computing and learning applications in space. These technologies
propose novel software and hardware designs inspired by biological neural
systems, with a focus on low-power and energy efficiency, which are highly
synergetic with space applications. The widespread availability of
neuromorphic Dynamic Vision sensors (?) and chips (?) has led to a recent
surge of publications on the use of event-based cameras and spiking neural
networks on-board spacecraft (?, ?, ?, ?), with an event-based sensor having
even recently been sent to the International Space Station (?). Of particular
interest for G&CNets is the neuromorphic promise to enable real-time
continuous learning, with the potential to revolutionize neural guidance and
control capabilities and robustness.

## Conclusions

In this study, we have reviewed a nascent trend in neural spacecraft guidance
and control that leverages an on-board deep artificial neural network (DNN) to
capture the correlation between the spacecraft’s state and its optimal
actions, inspired by the presence of optimality principles in human
sensorimotor actions. The proposed Guidance and Control Net (G&CNet)
architecture is computationally efficient, suitable for real-time on-board
processing and has shown great potential in representing complex optimal
state-feedback relations in various scenarios of interest while maintaining
many of the favorable attributes of more classical control methods.
Preliminary attempts to build trust in this approach have been presented that
successfully embed G&CNet on-board drones on hardware compatible with modern
space CPUs using time-optimal flights as a proxy for a real space guidance and
control system.

Looking ahead, we foresee the adoption of on-board neural guidance and control
becoming more widespread in the future, as it enables the necessary autonomy
to meet the ambitious goals of future space missions, while parsimoniously
utilizing on-board available resources.

Figure 1: Optimality principles determine the decision-making during different
phases of exploration missions. a) During an interplanetary phase, the
spacecraft dynamics is well identified. Uncertainties are limited and the
departure from a theoretical mass optimal guidance is of less importance also
thanks to the relatively slow dynamics involved. b) During a landing phase,
according to the specific mission profile, the adaptiveness and robustness of
the planned actions have a larger impact on the mission success, also
considering that human operators are typically too far away to allow re-
planning within an acceptable timeframe. c) During a planetary exploration
phase (e.g. rovers or flying drones) uncertainties are larger and optimality
principles such as careful use of available onboard energy need to be embedded
into highly disturbed and fast dynamics. Figure 2: G&CNets have a similar role
to Model Predictive Control in the architecture of an autonomous mission. A)
MPC iteratively solves on-board optimal control problems predicting state and
actions over a defined time horizon, based on an existing system model. This
results in possible optimality guarantees with full predictive information, at
the expense of significant on-board computational burden determined by the
complexity of the system model and optimal control problem to be solved. B) A
G&CNet inference directly transforms the system state into actions. B.1) When
trained using RL, an agent learns from experience the final probabilistic
policy, based on a critical reward-feedback loop with the environment. The
resulting architecture can be resilient to stochastic disturbances but is
often based on engineered reward functions that depart from the original
optimality principle assigned. B.2) When trained via supervised learning the
network captures a clear optimality principle in its structure, directly
inferring optimal actions from the state feedback at high frequency. Such a
solution allows for fast direct inference with limited hardware requirements
and is possibly subject to instability and lack of robustness when the state
falls outside the set used to train the network.  Figure 3: Challenges in
approximating optimal feedback with a G&CNet. a) Optimal control tasks can
have very high-dimensional solutions. Already in simple precession control, a
complex structure emerges. In this case, the task is to lead in the shortest
possible time, a precessing satellite to a uniform rotation around its
symmetry axis, thus canceling the components $\omega_{x},\omega_{y}$ of its
angular velocity. The resulting deterministic optimal control problem is one
rare case where an analytical solution can be derived, allowing us to peek
into the structure of the optimal policy over the entire state space.
According to the values of $\omega_{x},\omega_{y}$ the thrusters are switching
direction in correspondence of a complex and discontinuous switching line.
Resulting time-optimal trajectories are shown in color.b) The optimality
principle pursued affects the resulting control profile and its gradient. Here
the optimal control commands from energy-optimal to time-optimal quadcopter
landings are shown (?). c) Smooth control profiles result in smaller errors
compared to non-smooth bang-bang profiles when approximated by a G&CNET.
Figure 4: The backward generation of optimal examples (BGOE) technique, allows
to generate orders of magnitude larger datasets by perturbing one nominal
solution. a) The nominal solution for the case of a time-optimal transfer from
the asteroid belt to Earth (visualized in a rotating frame). b) Two bundles of
200,000 optimal trajectories found applying BGOE to the nominal solution.
Larger perturbations of the nominal trajectory result in better coverage of
conditions close to the Earth (short bundle), which reduces the likelihood
that the spacecraft lands outside of the training data (?). For comparison,
the generation of all 400,000 trajectories uses the same numerical resources
used to generate one nominal optimal solution.  Figure 5: G&CNets robustness
to model mismatch. Two examples of real autonomous flights of a Parrot™ AR
drone 2.0 in the TU Delft Cyberzoo: a) Unmodeled moments are detected in real-
time on-board and fed back to the G&CNet. b) Unexpected early saturation of
the motor revolutions per minute is present. The saturation is estimated on-
board and fed back to the G&CNet. In both cases, the improvements with respect
to the non-parametric version are evident. The initial drone position is also
shown with a white border. Figure 6: Embedding multiple task in one G&CNet.
Real autonomous flights of a Parrot™ AR drone 2.0 in the TU Delft Cyberzoo.
During this specific test, the same G&CNet is shown to have learned to imitate
the optimal feedback in two distinct tasks differing in the final waypoint
position. The position of the next waypoint is fed to the DNN as an extra
parameter. The initial drone position is also shown with a white border.

## References and Notes

  * 1. E. Todorov, M. I. Jordan, Optimal feedback control as a theory of motor coordination, Nature neuroscience 5, 1226 (2002).
  * 2. U. Eren, et al., Model predictive control in aerospace systems: Current state and opportunities, Journal of Guidance, Control, and Dynamics 40, 1541 (2017).
  * 3. B. Açıkmeşe, J. M. Carson, L. Blackmore, Lossless convexification of nonconvex control bound and pointing constraints of the soft landing optimal control problem, IEEE Transactions on Control Systems Technology 21, 2104 (2013).
  * 4. E. Todorov, Optimality principles in sensorimotor control, Nature Neuroscience 7, 907 (2004).
  * 5. C. Sánchez-Sánchez, D. Izzo, Real-time optimal control via deep neural networks: study on landing problems, Journal of Guidance, Control, and Dynamics 41, 1122 (2018).
  * 6. D. Tailor, D. Izzo, Learning the optimal state-feedback via supervised imitation learning, Astrodynamics 3, 361 (2019).
  * 7. D. Izzo, M. Märtens, B. Pan, A survey on artificial intelligence trends in spacecraft guidance dynamics and control, Astrodynamics 3, 287 (2019).
  * 8. A. Zavoli, L. Federici, Reinforcement learning for low-thrust trajectory design of interplanetary missions, arXiv preprint arXiv:2008.08501 (2020).
  * 9. J. Vreeburg, Spacecraft maneuvers and slosh control, IEEE Control Systems Magazine 25, 12 (2005).
  * 10. M. Reyhanoglu, J. Rubio Hervas, Nonlinear control of a spacecraft with multiple fuel slosh modes, 2011 50th IEEE Conference on Decision and Control and European Control Conference (2011), pp. 6192–6197.
  * 11. P. Servidia, R. Pena, Spacecraft thruster control allocation problems, IEEE Transactions on Automatic Control 50, 245 (2005).
  * 12. W. Cai, X. H. Liao, Y. D. Song, Indirect robust adaptive fault -tolerant control for attitude tracking of spacecraft, Journal of Guidance, Control, and Dynamics 31, 1456 (2008).
  * 13. N. Zhou, Y. Kawano, M. Cao, Neural network-based adaptive control for spacecraft under actuator failures and input saturations, IEEE Transactions on Neural Networks and Learning Systems 31, 3696 (2020).
  * 14. S. Yin, B. Xiao, S. X. Ding, D. Zhou, A review on recent development of spacecraft attitude fault tolerant control system, IEEE Transactions on Industrial Electronics 63, 3311 (2016).
  * 15. J. Melman, E. Mooij, R. Noomen, State propagation in an uncertain asteroid gravity field, Acta Astronautica 91, 8 (2013).
  * 16. Y. Ren, J. Shan, Reliability-based soft landing trajectory optimization near asteroid with uncertain gravitational field, Journal of Guidance, Control, and Dynamics 38, 1810 (2015).
  * 17. H. F. Grip, et al., Guidance and Control for a Mars Helicopter, 2018 AIAA Guidance, Navigation, and Control Conference (American Institute of Aeronautics and Astronautics, 2018).
  * 18. H. F. Grip, et al., Flight control system for NASA's mars helicopter, AIAA Scitech 2019 Forum (American Institute of Aeronautics and Astronautics, 2019).
  * 19. J. Balaram, M. Aung, M. P. Golombek, The Ingenuity Helicopter on the Perseverance Rover, Space Science Reviews 217 (2021).
  * 20. L. S. Pontryagin, V. G. Botlyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes (John Wiley & Sons, 1962).
  * 21. D. Izzo, R. Bevilacqua, C. Valente, Internal mesh optimization and runge-kutta collocation in a direct transcription method applied to interplanetary missions, 55th International Astronautical Congress of the International Astronautical Federation (2004).
  * 22. B. A. Conway, Spacecraft trajectory optimization, vol. 29 (Cambridge University Press, 2010).
  * 23. D. Lawden, Optimal Trajectories For Space Navigation. (Butterworth, 1963).
  * 24. T. Edelbaum, How many impulses/ques, 3rd and 4th Aerospace Sciences Meeting (1967), p. 7.
  * 25. J. E. Prussing, Optimal impulsive linear systems: Sufficient, The Journal of the Astronautical Sciences 43, 195 (1995).
  * 26. T. E. Carter, Necessary and sufficient conditions for optimal impulsive rendezvous with linear equations of motion, Dynamics and control 10, 219 (2000).
  * 27. E. Taheri, J. L. Junkins, How many impulses redux, The Journal of the Astronautical Sciences 67, 257 (2020).
  * 28. R. Bellman, R. E. Kalaba, et al., Dynamic programming and modern control theory, vol. 81 (Citeseer, 1965).
  * 29. E. Todorov, et al., Optimal control theory, Bayesian brain: probabilistic approaches to neural coding pp. 268–298 (2006).
  * 30. M. Bardi, I. C. Dolcetta, et al., Optimal control and viscosity solutions of Hamilton-Jacobi-Bellman equations, vol. 12 (Springer, 1997).
  * 31. O. Calin, Deep Learning Architectures (Springer, 2020), pp. 251–284.
  * 32. B. Mildenhall, et al., Nerf: Representing scenes as neural radiance fields for view synthesis, Communications of the ACM 65, 99 (2021).
  * 33. D. Izzo, P. Gómez, Geodesy of irregular small bodies via neural density fields, Communications Engineering 1, 48 (2022).
  * 34. G. Furano, et al., Towards the use of artificial intelligence on the edge in space systems: Challenges and opportunities, IEEE Aerospace and Electronic Systems Magazine 35, 44 (2020).
  * 35. G. Giuffrida, et al., The phi-sat-1 mission: The first on-board deep neural network demonstrator for satellite earth observation, IEEE Transactions on Geoscience and Remote Sensing 60, 1 (2022).
  * 36. G. Labrèche, et al., OPS-SAT Spacecraft Autonomy with TensorFlow Lite, Unsupervised Learning, and Online Machine Learning, 2022 IEEE Aerospace Conference (2022).
  * 37. A. S. Danielsen, T. A. Johansen, J. L. Garrett, Self-Organizing Maps for Clustering Hyperspectral Images On-Board a CubeSat, Remote Sensing 13, 4174 (2021).
  * 38. R. Pitonak, J. Mucha, L. Dobis, M. Javorka, M. Marusin, CloudSatNet-1: FPGA-Based Hardware-Accelerated Quantized CNN for Satellite On-Board Cloud Coverage Classification, Remote Sensing 14, 3180 (2022).
  * 39. B. Denby, B. Lucia, Orbital edge computing: Nanosatellite constellations as a new class of computer system, Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems (2020), pp. 939–954.
  * 40. F. C. Bruhn, N. Tsog, F. Kunkel, O. Flordal, I. Troxel, Enabling radiation tolerant heterogeneous GPU-based onboard data processing in space, CEAS Space Journal 12, 551 (2020).
  * 41. O. Mulekar, R. Bevilacqua, H. Cho, Metric to evaluate distribution shift from behavioral cloning for fuel-optimal landing policies, Acta Astronautica 203, 421 (2023).
  * 42. R. Furfaro, et al., Deep learning for autonomous lunar landing, 2018 AAS/AIAA Astrodynamics Specialist Conference (Univelt, 2018), vol. 167, pp. 3285–3306.
  * 43. L. Cheng, Z. Wang, Y. Song, F. Jiang, Real-time optimal control for irregular asteroid landings using deep neural networks, Acta Astronautica 170, 66 (2020).
  * 44. D. Izzo, E. Öztürk, Real-time guidance for low-thrust transfers using deep neural networks, Journal of Guidance, Control, and Dynamics 44, 315 (2021).
  * 45. D. Izzo, S. Origer, Neural representation of a time optimal, constant acceleration rendezvous, Acta Astronautica (2022).
  * 46. H. Li, H. Baoyin, F. Topputo, Neural networks in time-optimal low-thrust interplanetary transfers, IEEE Access 7, 156413 (2019).
  * 47. L. Cheng, Z. Wang, F. Jiang, C. Zhou, Real-time optimal control for spacecraft orbit transfer via multiscale deep neural networks, IEEE Transactions on Aerospace and Electronic Systems 55, 2436 (2018).
  * 48. L. Federici, B. Benedikter, A. Zavoli, Deep learning techniques for autonomous spacecraft guidance during proximity operations, Journal of Spacecraft and Rockets 58, 1774 (2021).
  * 49. A. Rubinsztejn, R. Sood, F. E. Laipert, Neural network optimal control in astrodynamics: Application to the missed thrust problem, Acta astronautica 176, 192 (2020).
  * 50. D. Izzo, D. Tailor, T. Vasileiou, On the stability analysis of deep neural network representations of an optimal state feedback, IEEE Transactions on Aerospace and Electronic Systems 57, 145 (2020).
  * 51. E. Trélat, Optimal control and applications to aerospace: some results and challenges, Journal of Optimization Theory and Applications 154, 713 (2012).
  * 52. O. Mulekar, H. Cho, R. Bevilacqua, Six-degree-of-freedom optimal feedback control of pinpoint landing using deep neural networks, AIAA SCITECH 2023 Forum (2023), p. 0689.
  * 53. S. Ross, G. Gordon, D. Bagnell, A reduction of imitation learning and structured prediction to no-regret online learning, Proceedings of the fourteenth international conference on artificial intelligence and statistics (JMLR Workshop and Conference Proceedings, 2011), pp. 627–635.
  * 54. C. I. Sprague, D. Izzo, P. Ögren, Learning dynamic-objective policies from a class of optimal trajectories, 2020 59th IEEE Conference on Decision and Control (CDC) (IEEE, 2020), pp. 597–602.
  * 55. S. Origer, C. De Wagter, R. Ferede, G. C. de Croon, D. Izzo, Guidance & control networks for time-optimal quadcopter flight, arXiv preprint arXiv:2305.02705 (2023).
  * 56. R. Ferede, G. C. de Croon, C. De Wagter, D. Izzo, An adaptive control strategy for neural network based optimal quadcopter controllers, arXiv preprint arXiv:2304.13460 (2023).
  * 57. B. Gaudet, R. Furfaro, Robust spacecraft hovering near small bodies in environments with unknown dynamics using reinforcement learning, AIAA/AAS Astrodynamics Specialist Conference, p. 5072.
  * 58. S. Willis, D. Izzo, D. Hennes, Reinforcement learning for spacecraft maneuvering near small bodies, AAS/AIAA Space Flight Mechanics Meeting (2016), vol. 158, pp. 1351–1368.
  * 59. D. Miller, J. A. Englander, R. Linares, Interplanetary low-thrust design using proximal policy optimization, 2019 AAS/AIAA Astrodynamics Specialist Conference, no. GSFC-E-DAA-TN71225 (2019).
  * 60. H. Yuan, D. Li, Deep reinforcement learning for rendezvous guidance with enhanced angles-only observability, Aerospace Science and Technology 129, 107812 (2022).
  * 61. C. E. Oestreich, R. Linares, R. Gondhalekar, Autonomous six-degree-of-freedom spacecraft docking with rotating targets via reinforcement learning, Journal of Aerospace Information Systems 18, 417 (2021).
  * 62. R. Furfaro, R. Linares, Waypoint-based generalized zem/zev feedback guidance for planetary landing via a reinforcement learning approach, 3rd International Academy of Astronautics Conference on Dynamics and Control of Space Systems, DyCoSS 2017 (Univelt Inc., 2017), pp. 401–416.
  * 63. Y. Song, M. Steinweg, E. Kaufmann, D. Scaramuzza, Autonomous drone racing with deep reinforcement learning, 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (IEEE, 2021), pp. 1205–1212.
  * 64. A. T. Azar, et al., Drone deep reinforcement learning: A review, Electronics 10, 999 (2021).
  * 65. S. Li, E. Öztürk, C. De Wagter, G. C. De Croon, D. Izzo, Aggressive online control of a quadrotor via deep network representations of optimality principles, 2020 IEEE International Conference on Robotics and Automation (ICRA) (IEEE, 2020), pp. 6282–6287.
  * 66. D. Evans, M. Merri, OPS-SAT: A ESA nanosatellite for accelerating innovation in satellite control, SpaceOps 2014 Conference (2014), p. 1702.
  * 67. B. McMahan, E. Moore, D. Ramage, S. Hampson, B. A. y Arcas, Communication-efficient learning of deep networks from decentralized data, Artificial intelligence and statistics (PMLR, 2017), pp. 1273–1282.
  * 68. A. Barredo Arrieta, et al., Explainable artificial intelligence (xai): Concepts, taxonomies, opportunities and challenges toward responsible ai, Information Fusion 58, 82 (2020).
  * 69. C. Brandli, R. Berner, M. Yang, S.-C. Liu, T. Delbruck, A 240 × 180 130 db 3 µs latency global shutter spatiotemporal vision sensor, IEEE Journal of Solid-State Circuits 49, 2333 (2014).
  * 70. M. Davies, et al., Loihi: A neuromorphic manycore processor with on-chip learning, IEEE Micro 38, 82 (2018).
  * 71. T.-J. Chin, S. Bagchi, A. Eriksson, A. van Schaik, Star tracking using an event camera, 2019 IEEE/CVF Conference on Computer Vision and Pattern Recognition Workshops (CVPRW) (IEEE, 2019).
  * 72. O. Sikorski, D. Izzo, G. Meoni, Event-based spacecraft landing using time-to-contact, 2021 IEEE/CVF Conference on Computer Vision and Pattern Recognition Workshops (CVPRW) (2021), pp. 1941–1950.
  * 73. S. McLeod, et al., Lecture Notes in Computer Science (Springer Nature Switzerland, 2023), pp. 3–20.
  * 74. L. Azzalini, E. Blazquez, A. Hadjiivanov, G. Meoni, D. Izzo, On the generation of synthetic event-based vision datasets for navigation and landing, 9th International Conference on Astrodynamics Tools and Techniques (ICATT) (2023).
  * 75. M. G. McHarg, et al., Falcon neuro: an event-based sensor on the international space station, Optical Engineering 61 (2022).


reflect monomorphisms and epimorphisms). As for stability, we use that the
inclusion $i:\mathsf{ppTree}\hookrightarrow{\sf Struct}_{*}(\sigma)$, being
fully faithful, reflect limits. This means that given a cone
$\lambda:X\Rightarrow J$ over a diagram $J:I\to\mathsf{ppTree}$, if $\lambda$
is a limit cone over $J$ when seen in ${\sf Struct}_{*}(\sigma)$, then it is
also a limit cone when seen in $\mathsf{ppTree}$. Thus, if we check that the
pullback of pp-trees is also a pp-tree, that means that the pullback of pp-
trees in ${\sf Struct}_{*}(\sigma)$ is the pullback in $\mathsf{ppTree}$, and
then since the factorisation system is stable in ${\sf Struct}_{*}(\sigma)$
(pullbacks of $\mathscr{Q}$-morphisms along $\mathscr{M}$-morphisms exist and
are $\mathscr{Q}$-morphisms), its restriction to $\mathsf{ppTree}$ will be
stable as well.

Recall that given a diagram in ${\sf Struct}_{*}(\sigma)$, its limit has as
universe the set-theoretical limit of the underlying universes (since the
forgetful functor to $\mathsf{Set}$ is a right adjoint). Thus it is easy to
check that the categorical product of relational structures coincides with the
standard notion of product of structures, 202020The universe of a product is
the product of the universes and interpretations of relations in a product
structure are the conjunction of interpretations in the factor structures.
while it is also easy to check that the categorical equaliser of two
relational homomorphisms $f,g:(\mathcal{A},a)\to(\mathcal{B},b)$ can be
constructed as the embedded substructure $(\mathcal{Z},z)\to(\mathcal{A},a)$
consisting of points $a^{\prime}\in|\mathcal{A}|$ such that
$f(a^{\prime})=g(a^{\prime})$. It is straightforward to verify that product of
two pp-trees is a pp-tree and that the equaliser of two homomorphisms between
pp-trees is also a pp-tree. 212121Consider two homomorphisms
$f,g:(\mathcal{A},a)\to(\mathcal{B},b)$ between trees such that
$f(a^{\prime})=g(a^{\prime})$ for some $a^{\prime}\in|\mathcal{A}|$. If
$a^{\prime}\neq a$, let $a^{\prime\prime}$ be the unique predecessor of
$a^{\prime}$. Then $f(a^{\prime\prime})=g(a^{\prime\prime})$ as well, since
otherwise $f(a^{\prime})=g(a^{\prime})$ would have two predecessors in
$\mathcal{B}$. Thus the equaliser of the homomorphisms is a subtree of the
domain. Hence, since a pullback is nothing more than the equalizer of a
product of homomorphisms, the pullback of two pp-trees is also a pp-tree. ∎

######  Proposition C.14.

$\mathsf{ppTree}$ is a path category.

###### Proof.

We have just seen that $(\mathscr{M},\mathscr{Q})$ as above is a stable proper
factorisation system for $\mathsf{ppTree}$. To see that $\mathsf{ppTree}$ has
all coproducts of small families of paths, we show that _a fortiori_ all small
coproducts exist in $\mathsf{ppTree}$. Recall that finite coproducts exist in
${\sf Struct}_{*}(\sigma)$. The universe of the binary coproduct
$(\mathcal{A},a)\amalg(\mathcal{B},b)$ is formed by taking the disjoint union
of the universes $|\mathcal{A}|$ and $|\mathcal{B}|$, and then identifying the
basepoints. A relation $R$ holds on a tuple of points in this universe iff all
the points can be traced back to either $\mathcal{A}$ or $\mathcal{B}$
exclusively, and moreover the tuple belonged to the interpretation of $R$ in
that structure.

Now, from the description above it should be clear that if $(\mathcal{A},a)$
and $(\mathcal{B},b)$ are pp-trees, then
$(\mathcal{A},a)\amalg(\mathcal{B},b)$ is too: it is a tree with height equal
to the maximum of the heights of the starting trees, and if a tuple belongs to
a relation, then that must have been the case in one of the starting
structures and thus the tuple constitutes a path in the structure. Finally,
because inclusions of categories reflect colimits,
$(\mathcal{A},a)\amalg(\mathcal{B},b)$ must also be the categorical coproduct
in $\mathsf{ppTree}$.

This establishes the existence of all finite coproducts. To extend this to all
small coproducts, note that the above construction can be generalized in a
straightforward way to a nonempty collection of $\mathbb{C}_{k}$-coalgebras.
As for the empty collection, its coproduct is the initial object, which is the
one-element universe in which no relations hold.

Finally, to see that $\mathsf{ppTree}$ satisfies the two out of three property
for paths, start by noticing that in a path there is exactly zero or one
element for each height. Homomorphisms between paths are injective, and thus
they preserve and reflect height. Given paths $P,Q,R$, homomorphisms
$P\xrightarrow{f}Q\xrightarrow{g}R$ such that $g\circ f$ is a
$\mathscr{Q}$-morphism (i.e. a surjective homomorphism) and given $q\in Q$,
let $p\in P$ be the preimage of $g(q)$. Then $f(p)=q$ since $q$ is the only
element of $Q$ of the appropriate height. Thus $f$ is also a
$\mathscr{Q}$-morphism. ∎

###### Proof of Lemma C.12.

We have already seen that $\mathsf{ppTree}$ is a path category. That every
path in $\mathsf{ppTree}$ is connected is straightforward from the
construction of small coproducts above, since a coproduct of paths
$\amalg_{i\in I}P_{i}$ is a tree whose only branching node (point with more
than one successor) is the root node. Thus the image of a homomorphism
$Q\to\amalg_{i\in I}P_{i}$ lies entirely in one of the $P_{i}$.

Let us now see that every object of $\mathsf{ppTree}$ is path-generated. Given
$(\mathcal{A},a)\in\mathsf{ppTree}$, consider the diagram
$\Pi_{(\mathcal{A},a)}:(\mathsf{ppTree}/(\mathcal{A},a))_{\mathscr{M}}\to\mathsf{ppTree}$
of all path embeddings into $(\mathcal{A},a)$, and consider the canonical
cocone under that diagram $\eta:\Pi_{(\mathcal{A},a)}\Rightarrow X$ whose leg
$\eta_{(P,f)}$ is $f$. In order to prove that this is a colimit cocone in
$\mathsf{ppTree}$, by taking representatives, we can assume that all paths $P$
in the diagram are embedded relational substructures inside $\mathcal{A}$, and
thus the legs of this cocone are the corresponding inclusions $i_{P}$. Now
consider a generic cocone
$\lambda:\Pi_{(\mathcal{A},a)}\Rightarrow(\mathcal{B},b)$ in $\mathsf{ppTree}$
over the same diagram, this time with nadir $(\mathcal{B},b)$. We must show
existence of a unique homomorphism $\varphi:(\mathcal{A},a)\to(\mathcal{B},b)$
such that it commutes with the legs of the cocones.

${P}$${Q}$${(\mathcal{A},a)}$${(\mathcal{B},b)}$$\scriptstyle{i_{P}}$$\scriptstyle{i_{Q}}$$\scriptstyle{\lambda_{P}}$$\scriptstyle{\lambda_{Q}}$$\scriptstyle{\exists!\varphi}$

Given $a^{\prime}\in|\mathcal{A}|$, let $\mathcal{A}_{a^{\prime}}$ denote the
unique path from $a$ to $a^{\prime}$. It is clear that if $\varphi$ exists,
then it must send
$a^{\prime}\mapsto\lambda_{\mathcal{A}_{a^{\prime}}}(a^{\prime})$. This choice
of $\varphi$ makes the corresponding triangles commute (i.e. $\varphi\circ
i_{P}=\lambda_{P}$); indeed, for any path $P$ containing $a^{\prime}$, it must
be the case that $\mathcal{A}_{a^{\prime}}\subseteq P$ and thus $\lambda_{P}$
and $\lambda_{\mathcal{A}_{a^{\prime}}}$ agree on $a^{\prime}$ since $\lambda$
is a cocone.

Now let us see that $\varphi$ is a homomorphism. It is straightforward that
$\varphi(a)=b$. To see that $\varphi$ preserves relations, let $R\in\sigma$ be
of arity $n$ and assume $R^{\mathcal{A}}(a_{1},\dots,a_{n})$ holds. Then
$a_{1},\dots,a_{n}$ must be all contained in $\mathcal{A}_{a_{n}}$, and thus
since $\lambda_{\mathcal{A}_{a_{n}}}$ is a homomorphism, it must be that
$R^{\mathcal{B}}(\lambda_{\mathcal{A}_{a_{n}}}(a_{1}),\dots,\lambda_{\mathcal{A}_{a_{n}}}(a_{n}))$,
i.e. $R^{\mathcal{B}}(\varphi(a_{1}),\dots,\varphi(a_{n}))$. ∎

Finally, a small observation completes the proof of Theorem C.11.

###### Proof of Theorem C.11.

We have just proven that $\mathsf{ppTree}$ is arboreal. By Remark C.3, for
every $k$, the full subcategory of paths in $\mathsf{ppTree}$, which we denote
by $\mathsf{ppTree}_{p}$, consists of those pp-trees which are moreover total
orders. Let $\mathsf{ppTree}_{p}^{k}$ be the full subcategory of
$\mathsf{ppTree}_{p}$ of paths of length at most $k$. This is clearly closed
under embeddings. It is also straightforward that $\mathsf{ppTree}_{p}^{k}$
embeds into $\mathsf{ppTree}_{p}^{k+1}$ for all $k$.

To show that $\\{\text{\sf{EM}}(\mathcal{C}_{k})\\}_{k\in\mathbb{N}}$ is a
resource-indexed arboreal category, we must see that the objects of
$\text{\sf{EM}}(\mathbb{C}_{k})$ are precisely those objects whose cocone of
path embeddings with domain in $\mathsf{ppTree}_{p}^{k}$ is a colimit cocone
in $\mathsf{ppTree}$. To this end, it is enough to show that in the proof of
Lemma C.12, if the object of $\mathsf{ppTree}$, in particular a tree, has
height at most $k$ and thus belongs to $\text{\sf{EM}}(\mathbb{C}_{k})$, then
all the paths in the diagram are actually objects of
$\mathsf{ppTree}_{p}^{k}$, that is, they all have length at most $k$. Indeed,
a path of length $>k$ cannot be embedded into a tree of height $\leq k$. Thus,
for $(\mathcal{A},a)\in\text{\sf{EM}}(\mathbb{C}_{k})$, the cocone of path
embeddings with codomain $(\mathcal{A},a)$ which was shown above to be a
colimit cocone in $\mathsf{ppTree}$ is also the cocone of path embeddings with
nadir $(\mathcal{A},a)$ and domains in $\mathsf{ppTree}_{p}^{k}$. ∎

### The abstract back-and-forth game in $\mathsf{ppTree}_{k}$ is the ${\rm
PPML}$ Bisimulation game

We now reproduce from [4] the definition of the abstract back-and-forth game
between objects of an arboreal category.

######  Definition C.15.

Let $\mathscr{C}$ be an arboreal category and let $X,Y\in\mathscr{C}$. The
_back-and-forth game_ $\mathscr{G}(X,Y)$ between $X$ and $Y$ is defined as
follows.

The game is played between two players, called Spoiler and Duplicator. The
state of the game at round $\ell$ is given by a pair of (equivalence classes
of) path embeddings $([m],[n])\in\mathbb{P}X\times\mathbb{P}Y$. We say that
$([m],[n])$ satisfies the _winning condition_ if the domains ${\rm dom}(m)$
and ${\rm dom}(n)$ are isomorphic.

The initial position is $(\bot_{X},\bot_{Y})$ where $\bot_{X}\colon P\to X$
and $\bot_{Y}\colon Q\to Y$ are the roots of $\mathbb{P}{X}$ and
$\mathbb{P}{Y}$, respectively. If $P$ and $Q$ are not isomorphic, then
Duplicator loses the game. Otherwise, assuming position
$([m],[n])\in\mathbb{P}{X}\times\mathbb{P}{Y}$ is reached after $\ell\geq 0$
rounds, position $\ell+1$ is determined as follows: either Spoiler chooses
some $[m^{\prime}]\succ[m]$ and Duplicator must respond with some
$[n^{\prime}]\succ[n]$, or Spoiler chooses some $[n^{\prime\prime}]\succ[n]$
and Duplicator must respond with $[m^{\prime\prime}]\succ[m]$. We say that
Duplicator wins the round $\ell+1$ if Duplicator is able to respond with a
move which is valid according to the preceding description and which moreover
makes the resulting state satisfy the winning condition. Otherwise, the game
ends and Duplicator loses immediately. A winning strategy for Duplicator
consists in a choice of a response that makes Duplicator win the round
$\ell+1$ for every move that Spoiler may make after any number of rounds
$\ell>0$.

Recall that each category in a resource-indexed arboreal category is in
particular arboreal. Thus we can speak of the back-and-forth-game in each
category $\text{\sf{EM}}(\mathbb{C}_{k})$.

######  Proposition C.16.

The $k$-round bisimulation game for ${\rm PPML}$ played between
$(\mathcal{A},a)$ and $(\mathcal{B},b)$,
$\mathcal{G}_{k}((\mathcal{A},a),(\mathcal{B},b))$, is equivalent to the back-
and-forth game
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$ in
the arboreal category $\text{\sf{EM}}(\mathbb{C}_{k})$ played between
$\mathbb{C}_{k}(\mathcal{A},a)$ and $\mathbb{C}_{k}(\mathcal{B},b)$. More
precisely, there exists a winning strategy for Duplicator in one of the two
games iff there exists one in the other.222222Although the proof given does
prove a certain equivalence between the games themselves, our precise
statement is given in terms of existence of winning strategies since this is
all we need and we do not present a formal notion of equivalence between
games.

###### Proof.

A position in the abstract back-and-forth game
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$ is
a pair
$([m],[n])\in\mathbb{P}\mathbb{C}_{k}(\mathcal{A},a)\times\mathbb{P}\mathbb{C}_{k}(\mathcal{B},b)$,
which by Remark C.4 can be seen as a pair of elements from
$\mathbb{C}_{k}\mathbb{C}_{k}(\mathcal{A},a)\times\mathbb{C}_{k}\mathbb{C}_{k}(\mathcal{B},b)$.
But $\mathbb{C}_{k}$ is idempotent, thus $\delta$ gives an identification
between positions $(m,n)$ in
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$ and
positions
$(s,t)\in\mathbb{C}_{k}(\mathcal{A},a)\times\mathbb{C}_{k}(\mathcal{B},b)$ in
the game in $\mathcal{G}_{k}((\mathcal{A},a),(\mathcal{B},b))$. This
correspondence also maps the starting position
$(\bot_{\mathbb{C}_{k}(\mathcal{A},a)},\bot_{\mathbb{C}_{k}(\mathcal{A},a)})$
of $\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$
to the starting position $([a],[b])$ of
$\mathcal{G}_{k}((\mathcal{A},a),(\mathcal{B},b))$. On the other hand, the
procedures by which a new position is obtained from the previous one in each
game coincide under this identification, and both games end after the $k$-th
round, since in the definition of
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$, it
is left implicit that the game can only continue if Spoiler has a valid move
to make, and Spoiler will not have such a valid move after playing the $k$-th
round. We thus reach the conclusion that
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$ can
be regarded as being the same as
$\mathcal{G}_{k}((\mathcal{A},a),(\mathcal{B},b))$, except for a possibly
different winning condition for Duplicator. We focus now on showing that the
two winning conditions are indeed equivalent.

Through the above mentioned correspondence, the winning condition of
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$,
namely that ${\rm dom}([m])\simeq{\rm dom}([n])$, can be restated as
corresponding to positions $(s,t)$ that satisfy

  * ($*$)

The embedded substructures
$(\mathbb{C}_{k}\mathcal{A})_{s}\subseteq\mathbb{C}_{k}(\mathcal{A},a)$ and
$(\mathbb{C}_{k}\mathcal{B})_{t}\subseteq\mathbb{C}_{k}(\mathcal{A},a)$, whose
points are the prefixes of $s$ and $t$, respectively, are isomorphic.

Thus we must show that for any position $(s,t)$ that is reachable during the
game, condition ($*$) is satisfied if and only if condition ($**$) below
holds:

  * ($**$)

for all $R\in\sigma$ of arity $R\leq\ell+1$, ${\rm last}_{n}(s)\in
R^{\mathcal{A}}\iff{\rm last}_{n}(t)\in R^{\mathcal{B}}$;

where $|s|=|t|=\ell+1$. We prove this by induction. The base case for
$([a],[b])$ is immediate. Now assume the result holds for any position
$(s,t)=([a_{0},\dots,a_{\ell}],[b_{0},\dots,b_{\ell}])$ obtained during round
$\ell$. If this position does not satisfy any of the two winning conditions
(and therefore, by inductive hypothesis, none of them), then Duplicator loses
the game and there is no next position to analyse. Otherwise, Duplicator wins
that round and the game progresses to round $\ell+1$. Let
$(s^{\prime},t^{\prime})=(s.a_{\ell+1},t.b_{\ell+1})$ be the next position.
Let $s_{j}:=[a_{0},\dots,a_{j}]$ and $t_{j}:=[b_{0},\dots,b_{j}]$ where
$j\in\\{0,\dots,\ell+1\\}$.

First let us see that condition ($*$) implies condition ($**$). For this, the
inductive hypothesis is not needed. Assuming that ($*$) holds for
$(s^{\prime},t^{\prime})$, given $R$ of arity $n\leq\ell+2$, we have that

$\displaystyle{\rm last}_{n}(s^{\prime})\in R^{\mathcal{A}}$
$\displaystyle\iff[s_{\ell+2-n},\dots,s^{\prime}]\in
R^{\mathbb{C}_{k}\mathcal{A}}$ (Def. $R^{\mathbb{C}_{k}\mathcal{A}}$)
$\displaystyle\iff[t_{\ell+2-n},\dots,t^{\prime}]\in
R^{\mathbb{C}_{k}\mathcal{B}}$ ($*$) $\displaystyle\iff{\rm
last}_{n}(t^{\prime})\in R^{\mathcal{B}}.$ (Def.
$R^{\mathbb{C}_{k}\mathcal{B}}$)

In the other direction, by contrapositive, assume that condition ($*$) does
_not_ hold for $(s^{\prime},t^{\prime})$. Then there exist $R\in\sigma$ of
arity $n$ and $j_{1},\dots,j_{n}\in\\{0,\dots,\ell+1\\}$ such that
$(s_{j_{1}},\dots,s_{j_{n}})\in R^{\mathbb{C}_{k}\mathcal{A}}$ and
$(t_{j_{1}},\dots,t_{j_{n}})\not\in R^{\mathbb{C}_{k}\mathcal{B}}$, or
viceversa. Given the definitions of $R^{\mathbb{C}_{k}\mathcal{A}}$ and
$R^{\mathbb{C}_{k}\mathcal{B}}$, it must be that $j_{1},\dots,j_{n}$ are
consecutive and non-repeating, and since the previous round had been won by
Duplicator, condition ($*$) holds for $(s,t)$, which immediately implies that
$[j_{1},\dots,j_{n}]=[\ell+2-n,\dots,\ell+1]$. Thus in particular either ${\rm
last}_{n}(s^{\prime})\in R^{\mathcal{A}}$ and ${\rm
last}_{n}(t^{\prime})\not\in R^{\mathcal{B}}$ or viceversa. ∎

### Open pathwise embeddings characterise $k$-bisimilarity

We are now in position to state and prove the main theorem of this Appendix.

######  Theorem C.17.

Two structures $(\mathcal{A},a),(\mathcal{B},b)\in{\sf Struct}_{*}(\sigma)$
are $k$-bisimilar iff there exists a span of open pathwise embeddings
$(\mathcal{C},c)\to\mathbb{C}_{k}(\mathcal{A},a)$ and
$(\mathcal{C},c)\to\mathbb{C}_{k}(\mathcal{B},b)$ with some
$\mathbb{C}_{k}$-coalgebra $(\mathcal{C},c)$ as common domain.

###### Proof.

By [4, Proposition 46], since ${\sf Struct}_{*}(\sigma)$ has binary products
(as was mentioned in the proof of C.13) and considering the resource-indexed
arboreal cover given by the comonadic adjunctions of
$\\{\mathbb{C}_{k}\\}_{k}$, there exists a span of open pathwise embeddings
with codomains $\mathbb{C}_{k}(\mathcal{A},a)$ and
$\mathbb{C}_{k}(\mathcal{A},a)$ if and only if Duplicator has a winning
strategy in the game
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$.

By Prop. C.16 this game coincides with
$\mathscr{G}(\mathbb{C}_{k}(\mathcal{A},a),\mathbb{C}_{k}(\mathcal{B},b))$,
and thus by Theorem 4.3, there exists such a span of open pathwise embeddings
iff
$(\mathcal{A},a)\mathrel{\underline{~{}~{}}{\leftrightarrow}}_{k}(\mathcal{B},b)$.
∎

### Open pathwise embeddings are the strong surjective homomorphisms

Finally, we unpack of the abstract notion of open pathwise embedding, which
generalises functional bisimulations, in our current context.

######  Definition C.18 ([4]).

Let $\mathscr{C}$ be a category equipped with a stable, proper factorisation
system. A morphism $f:X\to Y$ in $\mathscr{C}$ is said to be a _pathwise
embedding_ if for all path embeddings $e:P\to X$, $f\circ e$ is also a (path)
embedding. $f$ is said to be _open_ iff given any commutative square

${P}$${Q}$${X}$${Y}$$\scriptstyle{m}$$\scriptstyle{e}$$\scriptstyle{e^{\prime}}$$\scriptstyle{d}$$\scriptstyle{f}$

where $P,Q$ are paths and $e,e^{\prime},m$ are embeddings, there exists a
diagonal morphism $d:Q\to X$ making the two triangles commute.

In our case, that a homomorphism $f:(\mathcal{A},a)\to(\mathcal{B},b)$ is a
pathwise embedding means that it preserves embedded, linear substructures of
$(\mathcal{A},a)$. In particular, given a path $e$ of shape $\mathcal{P}$ in
$(\mathcal{A},a)$ (i.e. an embedding $e:(\mathcal{P},p)\to(\mathcal{A},a)$) it
can be pushed forward through $f$ to a path $f\circ e$ of shape $\mathcal{P}$
in $(\mathcal{B},b)$. The possibility of extending this path $f\circ e$ in
$(\mathcal{B},b)$ to a longer path in $(\mathcal{B},b)$, say of shape
$\mathcal{Q}$, is exactly what is encoded by the commutativity of the square

${(\mathcal{P},p)}$${(\mathcal{Q},q)}$${(\mathcal{A},a)}$${(\mathcal{B},b)}$$\scriptstyle{m}$$\scriptstyle{e}$$\scriptstyle{e^{\prime}}$$\scriptstyle{d}$$\scriptstyle{f}$
(2)

Thus if $f$ is also open, given such a commutative square we can find a path
of shape $\mathcal{Q}$ already in $(\mathcal{A},a)$, namely $d\circ m$, such
that it is mapped by $f$ to the extended path $e^{\prime}\circ m$. The reader
familiar with bounded morphisms in Modal Logic may be able to recognise that
notion in this definition.

######  Proposition C.19.

A homomorphism $f:(\mathcal{A},a)\to(\mathcal{B},b)$ between pp-trees is a
pathwise embedding if and only if it is strong.

###### Proof.

A pathwise embedding between pp-trees is necessarily strong since relations in
pp-trees only hold along chains of consecutive points; for any such chain in
$\mathcal{A}$ ending at $a^{\prime}$ we can take the path embedding
$e_{a}^{\prime}:(\mathcal{A}_{a^{\prime}},a)\to(\mathcal{A},a)$ where
$(\mathcal{A}_{a^{\prime}},a)$ is the embedded substructure of
$(\mathcal{A},a)$ spanned by the chain from $a$ to $a^{\prime}$ in
$\mathcal{A}$. $f$ being a pathwise embedding means that it is an embedding,
and thus strong, when restricted to this embedded substructure.

The other direction is immediate since assuming that $f$ is strong, given any
path embedding $e:(\mathcal{P},p)\to(\mathcal{A},a)$, $f\circ e$ is a
composition of strong homomorphisms. ∎

######  Proposition C.20.

Open pathwise embeddings between pp-trees are precisely the strong surjective
homomorphisms.

###### Proof.

Let $f:(\mathcal{A},a)\to(\mathcal{B},b)$ be an open pathwise embedding
between pp-trees. By Prop. C.19 $f$ is strong, thus we just need to show that
it is surjective. Let $b^{\prime}\in|\mathcal{B}|$.

Since $f$ is strong, in particular $a$ and $b$ satisfy precisely the same
unary relation symbols. Looking at Diagram 2, let $(\mathcal{P},p)$ be the
root of either $(\mathcal{A},a)$ or $(\mathcal{B},b)$ (which as we just said,
are isomorphic) seen as an embedded substructure (in particular
$|\mathcal{P}|=\\{p\\}$) and let $(\mathcal{Q},q)$ be
$\mathcal{B}_{b^{\prime}}$, the embedded substructure of $(\mathcal{B},b)$
spanned by the unique $R_{0}$-chain from $b$ to $b^{\prime}$. The outer square
commutes trivially (since all morphisms preserve basepoints) and all required
morphisms are embeddings, thus there exists a diagonal filler as in 2 in
virtue of which $b^{\prime}$ has a preimage $d(b^{\prime})$ in
$\mathcal{A}$.232323Using this procedure it is also straightforward to prove
that $f$ is strong without using the assumption of it being a pathwise
embedding; all that is required is that the basepoints of its domain and
codomain be isomorphic.

In the other direction, assume that $f:(\mathcal{A},a)\to(\mathcal{B},b)$ is
strong and surjective. By Prop C.19 $f$ is a pathwise embedding; let us see
that it is open. Given a commutative square as the one in Diagram 2, let $J$
be the height (length) of $\mathcal{Q}$ and for each $j\in\\{0,\dots,J$}, let
$q_{j}$ denote the unique point of $\mathcal{Q}$ of height $j$, so that
$|\mathcal{Q}|=\\{q_{0},\dots,q_{J}\\}$ where $q_{0}=q$ and $q_{J}$ is the
unique leaf of $\mathcal{Q}$ (i.e. the unique point with no successors). Fix a
preimage $a_{J}\in f^{-1}(e^{\prime}(q_{J}))$. An easy induction proves that
the unique $R_{0}$-chain from $a$ to $a_{J}$, which we denote by
$[a_{0},\dots,a_{J}]$ (where $a_{0}=a$) is an elementwise preimage of
$[e^{\prime}(q),\dots,e^{\prime}(q_{J})]$. Therefore we may define
$d(q_{j}):=a_{j}$ and this will make both triangles in 2 commute (the upper
left triangle commutes since $d\circ m(p^{\prime})$ has the same height as
$e(p^{\prime})$). To see that $d$ is a (strong) homomorphism, given
$R\in\sigma$ of arity $n$ and given $q_{j_{1}},\dots q_{j_{n}}\in\mathcal{Q}$,

$\displaystyle R^{\mathcal{Q}}(q_{j_{1}},\dots q_{j_{n}})$ $\displaystyle\iff
R^{\mathcal{B}}(e^{\prime}(q_{j_{1}}),\dots e^{\prime}(q_{j_{n}}))$
($e^{\prime}$ strong) $\displaystyle\iff R^{\mathcal{A}}(a_{j_{1}},\dots
a_{j_{n}})$ ($f$ strong) $\displaystyle\iff R^{\mathcal{A}}(d(q_{j_{1}}),\dots
d(q_{j_{n}})).$ (def.)

∎

Thus we obtain Theorem 5.11 as a corollary of Theorem C.17.

###### Proof of Theorem 5.11.

Combine Theorem C.17 and Proposition C.20. ∎