# Formal Guarantees of Timely Progress for Distributed Knowledge Propagation

Saswata Paul Stacy Patterson Carlos Varela Rensselaer Polytechnic Institute,
Troy, New York, 12180, USA<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Autonomous air traffic management (ATM) operations for urban air mobility
(UAM) will necessitate the use of distributed protocols for decentralized
coordination between aircraft. As UAM operations are time-critical, it will be
imperative to have formal guarantees of progress for the distributed protocols
used in ATM. Under asynchronous settings, message transmission and processing
delays are unbounded, making it impossible to provide deterministic bounds on
the time required to make progress. We present an approach for formally
guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge
propagation protocol by probabilistically modeling the delays using theories
of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The
guarantee states a probabilistic upper bound to the time for progress as a
function of the probabilities of the total transmission and processing delays
being less than two given values. We also showcase the development of a
library of formal theories, that is tailored towards reasoning about timely
progress in distributed protocols deployed in airborne networks, in the Athena
proof assistant.

##  1 Introduction

The integration of uncrewed aircraft systems (UAS) in the National Airspace
System (NAS) for urban air mobility (UAM) operations will pose significant
challenges for urban air traffic management in the near future. The UAS will
need to operate in highly congested uncontrolled urban airspaces to perform
tasks ranging from package delivery to passenger transportation. Under such
circumstances, it will be a complex task to ensure safe separation [11] among
the aircraft. The loss of safe separation can have catastrophic consequences
such as near mid-air collisions (NMAC) [35] and wake-vortex induced rolls
[41]. Centralized techniques for air traffic management, that require either
human air traffic controllers or dedicated ground stations for coordinating
the safe operation of aircraft, will be insufficient as they are prone to
human errors [59] and failures, and are economically infeasible [8].
Therefore, there is a need for developing decentralized _UAS traffic
management_ (UTM) protocols and standards for future UAM operations that will
allow aircraft to autonomously coordinate and maintain safe separation. Such
autonomous techniques will be amenable to formal verification, making them
suitable for safety-critical UAM applications.

Formal methods [60] can be used for the rigorous verification of critical
properties of autonomous UTM applications by using techniques like _model
checking_ and _theorem-proving_. However, the operational conditions presented
by UAM are expected to be highly dynamic in nature, making it infeasible to
exhaustively model them. Under such circumstances, it is possible to
probabilistically reason about these conditions to provide valuable non-
deterministic guarantees that can be used by the participating aircraft to
take important real-time operational decisions [52]. These guarantees can be
supported by pre-developed formal proofs that have been mechanically verified
for correctness under some reasonable assumptions about the conditions.

In [51] we have presented an autonomous protocol for UTM called Decentralized
Admission Control (DAC) in which aircraft connected through an asynchronous
vehicle-2-vehicle (V2V) [48] network called the Internet-of-Planes (IoP) [52]
can coordinate their use of a shared four-dimensional airspace. In DAC, an
airspace has a set of _owner_ aircraft which already have the authorization to
carry out a fixed set of _flight plans_ through the airspace (Fig. 1). The set
of flight plans corresponding to the owners is _safe_ , _i.e._ , there is no
possibility of NMACs between any two flight plans in the set. One or more
_candidate_ aircraft can use the knowledge of this set to compute a _conflict-
aware flight plan_ [53] that is compatible with all the owners. A candidate
can then propose its conflict-aware flight plan to the owners to request
authorization to use the airspace. Since the candidates do not consider each
other in their conflict-free proposals, the owners can only authorize a single
candidate at a time. When a candidate is authorized, the set of owners changes
to include this candidate, and all aircraft relevant to the airspace must be
informed about the new set of owners so that they can learn the new value.
Aircraft relevant to an airspace comprises of the set of new owners and the
set of candidates expected to try to enter the airspace in the future (this
includes the candidates who may have been previously denied authorization).
Therefore, after a candidate is authorized, a _knowledge propagation protocol_
is needed to propagate the knowledge of the new set of owners to all relevant
aircraft.

CandidatesAirspaceOwners

Figure 1: Aircraft trying to coordinate flight through a common airspace using
DAC (top view).

In [54] we have presented a Two-phase Acknowledge knowledge propagation
protocol (TAP) that can be used for sufficiently propagating the knowledge of
the new set of owners $\phi$ of an airspace to attain a safe state of
knowledge [19] for DAC. For TAP, we have formally proven consistency, which
implies that TAP will correctly propagate the knowledge, and eventual
progress, which implies that eventually, the safe state will be attained.
Although a guarantee of eventual progress alone is insufficient for time-
critical UAM applications, as it does not state any bound on the time for
successful propagation, it is a necessary precondition for providing formal
guarantees of timely progress, which can provide some useful time bounds. The
total clock time that is required for successful propagation is dependent on
three factors—message transmission delays, message processing delays, and the
number of messages involved. In asynchronous settings message delays are
unbounded, making it impossible to provide deterministic bounds on the total
time that may be required for successful propagation.

In the absence of deterministic time bounds, it is possible to provide
probabilistic bounds for the timely progress of distributed protocols by
modeling the factors affecting total time as stochastic processes. In this
paper, we formulate probabilistic timely progress guarantees for TAP (assuming
eventual progress) by using theories apposite to _low-altitude platforms_
(LAP) [12] of airborne communication such as _vehicular ad hoc networks_
(VANET) [24]. Particularly, we formalize the theory of the _Multicopy Two-Hop
Relay_ (MTR) protocol [40] to model message transmission delays in VANETs and
the M/M/1 queue system [38] to model message processing delays. We then use
the probabilistic bounds on these delays to provide sufficiently high-level
guarantees of timely progress that are useful for UAM applications. E.g., if a
timely progress guarantee states that “propagation will take at most 5 seconds
with a probability 98%", then an aircraft can choose to only compute flight
plans that start after 5 seconds to ensure that the plans don’t become
obsolete by the time that they are successfully propagated.

We have formalized our theory for timely progress in TAP using the Athena
proof assistant [3, 5]. Athena provides a specification and proof language
along with an interactive proof development environment. It is based on _many-
sorted first-order logic_ [43] and it uses a _natural deduction_ [4] style of
proofs. Athena is _sound_ , i.e., any method that successfully executes
produces a theorem that is guaranteed to be a logical consequence of the
_assumption base_. Athena also provides some helpful mechanisms to modularize
and organize theory in a _reusable_ manner. Using Athena, we have developed a
formal theory library that is tailored towards reasoning about timely progress
properties of distributed protocols deployed in airborne networks. This
library can be used for reasoning about time-critical decentralized UAM
applications.

Another important motivation behind developing a tailored library was to lay
the foundation for a _parameterized proof library_ that can be used in tandem
with the _dynamic data-driven applications systems_ (DDDAS) [15] paradigm for
the runtime verification of autonomous distributed applications [52].
Autonomous UAM applications like DAC are expected to operate in unpredictable
dynamic environments which cannot be completely modeled. Therefore, formal
proofs that are developed in the pre-deployment stages may cease to be useful
at runtime if the operational conditions assumed for the proofs do not
correspond to the actual operational conditions. In the DDDAS-assisted
approach, formal proofs can be parameterized by runtime-observable parameters
about the operational conditions of distributed protocols and it is possible
to augment the proofs in real-time using a _formal DDDAS feedback loop_ [52].
A parameterized proof library will make it possible to provide formal
guarantees that can be augmented with appropriate real-time parameters while
retaining the formal rigor. This will allow the development of highly adaptive
autonomous distributed UAM applications that will be capable of adapting to
the formal guarantees that are actually valid at runtime.

The main contributions of this paper are:

  * •

we formalize the theory of the Multicopy Two-Hop Relay (MTR) protocol to model
message transmission delays between aircraft,

  * •

we formalize the theory of the M/M/1 queue system to model message processing
delays in each aircraft,

  * •

we use the theory of MTR protocol and M/M/1 queue to provide machine-checkable
probabilistic guarantees of timely progress for TAP, and

  * •

we showcase the development of a formal proof library in Athena tailored
towards timely progress guarantees of distributed protocols in VANETs.

The paper is structured as follows: Section 2 describes TAP; Section 3
presents our timely progress guarantee for TAP; Section 4 showcases the
development of the proof library in Athena; Section 5 presents a discussion on
our approach towards developing the formal guarantees; Section 6 presents
prior work related to progress analysis and formalization of mathematical
theories; and Section 7 concludes the paper with a discussion about future
directions of work.

##  2 The Two-Phase Acknowledge Protocol

For decentralized UAM operations, aircraft will need to have heightened
knowledge about an airspace to operate with a sense of safety [54]. Fagin et
al. [19] succinctly explain this concern with the following example – _“..even
if all drivers in a society know the rules for following traffic lights and
follow them, that is not enough to make a driver “feel safe”. This is because
unless a driver knows that everyone else knows the rules and will follow them,
then the driver may consider it possible that some other driver, who does not
know the rules, may run a red light.”_. The knowledge propagation protocol
(TAP) for DAC ensures a state of knowledge in which every aircraft can feel
safe to operate. In knowledge logic [19], the expression $k_{i}\phi$
represents that _an agent $i$ knows the fact $\phi$_, and $E\phi$ represents
that _all agents in the system know $\phi$_. The expression $EE\phi$ (or
$E^{2}\phi$) represents a higher state of knowledge than $E\phi$ and implies
that every agent knows two facts—$\phi$ and $E\phi$. In the context of DAC,
$\phi$ represents the set of new owners after a candidate has been admitted
and $E^{2}\phi$ represents the required safe state of knowledge which implies
that all aircraft relevant to the airspace will know that all other aircraft
know about the same new set of owners. Aircraft relevant to an airspace
comprises of the set of new owners and any known candidate expected to try to
enter the airspace in the future. This allows any future candidate to use the
knowledge of $\phi$ to compute a correct conflict-aware plan.

###  2.1 The Protocol

