# Towards Partial Monitoring: It is Always too Soon to Give Up††thanks:
Cardoso’s work supported by Royal Academy of Engineering under the Chairs in
Emerging Technologies scheme.

Angelo Ferrando University of Genova
Genova, Italy<EMAIL_ADDRESS>The University of Manchester
Manchester, United Kingdom Rafael C. Cardoso The University of Manchester
Manchester, United Kingdom<EMAIL_ADDRESS>
###### Abstract

Runtime Verification is a lightweight formal verification technique. It is
used to verify at runtime whether the system under analysis behaves as
expected. The expected behaviour is usually formally specified by means of
properties, which are used to automatically synthesise monitors. A monitor is
a device that, given a sequence of events representing a system execution,
returns a verdict symbolising the satisfaction or violation of the formal
property. Properties that can (resp. cannot) be verified at runtime by a
monitor are called _monitorable_ and _non-monitorable_ , respectively. In this
paper, we revise the notion of monitorability from a practical perspective,
where we show how _non-monitorable_ properties can still be used to generate
_partial_ monitors, which can partially check the properties. Finally, we
present the implications both from a theoretical and practical perspectives.

##  1 Introduction

Runtime Verification (RV) is a well-known lightweight formal verification
technique [6]. Similar to other existing formal verification techniques, such
as Model Checking [10] and Theorem Proving [22], it aims to verify the system
behaviour, usually referred to as the System Under Analysis (SUA). Such a
system can be composed of both software and hardware components, and the
formal verification technique of choice is used to verify that everything
works as expected.

RV achieves the verification of the SUA through monitoring. Specifically,
starting from a formal property expressed in some formalism of choice, one (or
multiple) monitors are generated. A monitor is a device that, given a sequence
of events (a trace) that are generated by the system execution, it verifies
the conformance of such a trace with respect to the formal property. Since the
trace can be generated at runtime, the monitor can inform the system’s users
about unexpected behaviours; i.e., events which violate the formal
specification.

Differently from other formal verification techniques, RV is performed on the
execution of the system. The formal properties are verified on traces of
events generated by actual system executions. This is an important difference
with respect to more traditional formal verification techniques such as Model
Checking, where the verification is performed statically over an abstracted
model of the system. RV does not require any model, nor any other information
apart from execution traces, which makes it well suited to be used in _black-
box_ scenarios where not much is known about the SUA, such as in autonomous
systems. Moreover, from a computational perspective RV performs better than
traditional verification techniques; since monitors only take as input what
the SUA produces, without the need of going through a model. It has been shown
that RV offers polynomial time behaviour with respect to the length of the
analysed trace [21].

Providing certification for reliable autonomous systems is not an easy task
[12]. Formal verification of monolithic systems is already hard; to apply such
techniques in the context of autonomous, cyber-physical, or even robotic
systems makes it even more complicated. This is mainly due to the fact that
these systems are intrinsically unpredictable [23]; especially when Machine
Learning techniques are involved, such as Neural Networks [16]. In these
scenarios, RV may be of help, especially since it does not require a model of
the system and it can be deployed at runtime while the system is still
running. In this way, even though the system offers some unpredictable
aspects, by adding monitors it is possible to improve the system reliability.
In fact, since monitors can be deployed together with the system, the monitors
will be there to detect and possibly react accordingly in case of unexpected
behaviours (e.g., by triggering or implementing some mechanism to handle such
failures).

Unfortunately, some formal properties cannot be monitored at runtime. A formal
property is considered _monitorable_ , when it is possible to synthesise a
monitor which verifies it. In turn, a formal property is denoted as _non-
monitorable_ , when it is not possible to synthesise such a monitor. In
literature, there exists different definitions on the requirements for a
property to be considered monitorable [17]. Nonetheless, the most common
requirement for a property to be monitorable is that it should always be
possible to conclude the satisfaction or violation of the property. Which
means that there should not exist traces of events which make the property
never satisfied nor violated. The reason such kind of properties are usually
avoided is that the resulting monitors might be useless, since they may never
be able to conclude anything about the SUA. Because of this, RV approaches
usually focus on monitorable fragments of the properties to analyse. However,
as we will show in this paper, some of these non-monitorable properties may
still be worth to be analysed at runtime, even though if only partially.
Therefore, we pose the following research question:

Is it possible for monitors that are synthesised by non-monitorable properties
to be used in practice?

We suggest that a viable answer to this question is using _partial
monitoring_. Since a non-monitorable property does not give any assurance on
satisfaction or violation, we need to synthesise monitors which are capable of
_giving up_ on the verification process when it is clear that it will never
arrive at any conclusion. This is especially relevant in the context of
autonomous systems, where the availability of computational power and memory
might be limited (e.g., in embedded systems). In such context, the presence of
a component (the monitor) that arrives at a certain state where it does not do
anything useful anymore is not only pointless, but it is also a waste of
resources which could be better allocated. Thus, it is important to have
monitors capable of giving up on the verification of a property, in order to
safely reclaim otherwise used resources. At the same time, by using partial
monitors we can be less restrictive on the kind of formal properties we are
allowed to use, since a non-monitorable property can still be partially
monitored at runtime.

As a proof of concept, in this work we exemplify our approach in a robotic
application where an autonomous rover is deployed into a nuclear facility to
perform remote inspection. In this scenario, the dynamic environment makes it
hard to formally verify properties using traditional formal methods such as
model checking. Thus, we can use RV to formally verify at runtime how the
rover behaves. Using this application, we show that non-monitorable formal
properties have parts of it that can still be verified using a partial
monitor, as long as the monitor is capable of detecting when to give up. For
example, we can have partial monitors to detect that the rover does not stay
in areas with high-level of radiation, but if it observes a bad event (e.g.,
an event that would cause the monitor to be stuck in inconclusive states),
which would render the monitor useless, then it needs to give up.

In this paper, we briefly revise the notion of _monitorability_ [17, 3, 6,
26], where we focus more on its engineering implications for what concerns the
monitor synthesis. To do so, we present a straightforward extension of the
standard monitor synthesis for temporal properties in Linear Temporal Logic
(LTL), where we take into consideration that a monitor could fail to
completely verify an LTL property. We show how we can achieve this reasoning
at the monitor level, instead of the more standard way of doing this at the
property specification level. Specifically, we reduce the problem of a monitor
recognising when to give up to a reachability problem inside the monitor
representation.

The remainder of this paper is structured as follows. Section 2 presents some
background definitions and notation that are used in the paper. Section 3
revises the notion of monitorability and reports related works in literature.
Section 4 proposes our contribution, where the notion of partial monitoring is
introduced. Section 4.1 demonstrates the use of partial monitors in an
autonomous rover performing remote inspection tasks. In Section 4.2, we give
the details on how the approach described in this paper has been implemented.
Section 5 discusses the approach and its engineering implications in the
monitor synthesis. Finally, Section 6 concludes the paper with final remarks
and future research directions.

##  2 Preliminaries

A system $S$ has an alphabet $\Sigma$ containing all of its observable events.
Given an alphabet $\Sigma$, a _trace_ $\sigma=ev_{\\_}0ev_{\\_}1\ldots$, is a
sequence of events in $\Sigma$. $\sigma(i)$ is the i-th element of $\sigma$
(i.e., $ev_{\\_}i$), $\sigma^{i}$ is the suffix of $\sigma$ starting from $i$
(i.e., $ev_{\\_}iev_{\\_}{i+1}\ldots$), $\Sigma^{*}$ is the _set of all
possible finite traces_ over $\Sigma$, and $\Sigma^{\omega}$ is the _set of
all possible infinite traces_ over $\Sigma$.

The standard formalism to specify formal properties in RV is propositional
Linear Temporal Logic (LTL [25]). The relevant parts of the syntax of LTL are
as follows:

$\varphi=true\;|\;false\;|\;ev\;|\;(\varphi\land\varphi^{\prime})\;|\;(\varphi\lor\varphi^{\prime})\;|\;\lnot\varphi\;|\;(\varphi\;\mathop{\mathrm{\mathbf{U}}}\;\varphi^{\prime})\;|\;\mathchoice{{\tf@size
pt{}}}{{\tf@size pt{}}}{{\sf@size pt{}}}{{\ssf@size pt{}}}\varphi$

where $ev\in\Sigma$ is an event (a proposition), $\varphi$ is a formula,
$\mathop{\mathrm{\mathbf{U}}}$ stands for _until_ , and $\mathchoice{{\tf@size
pt{}}}{{\tf@size pt{}}}{{\sf@size pt{}}}{{\ssf@size pt{}}}$ stands for _next-
time_. In the rest of the paper, we also use the standard derived operators,
such as $(\varphi\rightarrow\varphi^{\prime})$ instead of
$(\lnot\varphi\lor\varphi^{\prime})$, $\varphi\;R\;\varphi^{\prime}$ instead
of $\lnot(\lnot\varphi\mathop{\mathrm{\mathbf{U}}}\lnot\varphi^{\prime})$,
$\square\varphi$ (_always_ $\varphi$) instead of ($false\;R\;\varphi$), and
$\lozenge\varphi$ (_eventually_ $\varphi$) instead of
($true\mathop{\mathrm{\mathbf{U}}}\varphi$).

Let $\sigma\in\Sigma^{\omega}$ be an infinite sequence of events over
$\Sigma$, the semantics of LTL is as follows:

$\displaystyle\sigma$ $\displaystyle\models$ $\displaystyle ev\textrm{ if
}ev\in\sigma(0)$ $\displaystyle\sigma$ $\displaystyle\models$
$\displaystyle\lnot\varphi\textrm{ if }\sigma\not\models\varphi$
$\displaystyle\sigma$ $\displaystyle\models$
$\displaystyle\varphi\land\varphi^{\prime}\textrm{ if
}\sigma\models\varphi\textrm{ and }\sigma\models\varphi^{\prime}$
$\displaystyle\sigma$ $\displaystyle\models$
$\displaystyle\varphi\lor\varphi^{\prime}\textrm{ if
}\sigma\models\varphi\textrm{ or }\sigma\models\varphi^{\prime}$
$\displaystyle\sigma$ $\displaystyle\models$
$\displaystyle\mathchoice{{\tf@size pt{}}}{{\tf@size pt{}}}{{\sf@size
pt{}}}{{\ssf@size pt{}}}\varphi\textrm{ if }\sigma^{1}\models\varphi$
$\displaystyle\sigma$ $\displaystyle\models$
$\displaystyle\varphi\mathop{\mathrm{\mathbf{U}}}\varphi^{\prime}\textrm{ if
}\exists_{\\_}{i\geq 0}.\sigma^{i}\models\varphi^{\prime}\textrm{ and
}\forall_{\\_}{0\leq j<i}.\sigma^{j}\models\varphi$

A trace $\sigma$ satisfies an atomic proposition ($ev$), if the event $ev$
belongs to the head (first element) of $\sigma$; which means, $ev$ has been
observed as initial event of the trace $\sigma$. A trace $\sigma$ satisfies
the negation of the LTL property $\varphi$, if $\sigma$ does not satisfy
$\varphi$. A trace $\sigma$ satisfies the conjunction of two LTL properties,
if $\sigma$ satisfies both properties. A trace $\sigma$ satisfies the
disjunction of two LTL properties, if $\sigma$ satisfies at least one of them.
A trace $\sigma$ satisfies next-time $\varphi$, if the suffix of $\sigma$
starting in the next step ($\sigma^{1}$) satisfies $\varphi$. Finally, a trace
$\sigma$ satisfies $\varphi\mathop{\mathrm{\mathbf{U}}}\varphi^{\prime}$, if
there exists a suffix of $\sigma$ s.t. $\varphi^{\prime}$ is satisfied, and
for all suffixes before it, $\varphi$ holds.