TAP considers an asynchronous, non-Byzantine system model in which agents may
fail temporarily and message delivery is reliable [21]. There is a non-empty
set of propagators, and a logically separate non-empty set of replicas. All
propagators know the set of replicas and the same value $\phi$. $E^{2}\phi$,
in the context of our protocol, implies that _all replicas know that all other
replicas know $\phi$_. The goal of every propagator is to propagate $\phi$
among all the replicas and eventually learn that $E^{2}\phi$ has been
achieved. Propagators and replicas are logical abstractions and may be
functionally implemented by the same physical node (_e.g.,_ an aircraft)
simultaneously. For DAC, the set of aircraft which know about the new set of
owners acts as the set of propagators and the set of all aircraft relevant to
the airspace acts as the set of replicas.

From the perspective of a propagator, TAP proceeds in two consecutive phases:

  * •

Phase 1

    1. (a)

The propagator sends a learn message with a value $\phi$ to each replica.

    2. (b)

A replica learns a value $\phi$ if and only if it receives a learn message
with the value $\phi$ from the propagator and it replies to the propagator
with a learnt message if and only if it has learned a value $\phi$.

  * •

Phase 2

    1. (a)

The propagator sends an all-know message to each replica if and only if it has
received learnt messages from all replicas.

    2. (b)

A replica learns that all replicas know the value $\phi$ if and only if it
receives an all-know message from the propagator and it replies to the
propagator with an acknowledgment message if and only if it has learned that
all replicas know the value $\phi$.

    3. (c)

The propagator learns $E^{2}\phi$ has been achieved if and only if it receives
acknowledgement messages from all replicas.

###  2.2 Progress in TAP

We have formally proven in [54] that under our system model, TAP will make
eventual progress under some suitable conditions. If eventual progress is
guaranteed for TAP, then the total time taken for successful propagation is
dependent on the following:

  1. 1.

message transmission delays,

  2. 2.

message processing delays, and

  3. 3.

the total number of messages involved.

From the perspective of a propagator, successful propagation involves a
deterministic number of messages. For each replica, $4$ messages are required,
so for $R$ replicas, the total number of messages required for successful
propagation is $4\times R$. However, in asynchronous settings, transmission
and processing delays are unbounded. Therefore, even with a deterministic
number of messages, it is impossible to provide a deterministic bound on the
time for progress.

##  3 Probabilistic Guarantees of Timely Progress

In the absence of deterministic solutions, it is possible to employ a
probabilistic approach for providing formal guarantees of timely progress.
This can be done by probabilistically reasoning about the message delays using
either theoretical models or data-driven models. In contrast to theoretical
models that are based on analytical results about system characteristics,
data-driven results are usually based on real-time or historical statistical
observations about the system. This paper focuses on using theoretical models
for reasoning about timely progress.

For UAM applications, it is desirable to choose theoretical models that are
appropriate for airborne networks like the IoP. Through the IoP, aircraft
should be able to not only communicate their own information but also relay
received information from other aircraft using a multi-hop ad hoc approach
[57]. Moreover, an aircraft can be considered to be a single server where
messages arrive, wait for some time until they are processed, and take some
time to be processed. This makes it appropriate to use queueing theory [38] to
reason about message processing delays. The M/M/1 system is an elementary
queue system that consists of a single server that processes all messages
which are received, making it a reasonable choice for modeling message
processing with respect to a single aircraft. M/M/1 system also provides some
useful analytical properties that make it possible to formally reason about
the message processing delays. Therefore, to formally derive timely progress
guarantees for TAP, we assume the following:

  * •

all aircraft use the MTR protocol for message transmission between each other,

  * •

each aircraft independently implements an M/M/1 queue to process the messages
that it receives,

  * •

the transmission delays of the messages are _independent and identically
distributed_ (i.i.d.),

  * •

the processing delays of the messages are i.i.d., and

  * •

the transmission delays are independent of the processing delays.

From the perspective of a propagator, if eventual progress is guaranteed, then
in the worst-case, when there is no concurrency in message transmission and
processing, the total time ($T_{S}$) taken for successful propagation can be
calculated by using the total number of messages that are involved ($N_{M}$),
and the transmission delay ($T_{D_{m}}$) and the processing delay
($T_{P_{m}}$) of each message $m$. Since we know that $N_{M}$ has a
deterministic value ($4\times R$) for TAP, the total time for the worst-case
scenario can, therefore, be obtained using Eq. 1.

$T_{S}=\sum_{m=1}^{N_{M}}T_{D_{m}}+\sum_{m=1}^{N_{M}}T_{P_{m}}$ (1)

Now, to derive a probabilistic bound on $T_{S}$, we first need to
probabilistically model $T_{D_{m}}$ and $T_{P_{m}}$ for every message $m$
involved in progress.

###  3.1 Modeling the Message Transmission Delays

_Two-hop relaying_ , for data transmission between a source and a destination
when the two nodes are not within transmission range, has been proposed to be
an efficient mode of communication in mobile ad hoc networks (MANET) [23].
Relaying has also been considered to be appropriate for airborne networks like
the IoP where two communicating aircraft may not always be within direct
_transmission range_ [57]. Therefore, to ensure that our assumptions about
message transmission delays in airborne networks are consistent with prior
work in the literature, we use the theory of the multicopy two-hop relay (MTR)
protocol. For this, we base our assumptions on the description of the MTR
protocol presented by Al Hanbali et al. [2].

In the basic two-hop relay protocol, there are a set of $M+1$ mobile nodes
whose trajectories are i.i.d. [23]. If a source node wants to transfer a
message to a destination node, it can either transmit it directly to the
destination, if the destination is within its transmission range, or, it can
transmit copies of the message to one or more relay nodes. A relay node can
transmit a copy of a message directly to the destination node if the two are
within the transmission range of the relay node. A relay node, however, cannot
transmit a copy of a message to another relay node. Each message, therefore,
makes a maximum of two hops—it is either transmitted directly from the source
to the destination, or it is transmitted through one intermediate relay node.

In the MTR protocol [2], transmission delay $T_{D_{m}}$ is the time taken for
the destination to receive a message $m$ or a copy of $m$ for the first time.
Two nodes _meet_ when they come within the transmission range of one another
and inter-meeting time is the time interval between two consecutive meetings
of a given pair of nodes. The inter-meeting times of all pairs of nodes are
i.i.d. with the common _cumulative distribution function_ (CDF) $G(t)$. The
source can only transmit a message to a relay that does not already hold a
copy. Message transmission between two nodes within range is instantaneous.
Each copy of a message has a time-to-live (TTL), which is the time after which
a relay has to drop an untransmitted copy.

To derive a probabilistic bound on the time taken to transmit a message using
MTR, we make the following assumptions:

  * •

the TTLs for all messages are unrestricted, _i.e._ , a message can be held by
a relay node until it can transmit it,

  * •

since delivery is instantaneous when the nodes meet and TTLs are unrestricted,
the inter-meeting time between the source and the destination ($T_{sd}$) or
between a relay $i$ and the destination ($T_{r_{i}d}$) also represents the
time taken by the source or the relay to directly deliver a message to the
destination,

$T_{D_{m}}=\mbox{min}\big{(}\\{T_{sd},T_{r_{1}d},...,T_{r_{M-1}d}\\}\big{)}$
(2)

  * •

the source node transmits the copy of a message to all $M-1$ relay nodes. A
message (or a copy) can, therefore, be delivered to the destination by the
source or any of the relay nodes. Hence, the actual time taken to deliver the
message will be the minimum of $\\{T_{sd},T_{r_{1}d},...,T_{r_{M-1}d}\\}$ (Eq.
2), and

  * •

the inter-meeting times of the mobile nodes are _exponentially distributed_
with the _rate parameter_ $\lambda_{MTR}$.

By using the above assumptions and necessary theories from probability, random
variables, and exponential distributions, we have formally derived the
following probabilistic bound on the time taken to deliver a message $m$ using
MTR:

$P\left(T_{D_{m}}\leq t\right)=1-(1-(1-e^{-\lambda_{MTR}t}))^{M}$ (3)

Now, the derivative of the above expression conforms to the _probability
density function_ (PDF) of an exponential distribution with rate parameter
$\lambda_{MTR}M$. Therefore, we can conclude that $T_{D_{m}}$ is exponentially
distributed with a rate parameter $\lambda_{D_{m}}=\lambda_{MTR}M$.

###  3.2 Modeling the Message Processing Delays

Queueing theory [10] has been extensively used in the literature for modeling
throughput in MANETs [33, 56, 61, 58]. An aircraft communicating using the IoP
can be considered to be a single server where messages arrive, wait some time
in a queue until they are processed, and take some time to be processed.
Therefore, for modeling the message processing delays in the aircraft, we use
theory of queues, particularly the _M/M/1_ queue system [38]. We choose the
M/M/1 queue system because it provides elegant analytical properties for
computing the total time $T_{P_{m}}$ required for a message $m$ to be
processed. This processing time includes the time spent in the queue and the
time spent in actually processing the message. An important property of
$T_{P_{m}}$ in the M/M/1 queue system is that $T_{P_{m}}$ is exponentially
distributed [10].

The M/M/1 queue system consists of a single server where customers arrive
according to a Poisson process [34]. It has the following characteristics
[10]:

  * •

the interarrival times of messages in the queue are exponentially distributed
with a rate parameter $\lambda_{a}$,

  * •

the service time of messages, which is the time spent in actually processing a
message, is exponentially distributed with a mean $1/\mu_{s}$,

  * •

the queue is managed by a single server, and

  * •

the number of message arrivals in an interval of length $\tau$ follows a
Poisson distribution [37] with a parameter $\lambda_{a}\tau$.

To probabilistically model $T_{P_{m}}$, we use Little’s theorem [39], which is
an important fundamental result in queueing theory. If $N_{q}$ and $T_{p}$
represent the average number of messages and the mean processing delay
(queueing delay + service delay) respectively111Note that
$T_{p}=\mathbf{E}\left[T_{P_{m}}\right]$ is the _mean_ or the _expected value_
of $T_{P_{m}}$., then Little’s Theorem states the useful relationship conveyed
in Eq. 4.

$N_{q}=\lambda_{a}T_{p}$ (4)

A proof of Little’s Theorem has been presented in [10], which we have
formalized222We present the detailed proof described in [10] to clearly
highlight the current deficiencies in our formalization.. The proof uses
$N(\tau)$, $\alpha(\tau)$, and $T(i)$ to represent the number of messages in
the system at time $\tau$, the number of messages that arrived in the interval
$[0,\tau]$, and the average time spent in the system by message $i$
respectively. The average arrival rate over the time period $[0,t]$ is then
given by:

$\lambda_{t}=\frac{\alpha(t)}{t}$ (5)

Similarly, the average processing delay of messages that arrived in the
interval $[0,t]$ is given by:

$T_{t}=\sum_{i=1}^{\alpha(t)}\frac{T(i)}{\alpha(t)}$ (6)

The average number of messages in the system in the interval $[0,t]$ is given
by:

$N_{t}=\frac{1}{t}\int_{0}^{t}N(\tau)d\tau$ (7)

Now, the graphical analysis of a FIFO system reveals the following [10]:

$\frac{1}{t}\int_{0}^{t}N(\tau)d\tau=\frac{1}{t}\sum_{i=1}^{\alpha(t)}T(i)$
(8)

Using Eq. 5 to Eq. 8, it can be shown that:

$N_{t}=\lambda_{t}T_{t}$ (9)

Assuming that the limits $N_{q}=\lim_{t\rightarrow\infty}N_{t}$,
$\lambda_{a}=\lim_{t\rightarrow\infty}\lambda_{t}$, and
$T_{p}=\lim_{t\rightarrow\infty}T_{t}$ exist, we can now obtain Eq. 4 to prove
Little’s Theorem.

Now, using the properties of the Poisson distribution, it has been shown in
[10] that:

$N_{q}=\frac{\lambda_{a}}{\mu_{s}-\lambda_{a}}$ (10)

Again, from Eq. 10 and Eq. 4, we can obtain the following relationship:

$T_{p}=\frac{1}{\mu_{s}-\lambda_{a}}$ (11)

Finally, since $T_{P_{m}}$ is exponentially distributed, its rate parameter
$\lambda_{P_{m}}$ can be obtained as333For an exponentially distributed random
variable, the rate parameter is the reciprocal of the mean.:

$\lambda_{P_{m}}=\frac{1}{\mathbf{E}\left[T_{P_{m}}\right]}=\frac{1}{T_{p}}=\mu_{s}-\lambda_{a}$
(12)

###  3.3 Probabilistic Bound on the Worst-Case Time

Using the rate parameters $\lambda_{D_{m}}$ and $\lambda_{P_{m}}$ for the
exponentially distributed message transmission and processing delays, we can
now provide a probabilistic bound on the worst-case time for progress $T_{S}$.
For that, let

$T_{D}=\sum^{N_{M}}_{m=1}T_{D_{m}}\ \ \ \ \ \&\ \ \ \ \
T_{P}=\sum^{N_{M}}_{m=1}T_{P_{m}}$ (13)

From Eq. 1 and Eq. 13, for any two real numbers $x$ and $y$, we can state:

$((T_{D}\leq x)\land(T_{P}\leq y))\implies(T_{S}\leq(x+y))$ (14)

Now, for two events, $A$ and $B$, the following statement holds [45]:

$(A\implies B)\implies(P(B)\geq P(A))$ (15)

Therefore, from Eq. 14 and Eq. 15, we get:

$P(T_{S}\leq(x+y))\geq P((T_{D}\leq x)\land(T_{P}\leq y))$ (16)

Since the processing delays are independent of the transmission delays, by the
product rule of independent events [20] we have444The product rule states that
for independent events $A$ and $B$, $P(A\land B)=P(A)\times P(B)$.:

$P((T_{D}\leq x)\land(T_{P}\leq y))=P(T_{D}\leq x)\times P(T_{P}\leq y)$ (17)

From Eq. 16 and Eq. 17 we have:

$P(T_{S}\leq(x+y))\geq P(T_{D}\leq x)\times P(T_{P}\leq y)$ (18)

Now, both $T_{D}$ and $T_{P}$ are sums of i.i.d. exponential random variables.
Therefore, $T_{D}$ and $T_{P}$ follow two different _Erlang distributions_
[37], each of which are parameterized by a _shape parameter_ (which is $N_{M}$
in both cases) and a rate parameter ($\lambda_{D_{m}}$ for $T_{D}$ and
$\lambda_{P_{m}}$ for $T_{P}$). The CDF of an Erlang distribution with shape
parameter $k$ and rate parameter $\lambda$ is given by:

$F_{\mbox{\tiny Er}}(t,k,\lambda)=1-\sum_{n=0}^{k-1}\frac{1}{n!}e^{-\lambda
t}(\lambda t)^{n}$ (19)

This can be used to compute the delay probabilities as follows:

$P(T_{D}\leq
x)=1-\sum_{n=0}^{N_{M}-1}\frac{1}{n!}e^{-\lambda_{D_{m}}x}(\lambda_{D_{m}}x)^{n}=F_{\mbox{\tiny
Er}}(x,N_{M},\lambda_{D_{m}})$ (20)

$P(T_{P}\leq
y)=1-\sum_{n=0}^{N_{M}-1}\frac{1}{n!}e^{-\lambda_{P_{m}}y}(\lambda_{P_{m}}y)^{n}=F_{\mbox{\tiny
Er}}(y,N_{M},\lambda_{P_{m}})$ (21)

From Eq. 18, Eq. 20, and Eq. 21, we can state the required bound on $T_{S}$:

$P(T_{S}\leq(x+y))\geq F_{\mbox{\tiny Er}}(x,N_{M},\lambda_{D_{m}})\times
F_{\mbox{\tiny Er}}(y,N_{M},\lambda_{P_{m}})$ (22)

where $N_{M}=4\times R$, $\lambda_{D_{m}}=\lambda_{MTR}M$ and
$\lambda_{P_{m}}=\mu_{s}-\lambda_{a}$.

We have mechanically verified all the equations described in this section in
Athena by using theory from limits, distributions, real numbers, and other
domains. However, currently, we have not formalized the theory required to
reason about Poisson distributions and graphical analysis, and, therefore,
have taken Eq. 8 and Eq. 10 as conjectures for our formal proofs. Both these
equations are established results from queuing theory that have been borrowed
from Bertsekas et al. [10] and we plan to prove them in future work.

##  4 A Library of Reusable Formal Theories in Athena

For verifying the correctness of distributed protocols that can be used in
autonomous UTM applications, it is oftentimes necessary to prove complex high-
level properties about the protocols. Formally proving the correctness of a
high-level property using an interactive proof assistant like Athena requires
access to a formalization of all the fundamental theories on which the high-
level property is based. _E.g.,_ for proving the correctness of Eq. 22, it is
necessary to formalize theories from a wide range of domains such as
probability, MTR, and queues. With the increasing complexity of the high-level
properties, it becomes very arduous and time-consuming to formalize such
fundamental theories from scratch, thereby making the task of verification
intractable. For this reason, we are developing a formal library in Athena
that is tailored for reasoning about high-level progress properties of
distributed protocols in airborne networks555Complete Athena code available at
http://wcl.cs.rpi.edu/pilots/fvcafp.

Athena provides a language for "proof programming" which relies on a
fundamental technique called _method call_. Method calls in Athena represent
logical _inference rules_ that can accept arguments of arbitrary types and are
higher-order [49]. Successful evaluation of a method call results in a
_theorem_ , which is then added to the _assumption base_. The assumption base
is a set of sentences that have either been proven to be correct by using
inference rules or asserted to be correct. Athena provides the _soundness_
guarantee that any theorem that is proven will be a direct consequence of
sentences already in the assumption base.

Athena allows the use of _modules_ that can be used to organize, partition,
and encapsulate theories into multiple logically separate _namespaces_.
Modules are dynamic in the sense that they can be extended at any time and
additional content can be added to them using the extend-module command (Fig.
2). This feature of Athena allows theories, which are logically separate from
one another, to be categorized and structured for brevity. It also makes it
easy to generalize theories for use in different contexts by importing them as
required.

⬇

# Module Prob being extended by module PrbIndRv

load "Athena_LibDDDAS/math/Prob/Prob.ath"