Thus, given an LTL property $\varphi$, we denote
$\llbracket{\varphi}\rrbracket$ the language of the property, i.e., the set of
traces which satisfy $\varphi$; namely
$\llbracket{\varphi}\rrbracket=\\{\sigma\;|\;\sigma\models\varphi\\}$.

In Definition 1, we present a general and formalism-agnostic definition of a
monitor. As mentioned before, a monitor is a function that, given a trace of
events in input, returns a verdict which denotes the satisfaction (resp.
violation) of a formal property over the trace.

######  Definition 1 (Monitor)

Let $S$ be a system with alphabet $\Sigma$, and $\varphi$ be an LTL property.
Then, a monitor for $\varphi$ is a function
$Mon_{\\_}{{\varphi}}:\Sigma^{*}\rightarrow\mathbb{B}_{\\_}3$, where
$\mathbb{B}_{\\_}3=\\{\top,\bot,?\\}$:

$Mon_{\\_}{{\varphi}}({\sigma})=\left\\{{\begin{tabular}[]{cl}$\top$&{\qquad$\forall_{\\_}{u\in\Sigma^{\omega}}.\sigma\bullet
u\in\llbracket{\varphi}\rrbracket$}\\\
$\bot$&{\qquad$\forall_{\\_}{u\in\Sigma^{\omega}}.\sigma\bullet
u\notin\llbracket{\varphi}\rrbracket$}\\\ $?$&{\qquad$otherwise$}\\\
\end{tabular}}\right.$

where $\bullet$ is the standard trace concatenation operator.

Intuitively, a monitor returns $\top$ if all continuations ($u$) of $\sigma$
satisfy $\varphi$; $\bot$ if all possible continuations of $\sigma$ violate
$\varphi$; $?$ otherwise. The first two outcomes are standard representations
of satisfaction and violation, while the third is specific to RV. In more
detail, it denotes when the monitor cannot conclude any verdict yet. This is
closely related to the fact that RV is applied while the system is still
running, and not all information about it are available. For instance, a
property might be currently satisfied (resp. violated) by the system, but
violated (resp. satisfied) in the (still unknown) future. The monitor can only
safely conclude any of the two final verdicts ($\top$ or $\bot$) if it is sure
such verdict will never change. The addition of the third outcome symbol $?$
helps the monitor to represent its position of uncertainty w.r.t. the current
system execution.

A monitor function is usually implemented as a Finite State Machine (FSM),
specifically a Moore machine (FSM where the output value of a state is only
determined by the state) [7, 8]. A Moore machine can be defined as a tuple
$\langle Q,q_{\\_}0,\Sigma,O,\delta,\gamma\rangle$, where $Q$ is a finite set
of states, $q_{\\_}0$ is the initial state, $\Sigma$ is the input alphabet,
$O$ is the output alphabet, $\delta:Q\times\Sigma\rightarrow Q$ is the
transition function mapping a state and an event to the next state, and
$\gamma:Q\rightarrow O$ is the function mapping a state to the output
alphabet.

In [8], Bauer et al. present the sequence of steps required to generate from
an LTL formula $\varphi$ the corresponding Moore machine instantiating the
$Mon_{\\_}{{\varphi}}$ function (as summarised in Figure 1).

$\textstyle{{Input}}$$\textstyle{{(i)Formula}}$$\textstyle{{(ii)NBA}}$$\textstyle{{(iii)\textrm{Emptiness
per
state}}}$$\textstyle{{(iv)NFA}}$$\textstyle{{(v)DFA}}$$\textstyle{{(vi)\textrm{Moore
machine}}}$$\textstyle{{\varphi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{A^{\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{F^{\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{{\hat{A}}^{\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{{\tilde{A}}^{\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\varphi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{Mon_{\\_}{{\varphi}}}}$$\textstyle{{\lnot\varphi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{A^{\lnot\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{F^{\lnot\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{{\hat{A}}^{\lnot\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{{\tilde{A}}^{\lnot\varphi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
Figure 1: Steps required to generate an FSM from an LTL formula $\varphi$. NBA
is Non-deterministic Büchi Automaton, NFA is Non-deterministic Finite
Automaton, and DFA is Deterministic Finite Automaton.

Given an LTL property $\varphi$, a series of transformations is performed on
$\varphi$, and its negation $\lnot\varphi$. Considering $\varphi$ in step
_(i)_ , first, a corresponding Büchi Automaton $A^{\varphi}$ is generated in
step _(ii)_. This can be obtained using Gerth et al.’s algorithm [14]. Such
automaton recognises the set of infinite traces that satisfy $\varphi$
(according to LTL semantics). Then, each state of $A^{\varphi}$ is evaluated;
the states that when selected as initial states in $A^{\varphi}$ do not
generate the empty language are then added to the $F^{\varphi}$ set in step
_(iii)_. With such a set, a Non-deterministic Finite State Automaton
$\hat{A}^{\varphi}$ is obtained from $A^{\varphi}$ by simply substituting the
final states of $A^{\varphi}$ with $F^{\varphi}$ in step _(iv)_.
$\hat{A}^{\varphi}$ recognises the finite traces (prefixes) that has at least
one infinite continuation satisfying $\varphi$ (since the prefix reaches a
state in $F^{\varphi}$). After that, $\hat{A}^{\varphi}$ is transformed
(Rabin–Scott powerset construction [27]) into its equivalent deterministic
version $\tilde{A}^{\varphi}$ in step _(v)_ ; this is possible since
deterministic and non-deterministic automata have the same expressive power.
The exact same steps are performed on $\lnot\varphi$, which bring to the
generation of the $\tilde{A}^{\lnot\varphi}$ counterpart. The difference
between $\tilde{A}^{\varphi}$ and $\tilde{A}^{\lnot\varphi}$ is that the
former recognises finite traces which have continuations satisfying $\varphi$,
while the latter recognises finite traces which have continuations violating
$\varphi$. Finally, a Moore machine can be generated as a standard automata
product between $\tilde{A}^{\varphi}$ and $\tilde{A}^{\lnot\varphi}$ in the
final step _(vi)_ , where the states are denoted as tuples $(q,q^{\prime})$,
with $q$ and $q^{\prime}$ belonging to $\tilde{A}^{\varphi}$ and
$\tilde{A}^{\lnot\varphi}$, respectively. The outputs are then determined as:
$\top$ if $q^{\prime}$ does not belong to the final states of
$\tilde{A}^{\lnot\varphi}$, $\bot$ if $q$ does not belong to the final states
of $\tilde{A}^{\varphi}$, and $?$ otherwise.

###### Example 1

Let $S$ be a system with alphabet
$\Sigma=\\{ev_{\\_}1,ev_{\\_}2,ev_{\\_}3\\}$, and $\varphi=\lozenge ev_{\\_}1$
be an LTL property to verify. In natural language, $\varphi$ reads as:
“eventually event $ev_{\\_}1$ is going to be observed”. The Moore machine
implementing the monitor function $Mon_{\\_}{{\varphi}}$ is reported in Figure
2. As long as events $ev_{\\_}2$ and $ev_{\\_}3$ are observed, the Moore
machine will stay in the initial state with output $?$. As long as it stays in
this state, there might be continuations where $ev_{\\_}1$ will never be
observed (i.e., the corresponding states in $\tilde{A}^{\varphi}$ and
$\tilde{A}^{\lnot\varphi}$ are both finals). But, when $ev_{\\_}1$ is
observed, then the state changes to a positive state, with output $\top$. In
fact, after observing $ev_{\\_}1$, any trace determines positively $\varphi$
since there is no continuation capable of violating $\varphi$ (i.e., the
corresponding state in $\tilde{A}^{\lnot\varphi}$ is not final).

?$\displaystyle\top$$\displaystyle ev_{\\_}{1}$$\displaystyle
ev_{\\_}{2},ev_{\\_}{3}$$\displaystyle*$inconclusive statepositive
state$\displaystyle*$any eventinitial state

Figure 2: Moore machine instantiated for the monitor generated by $\varphi$ of
Example 1.

##  3 Monitorability

_Monitorability_ [17] refers to the branch of RV focused on the delineation of
which formal properties can be monitored. It is crucial to understand
monitorability for performing efficient verification at runtime of formal
properties. However, the level of detail such notion is defined in the
literature may vary. It has a wide range of definitions, some are more
restrictive, while others are more flexible. A thorough presentation of the
existing variations of monitorability can be found in [3]; where the authors
report a complete guide on monitorability and its uses.

In this paper, we consider the definitions of monitorability introduced by
Pnueli and Zaks [26], where the concept of monitorability was generalised
w.r.t. its first appearance [17]. We chose their view of monitoriability since
it is one of the most commonly cited by the community and it is less
restrictive on the set of non-monitorable properties than other definitions
found in the literature.

###### Definition 2

A property $\varphi$ is ${\sigma}\textrm{-}monitorable$, where
$\sigma\in\Sigma^{*}$, if there is some $u\in\Sigma^{*}$ such that $\varphi$
is positively or negatively determined by $\sigma\bullet u$.

Definition 2 states that a property $\varphi$ is considered _monitorable_ with
respect to a finite trace of events $\sigma$, if we can find at least one
trace $u$, such that $\varphi$ is satisfied (i.e., $\sigma$ is a _good_
prefix) or violated (i.e., $\sigma$ is a _bad_ prefix) by the resulting
concatenated trace $\sigma\bullet u$. Intuitively, if a property is
${\sigma}\textrm{-}monitorable$, we know that for at least one possible trace
of events the monitor will be able to conclude the satisfaction or violation
of $\varphi$.

Following this reasoning, we define four different notions of monitorable
property. We start from less restrictive and move towards more restrictive
notions. Definition 3 uses a more relaxed notion of monitorability, where a
property $\varphi$ is considered _existentially_ monitorable when for at least
one trace of events $\sigma\in\Sigma^{*}$ it is possible to find a
continuation for which $\varphi$ is either satisfied or violated. Intuitively,
this means that some trace can bring the monitor to never conclude the
satisfaction or violation of $\varphi$. In the literature, these properties
are also known as _weak monitorable_ [9].

###### Definition 3

A property $\varphi$ is (existentially Pnueli-Zaks)
$\exists_{\\_}{PZ}\textrm{-}monitorable$ if it is
${\sigma}\textrm{-}monitorable$ for some finite trace $\sigma\in\Sigma^{*}$.
The class of all $\exists_{\\_}{PZ}\textrm{-}monitorable$ properties is
denoted as $\exists_{\\_}{PZ}$.

###### Example 2

Let us assume $\varphi=(ev_{\\_}1\land\lozenge
ev_{\\_}2)\lor(ev_{\\_}3\land\square\lozenge ev_{\\_}4)$, and
$\Sigma=\\{ev_{\\_}1,ev_{\\_}2,ev_{\\_}3,ev_{\\_}4\\}$. This is an example of
a $\exists_{\\_}{PZ}\textrm{-}monitorable$ property, since we can find some
$\sigma\in\Sigma^{*}$ for which $\varphi$ is ${\sigma}\textrm{-}monitorable$;
e.g., any trace starting with $ev_{\\_}1$ can eventually satisfy $\varphi$ (by
observing $ev_{\\_}2$). Furthermore, every trace $\sigma\in\Sigma^{*}$
starting with $ev_{\\_}3$ is not ${\sigma}\textrm{-}monitorable$, since there
is no continuation $u\in\Sigma^{*}$ s.t. $\sigma\bullet u$ positively or
negatively determines $\varphi$. Figure 3 reports the monitor obtained by
$\varphi$.

???$\displaystyle\bot$$\displaystyle\top$$\displaystyle
ev_{\\_}{1}$$\displaystyle ev_{\\_}{2}$$\displaystyle*\setminus
ev_{\\_}{2}$$\displaystyle*$$\displaystyle*$$\displaystyle
ev_{\\_}{3}$$\displaystyle
ev_{\\_}{2},ev_{\\_}{4}$$\displaystyle*$inconclusive statenegative
statepositive state$\displaystyle*$any event$\displaystyle*\setminus
ev_{\\_}{i}$any event but $\displaystyle ev_{\\_}{i}$initial state

Figure 3: Moore machine of the $\exists_{\\_}{PZ}\textrm{-}monitorable$
property $\varphi$ presented in Example 2.

Definition 4 introduces a more restrictive notion of monitorability, where a
property $\varphi$ is considered _universally_ monitorable when for all finite
traces $\sigma\in\Sigma^{*}$, it is possible to find a continuation for which
$\varphi$ is either satisfied or violated. This means that no trace can bring
the monitor to never conclude the satisfaction or violation of $\varphi$.

###### Definition 4

A property $\varphi$ is (universally Pnueli-Zaks)
$\forall_{\\_}{PZ}\textrm{-}monitorable$ if it is
${\sigma}\textrm{-}monitorable$ for all finite trace $\sigma\in\Sigma^{*}$.
The class of all $\forall_{\\_}{PZ}\textrm{-}monitorable$ properties is
denoted as $\forall_{\\_}{PZ}$.

###### Example 3

Let us assume $\varphi=(ev_{\\_}1\rightarrow\lozenge
ev_{\\_}2)\lor(ev_{\\_}3\rightarrow\square ev_{\\_}4)$, and
$\Sigma=\\{ev_{\\_}1,ev_{\\_}2,ev_{\\_}3,ev_{\\_}4\\}$. This is an example of
a $\forall_{\\_}{PZ}\textrm{-}monitorable$ property, since for every
$\sigma\in\Sigma^{*}$, the property is ${\sigma}\textrm{-}monitorable$; we can
always find a continuation $u\in\Sigma^{*}$ s.t. the $\varphi$ is positively
or negatively determined. This can be seen on the left branch where we have
the possibility to satisfy the property by observing (eventually) $ev_{\\_}2$
(positive); while on the right branch, we have the possibility to violate the
property by observing something different from $ev_{\\_}4$ (negative). Figure
4 reports the monitor obtained by $\varphi$.

??$\displaystyle\bot$$\displaystyle\top$$\displaystyle
ev_{\\_}{1}$$\displaystyle ev_{\\_}{2}$$\displaystyle*\setminus
ev_{\\_}{2}$$\displaystyle*$$\displaystyle
ev_{\\_}{2},ev_{\\_}{4}$$\displaystyle*$?$\displaystyle
ev_{\\_}{4}$$\displaystyle ev_{\\_}{3}$$\displaystyle*\setminus ev_{\\_}{4}$

Figure 4: Monitor (as Moore machine) of the
$\forall_{\\_}{PZ}\textrm{-}monitorable$ property $\varphi$ presented in
Example 3.

Monitorable properties are defined according to Definition 4 in a variety of
past research [8, 6, 21, 15, 17]. The reason for this is that any other notion
of monitorability, such as the one proposed in Definition 3, does not give any
guarantees on the monitor used to verify the property. Indeed, if we consider
Definition 3, there is no guarantee that eventually the monitor will encounter
a trace of events $\sigma$ for which no continuation determines $\varphi$
positively or negatively. If this happens, then the monitor will just become
pointless, because it will remain in an inconclusive state forever (i.e., it
will never conclude anything about $\varphi$). In such scenarios, we follow
the notation used in [8] to refer to such a trace of events $\sigma$ as an
_ugly_ prefix, since it represents a case where nothing can (and nothing will)
be concluded. In order to avoid these scenarios, more restrictive rules over
monitorability are usually imposed; of which Definition 4 is a key example.

Next, we show that by restricting even more the notion of monitorability, we
find _Safety_ and _Co-Safety_ properties [4]. Definition 5 denotes the
properties of the kind “nothing bad will ever happen”.

###### Definition 5

A property $\varphi$ is a _safety_ property if every
$\sigma\not\in\llbracket{\varphi}\rrbracket$ has a prefix that determines
$\varphi$ negatively. The class of safety properties is denoted as Safe.

These properties can only be violated at runtime, which means the resulting
monitor can only report negative and inconclusive verdicts. This is due to the
fact that safety properties are satisfied only by infinite traces of events,
and at runtime we only have access to finite traces.

An example of a safety property can be found in the right branch of $\varphi$
in Example 3, i.e., $\square ev_{\\_}4$. This is a safety property where the
expected behaviour is to observe $ev_{\\_}4$ indefinitely. Thus, any
$\sigma\in\Sigma^{*}$ (the $\Sigma$ of Example 3) can be extended with a
continuation $u\in\Sigma^{*}$ s.t. $\sigma\bullet u$ negatively determines
$\varphi$. There is no continuation $u\in\Sigma^{*}$ s.t. $\sigma\bullet u$
positively determines $\varphi$, but this is not actually required for being
monitorable.

On the same level of restrictiveness, we have _Co-Safety_ properties.
Definition 6 denotes the properties of the kind “something good will
eventually happen”.

###### Definition 6

A property $\varphi$ is a _co-safety_ property if every
$\sigma\in\llbracket{\varphi}\rrbracket$ has a prefix that determines
$\varphi$ positively. The class of co-safety properties is denoted as CoSafe.

These properties can only be satisfied at runtime, which means the resulting
monitor can only report positive and inconclusive verdicts. This is due to the
fact that co-safety properties are violated only by infinite traces of events.

An example of a co-safety property can be found in the left branch of
$\varphi$ in Example 3, i.e., $\lozenge ev_{\\_}2$. This is a co-safety
property where the expected behaviour is to observe eventually $ev_{\\_}2$.
Thus, any $\sigma\in\Sigma^{*}$ (the $\Sigma$ of Example 3) can be extended
with a continuation $u\in\Sigma^{*}$ s.t. $\sigma\bullet u$ positively
determines $\varphi$. There is no continuation $u\in\Sigma^{*}$ s.t.
$\sigma\bullet u$ negatively determines $\varphi$, but once again this is not
required for being monitorable.

Note that, to check if a property belongs to the Safe class it is a PSPACE
problem, while to check if a property is in the CoSafe class it is an EXPSPACE
problem [28].

Figure 5 represents the different monitorability classes as sets. On the left,
the largest set corresponds to $\exists_{\\_}{PZ}$, which only requires the
properties to have at least one good prefix. Then, we have
$\forall_{\\_}{PZ}$, which requires the properties to have only good prefixes.
After that, we find the _Safe_ and _CoSafe_ classes, which are included in
$\forall_{\\_}{PZ}$ by construction. Since for every safety (resp. co-safety)
property and $\sigma\in\Sigma^{*}$, we may find $u\in\Sigma^{*}$ s.t.
$\sigma\bullet u$ negatively (resp. positively) determines the property. On
the right, we have the rest of the properties, which are considered _non-
monitorable_. These are the properties for which there is no trace
$\sigma\in\Sigma^{*}$ which determines the property neither positively nor
negatively. Thus, properties for which all traces are ugly.

$\displaystyle\exists_{\\_}{PZ}$$\displaystyle\forall_{\\_}{PZ}$$\displaystyle
CoSafe$$\displaystyle Safe$$\displaystyle Non\ Monitorable$

Figure 5: Hierarchy of classes of monitorable properties.

Note that the more restrictive the conditions for a property to be considered
monitorable are, the less these properties will be used in practice for
achieving RV. Thus, one has to find a good balance to be able to discard as
few properties as possible, and at the same time to correctly handle the
possible lack of guarantees on the resulting monitoring process. The presence
of a monitor that can reach a state with nothing to report should be avoided,
or at least detected and handled.

In [26], Pnueli and Zaks propose a way to decide, given a finite trace
$\sigma$, if a property under consideration $\varphi$ is
${\sigma}\textrm{-}monitorable$. In this way, they can detect whether the
current observed trace is ugly and inform the user. The main difference with
our approach is at which level such check is performed. In their work this is
performed on the property; while in our work we perform it directly on the
monitor.

In [2, 13], the notion of monitorability is presented for linear and branching
flavours of Hennessy-Milner Logic with recursion (recHML) [19]. Differently
from us, they consider partial monitoring the monitors which derive from
either safety or co-safety properties (not both). Instead, we consider the
monitors which are not always capable of determining the property, either
positively or negatively.

It is important to note that a property can start monitorable (resp. non-
monitorable) and become non-monitorable (resp. monitorable) depending on the
information known about the SUA. In fact, as pointed out in [15], the
monitorability result w.r.t. a property may change under assumptions on the
SUA. If we know how the system behaves (e.g., a model of the system exists),
then we can rewrite the property accordingly and this can change the answer to
the monitorability question.

To the best of our knowledge, our work is the first that tackles the practical
implications of partial monitoring; where monitors are not assumed to be able
to always conclude the satisfaction or violation of the formal property under
analysis, and where it is not always simple to determine if a property is
monitorable or not.

##  4 Partial Monitoring

In this section, we introduce the notion of partial monitoring from a
practical perspective. First, we formally define partial monitors and show an
example of how it works based on a property from a previous example. Then, we
discuss the application and benefits of partial monitoring to an example of an
autonomous rover performing remote inspection tasks. Finally, we present the
implementation details of our tool, which is capable of automatically
synthesising partial monitors from existing monitors for non-monitorable
properties, and discuss the engineering aspects of our approach.

In Definition 1, we had a standard three-valued monitor. Usually, a monitor is
intended to be _complete_ , in the sense that a verdict is always assumed to
be returned. This happens due to the presence of the inconclusive verdict
($?$), which is returned until the satisfaction ($\top$) or violation ($\bot$)
of the property can be concluded. Nonetheless, in the standard definition, the
property is assumed to be $\forall_{\\_}{PZ}\textrm{-}monitorable$. Moreover,
most of the time these are safety properties, since RV is usually applied in
scenarios where it is used to verify that “nothing bad will ever happen”.

######  Definition 7 (Partial Monitor)

Let $S$ be a system with alphabet $\Sigma$, and $\varphi$ be an LTL property.
Then, a _partial monitor_ for $\varphi$ is a function
$Mon_{\\_}{{\varphi}}:\Sigma^{*}\rightarrow\mathbb{B}_{\\_}4$, where
$\mathbb{B}_{\\_}4=\\{\top,\bot,?,\upchi\\}$:

$Mon_{\\_}{{\varphi}}({\sigma})=\left\\{{\begin{tabular}[]{cl}$\top$&{\qquad$\forall_{\\_}{u\in\Sigma^{\omega}}.\sigma\bullet
u\in\llbracket{\varphi}\rrbracket$}\\\
$\bot$&{\qquad$\forall_{\\_}{u\in\Sigma^{\omega}}.\sigma\bullet
u\notin\llbracket{\varphi}\rrbracket$}\\\
$?$&{\qquad$\exists_{\\_}{u\in\Sigma^{*}}.((\forall_{\\_}{u^{\prime}\in\Sigma^{\omega}}.\sigma\bullet
u\bullet
u^{\prime}\in\llbracket{\varphi}\rrbracket)\lor(\forall_{\\_}{u^{\prime}\in\Sigma^{\omega}}.\sigma\bullet
u\bullet u^{\prime}\notin\llbracket{\varphi}\rrbracket))$}\\\
$\upchi$&{\qquad$otherwise$}\\\ \end{tabular}}\right.$

where $\bullet$ is the standard trace concatenation operator.

Definition 7 presents the notion of a _partial monitor_ , which differs from
Definition 1 in the values returned as outcome of the verification. An
additional output “give up” value is added, i.e., $\upchi$. With $\upchi$, the
monitor can explicitly give up on the current execution and inform the
user/system that there is no point in continuing to monitor this property. To
make the addition of this new output possible, we updated the condition for
returning $?$. The monitor now requires the existence of a future continuation
of $\sigma$ which will make the monitor conclude with a final verdict ($\top$
or $\bot$). If that is the case, then the monitor can conclude (for the
moment) an inconclusive verdict, and eventually, it might conclude a final
verdict. Otherwise, the monitor is unfortunately in a situation where $\sigma$
denotes an ugly prefix, where no possible continuation will ever allow the
monitor to conclude the satisfaction or violation of $\varphi$. When this
happens the monitor returns $\upchi$, which symbolises that it has given up on
the current analysis.

###### Example 4

Considering once again the property of Example 2,
$\varphi=(ev_{\\_}1\land\lozenge ev_{\\_}2)\lor(ev_{\\_}3\land\square\lozenge
ev_{\\_}4)$, with $\Sigma=\\{ev_{\\_}1,ev_{\\_}2,ev_{\\_}3,ev_{\\_}4\\}$. This
property is $\exists_{\\_}{PZ}\textrm{-}monitorable$, since not all
$\sigma\in\Sigma^{*}$ are ${\sigma}\textrm{-}monitorable$. For this reason
this property would usually be discarded, since no guarantees can be given
that the resulting monitor will be able to conclude anything. In this case, by
following Definition 7, we can update the monitor with the additional outcome
to represent the cases where it should give up. Figure 6 reports the partial
monitor obtained by updating the monitor from Figure 3.

?$\displaystyle\upchi$?$\displaystyle\bot$$\displaystyle\top$$\displaystyle
ev_{\\_}{1}$$\displaystyle ev_{\\_}{2}$$\displaystyle*\setminus
ev_{\\_}{2}$$\displaystyle*$$\displaystyle*$$\displaystyle
ev_{\\_}{3}$$\displaystyle ev_{\\_}{2},ev_{\\_}{4}$$\displaystyle*$

Figure 6: Partial monitor of the $\exists_{\\_}{PZ}\textrm{-}monitorable$
property $\varphi$ presented in Example 2. Here, we can note how the
previously inconclusive state on the right has now become a “give up” state
(grey colour).

Given a standard monitor, to obtain a partial monitor we add an additional
post-processing step after generating the Moore machine. From a Moore machine
representing the instantiation of a monitor, we compute for each state
labelled with $?$ the reachability of a state labelled with $\top$ or $\bot$.
Reaching these states means that the monitor cannot get stuck in an
inconclusive state indefinitely (i.e., it has no dead ends). This analysis can
be achieved in polynomial time w.r.t. the number of states and edges of the
Moore machine. Specifically, in the worst case scenario the time complexity is
$O(N^{2}+NE)$, with $N$ the number of states, and $E$ the number of edges.
But, to have a better understanding of the time complexity, it is important to
note the relation between $N$ and $\varphi$. In fact, the standard LTL monitor
synthesis procedure (Figure 1) generates a Moore machine with double
exponential size w.r.t. the size of the LTL property $|\varphi|$. Thus, if we
expand the time complexity w.r.t. to the property, we obtain that the approach
has time complexity $O(2^{2^{|\varphi|+1}}+2^{2^{|\varphi|}}E)$. Nonetheless,
properties are usually small in size, which makes the time complexity less
limiting.

###  4.1 A Remote Inspection Example

We demonstrate the usefulness of our approach by applying it to the remote
inspection example mentioned in the introduction. This example is based on a
simulation, first introduced in [29], of an autonomous rover deployed to
perform remote inspection of nuclear facilities. The rover has access to
sensors, which are used to detect the level of radiation, and a camera, which
is used to acquire images of tanks (containing radioactive material) to
perform an integrity analysis (e.g., deterioration of the container). The
objective of the rover is to patrol and inspect important locations (i.e.,
waypoints) around the facility. As part of the inspection of a particular
location, the rover has to take measurements of the radiation level when it
arrives in such location.

###### Example 5

We start by demonstrating our approach applied to this example with a very
simple property $\varphi=\square\lozenge inspect\\_tank\\_1$. This property is
shown in Figure 7, with Figure 7(a) containing the traditional Moore machine,
and then after applying our technique we can see in Figure 7(b) that the
monitor can only give up in this case. Intuitively, this property states that
it is always the case that eventually the rover will inspect the waypoint
_tank1_. Since the rover has to constantly patrol these waypoints, it makes
sense to represent this behaviour with such property. However, we note that
there are many other ways to write this property, and some may sacrifice
generalisation to write a property that is monitorable. That is a valid
approach, and for simple cases such as with this property it is indeed the
best solution, since after applying our approach we ended up with a monitor
that is only able to give up (i.e., no partial monitoring is possible).

?$\displaystyle*$

(a) Traditional Moore machine monitor generated from property $\varphi$.

$\upchi$$\displaystyle*$

(b) New monitor generated after applying our approach.

Figure 7: A simple property $\varphi=\square\lozenge inspect\\_tank\\_1$.

###### Example 6

Next, let us consider a more interesting property where we can demonstrate
that partial monitoring can indeed be useful:

$\displaystyle\varphi=radiation\\_low\;\mathop{\mathrm{\mathbf{U}}}((radiation\\_high\land\lozenge
move\\_to\\_decontamination)\lor$
$\displaystyle(radiation\\_medium\land\square\lozenge(inspect\\_tank\\_1\lor
inspect\\_tank\\_2\lor\ldots\lor inspect\\_tank\\_n)))$

This property says that we can observe the event radiation_low until we
observe either radiation_high or radiation_medium. Low, medium, and high
radiation refer to the level of radiation that is currently observed by the
radiation sensor. If radiation_high is observed, then eventually we have to
observe the event move_to_decontamination, which represents the command being
sent to move the rover to a decontamination zone (i.e., high level of
radiation can be dangerous to the rover). Otherwise, if we observe
radiation_medium, then we have to patrol one of the radiation tanks ($1\ldots
n$) to identify if there are any abnormalities.

??$\displaystyle\bot$$\displaystyle\top$$\displaystyle*$$\displaystyle*$$\displaystyle*$?$\displaystyle
rad\\_low$$\displaystyle
rad\\_high$$\displaystyle\begin{array}[]{{>{\displaystyle}l}}mv\\_dec,\\\
insp\\_t1,\\\ \ldots,\\\ insp\\_tn\end{array}$$\displaystyle
rad\\_medium$$\displaystyle\begin{array}[]{{>{\displaystyle}l}}rad\\_low,\\\
rad\\_high,\\\ insp\\_t1,\\\ \ldots,\\\ insp\\_tn\end{array}$$\displaystyle
mv\\_dec$

(a) Monitor (as Moore machine) for the property.

$\upchi$?$\displaystyle\bot$$\displaystyle\top$$\displaystyle*$$\displaystyle*$$\displaystyle*$?$\displaystyle
rad\\_low$$\displaystyle
rad\\_high$$\displaystyle\begin{array}[]{{>{\displaystyle}l}}mv\\_dec,\\\
insp\\_t1,\\\ \ldots,\\\ insp\\_tn\end{array}$$\displaystyle
rad\\_medium$$\displaystyle\begin{array}[]{{>{\displaystyle}l}}rad\\_low,\\\
rad\\_high,\\\ insp\\_t1,\\\ \ldots,\\\ insp\\_tn\end{array}$$\displaystyle
mv\\_dec$

(b) Updated monitor after applying our technique.

Figure 8: A property that deals with the different levels of radiation. _rad_
is short for radiation, _insp_ is short for inspection, _t_ is short for tank,
and _mv_dec_ is short for move to decontamination.

The monitor (represented as a Moore machine) for this more complex property is
shown in Figure 8. This monitor originally has three inconclusive states, as
shown in Figure 8(a). The first is the initial state which will stay
inconclusive when it observes _rad_low_ , until it observes _rad_high_ and
then moves to the left branch, or _rad_medium_ and then moves to the right
branch, or any other event and then moves to the centre branch. Since the
initial state is inconclusive, we have to expand it to look for positive and
negative states. The centre branch is immediately expanded into a negative
state, thus, we know that the initial state should remain inconclusive (i.e.,
not output give up). Looking at the left branch, we encounter the second
inconclusive state, but we can quickly notice that upon observing _mv_dec_ we
arrive in a positive state, thus, we also know that the inconclusive state in
the left branch should remain inconclusive. Finally, the third and last
inconclusive state can be found in the right branch. There is no transition
from this state to any other state that leads into positive or negative
states, therefore, this state should output give up. Figure 8(b) contains the
result of this reachability analysis.

###  4.2 Implementation

We made a Java program111https://github.com/AngeloFerrando/PartialMonitor
which implements the transformation from standard to partial monitor. This
tool depends on LamaConv222https://www.isp.uni-luebeck.de/lamaconv, a Java
library that is capable of translating expressions in temporal logics into
equivalent automata, and to generate monitors out of these automata. These
monitors can then be used for runtime verification and/or model checking. Our
tool calls LamaConv and makes it generate a standard three-valued LTL monitor.
After that, for each inconclusive state it performs a reachability analysis.
Each inconclusive state that cannot reach any non-inconclusive state (i.e.,
$\top$ or $\bot$ labelled states) is then labelled with $\upchi$ instead of
$?$. In this way, monitors can still be generated and used for partial
monitoring of non-monitorable properties, since ugly prefixes are explicitly
recognised and the monitoring process consequently interrupted.

From an engineering perspective, our tool takes as input an LTL property and
then provides a human-readable output. To be more precise, three input
parameters have to be set when executing our tool:

  1. 1.

the path to the folder containing LamaConv installation (where “
_rltlconv.jar_ ” can be found);

  2. 2.

$\varphi$, the LTL property that will be used for synthesising the monitor
(standard LTL syntax as accepted by LamaConv);

  3. 3.

$\Sigma$, the alphabet of the SUA.

Given the input described above, our tool starts by calling LamaConv, which
generates a character string in the intuitive Automata File Format (AFF)
format. This is then parsed by our tool into a Java object, and the
reachability analysis is performed to detect $\upchi$ (give up) states.

Our tool can generate two outputs, the updated AFF and/or a Java object. The
AFF can be directly read and processed as a string representation of the
monitor. When parsing this updated AFF into an application, the user should be
aware that the only change that our tool makes to the AFF is to update the
inconclusive states that were identified to never conclude the satisfaction or
violation of the property with a give up symbol (by replacing “?” with “x” in
the AFF). Otherwise, if using the Java object, then the tool can be included
directly as an external Java library, and the monitor can be used as a Java
object by calling the available methods. In this way, the monitor generated by
the tool can be easily integrated with third-party software.

##  5 Discussion

In this work, we presented an intuitive approach to make monitors capable of
giving up when necessary. As mentioned in Section 3, this is not the first
time the notion of monitorability has been studied. Nonetheless, w.r.t.
related work, we tackle the monitorability problem on a more practical level.
Indeed, there are plenty of works which study and explore the theoretical
aspects of what makes a property monitorable; but, not much has been done to
answer what we can do with monitorability in practice. For instance, when is
it the right time to give up on a property? Or more generally, what can we do
with a non-monitorable property? Naturally, there are scenarios where nothing
can be done. These are the cases when a property simply cannot be verified at
runtime, in any possible way (such as the property from Example 5). However,
there are scenarios where something can be rightfully concluded, albeit
partially. And these are the cases we aimed to exploit in this work. In
general, properties are expected to be fully monitorable (i.e.,
$\forall_{\\_}{PZ}\textrm{-}monitorable$), because when such constraint does
not hold, we do not have guarantees whether the monitor will ever conclude
anything useful. Nonetheless, if the monitor is capable of giving up by
recognising and handling ugly prefixes, then non-monitorable properties can be
monitored through the use of partial monitors.

Applying such analysis at the monitor level is very important, because this
does not only allow us to give up on the monitor at runtime, but also to reuse
our approach in various scenarios. Since the approach is based on the Moore
machine denoting the monitor (and not the property), it is formalism-agnostic
up to a certain level. Thus, we are not just limited to LTL for defining the
properties that can be used. We can use another logic as long as a Moore
machine can be synthesised. This would not require any modifications to our
approach at the theoretical level, but it does require changes in the
implementation. For example, either the logic can be converted into LTL if
possible, or an automaton representing the monitor needs to be generated (if
this automaton is a Moore machine we are done and ready to use our approach,
otherwise we need to convert it).

From a research perspective, by directly applying our approach on a Moore
machine, we also offer a much more reusable workflow. As long as a Moore
machine is generated, more challenging aspects can be explored. For instance,
Predictive Runtime Verification (PRV) [30, 20] can be deployed instead of
standard RV. In fact, works on PRV of LTL properties exist; where a model of
the system (a Büchi Automaton) is used to predict future events and to help
the monitor to conclude its verdict in advance (before actually observing the
events). In such works, the flow presented in Figure 1 is extended for
considering the model of the system as well. The important aspect for us is
that, even though the workflow is extended, the final result is still a Moore
machine, with the additional power of anticipating the conclusive outcomes.
Since our approach is directly applied on a Moore machine and not on the
property itself, we can still obtain partial monitoring for PRV by analysing
the resulting predictive Moore machine. This means we can apply our approach
to more challenging scenarios in the future, without the need to change
anything specific in the process.

To summarise, in this paper we introduced the notion of partial monitoring as
a practical view on monitorability, but it is important to note that the
theoretical aspects of partial monitorability are different and much harder to
tackle. On one hand we have partial monitoring, where we look into the
representation of an existing monitor and we identify if it has any states
where it should give up; if this is the case and the monitor still has other
valid states that are not give up, then we have a partial monitor. Partial
monitorability on the other hand, would deal with identifying what can make a
property partially monitorable; e.g., what is the relation of the chosen
logic’s operators with monitorability (if any) and how chaining these
operators together impacts monitorability, delineate the types of properties
that are more amenable and advantageous for partial monitoring, and so on.

##  6 Conclusions and Future Work

In this paper, we discussed the issue of handling monitors generated from non-
monitorable properties and how such monitors can be extended to give up when
no final verdict can be ever concluded. We described a practical technique to
perform reachability analysis of LTL monitors obtained using standard
synthesis approaches [8], and how the resulting _partial monitors_ can avoid
to get stuck in scenarios where no final verdict can be concluded, such as
when trying to monitor non-monitorable properties. We have demonstrated the
use of partial monitoring in an example from the robotics domain, where a
rover performing the inspection of a nuclear facility can be partially
verified at runtime using non-monitorable properties. We also described the
implementation details and engineering aspects of a tool that we developed to
automate the detection and synthesis of partial monitors.

This work has focused on the engineering and implications of monitorability
for the synthesis of partial monitors. In future work, we plan to extend the
approach to other formalisms, such as Metric Temporal Logic (MTL) [18], Signal
Temporal Logic (STL) [24], Runtime Monitoring Language (RML) [5], and so on.
We also want to integrate our approach with existing RV tools for autonomous
systems such as ROSMonitoring [11], which is a RV framework for the popular
middleware for robotic development Robot Operating System
(ROS)333https://www.ros.org/. Adding support to other formalisms requires
updates to the tool, since right now it can only take as input plain Moore
machines. This is important since more complex scenarios may require more
expressive formalisms than LTL, and the issue of having partial monitors (as
well as monitorability) arises in other formalisms as well.

## References

  * [1]
  * [2] Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2019): _Adventures in monitorability: from branching to linear time and back again_.  Proc. ACM Program. Lang. 3(POPL), pp. 52:1–52:29, 10.1145/3290365.
  * [3] Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir & Karoliina Lehtinen (2019): _An Operational Guide to Monitorability_.  In Peter Csaba Ölveczky & Gwen Salaün, editors: Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings, Lecture Notes in Computer Science 11724, Springer, pp. 433–453, 10.1007/978-3-030-30446-1_23.
  * [4] Bowen Alpern & Fred B. Schneider (1987): _Recognizing Safety and Liveness_.  Distributed Comput. 2(3), pp. 117–126, 10.1007/BF01782772.
  * [5] Davide Ancona, Luca Franceschini, Angelo Ferrando & Viviana Mascardi (2021): _RML: Theory and practice of a domain specific language for runtime verification_.  Sci. Comput. Program. 205, p. 102610, 10.1016/j.scico.2021.102610.
  * [6] Ezio Bartocci, Yliès Falcone, Adrian Francalanza & Giles Reger (2018): _Introduction to Runtime Verification_.  In Ezio Bartocci & Yliès Falcone, editors: Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science 10457, Springer, pp. 1–33, 10.1007/978-3-319-75632-5_1.
  * [7] Andreas Bauer, Martin Leucker & Christian Schallhart (2006): _Monitoring of Real-Time Properties_.  In S. Arun-Kumar & Naveen Garg, editors: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, Lecture Notes in Computer Science 4337, Springer, pp. 260–272, 10.1007/11944836_25.
  * [8] Andreas Bauer, Martin Leucker & Christian Schallhart (2011): _Runtime Verification for LTL and TLTL_.  ACM Trans. Softw. Eng. Methodol. 20(4), 10.1145/2000799.2000800.
  * [9] Zhe Chen, Yifan Wu, Ou Wei & Bin Sheng (2018): _Deciding weak monitorability for runtime verification_.  In Michel Chaudron, Ivica Crnkovic, Marsha Chechik & Mark Harman, editors: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, ACM, pp. 163–164, 10.1145/3183440.3195077.
  * [10] Edmund M Clarke (1997): _Model checking_.  In: International Conference on Foundations of Software Technology and Theoretical Computer Science, Springer, pp. 54–56, 10.1016/0304-3975(85)90223-3.
  * [11] Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mascardi (2020): _ROSMonitoring: A Runtime Verification Framework for ROS_.  In: Towards Autonomous Robotic Systems, Springer International Publishing, Cham, pp. 387–399, 10.1007/978-3-030-63486-540.
  * [12] Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Bernd-Holger Schlingloff, Michael Winikoff & Neil Yorke-Smith (2021): _Towards a framework for certification of reliable autonomous systems_.  Auton. Agents Multi Agent Syst. 35(1), p. 8, 10.1007/s10458-020-09487-2.
  * [13] Adrian Francalanza, Luca Aceto & Anna Ingólfsdóttir (2017): _Monitorability for the Hennessy-Milner logic with recursion_.  Formal Methods Syst. Des. 51(1), pp. 87–116, 10.1007/s10703-017-0273-z.
  * [14] Rob Gerth, Doron A. Peled, Moshe Y. Vardi & Pierre Wolper (1995): _Simple on-the-fly automatic verification of linear temporal logic_.  In Piotr Dembinski & Marek Sredniawa, editors: Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, IFIP Conference Proceedings 38, Chapman & Hall, pp. 3–18, 10.1007/978-0-387-34892-61.
  * [15] Thomas A. Henzinger & N. Ege Saraç (2020): _Monitorability Under Assumptions_.  In Jyotirmoy Deshmukh & Dejan Nickovic, editors: Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings, Lecture Notes in Computer Science 12399, Springer, pp. 3–18, 10.1007/978-3-030-60508-7_1.
  * [16] John A. Hertz, Anders Krogh & Richard G. Palmer (1991): _Introduction to the theory of neural computation_.  The advanced book program 1, Addison-Wesley.
  * [17] Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky & Mahesh Viswanathan (2002): _Computational Analysis of Run-time Monitoring - Fundamentals of Java-MaC_.  Electron. Notes Theor. Comput. Sci. 70(4), pp. 80–94, 10.1016/S1571-0661(04)80578-4.
  * [18] Ron Koymans (1990): _Specifying Real-Time Properties with Metric Temporal Logic_.  Real Time Syst. 2(4), pp. 255–299, 10.1007/BF01995674.
  * [19] Kim Guldstrand Larsen (1990): _Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion_.  Theor. Comput. Sci. 72(2&3), pp. 265–288, 10.1016/0304-3975(90)90038-J.
  * [20] Martin Leucker (2012): _Sliding between Model Checking and Runtime Verification_.  In: Runtime Verification, LNCS 7687, Springer, pp. 82–87, 10.1007/978-3-642-35632-210.
  * [21] Martin Leucker & Christian Schallhart (2009): _A brief account of runtime verification_.  J. Log. Algebraic Methods Program. 78(5), pp. 293–303, 10.1016/j.jlap.2008.08.004.
  * [22] Donald W. Loveland (1978): _Automated theorem proving: a logical basis_.  Fundamental studies in computer science 6, North-Holland.
  * [23] Joseph B. Lyons, Matthew A. Clark, Alan R. Wagner & Matthew J. Schuelke (2017): _Certifiable Trust in Autonomous Systems: Making the Intractable Tangible_.  AI Mag. 38(3), pp. 37–49, 10.1609/aimag.v38i3.2717.
  * [24] Oded Maler & Dejan Nickovic (2004): _Monitoring Temporal Properties of Continuous Signals_.  In Yassine Lakhnech & Sergio Yovine, editors: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, Lecture Notes in Computer Science 3253, Springer, pp. 152–166, 10.1007/978-3-540-30206-3_12.
  * [25] Amir Pnueli (1977): _The Temporal Logic of Programs_.  In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society, pp. 46–57, 10.1109/SFCS.1977.32.
  * [26] Amir Pnueli & Aleksandr Zaks (2006): _PSL Model Checking and Run-Time Verification Via Testers_.  In Jayadev Misra, Tobias Nipkow & Emil Sekerinski, editors: FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings, Lecture Notes in Computer Science 4085, Springer, pp. 573–586, 10.1007/11813040_38.
  * [27] Michael O. Rabin & Dana S. Scott (1959): _Finite Automata and Their Decision Problems_.  IBM J. Res. Dev. 3(2), pp. 114–125, 10.1147/rd.32.0114.
  * [28] A. Prasad Sistla (1994): _Safety, Liveness and Fairness in Temporal Logic_.  Formal Aspects Comput. 6(5), pp. 495–512, 10.1007/BF01211865.
  * [29] Thomas Wright, Andrew West, Mauro Licata, Nick Hawes & Barry Lennox (2021): _Simulating Ionising Radiation in Gazebo for Robotic Nuclear Inspection Challenges_.  Robotics 10(3), 10.3390/robotics10030086.
  * [30] Xian Zhang, Martin Leucker & Wei Dong (2012): _Runtime Verification with Predictive Semantics_.  In: NASA Formal Methods, LNCS 7226, Springer, pp. 418–432, 10.1007/978-3-642-28891-337.


# Snowmass 2021 White Paper:
Tabletop experiments for infrared quantum gravity

Daniel Carney  Physics Division, Lawrence Berkeley National Lab, Berkeley, CA,
USA  Yanbei Chen  Theoretical Astrophysics 350-17, California Institute of
Technology, Pasadena, CA, USA  Andrew Geraci  Center for Fundamental Physics,
Department of Physics and Astronomy, Northwestern University, Evanston, IL,
USA  Holger Müller  Department of Physics, University of California, Berkeley,
CA, USA  Cristian D. Panda  Department of Physics, University of California,
Berkeley, CA, USA  Philip C. E. Stamp  Department of Physics and Astronomy,
University of British Columbia, Vancouver, BC  Theoretical Astrophysics,
Cahill, California Institute of Technology, Pasadena CA, USA  Jacob M. Taylor
Joint Center for Quantum Information and Computer Science/Joint Quantum
Institute, University of Maryland/NIST, College Park, MD, USA

###### Abstract

Progress in the quantum readout and control of mechanical devices from single
atoms to large masses may enable a first generation of experiments probing the
gravitational interaction in the quantum regime, conceivably within the next
decade. In this Snowmass whitepaper, we briefly outline the possibilities and
challenges facing the realization of these experiments. In particular, we
emphasize the need for detailed theories of modifications to the usual
effective QFT of gravitons in the infrared regime $E/L^{3}\ll m_{\rm
Pl}/\ell_{\rm Pl}^{3}$ in which these experiments operate, and relations to
possible UV completions.

Submitted to the Proceedings of the US Community Study

on the Future of Particle Physics (Snowmass 2021)

###### Contents

  1. I Introduction
  2. II Gravitational entanglement and existence of gravitons
  3. III Gravitational breakdowns of linear quantum mechanics
  4. IV Outlook

##  I Introduction

In recent years, building on foundational conceptual proposals Feynman (1971);
Eppley and Hannah (1977); Page and Geilker (1981), a number of authors have
discussed the idea of performing lab-scale experiments to probe key questions
about the quantum nature of gravity Carney  _et al._ (2019). These experiments
aim to test whether perturbatively quantized general relativity, viewed as an
effective quantum field theory Weinberg (1979); Donoghue (1994, 1995); Burgess
(2004), correctly describes nature at low energies. A number of alternative
scenarios have been proposed. These include models involving the gravitational
breakdown of quantum mechanics Diosi (1986); Penrose (1996), mixed classical-
quantum models Rosenfeld (1963a); Møller  _et al._ (1962); Kibble and
Randjbar-Daemi (1980a), models of gravity as an emergent force111Of course,
some emergent gravity models reproduce the graviton EFT at long wavelengths
Maldacena (1998). However, it is interesting to ask if consistent alternatives
could exist. Jacobson (1995); Verlinde (2011), and ideas about holographic
effects in the infrared Chou  _et al._ (2017); Verlinde and Zurek .
Experiments which are conceivably realizable within the next decade can make
decisive statements about these models.

In this Snowmass white paper, we briefly outline this emerging research
program. We provide a non-exhaustive outlook on theoretical issues and
experimental realizations, focusing on major open questions and research
opportunities for the next decade. We emphasize, in particular, the need for
detailed, theoretically consistent models of infrared gravity which deviate
from the standard graviton effective field theory.

##  II Gravitational entanglement and existence of gravitons

An elementary question about quantum gravity is whether the metric is itself a
quantized degree of freedom. Dyson and others have argued that it is likely to
be impossible to construct a detector sensitive to single graviton events
Dyson (2004); Rothman and Boughn (2006); Dyson (2013). However, there is an
alternative path to studying this question, inspired by logic familiar to
information theorists: we could test if gravity can produce a state which is
provably non-classical, following the classic ideas of Bell Bell (1964);
Aspect  _et al._ (1981). See Figure 1. Here we discuss both the experimental
approaches and interpretation of such tests.

A large number of experimental proposals to test gravity’s ability to entangle
objects now exist Kafri and Taylor ; Bahrami  _et al._ (2015); Anastopoulos
and Hu (2015); Bose  _et al._ (2017); Marletto and Vedral (2017); Haine
(2021); Qvarfort  _et al._ (2020); Carlesso  _et al._ (2019); Miao  _et al._
(2020); Howl  _et al._ (2021); Matsumura and Yamamoto (2020); Carney  _et al._
(2021a, b); Streltsov  _et al._ (2022); Pedernales  _et al._ (2021); Liu  _et
al._ (2021); Datta and Miao (2021); Feng and Vedral (2022). Generally
speaking, the major difficulty comes from the need to keep quantum coherence
in a massive object over a timescale long enough to see the entanglement.
Present proposals generally require using masses at least at the nanogram
scale and maintaining coherence times on the order of milliseconds. Some
proposals additionally require the ability to initialize at least one of the
masses in quantum superposition of two spatially distinct states, presenting a
substantial additional challenge with the large masses required. However,
while challenging, it is conceivable that one or more of these could be
implemented successfully within the next ten years.

Broadly speaking, there are two main classes of experimental proposals. In
both cases, the goal is to rule out any model of gravity which is incapable of
generating entanglement between massive objects. The first class of
experiments aims to allow a pair of systems to interact gravitational, and use
a literal Bell test (or continuous-variable analogue) to demonstrate that the
resulting two-body state is entangled. The second class instead aims to rule
out some specific behavior in models in which gravity is non-entangling; for
example, these models often (and perhaps always) involve anomalous heating
and/or decoherence from the gravitational dynamics. To highlight the general
ideas, we describe two examples of promising candidate systems for such tests.

The first involves preparing a massive quantum superposition of a levitated
particle to generate a gravitational interaction between itself and a second
particle also prepared in a quantum superposition. The phase evolution induced
by the gravitational interaction of the two levitated neutral test masses
could detectably entangle them via gravity even when they are placed far
enough apart to keep other interactions at bay Bose  _et al._ (2017); Marletto
and Vedral (2017). Having an embedded spin provides a handle for preparing and
manipulating the superposition state along with a possible entanglement
witness. In particular, these spin degrees of freedom can be used to perform a
CHSH-type Bell test on the masses Bose  _et al._ (2017). Such an experiment
would require a cryogenic, low-noise environment to suppress additional
decoherence mechanisms.

Figure 1: Schematic of a gravitational entanglement test. Two masses $M_{\rm
source}$ and $m_{\rm probe}$ are prepared in some initial product state. The
source mass is then superposed into two locations; if gravity is quantized
according to effective field theory rules, the Newton potential part of the
gravitational field will likewise become superposed. The probe mass is then
allowed to interact and measure this field state, and a Bell-type inequality
can be measured to determine if the joint state of the two masses is
entangled.

The second approach trades mass for coherence and distance, using new
techniques in which atom interferometers have long free evolution times
enabled either by microgravity Peters  _et al._ (1999) or by trapping atoms
during their free fall with potentially macroscopic (mm- to cm-scale)
separations Xu  _et al._ (2019). In turn, these atoms interact with a massive
resonator similar to those proposed in the first approach. The entanglement
between the mass and atoms can in principle be detected, and on a more
immediate basis, the atoms provide an extremely sensitive probe of any
anomalous gravitational heating of the resonator Carney  _et al._ (2021a, b);
Streltsov  _et al._ (2022). The interaction between the oscillator and the
atom in a spatial superposition will weakly modulate the visibility of the
atom interferometer, which could be detected in an experiment with high
sensitivity and long interaction times. Interrogation times of 20 seconds have
been achieved by suspending the spatially separated atomic wave packets in an
optical lattice formed by the clean wavefronts of the optical cavity Xu  _et
al._ (2019).

Many theoretical questions need to be answered in order to fully understand
the implications of these experiments. For example, a basic question arises:
these experiments probe gravity in the Newtonian limit. If we observe
entanglement generation through the Newton potential, is there a precise sense
in which this actually demonstrates that the gravitational field is quantized?
A number of authors have argued in the affirmative Belenchia  _et al._ (2018);
Galley  _et al._ (2020); Christodoulou and Rovelli (2019); Marshman  _et al._
(2020); Carney (2022); Danielson  _et al._ (2021); see Anastopoulos and Hu
(2018); Marletto and Vedral (2020); Rydving  _et al._ (2021) for some
dissenting opinions. In Carney (2022), it was demonstrated that observation of
non-relativistic gravitational entanglement would require either that
quantized gravitational radiation exists or that gravity violates either
Lorentz invariance or unitarity. More work on these issues will be of great
value, especially in the context of models in which gravity could generate
violations of unitarity.

Perhaps more importantly, there is a deep need for detailed, consistent models
of gravity coupled to quantum matter in the infrared. Of course, the Einstein
equations can be expanded perturbatively and the fluctuations quantized as
gravitons, leading to a perfectly well-defined EFT at the energies probed in
these experiments Weinberg (1979); Donoghue (1994, 1995); Burgess (2004). If
we want to test whether this EFT is the right model of nature, it behooves us
to produce alternative models which would produce some other behavior in such
experiments. A variety of models of “classical” gravity coupled to quantum
matter have been produced in recent years, for example Kafri  _et al._ (2014);
Tilloy and Diósi (2016); Hall and Reginatto (2018); Oppenheim (2018);
Oppenheim and Weller-Davies (2022); Donadi and Bassi (2022). These models are
constructed precisely to avoid classic no-go theorems of Weinberg and
Polchinski Weinberg (1989); Polchinski (1991) by working entirely in the
context of linear quantum mechanics; in the next section, we separately
discuss ideas about gravitational breakdown of linear time evolution in the
quantum state. Most of these are non-relativistic models; construction of or
no-go theorems on non-entangling gravitational models which are fully
generally covariant will be extremely valuable. Classification of possible
visible signatures would also be very useful; as a concrete example, the
classical-quantum model of Kafri  _et al._ (2014) leads to anomalous heating
with a rate proportional to $G_{N}$, and there may be ways of ruling out such
effects which do not require the complete gravitational Bell test-type
experiments Altamirano  _et al._ (2018); Carney  _et al._ (2021a, b);
Streltsov  _et al._ (2022).

##  III Gravitational breakdowns of linear quantum mechanics

Feynman argued as early as the 50’s that one could envisage a breakdown of
quantum mechanics, caused by gravity, and that if this occurred, then
dimensional arguments would predict it to occur for rest masses of order the
Planck mass $m_{\rm pl}\approx 20~{}{\rm\mu g}$ Feynman (1957, 1971). He
suggested that this breakdown would show up in situations involving
delocalized quantum states, in particular for the double-slit system.

Since 1957, several related ideas have emerged. Kibble argued Kibble (1981)
that a low-energy theory of quantum gravity would involve a non-linear brand
of QFT, driven by the non-linear metric field dynamics. Many authors have
discussed semiclassical gravity, in which the spacetime metric is determined
by the expectation value of the stress-energy tensor Kibble and Randjbar-Daemi
(1980b); Møller (1962); Rosenfeld (1963b); Kiefer (2007); Hu and Verdaguer
(2020).

More recently Penrose Penrose (1996); Marshall  _et al._ (2003) argued that if
a quantum superposition involved a massive body in different positions, the
“mismatch” between the different relevant spacetime metrics would cause a
relative phase uncertainty between them, a kind of “intrinsic decoherence” in
nature. He and others tried to use the non-linear Schrodinger-Newton equation
to predict departures from QM caused by Newtonian gravity Moroz  _et al._
(1998); Tod and Moroz (1999). In a different development, Diosi and others
Diósi (2014); Bassi  _et al._ (2013) examined a variant of the “stochastic
collapse” theories pioneered by Ghirardi et al. Ghirardi  _et al._ (1990); in
these “Continuous Stochastic Localization” (CSL) models, an extraneous noise
source associated with Newtonian gravity is supposed to collapse quantum wave-
functions. Such an external one-way noise field, a random energy source which
acts on the visible universe but is not itself perturbed, makes such theories
strictly phenomenological. Apart from the work of Kibble Kibble (1981), none
of these analyses are relativistic, nor have they been generalized to
relativistic fields.

There has also been criticism of non-linear theories. Some internal
inconsistencies of semiclassical gravity have been highlighted (notably by
Kibble Kibble (1981)). Furthermore, when quantum measurements are introduced
to non-linear theories of quantum mechanics, the non-collapse of quantum
states will violate classical gravity phenomenology Page and Geilker (1981),
while the collapse of quantum states may lead to superluminal communication
Polchinski (1991); Gisin (1989, 1990). It was shown that in nonlinear
theories, different ways of introducing quantum collapse and Born’s rule can
lead to different phenomenology Helou  _et al._ (2017), and that some
formulations might be immune to superluminal communications Kafri  _et al._
(2014); Helou (2019); Kaplan and Rajendran (2022).

An example of a consistent nonlinear theory of quantum gravity is provided by
the Correlated Worldline (CWL) theory of Stamp and collaborators Barvinsky
_et al._ (2018, 2021); Wilson-Gerow and Stamp (2022). This is a quantum field
theory of low-energy gravity in which gravitational correlations between
Feynman paths are built in at a fundamental level. These correlations violate
the superposition principle and make the theory non-linear; but the theory has
been shown to be consistent in that it has a consistent classical limit
(Einstein’s theory), consistent expansions in $\hbar$ and in $G_{N}$, and
satisfies all the relevant Ward identities Barvinsky  _et al._ (2018, 2021).
In fact exact solutions can be given for the propagators and equations of
motion in the CWL theory, which allow deviations from quantum mechanics to be
calculated with no adjustable parameters Wilson-Gerow and Stamp (2022); no
superluminal communication appears in these solutions. Predictions from this
theory for real experiments, when quantum measurement processes are involved,
will soon appear.

One of the great attractions of this field is that the theories are within
reach of experimental test. At the most massive end, quantum optomechanical
techniques allow, in principle, the transfer of the quantum coherence of light
to massive mechanical degrees of freedom, up to the 40 kg used in the LIGO
gravitational wave detectors Yu  _et al._ (2020). This could potentially be
used to demonstrate quantum trajectories and macroscopic quantum entanglement
at this scale. At mesoscopic scales, two groups have recently prepared
nanoparticles trapped in optical potentials near quantum pure states,
observing quantum trajectories of the particles and preparing non-classical
out-going light fields Delić  _et al._ (2020); Magrini  _et al._ (2021);
Militaru  _et al._ (2022). Rapid progress is now expected in the preparation
of much larger masses in non-classical states, as well as in the probing of
gravitational coupling between both small and intermediate-sized masses
Schmöle  _et al._ (2016); Cataño-Lopez  _et al._ (2020); Westphal  _et al._
(2021). We expect an explosion of experimental activity in this area in the
next few years.

##  IV Outlook

In this brief Snowmass 2021 contribution, we have provided some specific
examples of models and tests of the quantum behavior of gravitational
interactions that can be probed with realistic, tabletop experiments. There is
a clear need for further theoretical work. While a number of models have now
been proposed as alternative hypotheses, to be tested against the usual
graviton EFT picture, many have crucial open questions about their generally
covariant completions, renormalization, and detailed predictions in future
experiments. Studies of these models in astrophysical and cosmological
scenarios are almost non-existent and would be very interesting. Moreover,
while a number of experimental proposals now exist, there is considerable room
for new proposals which can alleviate some of the substantial technical
challenges involved. This includes both proposals for variants on the above
experiment and proposals for testing entirely new predictions from these
models, including the graviton effective field theory. We expect continued
rapid progress in this emerging research direction over the next decade, and
look forward to the first generation of real experimental tests of the quantum
nature of gravity.

## References

  * Feynman (1971) R. P. Feynman,  _Lectures on Gravitation, 1962-63_ (California Institute of Technology, 1971).
  * Eppley and Hannah (1977) K. Eppley and E. Hannah, “The necessity of quantizing the gravitational field,” Foundations of Physics 7, 51–68 (1977).
  * Page and Geilker (1981) D. N. Page and C. D. Geilker, “Indirect evidence for quantum gravity,” Physical Review Letters 47, 979 (1981).
  * Carney  _et al._ (2019) D. Carney, P. C. E. Stamp, and J. M. Taylor, “Tabletop experiments for quantum gravity: a user’s manual,” Classical and Quantum Gravity 36, 034001 (2019).
  * Weinberg (1979) S. Weinberg, “Phenomenological Lagrangians,” Physica A96, 327–340 (1979).
  * Donoghue (1994) J. F. Donoghue, “General relativity as an effective field theory: The leading quantum corrections,” Phys. Rev. D50, 3874–3888 (1994), arXiv:gr-qc/9405057 [gr-qc] .
  * Donoghue (1995) J. F. Donoghue, “Introduction to the effective field theory description of gravity,” in  _Advanced School on Effective Theories Almunecar, Spain, June 25-July 1, 1995_ (1995) arXiv:gr-qc/9512024 [gr-qc] .
  * Burgess (2004) C. P. Burgess, “Quantum gravity in everyday life: General relativity as an effective field theory,” Living Rev. Rel. 7, 5–56 (2004), arXiv:gr-qc/0311082 [gr-qc] .
  * Diosi (1986) L. Diosi, “A quantum-stochastic gravitation model and the reduction of the wavefunction,” Thesis, Hungarian Academy of Sciences (1986).
  * Penrose (1996) R. Penrose, “On gravity’s role in quantum state reduction,” Gen. Rel. Grav. 28, 581–600 (1996).
  * Rosenfeld (1963a) L. Rosenfeld, “On quantization of fields,” Nuclear Physics 40, 353 – 356 (1963a).
  * Møller  _et al._ (1962) C. Møller _et al._ , “Les théories relativistes de la gravitation,” Colloques Internationaux CNRS 91, 1–96 (1962).
  * Kibble and Randjbar-Daemi (1980a) T. W. B. Kibble and S. Randjbar-Daemi, “Nonlinear Coupling of Quantum Theory and Classical Gravity,” J. Phys. A13, 141 (1980a).
  * Maldacena (1998) J. M. Maldacena, “The Large N limit of superconformal field theories and supergravity,” Adv. Theor. Math. Phys. 2, 231–252 (1998), arXiv:hep-th/9711200 .
  * Jacobson (1995) T. Jacobson, “Thermodynamics of space-time: The Einstein equation of state,” Phys. Rev. Lett. 75, 1260–1263 (1995), arXiv:gr-qc/9504004 [gr-qc] .
  * Verlinde (2011) E. P. Verlinde, “On the Origin of Gravity and the Laws of Newton,” JHEP 04, 029 (2011), arXiv:1001.0785 [hep-th] .
  * Chou  _et al._ (2017) A. Chou, H. Glass, H. R. Gustafson, C. Hogan, B. L. Kamai, O. Kwon, R. Lanza, L. McCuller, S. S. Meyer, J. Richardson, _et al._ , “The holometer: an instrument to probe planckian quantum geometry,” Classical and Quantum Gravity 34, 065005 (2017).
  * (18) E. P. Verlinde and K. M. Zurek, “Observational signatures of quantum gravity in interferometers,” arXiv:1902.08207 [gr-qc] .
  * Dyson (2004) F. Dyson, “The world on a string,” New York Review of Books 51 (2004).
  * Rothman and Boughn (2006) T. Rothman and S. Boughn, “Can gravitons be detected?” Found. Phys. 36, 1801–1825 (2006).
  * Dyson (2013) F. Dyson, “Is a graviton detectable?” Int. J. Mod. Phys. A 28, 1330041 (2013).
  * Bell (1964) J. S. Bell, “On the einstein podolsky rosen paradox,” Physics Physique Fizika 1, 195 (1964).
  * Aspect  _et al._ (1981) A. Aspect, P. Grangier, and G. Roger, “Experimental tests of realistic local theories via bell’s theorem,” Phys. Rev. Lett. 47, 460 (1981).
  * (24) D. Kafri and J. M. Taylor, “A noise inequality for classical forces,” arXiv:1311.4558 [quant-ph] .
  * Bahrami  _et al._ (2015) M. Bahrami, A. Bassi, S. McMillen, M. Paternostro, and H. Ulbricht, “Is Gravity Quantum?” (2015), arXiv:1507.05733 [quant-ph] .
  * Anastopoulos and Hu (2015) C. Anastopoulos and B.-L. Hu, “Probing a gravitational cat state,” Class. Quantum Gravity 32, 165022 (2015).
  * Bose  _et al._ (2017) S. Bose, A. Mazumdar, G. W. Morley, H. Ulbricht, M. Toroš, M. Paternostro, A. A. Geraci, P. F. Barker, M. Kim, and G. Milburn, “Spin entanglement witness for quantum gravity,” Physical Review Letters 119, 240401 (2017).
  * Marletto and Vedral (2017) C. Marletto and V. Vedral, “Gravitationally induced entanglement between two massive particles is sufficient evidence of quantum effects in gravity,” Physical review letters 119, 240402 (2017).
  * Haine (2021) S. A. Haine, “Searching for signatures of quantum gravity in quantum gases,” New J. Phys. 23, 033020 (2021).
  * Qvarfort  _et al._ (2020) S. Qvarfort, S. Bose, and A. Serafini, “Mesoscopic entanglement through central–potential interactions,” J. Phys. B 53, 235501 (2020), arXiv:1812.09776 [quant-ph] .
  * Carlesso  _et al._ (2019) M. Carlesso, A. Bassi, M. Paternostro, and H. Ulbricht, “Testing the gravitational field generated by a quantum superposition,” New J. Phys. 21, 093052 (2019), arXiv:1906.04513 [quant-ph] .
  * Miao  _et al._ (2020) H. Miao, D. Martynov, H. Yang, and A. Datta, “Quantum correlations of light mediated by gravity,” Phys. Rev. A 101, 063804 (2020).
  * Howl  _et al._ (2021) R. Howl, V. Vedral, D. Naik, M. Christodoulou, C. Rovelli, and A. Iyer, “Non-gaussianity as a signature of a quantum theory of gravity,” PRX Quantum 2, 010325 (2021).
  * Matsumura and Yamamoto (2020) A. Matsumura and K. Yamamoto, “Gravity-induced entanglement in optomechanical systems,” Phys. Rev. D 102, 106021 (2020), arXiv:2010.05161 [gr-qc] .
  * Carney  _et al._ (2021a) D. Carney, H. Müller, and J. M. Taylor, “Using an atom interferometer to infer gravitational entanglement generation,” PRX Quantum 2, 030330 (2021a), arXiv:2101.11629 [quant-ph] .
  * Carney  _et al._ (2021b) D. Carney, H. Muller, and J. M. Taylor, “Comment on ”Using an atom interferometer to infer gravitational entanglement generation”,” (2021b), arXiv:2111.04667 [quant-ph] .
  * Streltsov  _et al._ (2022) K. Streltsov, J. S. Pedernales, and M. B. Plenio, “On the Significance of Interferometric Revivals for the Fundamental Description of Gravity,” Universe 8, 58 (2022), arXiv:2111.04570 [quant-ph] .
  * Pedernales  _et al._ (2021) J. S. Pedernales, K. Streltsov, and M. B. Plenio, “Enhancing Gravitational Interaction between Quantum Systems by a Massive Mediator,” (2021), arXiv:2104.14524 [quant-ph] .
  * Liu  _et al._ (2021) Y. Liu, J. Mummery, J. Zhou, and M. A. Sillanpää, “Gravitational forces between nonclassical mechanical oscillators,” Phys. Rev. Applied 15, 034004 (2021).
  * Datta and Miao (2021) A. Datta and H. Miao, “Signatures of the quantum nature of gravity in the differential motion of two masses,” (2021), arXiv:2104.04414 [gr-qc] .
  * Feng and Vedral (2022) T. Feng and V. Vedral, “Amplification of Gravitationally Induced Entanglement,” (2022), arXiv:2202.09737 [quant-ph] .
  * Peters  _et al._ (1999) A. Peters, K. Y. Chung, and S. Chu, “Measurement of gravitational acceleration by dropping atoms,” Nature 400, 849–852 (1999).
  * Xu  _et al._ (2019) V. Xu, M. Jaffe, C. D. Panda, S. L. Kristensen, L. W. Clark, and H. Müller, “Probing gravity by holding atoms for 20 seconds,” Science 366, 745–749 (2019).
  * Belenchia  _et al._ (2018) A. Belenchia, R. Wald, F. Giacomini, E. Castro-Ruiz, C. Brukner, and M. Aspelmeyer, “Quantum Superposition of Massive Objects and the Quantization of Gravity,” (2018), arXiv:1807.07015 [quant-ph] .
  * Galley  _et al._ (2020) T. D. Galley, F. Giacomini, and J. H. Selby, “A no-go theorem on the nature of the gravitational field beyond quantum theory,” (2020), arXiv:2012.01441 [quant-ph] .
  * Christodoulou and Rovelli (2019) M. Christodoulou and C. Rovelli, “On the possibility of laboratory evidence for quantum superposition of geometries,” Phys. Lett. B 792, 64–68 (2019).
  * Marshman  _et al._ (2020) R. J. Marshman, A. Mazumdar, and S. Bose, “Locality and entanglement in table-top testing of the quantum nature of linearized gravity,” Phys. Rev. A 101, 052110 (2020).
  * Carney (2022) D. Carney, “Newton, entanglement, and the graviton,” Phys. Rev. D 105, 024029 (2022), arXiv:2108.06320 [quant-ph] .
  * Danielson  _et al._ (2021) D. L. Danielson, G. Satishchandran, and R. M. Wald, “Gravitationally Mediated Entanglement: Newtonian Field vs. Gravitons,” (2021), arXiv:2112.10798 [quant-ph] .
  * Anastopoulos and Hu (2018) C. Anastopoulos and B.-L. Hu, “Comment on ”A Spin Entanglement Witness for Quantum Gravity” and on ”Gravitationally Induced Entanglement between Two Massive Particles is Sufficient Evidence of Quantum Effects in Gravity”,” (2018), arXiv:1804.11315 [quant-ph] .
  * Marletto and Vedral (2020) C. Marletto and V. Vedral, “Witnessing nonclassicality beyond quantum theory,” Physical Review D 102, 086012 (2020).
  * Rydving  _et al._ (2021) E. Rydving, E. Aurell, and I. Pikovski, “Do Gedankenexperiments compel quantization of gravity?” (2021), arXiv:2107.07514 [gr-qc] .
  * Kafri  _et al._ (2014) D. Kafri, J. M. Taylor, and G. J. Milburn, “A classical channel model for gravitational decoherence,” New J. Phys. 16, 065020 (2014), arXiv:1401.0946 [quant-ph] .
  * Tilloy and Diósi (2016) A. Tilloy and L. Diósi, “Sourcing semiclassical gravity from spontaneously localized quantum matter,” Physical Review D 93, 024026 (2016).
  * Hall and Reginatto (2018) M. J. W. Hall and M. Reginatto, “On two recent proposals for witnessing nonclassical gravity,” J. Phys. A 51, 085303 (2018), arXiv:1707.07974 [quant-ph] .
  * Oppenheim (2018) J. Oppenheim, “A post-quantum theory of classical gravity?” (2018), arXiv:1811.03116 [hep-th] .
  * Oppenheim and Weller-Davies (2022) J. Oppenheim and Z. Weller-Davies, “The constraints of post-quantum classical gravity,” JHEP 02, 080 (2022), arXiv:2011.15112 [hep-th] .
  * Donadi and Bassi (2022) S. Donadi and A. Bassi, “Seven non-standard models coupling quantum matter and gravity,” (2022), arXiv:2202.13542 [quant-ph] .
  * Weinberg (1989) S. Weinberg, “Precision Tests of Quantum Mechanics,”  _The Oskar Klein memorial lectures. Vol. 1: Lectures by C.N. Yang and S. Weinberg with translated reprints by O. Klein_ , Phys. Rev. Lett. 62, 485 (1989).
  * Polchinski (1991) J. Polchinski, “Weinberg’s nonlinear quantum mechanics and the EPR paradox,” Phys. Rev. Lett. 66, 397–400 (1991).
  * Altamirano  _et al._ (2018) N. Altamirano, P. Corona-Ugalde, R. B. Mann, and M. Zych, “Gravity is not a Pairwise Local Classical Channel,” Class. Quant. Grav. 35, 145005 (2018), arXiv:1612.07735 [quant-ph] .
  * Feynman (1957) R. P. Feynman, in  _Report from Chapel Hill conference_ , edited by C. M. DeWitt and D. Rickles (1957) [See particularly session VIII, sections 22, 23].
  * Kibble (1981) T. W. B. Kibble, “Is a semi-classical theory of gravity viable?” in  _Quantum Gravity 2: A Second Oxford Symposium_ , edited by C. J. Isham, R. Penrose, and D. W. Sciama (Oxford Univ. Press, 1981) pp. 63–80.
  * Kibble and Randjbar-Daemi (1980b) T. W. B. Kibble and S. Randjbar-Daemi, “Non-linear coupling of quantum theory and classical gravity,” Journal of Physics A: Mathematical and General 13, 141 (1980b).
  * Møller (1962) C. Møller, “Les théories relativistes de la gravitation,” Colloques internationaux CNRS 91 (1962).
  * Rosenfeld (1963b) L. Rosenfeld, “On quantization of fields,” Nuclear Physics 40, 353–356 (1963b).
  * Kiefer (2007) C. Kiefer,  _Quantum Gravity_ (Oxford University Press, 2007).
  * Hu and Verdaguer (2020) B.-L. B. Hu and E. Verdaguer,  _Semiclassical and Stochastic Gravity: Quantum Field Effects on Curved Spacetime_ (Cambridge University Press, 2020).
  * Marshall  _et al._ (2003) W. Marshall, C. Simon, R. Penrose, and D. Bouwmeester, “Towards quantum superpositions of a mirror,” Physical Review Letters 91, 130401 (2003).
  * Moroz  _et al._ (1998) I. M. Moroz, R. Penrose, and P. Tod, “Spherically-symmetric solutions of the schrödinger-newton equations,” Classical and Quantum Gravity 15, 2733 (1998).
  * Tod and Moroz (1999) P. Tod and I. M. Moroz, “An analytical approach to the schrödinger-newton equations,” Nonlinearity 12, 201 (1999).
  * Diósi (2014) L. Diósi, “Gravity-related spontaneous wave function collapse in bulk matter,” New Journal of Physics 16, 105006 (2014).
  * Bassi  _et al._ (2013) A. Bassi, K. Lochan, S. Satin, T. P. Singh, and H. Ulbricht, “Models of wave-function collapse, underlying theories, and experimental tests,” Reviews of Modern Physics 85, 471 (2013).
  * Ghirardi  _et al._ (1990) G. Ghirardi, R. Grassi, and A. Rimini, “Continuous-spontaneous-reduction model involving gravity,” Physical Review A 42, 1057 (1990).
  * Gisin (1989) N. Gisin, “Stochastic quantum dynamics and relativity,” Helv. Phys. Acta 62, 363–371 (1989).
  * Gisin (1990) N. Gisin, “Nonlocality and nonlinear quantum mechanics,” Phys. Lett. A 143, 1–7 (1990).
  * Helou  _et al._ (2017) B. Helou, J. Luo, H.-C. Yeh, C.-g. Shao, B. Slagmolen, D. E. McClelland, and Y. Chen, “Measurable signatures of quantum mechanics in a classical spacetime,” Physical Review D 96, 044008 (2017).
  * Helou (2019) B. M. Helou,  _Testing alternative theories of Quantum Mechanics with Optomechanics, and effective modes for Gaussian linear Optomechanics_ , Ph.D. thesis, California Institute of Technology (2019).
  * Kaplan and Rajendran (2022) D. E. Kaplan and S. Rajendran, “Causal framework for nonlinear quantum mechanics,” Phys. Rev. D 105, 055002 (2022), arXiv:2106.10576 [hep-th] .
  * Barvinsky  _et al._ (2018) A. O. Barvinsky, D. Carney, and P. C. E. Stamp, “Structure of Correlated Worldline Theories of Quantum Gravity,” Phys. Rev. D 98, 084052 (2018), arXiv:1806.08043 [gr-qc] .
  * Barvinsky  _et al._ (2021) A. O. Barvinsky, J. Wilson-Gerow, and P. C. E. Stamp, “Correlated Worldline theory: Structure and Consistency,” Phys. Rev. D 103, 064028 (2021), arXiv:2011.03601 [gr-qc] .
  * Wilson-Gerow and Stamp (2022) J. Wilson-Gerow and P. C. E. Stamp, “Propagators in the Correlated Worldline Theory of Quantum Gravity,” Phys. Rev. D in press (2022), arXiv:2011.14242 [gr-qc] .
  * Yu  _et al._ (2020) H. Yu, L. McCuller, M. Tse, N. Kijbunchoo, L. Barsotti, and N. Mavalvala, “Quantum correlations between light and the kilogram-mass mirrors of ligo,” Nature 583, 43–47 (2020).
  * Delić  _et al._ (2020) U. Delić, M. Reisenbauer, K. Dare, D. Grass, V. Vuletić, N. Kiesel, and M. Aspelmeyer, “Cooling of a levitated nanoparticle to the motional quantum ground state,” Science 367, 892–895 (2020).
  * Magrini  _et al._ (2021) L. Magrini, P. Rosenzweig, C. Bach, A. Deutschmann-Olek, S. G. Hofer, S. Hong, N. Kiesel, A. Kugi, and M. Aspelmeyer, “Real-time optimal quantum control of mechanical motion at room temperature,” Nature 595, 373–377 (2021).
  * Militaru  _et al._ (2022) A. Militaru, M. Rossi, F. Tebbenjohanns, O. Romero-Isart, M. Frimmer, and L. Novotny, “Ponderomotive squeezing of light by a levitated nanoparticle in free space,” arXiv preprint arXiv:2202.09063 (2022).
  * Schmöle  _et al._ (2016) J. Schmöle, M. Dragosits, H. Hepach, and M. Aspelmeyer, “A micromechanical proof-of-principle experiment for measuring the gravitational force of milligram masses,” Classical and Quantum Gravity 33, 125031 (2016).
  * Cataño-Lopez  _et al._ (2020) S. B. Cataño-Lopez, J. G. Santiago-Condori, K. Edamatsu, and N. Matsumoto, “High Q mg-scale monolithic pendulum for quantum-limited gravity measurements,” Phys. Rev. Lett. 124, 221102 (2020), arXiv:1912.12567 [quant-ph] .
  * Westphal  _et al._ (2021) T. Westphal, H. Hepach, J. Pfaff, and M. Aspelmeyer, “Measurement of gravitational coupling between millimetre-sized masses,” Nature 591, 225–228 (2021).