extend-module Prob {

module PrbIndRv {

# contents of module PrbIndRv

...

}

Figure 2: Extending modules in Athena.

We have used our Athena library to formalize and verify all the high-level
properties and theorems mentioned in Section 3. For this purpose, we have
formalized theories necessary to reason about distributed protocols in
airborne networks by adding constructs that can be used to specify the
properties of interest. _E.g._ , we have created a domain of distributed
protocols DistProt that has properties which represent the characteristics of
the operational environment such as dpTotTim (the total time for progress),
msGetTd (the message transmission delays) and msGetTp (the message processing
delays). The Athena code for Eq. 16, which uses these constructs to define the
probabilistic relationship between the total processing time, the message
transmission delays, and the message processing delays, is given in Fig. 3.

⬇

# The relationship between total time for progress and message delays

define THEOREM-P-TS>=P-TD&TP :=

(forall DP r1 r2 .

((Prob.probE (Prob.consE Prob.<= (dpTotTim DP) (r1 + r2)))

>=

(Prob.probE

(Prob.cons2E

(Prob.consE Prob.<= (Random.SUM (msGetTd (dpGetMsgs DP))) r1)

(Prob.consE Prob.<= (Random.SUM (msGetTp (dpGetMsgs DP))) r2)))))

Figure 3: The representation of Eq. 16 in Athena.

Similarly to DistProt, we have specified a domain of networks called Network,
a domain of network protocols called PrtType that can represent protocols like
MTR, a domain of queues called Queue to represent queuing models like M/M/1,
and other specialized theories to reason about distributed protocols
implemented over ad hoc airborne networks.

⬇

# Expected value of message processing delays in M/M/1 queue

conclude THEOREM-mean-T-value

...

let{

...

N_d :=

( (Dist.ratePar (Random.pdf (srvcTm Q))) # mu_s

-

(Dist.ratePar (Random.pdf (cstArRat Q))) # lambda_a

);

...

}

(!chain [ T

= (N * (1.0 / L)) [T=N-x-inv-L]

= ((L / N_d) * (1.0 / L)) [N=L-by-N_d]

= (1.0 / N_d) [conn-2-a-by-d-x-b-by-a]

])

Figure 4: A snippet from the proof of Eq. 11 in Athena.

Athena supports the use of _tactics_ for interactively guiding the proof
development of higher-level proof obligations from lower-level facts in the
assumption base. There are built-in methods in Athena that can be used to
implement tactics for both _forward_ and _backward_ reasoning. _E.g.,_ Fig. 4
shows the use of the built-in chain method for deriving the proof of Eq. 11
using forward reasoning, where T represents $T_{p}$ and N_d represents
$\mu_{s}-\lambda_{a}$. In the future, we aim to define specialized methods
that can be used as tactics for reasoning about distributed protocols.

⬇

# The relationship between cdf and probability

define cdf-prob-conjecture :=

(forall x R . ((Random.cdf x R) = (probE (consE <= x R))))

Figure 5: The relationship between CDF and probability defined as a conjecture
in Athena.

One of our goals while developing the library in Athena was reusability. As
the proofs of different independent high-level properties are often dependent
on common fundamental theories, it becomes beneficial to design the common
theories in a manner that makes them reusable in different contexts. _E.g.,_
the statement cdf-prob-conjecture (Fig. 5), which defines that the CDF
$G_{X}(x)$ of a random variable $X$ is the probability that $X\leq x$ for all
reals $x$, has been used in various contexts throughout our formalization of
the results presented in Section 3 (Fig. 6).

⬇

# Proof of P(min[X1,X2,...] <= y) = 1 - (1- G(X))^N

conclude THEOREM-probability-MIN-<=-IID-RVS-Gx

...

conn-to-cdf-prob := (!uspec (!uspec cdf-prob-conjecture (Random.rvSetIdElmnt
rvSet)) R)

...

# Probabilistic bound on customer delay for M/M/1 queue

conclude THEOREM-cstDly-prob

...

conn-2-cdf-prob-conjecture := (!uspec (!uspec Prob.cdf-prob-conjecture (cstDly
Q)) r)

...

Figure 6: Some instances where the cdf-prob-conjecture has been reused.

At present, our extension to the Athena library consists of 71 axioms and 27
theorems, including the high-level properties of distributed protocols and
other domains described in this paper. It is composed of theories from three
main domains—distributed systems, mathematics, and network theory. Within each
domain, there are theories from various related sub-domains. _E.g.,_ under
mathematics, we have theories from probability, queues, random variables,
functions, and distributions. Fig. 7 depicts the current logical hierarchy of
our extension to the Athena library and the dependencies between the various
modules representing the different logical domains and sub-domains. As our
primary goal was to develop high-level probabilistic progress properties of
TAP that can be directly useful for UAM purposes, we adopted a top-down
approach of proof development where we only developed the lower-level theories
that were required to support the higher-level properties of interest to us.
In most of the cases, we have tried to use only fundamental facts from the
various domains as axioms, but there are instances in our formulation where we
have currently taken some well-established results from the domains as
conjectures that we aim to prove in future work (e.g., Eq. 10, cdf-prob-
conjecture).

Figure 7: Current hierarchy of our extension to Athena’s library for reasoning
about distributed protocols in VANETs (does not depict Athena’s built-in
library).

##  5 Discussion

The availability of probabilistic guarantees of timely progress for autonomous
distributed coordination protocols will allow the participating agents to make
educated operational decisions. _E.g._ , if candidates for DAC know that it
will take at most $x$ seconds to propagate the knowledge of their accepted
plans with $99.99\%$ probability, then they can safely decide to compute plans
that start after $x$ seconds, to ensure that the plans do not become stale.
Since the guarantees we have presented in Section 3 are based on well-
established theoretical models of VANETs, it makes them suitable for safety-
critical airborne applications like DAC, where aircraft will need to
coordinate over ad hoc networks in a decentralized manner. Two-hop relaying
has been proposed to be an efficient mode of communication in VANETs [23] and
since each aircraft will be independently responsible for processing all the
messages sent to it, we believe that the proposed combination of the MTR
protocol and the M/M/1 queue system is a reasonable approach for formally
modeling communication between aircraft over the IoP.

Autonomous decentralized operations of mobile agents are complex in nature.
Such operations involve many interlinked aspects such as the mobility of the
agents, the characteristics of the communication network, the internal
computational capabilities of the agents, and the interaction between the
agents. Therefore, to formally reason about such operations, it is necessary
to holistically consider all these important aspects. Achieving this in a
machine-verifiable manner requires access to formal constructs, that are
sufficiently expressive to correctly and completely specify such aspects, in
some machine-readable formal language. Developing such expressive formal
constructs in a machine-readable language is a challenging task since it
requires domain knowledge of all aspects of the system that need to be
specified, strong knowledge of formal logic and reasoning techniques,
experience and familiarity with the language in which the constructs are to be
specified, and a significant amount of time and effort.

In the absence of a pre-existing formal library that provides the necessary
formal constructs to express some system, every time high-level properties of
the system need to be verified, engineers have to develop the required
formalizations from the ground up, often making the task of verification
intractable. _E.g._ , when we set out to specify timely progress properties
for TAP using the theory of MTR protocol and M/M/1 queue system, we required
theories in Athena to express constructs such as networks, mobility models,
communication models, inter-agent interactions, queues, and distributed
protocols, which were necessary to express the concepts presented in Section
3. For that reason, we developed most of the symbols, domains, and
relationships necessary to comprehensibly express all the assumptions and
specifications using the capabilities of Athena’s many-sorted first-order
logic. We have tried to make the specifications reusable to different contexts
so that further expansion of the library can be aided by using the existing
specifications as building blocks rather than requiring to redevelop them for
use in other contexts. In our experience, efficiently designing reusable
formal structures to express interconnected theories requires several
iterations where the specifications need to be improved to be more general as
new contexts for application are identified. Another challenge is the
meaningful modularization of the developed theories into appropriate
categories to make it easy to import them independently in different contexts.
This is important because when theories are imported during proof development,
they are automatically added to the assumption base. Well-defined modules
allow theories to be imported only as needed without making the assumption
base unnecessarily large. This is an evolving project and we are certain that
as more theory is added to the library, many of the formalizations in our
current library will need to be redesigned in order to make them more general
and better-organized.

During the development of our high-level formal guarantees of timely progress
for TAP in Athena, we have relied on some theories which we have not formally
verified in Athena, but have used them as conjectures for the proofs.
Nevertheless, we believe that this does not invalidate the results we have
presented in the paper or diminish their importance in any way. This is
because all the conjectures we have used are well-established facts in the
literature of the respective domains and have been informally proven beyond a
reasonable doubt. Since we were more interested in verifying the novel higher-
level properties of timely progress for TAP that we have presented in Section
3, in the interest of time, we decided to take some of these well-established
theories as foundations for developing our higher-level guarantees since our
library currently lacks the necessary formal theory to mechanically verify
them. However, if time is not a concern, it should be possible to develop the
proofs of these theories in Athena from just the fundamental axioms of the
corresponding domains.

To the best of our knowledge, at the time of publication, our extension to the
Athena library is the only library that provides a tailored formal foundation
for reasoning about autonomous distributed coordination in airborne networks
based on the theory of VANETs and queuing systems. Therefore, we believe that
our contribution will make the task of reasoning about properties of other
distributed coordination protocols, which are implemented using MTR and the
M/M/1 queue, in Athena easier in the future as a significant amount of
reusable formal constructs to express such properties have already been
developed. Nonetheless, additional theories will be required to reason about
distributed protocols involving a non-deterministic number of messages (_e.g._
, the _Synod consensus protocol_ [51]). Our eventual goal is to expand the
library by adding additional theories from distributions, queues, airborne
networks, message sequences, and other necessary domains to support reasoning
about a variety of distributed protocols that can be employed for autonomous
decentralized UAM applications.

##  6 Related Work

There is existing work in the literature on the informal analysis of timely
progress of consensus. Attiya et al. [7] provided lower-bounds on the time for
progress in round-based [17] consensus protocols. Attiya et al. [6] analyzed
the time complexity of solving distributed decision problems. Berman et al.
[9] studied the number of message rounds involved in various consensus
protocols.

Existing work on machine-verified guarantees has mainly analyzed eventual
progress. McMillan  _et al._ [44] have proven eventual progress of Stoppable
Paxos [42] in Ivy [50]. Dragoi et al. [18] and Debrat et al. [16] have proven
eventual progress in _LastVoting_ [14]. Hawblitzel  _et al._ [31, 32] have
proven eventual progress for a Multi-Paxos implementation using Dafny [36]. In
[51], we have verified eventual progress in the Synod consensus protocol using
Athena.

Formalization of mathematical theories has also been presented in the
literature. Hasan [25] presented formalizations of statistical properties of
discrete random variables in the HOL Theorem Prover [22]. Hasan  _et al._ have
formalized properties of the standard uniform random variable [26], discrete
and continuous random variables [27, 29], tail distribution bounds [28], and
conditional probability [30]. Mhamdi  _et al._ [46, 47] have extended Hasan et
al.’s work by formalizing measure theory and the Lebesque integral in HOL. HOL
formalizations of the Poisson process, continuous chain Markov process, and
M/M/1 queue have been presented in [13]. Qasim [55] has used Mhamdi et al.’s
work to formalize the standard normal variable.

In contrast to the existing work, we have developed formal theories tailored
towards machine-verifiable timely progress guarantees for distributed
protocols using models appropriate for airborne networks and have presented
the timely progress guarantee of a knowledge propagation protocol that can be
used for autonomous decentralized UAM applications.

##  7 Conclusion and Future Work

In this paper, we have presented a formal probabilistic guarantee of timely
progress for the Two-phase Acknowledge knowledge propagation protocol by using
theories from the Multi-copy Two-Hop Relay protocol and the M/M/1 queue system
to reason about the non-deterministic message delays. Since the progress
guarantee provides useful probabilistic bounds on the time that may be
required to make progress, it is more useful than a guarantee of eventual
progress for time-critical UAM applications of the knowledge propagation
protocol. We have also showcased the development of a formal library in Athena
for mechanically verifying the timely progress guarantee. In the future,
autonomous UAM applications will require participating aircraft to employ
different types of distributed protocols for achieving different operational
goals such as maintaining safe separation, autonomously coordinating
operations through a shared airspace, etc. Our proof library has, therefore,
been tailored to be reusable for reasoning about the timely progress of a
variety of distributed protocols that can be used for such autonomous
applications.

Currently, our formalizations have some high-level conjectures since our
current library lacks the theories required to formally verify them. In the
future, we plan to formalize the necessary fundamental theories required to
prove these conjectures as theorems. The library also does not support the
complete formalization of timely progress if the number of messages is non-
deterministic. Therefore, another potential direction of future work is to add
additional theories to the library to allow reasoning about distributed
protocols that involve a non-deterministic number of messages, such as the
Synod consensus protocol. In the future, we would also like to model other
routing protocols suitable for VANETs in addition to MTR so that appropriate
guarantees can be provided depending on actual implementations.

Acknowledgment: This research was partially supported by the National Science
Foundation (NSF), Grant No. – CNS-1816307 and the Air Force Office of
Scientific Research (AFOSR), DDDAS Grant No. – FA9550-19-1-0054.

## References

  * [1]
  * [2] Ahmad Al Hanbali, Arzad A Kherani & Philippe Nain (2007): _Simple Models for the Performance Evaluation of a Class of Two-Hop Relay Protocols_.  In: International Conference on Research in Networking, Springer, pp. 191–202, 10.1007/978-3-540-72606-7_17.
  * [3] Konstantine Arkoudas: _Athena_.  Available at http://proofcentral.org/athena.
  * [4] Konstantine Arkoudas (2005): _Simplifying Proofs in Fitch-Style Natural Deduction Systems_.  Journal of Automated Reasoning 34(3), pp. 239–294, 10.1007/s10817-005-9000-3.
  * [5] Konstantine Arkoudas & David Musser (2017): _Fundamental Proof Methods in Computer Science: A Computer-Based Approach_.  MIT Press, 10.1017/s1471068420000071.
  * [6] Hagit Attiya & Taly Djerassi-Shintel (2001): _Time Bounds for Decision Problems in the Presence of Timing Uncertainty and Failures_.  Journal of Parallel and Distributed Computing 61(8), pp. 1096–1109, 10.1006/jpdc.2001.1730.
  * [7] Hagit Attiya, Cynthia Dwork, Nancy Lynch & Larry Stockmeyer (1994): _Bounds on the Time to Reach Agreement in the Presence of Timing Uncertainty_.  Journal of the ACM (JACM) 41(1), pp. 122–152, 10.21236/ada229766.
  * [8] Swee Balachandran, Christopher Manderino, César Muñoz & María Consiglio (2020): _A Decentralized Framework to Support UAS Merging and Spacing Operations in Urban Canyons_.  In: 2020 International Conference on Unmanned Aircraft Systems (ICUAS), IEEE, pp. 204–210, 10.1109/icuas48674.2020.9213973.
  * [9] Piotr Berman, Juan A Garay, Kenneth J Perry et al. (1989): _Towards Optimal Distributed Consensus_.  In: FOCS, 89, pp. 410–415, 10.1109/sfcs.1989.63511.
  * [10] Dimitri P Bertsekas, Robert G Gallager & Pierre Humblet (1992): _Data Networks_.  2, Prentice-Hall International New Jersey.
  * [11] Marc Brittain & Peng Wei (2018): _Autonomous Aircraft Sequencing and Separation with Hierarchical Deep Reinforcement Learning_.  In: Proceedings of the International Conference for Research in Air Transportation.
  * [12] Xianbin Cao, Peng Yang, Mohamed Alzenad, Xing Xi, Dapeng Wu & Halim Yanikomeroglu (2018): _Airborne Communication Networks: A Survey_.  IEEE Journal on Selected Areas in Communications 36(9), pp. 1907–1926, 10.1109/jsac.2018.2864423.
  * [13] Donia Chaouch (2015): _Formalization of Continuous Time Markov Chains with Applications in Queueing Theory_.  Master’s thesis, Concordia University.
  * [14] Bernadette Charron-Bost & André Schiper (2009): _The Heard-Of Model: Computing in Distributed Systems With Benign Faults_.  Distributed Computing 22(1), pp. 49–71, 10.1007/s00446-009-0084-6.
  * [15] Frederica Darema (2004): _Dynamic Data-Driven Application Systems: A New Paradigm for Application Simulations and Measurements_.  In: Computational Science-ICCS 2004, Springer, pp. 662–669, 10.1007/978-3-540-24688-6_86.
  * [16] Henri Debrat & Stephan Merz (2012): _Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model_.  Archive of Formal Proofs 2012\.
  * [17] Carole Delporte-Gallet, Hugues Fauconnier, Rachid Guerraoui & Bastian Pochon (2007): _The Perfectly Synchronized Round-Based Model of Distributed Computing_.  Information and Computation 205(5), pp. 783–815, 10.1016/j.ic.2006.11.003.
  * [18] Cezara Drăgoi, Thomas A Henzinger & Damien Zufferey (2016): _PSync: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms_.  In: ACM SIGPLAN Notices, 51, ACM, pp. 400–415, 10.1145/2837614.2837650.
  * [19] Ronald Fagin, Joseph Y Halpern, Yoram Moses & Moshe Vardi (2004): _Reasoning About Knowledge_.  MIT press, 10.7551/mitpress/5803.001.0001.
  * [20] Robert G Gallager (2013): _Stochastic Processes: Theory for Applications_.  Cambridge University Press, 10.1017/cbo9781139626514.
  * [21] László Gönczy, Máté Kovács & Dániel Varró (2007): _Modeling and Verification of Reliable Messaging by Graph Transformation Systems_.  Electronic Notes in Theoretical Computer Science 175(4), pp. 37–50, 10.1016/j.entcs.2007.04.015.
  * [22] Michael JC Gordon (1989): _Mechanizing Programming Logics in Higher Order Logic_.  In: Current trends in hardware verification and automated theorem proving, Springer, pp. 387–439, 10.1007/978-1-4612-3658-0_10.
  * [23] Matthias Grossglauser & David NC Tse (2002): _Mobility Increases the Capacity of Ad Hoc Wireless Networks_.  IEEE/ACM transactions on networking 10(4), pp. 477–486, 10.1109/tnet.2002.801403.
  * [24] Mustafa Maad Hamdi, Lukman Audah, Sami Abduljabbar Rashid, Alaa Hamid Mohammed, Sameer Alani & Ahmed Shamil Mustafa (2020): _A Review of Applications, Characteristics and Challenges in Vehicular Ad-Hoc Networks (VANETs)_.  In: 2020 International Congress on Human-Computer Interaction, Optimization and Robotic Applications (HORA), IEEE, pp. 1–7, 10.1109/hora49412.2020.9152928.
  * [25] Osman Hasan (2008): _Probabilistic Analysis Using Theorem Proving_.  In: 21 st International Conference on Theorem Proving in Higher Order Logics, Citeseer, p. 21.
  * [26] Osman Hasan & Sofiène Tahar (2007): _Formalization of the Standard Uniform random variable_.  Theoretical Computer Science 382, pp. 71–83, 10.1016/j.tcs.2007.05.009.
  * [27] Osman Hasan & Sofiène Tahar (2008): _Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables_.  Journal of Automated Reasoning 41(3-4), pp. 295–323, 10.1007/s10817-008-9113-6.
  * [28] Osman Hasan & Sofiene Tahar (2009): _Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover_.  Mathematical Methods in the Applied Sciences 32(4), pp. 480–504, 10.1002/mma.1055.
  * [29] Osman Hasan & Sofiene Tahar (2010): _Formal Probabilistic Analysis: A Higher-Order Logic Based Approach_.  In: International Conference on Abstract State Machines, Alloy, B and Z, Springer, pp. 2–19, 10.1007/978-3-642-11811-1_2.
  * [30] Osman Hasan & Sofiène Tahar (2011): _Reasoning About Conditional Probabilities in a Higher-Order-Logic Theorem Prover_.  Journal of Applied Logic 9(1), pp. 23–40, 10.1016/j.jal.2011.01.001.
  * [31] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty & Brian Zill (2015): _IronFleet: Proving Practical Distributed Systems Correct_.  In: Proceedings of the 25th Symposium on Operating Systems Principles, ACM, pp. 1–17, 10.1145/2815400.2815428.
  * [32] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty & Brian Zill (2017): _IronFleet: Proving Safety and Liveness of Practical Distributed Systems_.  Communications of the ACM 60(7), pp. 83–92, 10.1145/3068608.
  * [33] Rashmi Kushwah, Shashikala Tapaswi & Ajay Kumar (2020): _Multipath Delay Analysis Using Queuing Theory for Gateway Selection in Hybrid MANET_.  Wireless Personal Communications 111(1), pp. 9–32, 10.1007/s11277-019-06842-9.
  * [34] Günter Last & Mathew Penrose (2017): _Lectures on the Poisson Process_.  7, Cambridge University Press, 10.1017/9781316104477.007.
  * [35] Seung Man Lee, Chunki Park, Marcus A Johnson & Eric R Mueller (2013): _Investigating Effects of Well Clear Definitions on UAS Sense-And-Avoid Operations in Enroute and Transition Airspace_.  In: 2013 Aviation Technology, Integration, and Operations Conference, 10.2514/6.2013-4308.
  * [36] K. Rustan M. Leino (2010): _Dafny: An Automatic Program Verifier for Functional Correctness_.  In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, Springer, pp. 348–370, 10.1007/978-3-642-17511-4_20.
  * [37] Alberto Leon-Garcia (1994): _Probability and Random Processes for Electrical Engineering_ , 2nd edition.  Addison-Wesley, Reading, MA.
  * [38] Lester Lipsky (2009): _M/M/1 Queue_.  Queueing Theory: A Linear Algebraic Approach, pp. 33–75, 10.1007/978-0-387-49706-8_2.
  * [39] John DC Little (1961): _A Proof for the Queuing Formula: L= $\lambda$ W_.  Operations research 9(3), pp. 383–387, 10.1287/opre.9.3.383.
  * [40] Jiajia Liu, Xiaohong Jiang, Hiroki Nishiyama & Nei Kato (2013): _On the Delivery Probability of Two-Hop Relay MANETs with Erasure Coding_.  IEEE Transactions on Communications 61(4), pp. 1314–1326, 10.1109/tcomm.2013.020413.120198.
  * [41] Robert Luckner, Gordon Höhne & Michael Fuhrmann (2004): _Hazard Criteria for Wake Vortex Encounters During Approach_.  Aerospace Science and Technology 8(8), pp. 673–687, 10.1016/j.ast.2004.06.008.
  * [42] Dahlia Malkhi, Leslie Lamport & Lidong Zhou (2008): _Stoppable Paxos_.  Technical Report, Microsoft Research.
  * [43] Maria Manzano (1996): _Extensions of First-Order Logic_.  Cambridge University Press.
  * [44] Kenneth L McMillan & Oded Padon (2018): _Deductive Verification in Decidable Fragments with Ivy_.  In: Static Analysis, Springer, pp. 43–55, 10.1007/978-3-319-99725-4_4.
  * [45] Ronald Meester & Klaas Slooten (2021): _Some Philosophy of Probability, Statistics, and Forensic Science_ , p. 1–29.  Cambridge University Press, 10.1017/9781108596176.002.
  * [46] Tarek Mhamdi, Osman Hasan & Sofiène Tahar (2010): _On the Formalization of the Lebesgue Integration Theory in HOL_.  In: International Conference on Interactive Theorem Proving, Springer, pp. 387–402, 10.1007/978-3-642-14052-5_27.
  * [47] Tarek Mhamdi, Osman Hasan & Sofiène Tahar (2013): _Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL_.  ACM Transactions on Embedded Computing Systems 12(1), 10.1145/2406336.2406349.
  * [48] Andreas F Molisch, Fredrik Tufvesson, Johan Karedal & Christoph F Mecklenbrauker (2009): _A Survey on Vehicle-to-Vehicle Propagation Channels_.  IEEE Wireless Communications 16(6), pp. 12–22, 10.1109/mwc.2009.5361174.
  * [49] David R. Musser & Carlos A. Varela (2013): _Structured Reasoning About Actor Systems_.  In: Proceedings of the 2013 Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE!, ACM, New York, NY, USA, pp. 37–48, 10.1145/2541329.2541334.
  * [50] Oded Padon, Kenneth L McMillan, Aurojit Panda, Mooly Sagiv & Sharon Shoham (2016): _Ivy: Safety Verification by Interactive Generalization_.  ACM SIGPLAN Notices 51(6), pp. 614–630, 10.1145/2980983.2908118.
  * [51] Saswata Paul, Gul A. Agha, Stacy Patterson & Carlos A. Varela (2021): _Verification of Eventual Consensus in Synod using a Failure-Aware Actor Model_.  In: Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021), pp. 249–267, 10.1007/978-3-030-76384-8_16.
  * [52] Saswata Paul, Fotis Kopsaftopoulos, Stacy Patterson & Carlos A. Varela (2020): _Dynamic Data-Driven Formal Progress Envelopes for Distributed Algorithms_.  In: Dynamic Data-Driven Application Systems, pp. 245–252, 10.1007/978-3-030-61725-7_29.
  * [53] Saswata Paul, Stacy Patterson & Carlos A. Varela (2019): _Conflict-Aware Flight Planning for Avoiding Near Mid-Air Collisions_.  In: The 38th AIAA/IEEE Digital Avionics Systems Conference, San Diego, CA, pp. 1–10, 10.1109/dasc43569.2019.9081658.
  * [54] Saswata Paul, Stacy Patterson & Carlos A. Varela (2020): _Collaborative Situational Awareness for Conflict-Aware Flight Planning_.  In: The 39th IEEE/AIAA Digital Avionics Systems Conference, pp. 1–10, 10.1109/dasc50938.2020.9256620.
  * [55] Muhammad Qasim (2016): _Formalization of Normal Random Variables_.  Master’s thesis, Concordia University, 10.1016/j.entcs.2013.09.001.
  * [56] Xinbing Wang, Qiuyu Peng & Yingzhe Li (2012): _Cooperation Achieves Optimal Multicast Capacity-Delay Scaling in MANET_.  IEEE Transactions on Communications 60(10), pp. 3023–3031, 10.1109/tcomm.2012.081512.110535.
  * [57] Yang Wang & Yiyuan J Zhao (2006): _Fundamental Issues in Systematic Design of Airborne Networks for Aviation_.  In: 2006 IEEE Aerospace Conference, IEEE, pp. 8–pp, 10.1109/aero.2006.1655882.
  * [58] Xia Wen-jie, Yan Han & Liu Feng-yu (2011): _The Analysis of M/M/1 Queue Model with N Policy for Damaged Nodes in MANET_.  In: 2011 IEEE International Conference on Computer Science and Automation Engineering, 1, IEEE, pp. 289–294, 10.1109/csae.2011.5953224.
  * [59] David Wing & William Cotton (2011): _For Spacious Skies: Self-Separation with "Autonomous Flight Rules" in US Domestic Airspace_.  10.2514/6.2011-6865.
  * [60] Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui & John Fitzgerald (2009): _Formal Methods: Practice and Experience_.  ACM Computing Surveys 41(4), pp. 1–36, 10.5555/3065491.3065655.
  * [61] Shouyi Yin & Xiaokang Lin (2004): _MALB: MANET Adaptive Load Balancing_.  In: IEEE 60th Vehicular Technology Conference, 2004, 4, IEEE, pp. 2843–2847, 10.1109/vetecf.2004.1400578.


Also at ]the University of Chicago, Chicago, IL 60637 Also at ]Argonne
National Laboratory, Lemont, IL 60439

# Accelerator and Beam Physics: Grand Challenges and Research Opportunities

S. Nagaitsev<EMAIL_ADDRESS>[  V. Shiltsev  A. Valishev  T. Zolkin
Fermilab, Batavia, IL 60510  J.-L. Vay  Lawrence Berkeley National Laboratory,
Berkeley, CA 94720  M. Bai  Y. Cai  M.J. Hogan  Z. Huang  J. Seeman  B. Dunham
X. Huang  SLAC National Accelerator Laboratory, Stanford, CA 94025  T. Roser
M. Minty  Brookhaven National Accelerator Laboratory, Upton, NY 11973  J.
Rosenzweig  UCLA, Los Angeles, CA 90095  P. Piot  Northern Illinois
University, DeKalb, IL 60115  [  J. Power  J. M. Byrd  Argonne National
Laboratory, Lemont, IL 60439  A. Seryi  Jefferson Lab, Newport News, VA 23606
S. Lund  Michigan State University, East Lansing, MI 48824  J.R. Patterson
Cornell University, Ithaca, NY 14853

###### Abstract

Accelerator and beam physics (ABP) is the science of the motion, generation,
acceleration, manipulation, prediction, observation and use of charged
particle beams. It focuses on fundamental long-term accelerator and beam
physics research and development. Accelerator and beam physics research has
resulted in important advances in accelerator science, yet support for this
research is declining. NSF has terminated its program in Accelerator Science
and funding by DOE through GARD and Accelerator Stewardship has been steady or
declining. The declining support for accelerator research will slow advances
and threaten student training and work-force development in accelerator
science. We propose a robust and scientifically challenging program in
accelerator and beam physics, which will position the field of US High Energy
Physics to be productive and competitive for decades to come.

##  I Executive Summary

The US Accelerator and Beam Physics R&D program explores and develops the
science of accelerators and beams to make future accelerators better, cheaper,
safer, and more reliable. Particle accelerators can be used to better
understand our universe and to aid in solving societal challenges.

The primary scientific mission of ABP R&D is to address and resolve the four
Accelerator and Beam Physics Grand Challenges (GC):

Grand Challenge 1 (beam intensity): How do we increase beam intensities by
orders of magnitude?

Grand Challenge 2 (beam quality): How do we increase beam phase-space density
by orders of magnitude, towards the quantum degeneracy limit?

Grand Challenge 3 (beam control): How do we measure and control the beam
distribution down to the level of individual particles?

Grand Challenge 4 (beam prediction): How do we develop predictive “virtual
particle accelerators”?

Other equally important ABP missions are associated with the overall HEP
missions:

  * •

Advance the physics of accelerators and beams to enable future accelerators.

  * •

Develop conventional and advanced accelerator concepts and tools to disrupt
existing costly technology paradigms.

  * •

Guide and help to fully exploit science at the HEP accelerator R&D beam
facilities and operational accelerators.

  * •

Educate and train future accelerator physicists.

We propose a robust and scientifically challenging program in accelerator and
beam physics to address the Grand Challenges. This will help position the
field of US High Energy Physics to be productive and competitive for decades
to come. We also call for a systematic and organized effort in research into
the early conceptual integration, optimization, and maturity evaluation of
future and advanced accelerator concepts. We emphasize that the accelerator
and beam test facilities are critical to enabling groundbreaking research and
to addressing the Grand Challenges. Finally, we remind that it is important to
maintain support for the existing cross-cutting educational mechanisms in the
field of accelerator science and technology such as US Particle Accelerator
School (USPAS) and the Center for Bright Beams (CBB).

##  II Accelerator and Beam Physics Grand Challenges

Grand Challenge 1 (beam intensity): How do we increase beam intensities by
orders of magnitude?

Beam intensities in existing accelerators are limited by collective effects
and particle losses. A complete and robust understanding of these effects is
necessary to help overcome the limits and increase beam intensities by orders
of magnitude. Grand Challenge #1 addresses the question: “How do we increase
beam intensities by orders of magnitude?”

Future demands for beams will exceed present capabilities by at least an order
of magnitude in several parameter regimes such as average beam power and peak
beam intensity. Ultimately, the beam intensities attainable in present
accelerators are limited by collective effects and particle losses from
various sources, e.g. space-charge forces, beam instabilities, and beam
injection losses. How do we overcome the collective forces in the beam that
deteriorate beam properties and lead to beam losses? A robust understanding of
these effects in real accelerators does not yet exist. Additionally,
theoretical, computational, and instrumentation tools to address this
challenge are not yet fully developed at the precision level required by
modern beam applications (see GC #3 and #4).

Scientific impacts and dividends

  * •

Deliver an order of magnitude increase or more in secondary particle fluxes
from proton and heavy-ion driver applications;

  * •

Improve performance of beam-driven wakefield accelerators;

  * •

Enable ultrashort electron bunches for collider applications;

  * •

Enable first generation of accelerator-driven energy systems;

  * •

Inform challenges associated with beam quality, control and prediction.

Grand Challenge 2 (beam quality): How do we increase beam phase-space density
by orders of magnitude, towards the quantum degeneracy limit?

Most applications of accelerators depend critically on the beam intensity and
directionality (or beam emittance), in order to enable new capabilities or to
optimize the signal to noise ratio. Addressing this grand challenge will yield
unprecedented beam qualities that can revolutionize applications of particle
accelerators. Grand Challenge #2 addresses the question: “How do we increase
the beam phase space density by order of magnitude, towards the quantum
degeneracy limit?”

The beam phase-space density is a determining factor for the luminosity of
high-energy colliders, for the brightness of photon sources based on storage
rings or free-electron lasers (FELs), and on emergent instruments using
electrons to probe matter — ultra-relativistic electron diffraction and
microscopy. Pushing beam phase-space density beyond the current state-of-the-
art has tremendous payoffs for discovery sciences driven by accelerators. It
will permit FELs with new capabilities, enable femtosecond to attosecond
resolution electron imaging, and provide new tools for future collider
development through source and wakefield accelerator research. Research topics
span frontier schemes for generating high-brightness electron and
proton/hadron beams; controlling space charge and coherent radiation effects
and other collective instabilities; preserving beam brightness during beam
generation and acceleration, compression and manipulations; and developing
novel techniques for beam cooling to increase phase-space density.

Scientific impacts and dividends

  * •

Create new paths for dramatically increased collider luminosity;

  * •

Enable compact wakefield-based colliders;

  * •

Significantly enhance the brightness and wavelength reach of modern X-ray
sources;

  * •

Enable schemes for compact FELs;

  * •

Create beam-based tools with unprecedented temporal and spatial resolution.

Grand Challenge 3 (beam control): How do we measure and control the beam
distribution down to the level of individual particles?

An accelerator application benefits most when the beam distribution is
specifically matched to that application. This challenge aims to replace
traditional methods that use beams of limited shapes with new methods that
generate tailored beams. It also aims to provide new research opportunities,
enabled by detecting and controlling individual particles in accelerators and
storage rings. Grand Challenge #3 addresses the question: “How do we measure
and control the beam distribution down to the individual particle level?”

A given accelerator application is best served by a beam with a specific
distribution, matched to the application. These applications may include, for
example, extra-short electron bunches from photo-cathodes for colliders or
proton injection painting to mitigate losses in high-intensity synchrotrons.
The goal of controlling and creating specific beam distributions at a fine
level represents a paradigm shift from traditional approaches, based on rms or
higher-level beam properties. This new approach presents significant
challenges in beam dynamics and diagnostics as well as in accelerator design
and operation. This grand challenge seeks to develop techniques, beam
diagnostics, and beam collimation methods with the ultimate goal of
controlling the complete 6D phase space distribution at the individual
particle level and near-term milestones capable of controlling and detecting
the beam distribution towards the attosecond time scale and nanometer spatial
scale. An associated objective is to develop techniques to track and control
individual particles or pre-formatted groups of particles. In addition, given
the complexity of these 6D distributions and the associated collective
effects, the use of machine learning and artificial intelligence (ML/AI) to
control the beam distribution (in simulations or during accelerator operation)
should be explored.

Scientific impacts and dividends

  * •

Substantially increase luminosity in future colliders;

  * •

Mitigate beam losses;

  * •

Improve the performance of future advanced collider concepts;

  * •

Enable table-top coherent light sources;

  * •

Enable quantum science experiments.

Grand Challenge 4 (beam prediction): How do we develop predictive “virtual
particle accelerators”?

Developing “virtual particle accelerators” will provide predictive tools that
enable fast computer modeling of particle beams and accelerators at
unprecedented levels of accuracy and completeness. These tools will enable or
speed up the realization of beams of extreme intensity and quality, as well as
enabling control of the beam distribution reaching down to the level of
individual particles. Grand Challenge #4 addresses the question: “How do we
develop predictive ‘virtual particle accelerators’?”

The importance of particle accelerators to society, along with their
increasing complexity and the high cost of new accelerator facilities, demand
that the most advanced computing and ML/AI tools be brought to bear on R&D
activities in particle beam and accelerator science [1, 2]. Pushing the limits
in beam intensity, quality and control demands more accurate, more complete
and faster predictive tools, with an ultimate goal of virtual accelerators.
The development of such tools requires continuous advances in fundamental beam
theory and applied mathematics, improvements in mathematical formulations and
algorithms, and their optimized implementation on the latest computer
architectures. The modeling of beams at extreme intensities and levels of
quality, and the design of accelerators that deliver them, also call for
integrated predictive tools that can take advantage of high-performance
computing. Full integration of machine learning tools (and their further
development when needed) will be essential to speed up the realization and
boost the power of virtual particle accelerators.

Scientific impacts and dividends

  * •

Deliver an integrated ecosystem of predictive tools for accurate, complete and
fast modeling of particle accelerators and beams;

  * •

Enable virtual accelerators that can predict the behavior of particle beams in
accelerators “as designed” or “as built”;

  * •

Provide the predictive tools that will enable or speed up the realization of
the beam intensity, quality, and control grand challenges;

  * •

Develop mathematical and algorithmic tools that benefit from — and contribute
to — synergistic developments beyond particle beam and accelerator science.;

  * •

Maximize the benefits from - and to – ML/AI tools for beam science and
accelerator design.

##  III Proposed Accelerator and Beam Physics Research Areas

The research community input during the two ABP workshops [3, 4, 5] indicated
the following areas of research are needed to address the above Grand
Challenges (GC).

Single-particle dynamics and nonlinear phenomena; polarized-beams dynamics

\- This impacts GC 1 and 2 and benefits from addressing GC 3 and 4.

Collective effects (space-charge, beam-beam, and self-interaction via
radiative fields, coherent synchrotron radiation, e.g.) and mitigation.

\- This impacts GC 1 and 2, and benefits from addressing GC 3 and 4.

Beam instabilities, control, and mitigation; short- and long-range wakefields.

\- This impacts GC 1 and 2, and benefits from addressing GC 3 and 4.

High-brightness / low-emittance beam generation, and high peak-current,
ultrashort bunches.

\- This impacts GC 2, and benefits from addressing GC 3 and 4.

Beam quality preservation and advanced beam manipulations; beam cooling and
radiation effects in beam dynamics.

\- This impacts GC 2, and benefits from addressing GC 3 and 4.

Advanced accelerator instrumentation and controls.

\- This impacts GC 3.

High-performance computing algorithms, modeling and simulation tools.

\- This impacts GC 4.

Fundamental accelerator theory and applied math.

\- This impacts all Grand Challenges.

Machine learning and artificial intelligence.

\- This impacts GC 3 and 4 in the short term and GC 1 and 2 in the long term.

Early conceptual integration, optimization, and maturity evaluation of
accelerator concepts.

\- This focuses on science and technology gaps and bridges between various R&D
efforts.

##  IV Test Facilities

Demonstrating the viability of emerging accelerator and beam physics research
ultimately relies on experimental validation. The US (both at national
laboratories and universities), has a portfolio of beam test facilities
capable of providing beams over a wide range of parameters used to perform
research critical to advancing accelerator S&T related to high-energy physics,
basic energy science, and beyond. These accelerator test facilities have
notably have enabled groundbreaking research in accelerator research essential
to developing the next generation of energy-frontier and intensity-frontier
user facilities; see Ref. [6] for an overview of the current portfolio.

The facilities include GARD-sponsored infrastructure whose principal mission
is to support broad participation from the community of accelerator scientists
including from Universities, Industry, and National Laboratories. These
facilities enable research pertinent to APB and provide ideal platforms for
training future accelerator scientists.

There are several ABP research facilities, such as FACET (SLAC), AWA (ANL),
ATF (BNL), BTF (ORNL), IOTA/FAST (FNAL), and facilities at universities,
including CBETA (Cornell), MEDUSA (Cornell), PEGASUS (UCLA) and CYBORG (UCLA).
Such facilities are invaluable for advancing new accelerator concepts and
technologies, but a significant fraction of them are aging or sharing
infrastructure with user facilities which significantly reduces their
throughput.

It is critical for the US accelerator program to provide robust funding to
operate, maintain, and upgrade these accelerator test facilities so that they
remain productive for ABP. Likewise, a green-field national facility should be
considered to remain competitive with the significant infrastructure
development started, e.g., in Europe [7, 8].

##  V Early conceptual integration, optimization, and maturity evaluation of
accelerator concepts

We call for a systematic and organized effort of the accelerator community in
research into the early conceptual integration, optimization, and maturity
evaluation of future and advanced accelerator concepts. The ABP R&D program is
the most appropriate and capable in the United States of providing the
systematic support of this effort.

At the ABP Roadmap Workshop # 2 [4] we reviewed the research needs and
opportunities which would help improve existing complex accelerators, and
develop new concepts of future single-beam and colliding beam facilities. The
emphasis was on how all the accelerator physics constraints, engineering
technical challenges, and environmental impacts are integrated and optimized
to arrive at the desired overall conceptual design. We identified two general
areas – near- and longer- term accelerators (see Refs.[9] and [10] for more
details).

###  V.1 Near term accelerators

Accelerator physics topics for the near term ($<$10 years), for example,
related to well established facility projects with CDRs/TDRs. They do not
strongly rely on ABP for the present design choices or performance projections
but could greatly benefit from R&D that may result in future upgrades,
performance enhancements, cost risk mitigation, or shorter commissioning
period. The possibilities are:

####  V.1.1 High Power Proton Sources (1 MW – multi-MW):

a) Beam physics issues related to beam loss control (space-charge,
instabilities, collimation, e-lens compensation, integrable optics) will
benefit from innovative approaches, theoretical and experimental studies (at
e.g. IOTA, and operational accelerators in the US and abroad) and validated
computer models and codes. A key challenge would be to reduce particle losses
(dN/N) at a faster rate than increases in achieved beam intensity (power) (N).

b) Expanded small topical national and international collaborations could
prove quite successful and useful, as well as collaborative work synergistic
with the goals of EIC, MC, NUSTORM and ADS.

####  V.1.2 Circular e+e- colliders (FCCee, CepC):

a) Several new developments call for expansion of general studies of:
optimized beam and beam-beam parameters for circular Z-W-Higgs-Top factories
including 3D beam size flip-flop from the beam-beam effect, polarization, IR
collision optimization, and ep interactions in a collider.

b) An Interaction Region (IR) design with gamma-gamma laser-beam conversion
should be performed, in parallel with possible design considerations of the
high-power laser system.

c) Pico-meter vertical emittance preservation techniques in high-charge
circular colliders with strong focusing IRs, detector solenoids, and beam-beam
effects (in synergy with SuperKEKB).

####  V.1.3 Linear e+e- Colliders (ILC, CLIC, C3):

a) To reduce the expected commissioning time of linear colliders, end-to-end
emittance preservation simulations (including parallel processing) as well as
tuning tools (e.g., ML/AI) for linear colliders should be developed.
Experimental tests of the beam-based alignment techniques in presence of
realistic external noise sources are needed and possible at high-energy low-
emittance linac-based facilities such as XFEL, LCLS-II, and FACET-II.

b) Novel new techniques for linear collider, such as a plasma-based final
focus or a cryogenic normal conducting RF linac design, need to be evaluated
and advanced through comprehensive beam physics studies performed in tandem
facility design and cost analysis.

####  V.1.4 Hadron Colliders (FCChh, SppC, HE-LHC, EIC):

a) Accelerator physics issues for vacuum system designs with electron cloud
interactions in TeV hadron colliders with bunch spacing less than 25 nano-
seconds.

b) Over the next decade, many valuable accelerator physics explorations can be
done at CERN, RHIC, IOTA, and other accelerators on topics of importance
ranging from more efficient collimation techniques, to electron lenses, to
dynamic aperture optimization methods.

c) Magnet design studies aimed at higher fields, cost reduction, and better
field quality, especially for lower injection energy or with possible new
integrable optics solutions.

d) Studies aiming towards obtaining lower emittances from new particle sources
for injecting beams in high-bunch-charge colliders, generation of high
intensity ion species, and high energy damping.

e) Exploration of lower cost hadron main colliding rings by using top-up
injection.

###  V.2 Longer term accelerators

Accelerator physics problems for long term accelerator facility plans ($>$10
years), those with intermediate readiness and others close to “strawman”
machine designs, with advanced concepts, ERL-based, or low wall plug power,
that are crucial to make those accelerators scientifically, technically, and
fiscally possible. The low environmental impact of future accelerators is now
one of the driving accelerator design criteria. The optimization studies can
help focus on the new techniques or capabilities that have the highest future
potential.

####  V.2.1 Superbeams 3-10 MW (PIP-III) and Neutrino Factories:

a) Beam physics and design optimization studies towards conceptual design of
3-10 MW superbeam facility design (focusing on power efficiency and cost per
physics result outcome).

b) Optics/DA methods needed (integral, VFFAG) to increase the beam lifetime in
racetracks of NuFact.

c) Very-fast-ramping and high-field radiation-hard magnets (expanding on the
US MDP), very high power tunable RF (expanding on the GARD RF roadmap), and
laser stripping injection schemes.

####  V.2.2 Muon Collider and Neutrino Sources (Higgs-3-14 TeV MC):

a) Design optimization studies toward scientifically, technically, and
fiscally possible muon collider, ideally, via joining the world muon effort,
aimed at a CDR in 5-7 years (a TDR in 10-15 years).

b) Studies of new and improved muon emittance cooling mechanisms – from six
dimensional cooling to positron ring-based muon sources. Final stage muon
cooling studies are needed.

c) Explore challenges and opportunities of orders of magnitude higher muon
production rates.

d) Accelerator protection from decaying muons and neutrino radiation hazard
mitigation.

e) Very-fast-ramping and high-field radiation-hard magnets (expanding on the
US MDP).

####  V.2.3 Advanced Concept Colliders AAC (Beam-Plasma, Laser- Plasma, DWA,
Microstructures):

a) New collider concepts with overall comprehensive design optimization and
systematic accounting of all beam physics and technology related issues. For
example, these are needed to progress the AAC collider optimization beyond
current “strawman design” status. These studies should be coordinated with
concurrent conceptual development of detectors.

b) Optimized AAC electron acceleration technology for a collider; optimized
positron acceleration; plasma multi-cell layout optimization, and the physics
of drive beam instabilities and optimization.

c) Optimized beam power to wall-plug power efficiency.

d) Overall cost reduction and component damage and lifetime studies for the
AAC colliders.

##  VI Education and Training

It is critical to maintain support for and improve the existing cross-cutting
educational mechanisms in the field of accelerator science and technology.
Training the workforce and recruiting talent to drive future cutting-edge
projects remains a challenge. Specialized training provided by the US Particle
Accelerator School must remain available and accessible to students and early
career scientists. Healthy university-based research is needed for its
excellent graduate training and to provide visibility on campuses, which draws
in talent to the field. The campus presence also increases the effectiveness
of the DOE Traineeships in Accelerator Science $\&$ Engineering and other
programs. Points such as these are expanded on in the AF1 white paper on
education, outreach, and diversity[11]. The grand challenge problems (Sec. 2)
emphasize advances from fundamental physics that will provide a potent draw
for student talent in our field. Similarly, cutting-edge test facilities (Sec.
4) will provide students with mentoring opportunities with established
scientists and engineers for their research and thesis projects to improve
training.

##  VII Integration of computational and ML tools across facilities

We call for effective coordination, maintenance and standardization of
computational and ML tool developments. Dedicated support of this effort would
critically benefit accelerator and beam physics modeling across facilities.

## References

  * [1] D. Sagan, M. Berz, N. Cook, Y. Hao, G. Hoffstaetter, A. Huebl et al., _Simulations of future particle accelerators: issues and mitigations_ , _Journal of Instrumentation_ 16 (2021) T10002.
  * [2] J.-L. Vay, A. Huebl, R. Lehe, N. Cook, R. England, U. Niedermayer et al., _Modeling of advanced accelerator concepts_ , _Journal of Instrumentation_ 16 (2021) T10003.
  * [3] “GARD ABP workshop #1.” https://conferences.lbl.gov/event/279/.
  * [4] “GARD ABP workshop #2.” https://indico.fnal.gov/event/22709/.
  * [5] S. Nagaitsev, Z. Huang, J. Power, J.L. Vay, P. Piot, L. Spentzouris et al., “Accelerator and Beam Physics Research Goals and Opportunities.” https://arxiv.org/abs/2101.04107, 2021.
  * [6] C. Clarke, E. Esarey, C. Geddes, M.J. Hogan, G. Hoffstaetter, S. Nagaitsev et al., “Beam Test Facilities for R&D in Accelerator Science and Technologies.” Snowmass21 whitepaper, 2022.
  * [7] R. Assmann, M. Weikum, T. Akhter, D. Alesini, A. Alexandrova, M. Anania et al., _EuPRAXIA Conceptual Design Report_ , _The European Physical Journal Special Topics_ 229 (2020) 3675 .
  * [8] C. Adolphsen, D. Angal-Kalinin, T. Arndt, M. Arnold, R. Assmann, B. Auchmann et al., _European Strategy for Particle Physics–Accelerator R &D Roadmap_, _arXiv preprint arXiv:2201.07895_ (2022) .
  * [9] V. Shiltsev and F. Zimmermann, _Modern and future colliders_ , _Reviews of Modern Physics_ 93 (2021) 015006.
  * [10] V. Shiltsev, _Superbeams and neutrino factories—two paths to intense accelerator-based neutrino beams_ , _Modern Physics Letters A_ 35 (2020) 2030005.
  * [11] M. Bai et al., _Snowmass AF1 White Paper: Strategies in Education, Outreach, and Inclusion to Enhance the US Workforce in Accelerator Science and Engineering_ , 2022.