itemizestditemize

# Monitoring and Diagnosability of Perception Systems

Pasquale Antonante David I. Spivak Luca Carlone
Massachusetts Institute of Technology
Cambridge, MA 02139
{antonap, dspivak<EMAIL_ADDRESS>
###### Abstract

Perception is a critical component of high-integrity applications of robotics
and autonomous systems, such as self-driving cars. In these applications,
failure of perception systems may put human life at risk, and a broad adoption
of these technologies relies on the development of methodologies to guarantee
and monitor safe operation as well as detect and mitigate failures. Despite
the paramount importance of perception systems, currently there is no formal
approach for system-level monitoring. In this work, we propose a mathematical
model for runtime monitoring and fault detection of perception systems.
Towards this goal, we draw connections with the literature on self-
diagnosability for multiprocessor systems, and generalize it to (i) account
for modules with heterogeneous outputs, and (ii) add a temporal dimension to
the problem, which is crucial to model realistic perception systems where
modules interact over time. This contribution results in a graph-theoretic
approach that, given a perception system, is able to detect faults at runtime
and allows computing an upper-bound on the number of faulty modules that can
be detected. Our second contribution is to show that the proposed monitoring
approach can be elegantly described with the language of _topos theory_ ,
which allows formulating diagnosability over arbitrary time intervals.

An updated version of this paper can be found at
http://arxiv.org/abs/2011.07010

##  1 Introduction

The automotive industry is undergoing a change that could revolutionize
mobility. Self-driving cars promise a deep transformation of personal mobility
and have the potential to improve safety, efficiency (_e.g.,_ commute time,
fuel), and induce a paradigm shift in how entire cities are designed [1]. One
key factor that drives the adoption of such technology is the capability of
ensuring and monitoring safe execution. Consider Uber’s fatal self-driving
crash [2] in 2018: the report from the National Transportation Safety Board
stated that “inadequate safety culture” contributed to the fatal collision
between the autonomous vehicle and the pedestrian. The lack of safety
guarantees, combined with the unavailability of formal monitoring tools, is
the root cause of these accidents and has a profound impact on the user’s
trust. The AAA’s survey [3] shows that 71% of Americans claim to be afraid of
riding in a self-driving car. This is a clear sign that the industry needs a
sound methodology, embedded in the design process, to guarantee safety and
build public trust.

While safety guarantees have been investigated in the context of control and
decision-making [4, 5], the state of the art is still lacking a formal and
broadly applicable methodology for monitoring _perception systems_ , which
constitute a key component of any autonomous vehicle. Perception systems
provide functionalities such as localization and obstacle mapping, lane
detection, detection and tracking of other vehicles and pedestrians, among
others.

State of Practice. The automotive industry currently uses five classes of
methods to claim the safety of an autonomous vehicle (AV) [6], namely: miles
driven, simulation, scenario-based testing, disengagement, and proprietary.
The _miles driven_ approach is the most commonly used, and is based on the
statistical argument that if the probability of crashes per mile is lower in
autonomous vehicles than for humans, then autonomous vehicles are safer. This
approach is problematic since the meaningful111Driving on empty streets
provides less evidence of safety than driving in dense urban environments.
number of fault-free miles that the AV should drive is significant—on the
order of billions of miles [7, 6]—which would require years to achieve and
would not enable frequent software updates. The same approach can be made more
scalable through _simulation_ , but unfortunately creating a life-like
simulator is an open problem, for some aspects even more challenging than
self-driving itself. _Scenario-based_ testing is based on the idea that if we
can enumerate all the possible driving scenarios that could occur, then we can
simply expose the AV (via simulation, closed-track testing, or on-road
testing) to all of those scenarios and, as a result, be confident that the AV
will only make safe driving decisions. However, enumerating all possible
corner cases is a daunting (and system-dependent) task. Finally,
_disengagement_ [8] is defined as the moment when a human safety driver has to
intervene in order to prevent a hazardous situation. However, while less
frequent disengagements indicate an improvement of the AV behavior, they do
not give evidence of the system safety.

An established methodology to ensure safety throughout the life cycle of an
automotive system is to use a _standard_ that every manufacturer has to comply
with. In the automotive industry, the standard ISO 26262 (Road vehicles -
functional safety) [9] is a risk-based safety standard that applies to
electronic systems in production vehicles, including driver assistance and
vehicle dynamics control systems. A key issue is that ISO 26262 relies on the
presence of human drivers (and mostly focuses on electronic systems rather
than algorithmic aspects) hence it does not readily apply to fully autonomous
vehicles [10]. The recent ISO 21448 (Road vehicles - Safety of the intended
functionality) [11] is intended to complement ISO 26262. It provides guidance
on the applicable design, verification, and validation measures needed to
achieve the safety at higher levels of automation. The standard has been first
publicly released in 2019, and—while stressing the key role of perception—it
only provides high-level considerations to inform stakeholders. In June 2019,
11 major stakeholder in the automated driving industry including Aptiv, Baidu,
BMW, Intel, and Volkswagen published a report [12] on safety in autonomous
driving. The report focuses on highly autonomous vehicles, presenting an
overview of safety by design and providing a sound discussion of the
verification and validation of such systems. The report proposes a
verification and validation approach mainly based on testing, and suggests the
use of _monitors_ to detect off-nominal performance at the system and
subsystem level (including neural networks).

Perception has been subject to increasing attention also outside the automated
driving industry. For instance, autonomous aerial vehicles are expected to
disrupt air mobility in the same way autonomous cars are disrupting urban
mobility [13, 14]. A recent report from the European Union Aviation Safety
Agency (EASA) [15] acknowledges both the importance of such technologies and
the lack of standardized methods to guarantee trustworthiness of such systems.
The report [15] considers an automatic landing system as case study and
investigates the challenges in developing trustworthy AI, with focus on
machine learning.

These reports and standards stress the important role of perception for
autonomous systems and motivate us to design a rigorous framework for system-
level perception monitoring.

Related Work. Formal methods [16] have been recently used as a tool to study
safety of autonomous systems. Formal methods use mathematical models to
analyze and verify part of a program. The insight here is that these
mathematical models can be used to rigorously prove properties of the modeled
program. This approach has been successful for decision systems, such as
obstacle avoidance [4] and road rule compliance [17]. This is mainly due to
the fact that decisional specifications are usually model-based and have well-
defined semantics [5]. The challenge in applying this approach to perception
is related to the complexity of modeling the physical environment [18], and
the trade-off between evidence for certification and tractability of the model
[19].

Relevant to the approach presented is this paper is the class of _runtime
verification_ methods. Runtime verification is an online approach based on
extracting information from a running system and using it to detect (and
possibly react to) observed behaviors satisfying or violating certain
properties [20]. Traditionally, the task of evaluating whether a module is
working properly was assigned to a monitor, which verifies some input/output
properties on the module alone. Balakrishnan  _et al._ [21] use Timed Quality
Temporal Logic (TQTL) to reason about desiderable spatio-temporal properties
of a perception algorithm. Kang  _et al._ [22] use model assertions, which
similarly place a logical constraint on the output of a module to detect
anomalies. We argue that this paradigm does not fully capture the complexity
of perception pipelines: while monitors can still be used to infer the state
of a single module, perception pipelines provide an additional opportunity to
cross check the _compatibility_ of results across different modules. In this
paper we try to address this limitation.

Performance guarantees for perception have been investigated for specific
problems. In particular, related work on _certifiable algorithms_ [23, 24, 25]
provides algorithms that are capable of identifying faulty behaviors during
execution. These related works mostly focus on specific algorithms, while our
goal is to establish monitoring for perception _systems_ , including multiple
interacting modules and algorithms.

Contribution. In this paper we develop a methodology to detect and identify
faulty modules in a perception pipeline at runtime. In particular, we address
two questions (adapted from [26]):  (i) _Can I (as a developer) verify that
the perception algorithm is providing reliable interpretations of the
perception data?_ (ii) _Can I (as regulator) trace the steps that led to an
accident caused by an autonomous vehicle?_ Towards this goal, we draw
connections with the literature on self-diagnosability for multiprocessor
systems, and generalize it to (i) account for modules with heterogeneous
outputs, and (ii) add a temporal dimension to the problem to account for
modules interacting over time. This contribution results in a graph-theoretic
approach that, given a perception system, is able to detect faults at runtime
and allows computing an upper-bound on the number of faulty modules that can
be detected. This upper bound is related to the level of redundancy within the
system and provides a quantitative measure of robustness. Our second
contribution is to show that the proposed monitoring approach can be elegantly
described with the language of _topos theory_ [27, 28] and allows formulating
diagnosability and faults detection over arbitrary time intervals.

##  2 An Example of Perception Pipeline

Consider the system depicted in Fig. 1: this is an example of perception
system used to localize an autonomous vehicle (AV) using multiple sensor
streams. We are going to use this system as a running example throughout the
paper to elucidate our mathematical model.

Figure 1: Example of localization system for Autonomous Vehicles.

In Fig. 1, the AV observes the world through noisy sensors, each of which
provides information to various perception modules. These perception modules
collect, organize, and interpret sensory information in order to create a
model of the world. In this paper, for the sake of simplicity, we consider a
world model that includes only the absolute pose—position and heading—of the
AV, an element of the 3-dimensional Special Euclidean group $\mathrm{SE}(3)$.

In Fig. 1, each rectangle inside the “Perception” box represents a _perception
module_ , while each arrow represents a data stream. Let $V$ denote a set of
_variables_ ; in our example,
$V=\\{v_{\mathrm{gps}},v_{\mathrm{map}},v_{\mathrm{lidar}},v_{\mathrm{imu}},v_{\mathrm{camera}},v_{\mathrm{abs}},v_{\mathrm{odom}}\\}$.
We can tag each arrow with the variable it carries. Moreover, each variable
has its own type. Let $\operatorname{Type}:V\to\mathbf{Set}$ be a map; we say
that $\operatorname{Type}(v)$ is the type of variable $v$. For example,
$\operatorname{Type}(v_{\mathrm{imu}})={{\mathbb{R}}^{6}}$, a real vector of 6
elements listing the acceleration and angular velocities measured by the
Inertial Measurement Unit (IMU). At any instant of time, the system takes the
measurements from the sensors and estimates the AV’s absolute pose, denoted by
$v_{\mathrm{abs}}$. Let us analyze the modules in Fig. 1:

  * •

The Global Positioning System (GPS) provides raw latitude and longitude data
to the _GPS reader_ , which packages this information and sends it to _GPS
Data Processing_ , which in turn estimates the car’s absolute pose (variable
$v_{\mathrm{abs}}$).

  * •

The Light Detection and Ranging (LIDAR) sensor uses light in the form of a
pulsed laser to measure reflection distances, producing a 3D point cloud of
the surrounding environment; the _LIDAR reader_ gets the point cloud while the
_LIDAR Registration_ module estimates the relative motion between consecutive
time instants by comparing consecutive scans [23], The estimate of the
relative motion of the AV is commonly referred to as “odometry” in robotics
[29] (variable $v_{\mathrm{odom}}$).

  * •

The _High Definition Map Localization_ uses a given high definition map of the
environment to estimate the absolute position (variable $v_{\mathrm{abs}}$) of
the vehicle by comparing the LIDAR scan with the map.

  * •

The _Cameras_ provide images of the environment, the _Camera reader_ collects
raw images, while the _Visual Odometry_ module estimates the relative motion
of the vehicle by comparing two consecutive images (variable
$v_{\mathrm{odom}}$).

  * •

The _Inertial Measurement Unit_ (IMU) measures accelerations and angular
velocities of the car, then by integrating these values over time, _IMU
integration_ estimates the relative motion of the vehicle (variable
$v_{\mathrm{odom}}$).

  * •

Finally, the _Pose-Graph Optimization_ [29] module estimates the vehicle’s
pose by fusing the noisy absolute and relative pose measurements produced by
the other modules.

Errors are common throughout this pipeline, so it is crucial for the system to
self-diagnose these errors in real time, discard outliers, and produce
reliable estimates of the car’s pose (which can be then used for planning and
control purposes). For instance, when operating near tall buildings, the GPS
can provide unreliable measurements. Similarly, when used in crowded scenes,
visual odometry can provide incorrect motion estimates. In the next sections
we study how faults can be diagnosed, using this perception system as an
example.

##  3 Monitoring of Perception Systems

Our first contribution is to develop a mathematical model for monitoring and
fault diagnosis in perception systems. Towards this goal, we draw connections
with the literature on fault diagnosis in multiprocessors systems, which has
been extensively studied since the late 1960s. Section 3.1 reviews the notion
of diagnosability and existing results for fault detection and to characterize
diagnosable systems using the PMC (Preparata, Metze, and Chien) model [30].
Section 3.2 extends the notion of diagnosability to perception systems and
discusses how to model temporal aspects arising in real AV applications.

###  3.1 Diagnosability

In the PMC [30] model, a set of independent _processors_ is assembled such
that each processor has the capability to communicate with a subset of the
other processors, and all of the processors perform the same computation. In
such system a fault occurs whenever the outputs of a processor differs from
the outputs of fault-free processors; the problem is to identify which is
which. Each processor is assigned a particular subset of the other processors
for the purpose of testing. Using a comparison-based mechanism, the model aims
to characterize the set of faulty processors. Clearly, it is not possible to
determine the faulty subset in general, so much of the literature on
multiprocessor diagnosis considers two fundamental questions [31]:  (i) Given
a collection of processors and a set of tests, what is the maximum number of
arbitrary processors which can be faulty such that the set of faulty
processors can be uniquely identified?  (ii) Given a set of test results, does
there exist an efficient procedure to identify the faulty processors?  The key
tool to address these questions is the _diagnostic graph_ [30].

Diagnostic Graph. At any given time, each processor is assumed to be in one of
two states: _faulty_ or _fault-free_. Diagnosis is based on the ability of
processors to test— _i.e.,_ to provide an opinion about the faultiness
of—other processors. Formally we assume that each processor implements one or
more _consistency functions_ ; these are Boolean functions that return _pass_
($0$) or _fail_ ($1$), depending on whether the output of two processors is in
agreement.

To perform the diagnosis, we follow [30] and model the problem as a directed
graph $D=(U,E)$, where $U$ is the set of processors, while the edges $E$
represent the test assignments. In particular, for an edge $(i,j)\in E$, we
say that node $i$ is testing node $j$. The outcome of this test is the result
of the consistency functions of $i$, in other words $1$ (resp. $0$) if $i$
evaluates $j$ as faulty (resp. fault-free). Fault-free processors are assumed
to provide correct test results, whereas no assumption is made about tests
executed by faulty processors: they may produce correct or incorrect test
outcomes. We call $D$ the _diagnostic graph_.

The collection of all test results for a test assignment $E$ is called a
_syndrome_. Formally, a syndrome is a function $\sigma:E\to\\{0,1\\}$. The
syndrome is processed by an external entity which diagnoses the system, that
is, makes some determination about the faultiness status of every processor in
the system. The notion of $t$-diagnosability formalizes when it is possible to
use the syndrome to diagnose and identify faults in a system.

######  Definition 1 ($t$-diagnosability [30]).

A diagnostic graph $D=(U,E)$ with $|U|=n$ processors is _$t$ -diagnosable_
($t<n$) if, given any syndrome, all faulty processors can be identified,
provided that the number of faults presented does not exceed $t$.

What makes fault detection challenging is the fact that we can have multiple
processors that provide incorrect results but are consistent with each other.
This is formalized by the notion of consistent fault set.

######  Definition 2 (Consistent fault set [30]).

For a syndrome $\sigma$, denote the test outcome assigned to the edge $(i,j)$
by $\sigma_{ij}\in\\{0,1\\}$. For a $t$-diagnosable graph $D=(U,E)$ and a
syndrome $\sigma$, a subset $F\subseteq U$ is a _$t$ -consistent fault set_ if
and only if

  1. (i)

$|F|\leq t$;

  2. (ii)

if $\sigma_{ij}=1$ then either $i\in F$ or $j\in F$

  3. (iii)

if $i,j\in U\setminus F$ then $\sigma_{ij}=0$.

Item (ii) in Definition 2 says that if $\sigma_{ij}=1$ ($i$ disagrees with
$j$) then at least one between $i$ and $j$ must be outside the consistent
fault set. Item (iii) states that processors outside the faulty set are in
agreement with each other; note that the condition is not _if and only if_
because we are assuming that tests performed by faulty nodes are unreliable
(see example in Fig. 2), therefore we can have $\sigma_{ij}=0$ when $i$ is
faulty and returns a wrong test result.

Example. Consider the simple example in Fig. 2 (adapted from [30]). For the
graph in Fig. 2, a syndrome will be represented as a list of five elements,
$(\sigma_{12},\sigma_{23},\sigma_{34},\sigma_{45},\sigma_{51})$. Assume
exactly one of the processors, say  1 (w.l.o.g), is faulty. Then
$\sigma_{23}=\sigma_{34}=\sigma_{45}=0$ and $\sigma_{51}=1$, _i.e.,_ 5
correctly identifies  1 as faulty and $\sigma_{12}$ could be either 0 or 1:
being a faulty node,  1 may or may not correctly diagnose  2 ; in the figure
we label that edge by $x$. In this simple case it is easy to check that,
assuming there is only one faulty processor, we can correctly identify that
the faulty processor is  1 . It is natural to ask: can we identify a faulty
condition with two faulty processors? In this graph, we cannot: to prove that,
it is sufficient to show that two different faulty conditions generate the
same syndrome (Fig. 2c).

(a)

(b)

(c)

Figure 2: (a) Example of diagnostic graph with five processors and (b)-(c) two
faulty conditions (faulty processors shown in red) exhibiting the same
syndrome.

The problem of determining the maximum value of $t$ for which a given system
is $t$-diagnosable is called the _diagnosability problem_. We denote the
maximum value of $t$-diagnosability of a graph $D$ by $t(D)$.

####  3.1.1 Characterization of $t$-diagnosability

Consider a directed graph $D=(U,E)$. For $i\in U$, we denote by
$\delta_{\textnormal{in}}(i)$ the number of edges directed toward $i$ (in-
degree). We denote by $\delta_{\textnormal{in}}(D)=\min_{i\in
U}d_{\textnormal{in}}(i)$ the minimum in-degree of the graph. Moreover, we
denote $\Gamma(i)=\\{j\in U\mid(i,j)\in E\\}$ the _testable_ set of $i$
(outgoing neighbors of $i$). Finally, for $X\subset U$, denote
$\Gamma(X)=\\{\bigcup_{i\in X}\Gamma(i)\setminus X\\}$.

We can now state the following fundamental theorem.

######  Theorem 3 (Characterization of $t$-diagnosability [32]).

Let $D=(U,E)$ be a diagnostic graph with $|U|=n$ processors. Then $D$ is
$t$-diagnosable if and only if

  1. (i)

$n\geq 2t+1$;

  2. (ii)

$\delta_{\textnormal{in}}(D)\geq t$; and

  3. (iii)

for each integer $p$ with $0\leq p<t$, and each $X\subset U$ with $|X|=n-2t+p$
we have $|\Gamma(X)|>p$.

Using Theorem 3 we can quickly find that the maximum $t$ in the graph in Fig.
2 is $t=1$ because $t\leq\lfloor\frac{n-1}{2}\rfloor=2$ and
$t\leq\delta_{\textnormal{in}}(D)=1$. Moreover, condition (iii) holds ($t=1$
forces $p=0$ and each $X\subseteq U$ with $|X|=3$ has $|\Gamma(X)|>0$).

A naive implementation of Theorem 3 would lead to an algorithm of time
complexity $O(n^{t+2})$ [33]. Bhat [33] propose an improved algorithm to find
the maximum $t$ of an arbitrary graph in $O(n^{u+2}\log_{2}(u))$ where
$u=\min\\{\delta_{\textnormal{in}}(D),\lfloor(n-1)/2\rfloor\\}$. Since this
approach can be impractical for large graphs, they also propose a polynomial
algorithm to find a suboptimal value of $t$ in $O(|U|^{3/2}+|E|)$.

####  3.1.2 Fault Detection

Once we have a syndrome on a $t$-diagnosable graph, we would like to actually
identify the set of faulty processors, provided that the number of faults does
not exceed $t$. Dahbura  _et al._ [31] showed that the problem of identifying
the set of faulty processors is related to the problem of finding the minimum
vertex cover set of an undirected graph (i.e. the smallest set $C$ of vertices
such that every edge has an endpoint in $C$). In general, the problem of
finding a minimum vertex cover is in the class of NP-complete problems,
meaning that there is no known deterministic algorithm that is guaranteed to
solve the problem in polynomial time, but the validity of any solution can be
tested in polynomial time. However, the work [31] exploits some special
properties of $t$-diagnosable graphs to propose an algorithm with time
complexity $O(n^{2.5})$ for fault identification. In a later work, Sullivan
[34] proposes an algorithm with time complexity $O(t^{3}+|E|)$ for fault
identification and proved that this is the tightest bound if $t$ is
$o(n^{5/6})$. These results ensure us that fault identification is practical
in real-time and scales well with bigger diagnostic graphs.

###  3.2 Diagnosability for Perception

In this section we generalize the approach of Section 3.1 to make it
applicable to perception systems. In particular, while in Section 3.1 multiple
processors perform the same computation and yield the same type of output,
perception systems are characterized by the fact that each module produces
different variables and potentially at different rates (Fig. 1). Therefore, in
order to build on the diagnosability framework described in the previous
section, we have to  (i) define consistency functions for a perception system
with arbitrary modules, and  (ii) capture temporal aspects that are missing in
the original PMC model [30]

Figure 3: Example of diagnostic graph $D=(U,E)$ for the localization pipeline
in Fig. 1.

####  3.2.1 Perception Consistency Functions

Consistency functions are used to implement pairwise tests for each edge in a
diagnostic graph. Due to the heterogeneity of the modules of a perception
system, we can have different types of consistency functions, which we
describe in the rest of this section. Using these consistency functions, we
can build a diagnostic graph: for instance, in Fig. 3 we report an example of
diagnostic graph for the localization example in Fig. 1.

Input and Output admissibility. Consider the case in which the camera captures
a very dark image caused by a sudden change of brightness in the scene. Upon
receiving camera images, the Visual Odometry module can detect the
underexposed image as unintended and report a failure from testing the camera
module. If we look at the example in Fig. 1, we can capture this test as an
edge between modules $\leavevmode\hbox to13.76pt{\vbox
to13.76pt{\pgfpicture\makeatletter\hbox{\hskip 6.88237pt\lower-6.88237pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{10}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{5}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$. In perception
systems, this type of consistency function is very common. Following the same
reasoning we can add a consistency checks between any module and its
predecessor, for example, if the point cloud provided by the LIDAR (  3 ) to
LIDAR Registration (  8 ) contains $N$ coincident points we clearly have a
fault in the LIDAR module. These edges are added to the diagnosis graph in
Fig. 3. Note that using this logic we can also monitor output admissibility
(the output of a module will be the input of another).

Input Consistency. Consider the IMU integration module, suppose it receives
data from three IMUs, the module can compare the three noisy measurements and
detect if one of the three does not agree with the others; for example an IMU
provides very different acceleration measurements. Hence the IMU integration
module can test the three IMU reader modules.

Output Consistency. Consider the GPS reader and the Map reader. They don’t
directly share information but suppose that a GPS measurement return a
latitude and longitude that the map predicts to be occupied by water. The map
reader, using this information, can identify the faulty measurement of the
GPS, returning fail whenever testing the GPS. In our perception example, this
test correspond to an edge $\leavevmode\hbox to13.76pt{\vbox
to13.76pt{\pgfpicture\makeatletter\hbox{\hskip 6.88237pt\lower-6.88237pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{2}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{1}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ and/or
$\leavevmode\hbox to13.76pt{\vbox
to13.76pt{\pgfpicture\makeatletter\hbox{\hskip 6.88237pt\lower-6.88237pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{2}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{6}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$.

Input/Output Consistency. Consider the case in which Visual Odometry is not
able to correctly estimate the pose of the vehicle. After fusing all the
incoming pose measurements, the Pose-Graph Optimization module  11 , can
identify that visual odometry produced an off-nominal value [35]. Input/Output
consistency differs from Input consistency in that it needs to compute the
output variable in order to test the validity of the inputs. In our system
this example corresponds to the edges $\leavevmode\hbox to13.76pt{\vbox
to13.76pt{\pgfpicture\makeatletter\hbox{\hskip 6.88237pt\lower-6.88237pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{11}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{6}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$, $\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{11}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{7}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$, …,
$\leavevmode\hbox to13.76pt{\vbox
to13.76pt{\pgfpicture\makeatletter\hbox{\hskip 6.88237pt\lower-6.88237pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{11}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\to\leavevmode\hbox
to13.76pt{\vbox to13.76pt{\pgfpicture\makeatletter\hbox{\hskip
6.88237pt\lower-6.88237pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{6.68237pt}{0.0pt}\pgfsys@curveto{6.68237pt}{3.69061pt}{3.69061pt}{6.68237pt}{0.0pt}{6.68237pt}\pgfsys@curveto{-3.69061pt}{6.68237pt}{-6.68237pt}{3.69061pt}{-6.68237pt}{0.0pt}\pgfsys@curveto{-6.68237pt}{-3.69061pt}{-3.69061pt}{-6.68237pt}{0.0pt}{-6.68237pt}\pgfsys@curveto{3.69061pt}{-6.68237pt}{6.68237pt}{-3.69061pt}{6.68237pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-3.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\minipage[t]{11.3811pt}\leavevmode\hbox{}{10}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$.

Example. Each module in Fig. 1 can use one or more of these consistency
functions described above to test other modules in the system. Each test can
detect a subset of failures that might occur, so the combination of all
available tests maximize the set of detectable faults in the system. In Fig.
3, we report an example of diagnostic graph for the localization example in
Fig. 1. By inspection and using condition (ii) in Theorem 3, we know that
$t\leq 2$ because  6 has in-degree equal to $2$. By checking condition (iii)
we discover that the graph is in fact only $1$-diagnosable. In particular, for
$t=2$, $p=1$ and $X=\\{1,2,3,4,5,8,9,10\\}$ ($|X|=11-4+1=8$) we have that
$\Gamma(X)=\\{11\\}$ therefore $|\Gamma(X)|\leq p$. This means we can uniquely
identify faulty modules only in the case where just one such fault occurs.

####  3.2.2 Temporal Diagnostic Graphs

In the previous section, we considered instantaneous fault diagnosis. In other
words, at any iteration, given a diagnostic graph and a syndrome we can detect
and identify faulty processors only considering tests occurring at that time
instant. However, perception modules evolve over time and considering the
temporal dimension allows adding temporal checks and modeling systems with
modules operating at multiple frequencies. In the following, we extend the
notion of diagnostic graphs to account for the temporal dimension of
perception.

In a perception pipeline, different modules publish information at different
frequencies. For example consider the system in Fig. 1. Within each second,
the IMU publishes 100 times, whereas the GPS reader only publishes once. We
can thus take the subgraph $D^{\prime}\subseteq D$ on nodes according to
minimum publishing frequencies and with edges that have both endpoints in
$D^{\prime}$. For instance, consider the nodes that publish at least at
$100\text{\,}\mathrm{Hz}$, those nodes are  4 ,  9 , and  11 . The resulting
subgraph of $D$ that we would obtain taking these nodes in depicted in Fig.
4a. Note that we might have different subgraphs for each publishing frequency
as in Fig. 4. Clearly we can perform fault detection over each of these
“instantaneous” diagnostic graphs. However, as mentioned above, considering
the evolution of the system over time provides further opportunities for fault
detection.

(a)

(b)

(c)

(d)

Figure 4: Subgraphs of the diagnostic graph in Fig. 3, one for each publishing
frequency.

If we consider an arbitrary interval $[a,b]$ of time (taken in seconds), over
the interval we have the opportunity to collect multiple diagnostic graphs
with their syndromes (Fig. 5). Furthermore, the output of the modules of these
graphs cannot be arbitrary, and must have some temporal consistency. For
instance, because motion is continuous, measurements of the AV pose at
consecutive times should be close to one another. Another example is that,
since the AV has a limited braking power (imposed by physical constraints), a
set of consecutive IMU acceleration measurements cannot exceed some bounds.
Therefore the diagnostic graphs at different moments in time can be connected
via temporal consistency function, _i.e.,_ we can make tests (or edges) that
go across time. We call the collection of the diagnostic graphs in the time
interval $[a,b]$ and the corresponding temporal edges a $[a,b]$-temporal
diagnostic graph (Fig. 5). The simplest form of _temporal consistency_
involves an edge connecting two identical nodes occurring at consecutive time
steps, _e.g.,_ two consecutive IMU measurements. However it can easily be
extended to different modules and neighboring (but not adjacent) time steps.

Besides being more expressive, this approach has the potential to greatly
increase the $t$-diagnosability of the system. Intuitively, the temporal
diagnostic graph becomes larger, but also more diagnosable, when longer
intervals of time are considered.

######  Corollary 4.

If $D\subseteq D^{\prime}$ are two graphs with the same set of vertices, then
$t(D)\leq t(D^{\prime})$.

###### Proof.

Assume conditions (i), (ii), and (iii) hold for $\langle D,t\rangle$. Since
$D$ and $D^{\prime}$ have the same number of processors, condition (i) holds
for $\langle D^{\prime},t\rangle$. Since
$\delta_{\mathrm{in}}(D)\leq\delta_{\mathrm{in}}(D^{\prime})$ and for every
$X\subseteq U$ we have $\Gamma_{D}(X)\leq\Gamma_{D^{\prime}}(X)$, conditions
(ii) and (iii) hold also for $\langle D^{\prime},t\rangle$. ∎

We can prove that the $t$-diagnosability is monotonic under temporal
restriction.

######  Proposition 5.

Let $D=(\textsf{U},\textsf{E})$ be a diagnostic graph. Suppose given subsets
$\textsf{U}_{i}\subseteq\textsf{U}$ that cover U, in the sense that
$\textsf{U}=\cup_{i\in I}U_{i}$, and for each $i\in I$, let $D_{i}\subseteq D$
be the largest subgraph with vertices $\textsf{U}_{i}$. Then if each $D_{i}$
is $t$-diagnosable, so is $D$.

###### Proof.

Assume each $D_{i}$ is $t$-diagnosable, and suppose that $\sigma$ is a
syndrome for a $t$-consistent fault set on $D$ (so it has at most $t$-many
faulty nodes). Then its restriction to each $D_{i}$ has fewer than $t$-many
faulty nodes, so the faulty nodes in $D_{i}$ can be accurately diagnosed.
Since every node is in some $D_{i}$, every node can be accurately diagnosed,
so $D$ is $t$-diagnosable. ∎

Example. Let us consider a small interval of time, say $[a,a+0.02]$. In such
an interval of time we should get three different diagnostic graphs for the
$100\text{\,}\mathrm{Hz}$ rate (see Fig. 4a). Each of those graph is
$1$-diagnosable. Now suppose we can test consistency across one and two
consecutive instants, obtaining the temporal diagnostic graph in Fig. 5. The
diagnosability of the temporal diagnostic graph in Fig. 5 is now
$3$-diagnosable (_cf._ Theorem 3). From this example, one can see the
advantages of including the temporal dimension for fault diagnosis.

Figure 5: Example of _temporal diagnostic graph_ over a small time interval
($0.02\text{\,}\mathrm{s}$).

##  4 Temporal Type Theory

This section shows that temporal diagnostic graphs can be elegantly described
with the language of _topos theory_. In particular, in order to organize the
information of multiple graphs that interact over time-intervals of varying
length, as well as the diagnosability and collection of faulty nodes in these
graphs, we use the mathematical language of _temporal type theory_ as
described in [36]. In the following, Section 4.1 briefly reviews basic
concepts of topos theory, while Section 4.2 tailors these concepts to temporal
diagnostic graphs.

###  4.1 Sheaves, Behavior Types, and Toposes

In temporal type theory, one models various types of behavior using data
structures called _sheaves_. A sheaf $B$ assigns a set $B(a,b)$ to each open
interval $(a,b)\subseteq\mathbb{R}$, understood as the set of _possible
behaviors_ that can occur over the time-window $(a,b)$. For any subinterval
$(a^{\prime},b^{\prime})\subseteq(a,b)$, the sheaf also assigns a _restriction
map_ $-\big{|}_{[a^{\prime},b^{\prime}]}\colon B(a,b)\to
B(a^{\prime},b^{\prime})$, which crops the behavior $\beta\in B(a,b)$ to the
subwindow, returning some $\beta\big{|}_{[a^{\prime},b^{\prime}]}\in
B(a^{\prime},b^{\prime})$.

Every aspect of the vehicle motion and the perception system considered in
this paper has a representation in this common language of behavior types. For
example, at any moment of time, every variable $v\in V$ of type
$\operatorname{Type}(v)$ has an associated a behavior type

$\mathrm{Var}_{v}(a,b)\coloneqq\\{x\colon(a,b)\to\operatorname{Type}(v)\textnormal{,
continuous}\\}$

where the restriction map
$-\big{|}_{[a^{\prime},b^{\prime}]}\colon\mathrm{Var}_{v}(a,b)\to\mathrm{Var}_{v}(a^{\prime},b^{\prime})$
is given by composition. That is, given $x\in\mathrm{Var}_{v}(a,b)$, define
$x\big{|}_{[a^{\prime},b^{\prime}]}$ to be the composite
$(a^{\prime},b^{\prime})\subseteq(a,b)\xrightarrow{x}\operatorname{Type}(v)$.
Below we will discuss behavior types for diagnosing faults in the perception
pipeline as data arrives over intervals of time. To do so, we first construct
the behavior type $\mathrm{Grph}$ of all temporal diagnostic graphs. A
$(a,b)$-behavior, _i.e.,_ element of $\mathrm{Grph}(a,b)$, consists of a graph
$G=(U,E)$ together with a function $U\to(a,b)$, meaning that each node is
assigned a moment in that interval, indicating the moment at which it occurs.
For any $(a^{\prime},b^{\prime})\in(a,b)$, the restriction map sends $G$ to
$G\big{|}_{[a^{\prime},b^{\prime}]}$, the maximal subgraph on the nodes that
exist within the subinterval $(a^{\prime},b^{\prime})$; in other words it
includes all the edges from $G$ between those nodes.

All possible behavior types, as sheaves, form a _topos_ $\mathcal{B}$. A topos
is a well-studied algebraic system that has many useful formal properties [27,
28]. For example behavior types $A,B$ can be added (a behavior of $A+B$ is a
behavior of $A$ or a behavior of $B$), multiplied (a behavior of $A\times B$
consists of a pair $(a,b)$ of behaviors), exponentiated, etc. Moreover every
topos comes equipped with its own _internal language_ , which includes a full-
fledged constructive logic. In the internal language of $\mathcal{B}$, the
booleans are replaced with a notion of temporal truth values, a behavior type
$\mathtt{Prop}$ of all propositions. It comes equipped with all the constants,
operations, and quantifiers,
$\mathtt{true},\mathtt{false},\wedge,\vee,\Rightarrow,\neg,\forall,\exists$.
The internal language can be used to provide very short and intuitive
descriptions of complex objects. One writes the description set-
theoreatically, and then the topos machinery turns that description into one
that varies in time. For example, if one writes the standard definition of
vector space in the internal language, the result will be a vector space
changing in time.

Example. We can use the internal language to define the sheaf of _upper-
bounded naturals_ , denoted $\overline{\mathbb{N}}$. In the internal language
it is defined by
$\overline{\mathbb{N}}\coloneqq\\{u:\mathbb{N}\to\mathtt{Prop}\mid\forall
n:\mathbb{N},u(n)\Rightarrow u(n+1)\\}$, meaning “if $n$ is an upper bound,
then so is $n+1$”. This translates to saying that a behavior
$u\in\overline{\mathbb{N}}(a,b)$ assigns a natural number to each open
subinterval of $(a,b)$, and smaller subintervals can be assigned smaller
natural numbers.

###  4.2 Temporal Diagnostic Graphs as Behavior Types

Temporal diagnostic graphs such as the one in Fig. 5 have a special property:
any clipping to a subinterval has a lower diagnosability number. To be more
precise, let $D=(U,E)$ be a graph and for any $a\leq b\in\mathbb{N}$, let
$D_{[a,b]}=(U_{[a,b]},E_{[a,b]})$ denote the graph with vertices
$U_{[a,b]}=\\{(\tau,i)\in\mathbb{N}\times U\mid a\leq\tau\leq b\\}$ and edges

$E_{[a,b]}=\big{\\{}\left((\tau,i),(\tau,j)\right)\mid(i,j)\in
E\big{\\}}\;\cup\;\big{\\{}((\tau,i),(\tau+1,i))\mid i\in U,a\leq\tau\leq
b-1\big{\\}}$

Thus, the graph $U_{[a,b]}$ consists of $b-a+1$ copies of $D$, as well as
edges connecting corresponding nodes across neighboring copies. For example
$D_{[a,a]}\cong D$, whereas we can imagine $D_{[a,a+1]}$ as two panes, each a
copy of $D$, and an edge from each node in the first pane to the corresponding
node in the second pane.

Now for any frequency $f$ and graph $D=(U,E)$, consider a temporal graph
$\overline{D}$ with $\overline{D}(a,b)=D_{\big{[}\lceil a/f\rceil,\lfloor
b/f\rfloor\big{]}}$,222Note that the graph in Fig. 5 has strictly more edges
than $D_{[0,2]}$, so we can still conclude the result from Corollary 4. where
each vertex $(i,u)$ is sent to the time $\lceil a/f\rceil+f\cdot i$. It
consists of multiple panes, spaced $f$-apart, each isomorphic to $D$. We call
temporal graphs constructed as $\overline{D}$ was above _time-regular graphs_
and denote the subsheaf of time-regular graphs by
$\mathrm{Grph_{tReg}}\subseteq\mathrm{Grph}$.

It follows from Proposition 5 that if one clips a time-regular graph
$\overline{D}(a,b)$ to a smaller interval $(a^{\prime},b^{\prime})$, the
result will have a smaller diagnosability number. Thus we obtain a map of
sheaves $t\colon\mathrm{Grph_{tReg}}\to\overline{\mathbb{N}}$, sending each
time-regular graph $D$ to its diagnosability number $t(D)$. Note that this
contains a large amount of information: $D$ is not just one graph but a graph
$D(a,b)$ for every duration of time, and similarly $t(D)$ consists of a
natural number $t(D)(a,b)\in\mathbb{N}$ for every interval $(a,b)$.

Using the language of temporal type theory we can also model fault detection
over arbitrary intervals. Suppose actual data is coursing through the
perception pipeline. For every interval $(a,b)$ of time, we have a
diagnosability graph $D(a,b)$, and every node in it has published values for
each of its variables. This induces a function $\mathtt{Fault\\_free}\colon
U\to\mathtt{Prop}$, that sends every module $i\in U$ to the union of all
subintervals throughout which it is fault-free. The perception system is
trying to infer this function, but on short intervals does not have enough
data to determine it. Thus it returns $\mathtt{Not\\_known\\_faulty}\colon
U\to\mathtt{Prop}$ with
$\mathtt{Fault\\_free}\Rightarrow\mathtt{Not\\_known\\_faulty}$. For short
intervals, when the $t$-diagnosability number is low, this will often be a
strict inclusion: some faulty nodes may fail to be diagnosed. However by
auditing longer intervals, the decision layer can often _ex post facto_
diagnose the faulty nodes and obtain an equality.

##  5 Conclusion

We presented a novel methodology for fault diagnosis in perception systems.
Towards this goal, we drew connections with the literature on diagnosability
for multiprocessors systems and generalized it to account for heterogeneous
modules interacting over time, as the ones arising in perception systems. In
particular, we showed that considering the temporal dimension, _i.e.,_
assessing the consistency of the system behavior over time, has the potential
to enhance diagnosability, while still enabling the use of existing tools for
fault detection. Finally, we showed that the proposed monitoring approach can
be elegantly described with the language of _topos theory_ which allows the
formulation of diagnosability and fault detection over arbitrary time
intervals. While the approach is fairly general and applicable to a variety of
perception systems, we considered a _localization_ system as a case study.

We believe that the proposed notion of _temporal diagnostic graphs_ can
complement the literature and enhance the current practice, contributing to
the goal of achieving safety and trustworthiness in autonomous vehicle
applications. For instance, a system designer can use the tools proposed in
this paper to assess the diagnosability before deploying the vehicle on public
roads, or design the system in such a way that its fault diagnosability is
maximized. While deployed, the proposed framework allows the vehicle to have a
greater awareness of its operational envelope and enables real-time perception
monitoring via runtime diagnosability. Finally, for regulators, system-level
guarantees provide a more solid and rigorous ground for certification, and, in
the unfortunate case of an accident, the proposed approach increases
accountability by providing formal evidence about the root cause of the
failures.

This work opens a number of avenues for future work. First, we plan to provide
more examples of perception systems that can be modeled with (and can benefit
from) the proposed monitoring approach. Second, we plan to build on the
results presented in this paper to model an entire AV software architecture
using the language of temporal type theory.

truemoreauthor

truemoreauthor

## References

  * [1] Gary Silberg et al.  “Self-driving cars: The next revolution”  In _White paper, KPMG LLP & Center of Automotive Research_ 9.2, 2012, pp. 132–146
  * [2] NTSB  “Collision Between Vehicle Controlled by Developmental Automated Driving System and Pedestrian, Tempe, Arizona”, 2018  URL: https://www.ntsb.gov/investigations/AccidentReports/Reports/HAR1903.pdf
  * [3] American Automobile Association  “Three in Four Americans Remain Afraid of Fully Self-Driving Vehicles”, https://newsroom.aaa.com/2019/03/americans-fear-self-driving-cars-survey/, 2019
  * [4] Stefan Mitsch, Khalil Ghorbal, David Vogelbacher and André Platzer  “Formal verification of obstacle avoidance and navigation of ground robots”  In _The International Journal of Robotics Research_ 36.12 SAGE Publications Sage UK: London, England, 2017, pp. 1312–1340
  * [5] Mohammed Foughali et al.  “Formal verification of complex robotic systems on resource-constrained platforms”  In _2018 IEEE/ACM 6th International FME Workshop on Formal Methods in Software Engineering (FormaliSE)_ , 2018, pp. 2–9
  * [6] S. Shalev-Shwartz, S. Shammah and A. Shashua  “On a Formal Model of Safe and Scalable Self-driving Cars”  In _ArXiv_ abs/1708.06374, 2017
  * [7] Nidhi Kalra and Susan M Paddock  “Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability?”  In _Transportation Research Part A: Policy and Practice_ 94 Elsevier, 2016, pp. 182–193
  * [8] IEEE Connected Vehicles  “Google reports self-driving car disengagements”, 2015  URL: https://site.ieee.org/connected-vehicles/2015/12/15/
  * [9] ISO Standard  “Road vehicles – Functional safety” ISO 26262-1:2011, 2011
  * [10] P. Koopman and M. Wagner  “Challenges in Autonomous Vehicle Testing and Validation”  In _SAE Int. J. Trans. Safety_ 4.1, 2016
  * [11] ISO Standard  “Road vehicles — Safety of the intended functionality” ISO/PAS 21448:2019(en), 2019
  * [12] Aptiv et al.  “Safety First for Automated Driving”, 2019  URL: https://www.daimler.com/innovation/case/autonomous/safety-first-for-automated-driving-2.html
  * [13] Uber  “Fast-Forwarding to a Future of On-Demand Urban Air Transportation”, 2016  URL: https://d1nyezh1ys8wfo.cloudfront.net/static/PDFs/Elevate%2BWhitepaper.pdf
  * [14] EHang  “WhitePaper on Urban Air Mobility Systems”, 2020  URL: https://www.ehang.com/app/en/EHang%20White%20Paper%20on%20Urban%20Air%20Mobility%20Systems.pdf
  * [15] EASA and Daedalean  “Concepts of Design Assurance for Neural Networks” (pdf), 2020
  * [16] Félix Ingrand  “Recent trends in formal validation and verification of autonomous robots software”  In _2019 Third IEEE International Conference on Robotic Computing (IRC)_ , 2019, pp. 321–328
  * [17] Nima Roohi et al.  “Self-driving vehicle verification towards a benchmark”  In _arXiv preprint arXiv:1806.08810_ , 2018
  * [18] S. Seshia and D. Sadigh  “Towards Verified Artificial Intelligence”  In _ArXiv_ abs/1606.08514, 2016
  * [19] Matt Luckcuck et al.  “Formal specification and verification of autonomous robotic systems: A survey”  In _ACM Computing Surveys (CSUR)_ 52.5 ACM New York, NY, USA, 2019, pp. 1–41
  * [20] Ezio Bartocci and Yliès Falcone  “Lectures on Runtime Verification: Introductory and Advanced Topics”  Springer, 2018
  * [21] A. Balakrishnan et al.  “Specifying and Evaluating Quality Metrics for Vision-based Perception Systems”  In _Design, Automation Test in Europe Conference Exhibition (DATE)_ , 2019, pp. 1433–1438
  * [22] Daniel Kang, Deepti Raghavan, Peter Bailis and Matei Zaharia  “Model assertions for debugging machine learning”  In _NIPS_ , 2018
  * [23] H. Yang, J. Shi and L. Carlone  “TEASER: Fast and Certifiable Point Cloud Registration” (pdf) In _arXiv preprint arXiv: 2001.07715_ , 2020
  * [24] H. Yang and L. Carlone  “In Perfect Shape: Certifiably Optimal 3D Shape Reconstruction from 2D Landmarks” Arxiv version: 1911.11924, (pdf) In _IEEE Conf. on Computer Vision and Pattern Recognition (CVPR)_ , 2020
  * [25] Jesus Briales, Laurent Kneip and Javier Gonzalez-Jimenez  “A Certifiably Globally Optimal Solution to the Non-Minimal Relative Pose Problem”  In _IEEE Conf. on Computer Vision and Pattern Recognition (CVPR)_ , 2018
  * [26] Miles Brundage et al.  “Toward Trustworthy AI Development: Mechanisms for Supporting Verifiable Claims”  In _arXiv preprint arXiv:2004.07213_ , 2020
  * [27] Saunders MacLane and Ieke Moerdijk  “Sheaves in geometry and logic: A first introduction to topos theory”  Springer Science & Business Media, 2012
  * [28] Peter T Johnstone  “Sketches of an elephant: A topos theory compendium”  Oxford University Press, 2002
  * [29] C. Cadena et al.  “Past, Present, and Future of Simultaneous Localization and Mapping: Toward the Robust-Perception Age” arxiv preprint: 1606.05830, (pdf) In _IEEE Trans. Robotics_ 32.6, 2016, pp. 1309–1332  DOI: 10.1109/TRO.2016.2624754
  * [30] Franco P Preparata, Gernot Metze and Robert T Chien  “On the connection assignment problem of diagnosable systems”  In _IEEE Transactions on Electronic Computers_ IEEE, 1967, pp. 848–854
  * [31] Anton T. Dahbura and Gerald M. Masson  “An $O(n^{2.5})$ fault identification algorithm for diagnosable systems”  In _IEEE Transactions on Computers_ IEEE, 1984, pp. 486–492
  * [32] S Louis Hakimi and Ashok T Amin  “Characterization of connection assignment of diagnosable systems”  In _IEEE Transactions on Computers_ 100.1 IEEE, 1974, pp. 86–88
  * [33] KVS Bhat  “Algorithms for finding diagnosability level and t-diagnosis in a network of processors”  In _Proceedings of the ACM’82 conference_ , 1982, pp. 164–168
  * [34] Gregory F. Sullivan  “An $O(t^{3}+|E|)$ fault identification algorithm for diagnosable systems”  In _IEEE Transactions on Computers_ 37.4 IEEE, 1988, pp. 388–397
  * [35] P. Lajoie, S. Hu, G. Beltrame and L. Carlone  “Modeling Perceptual Aliasing in SLAM via Discrete-Continuous Graphical Models” extended ArXiv version: (pdf), Supplemental Material: (pdf) In _IEEE Robotics and Automation Letters (RA-L)_ , 2019
  * [36] P. Schultz and D.I. Spivak  “Temporal Type Theory: A topos-theoretic approach to systems and behavior”  Springer, Birkhauser, 2019


<concept_desc>Security and privacy Distributed systems security</concept_desc>
<concept_desc>Computer systems organization Reliability</concept_desc>
<concept_desc>Computer systems organization Availability</concept_desc>
<concept_desc>Information systems Record and block layout</concept_desc>
<concept_desc>Information systems Distributed storage</concept_desc>
<concept_desc>Applied computing Electronic commerce</concept_desc>

[500]Security and privacy Distributed systems security
[500]Computer systems organization Reliability
[300]Computer systems organization Availability
[300]Information systems Record and block layout
[100]Information systems Distributed storage
[300]Applied computing Electronic commerce

§ INTRODUCTION

§ SUPPLY CHAIN: A RUNNING EXAMPLE

§ DESIGN

§.§ Structure of a Block

§.§.§ Attestations

§.§.§ Labels

§.§.§ Availability Policies

§.§.§ Integrity Policies

§.§ Consensus

§.§ Structure of a Reference

Matthew suggests that the “Life of a Block” subsection is
wholly redundant with preceeding material, and so it has been
commented out.

§.§ Chains

§.§ Entanglement

§.§ Incentives

§ CONSISTENCY PROPERTIES

§.§ Joins and Meets

§.§ Causal Consistency

§.§ Chain Properties

§.§.§ Chains as Objects

§.§.§ Blocks as Transactions

§ APPLICATIONS

§.§ Simulating Existing Chains

§.§ Object Model

§.§.§ Supply Chain

§.§.§ Conflicts & Perceived Serializability

§.§ Banking

§.§ Timestamping

§ IMPLEMENTATION

§.§ Experimental Setup

§.§ Performance

§.§ Discussion

§ EVALUATION

§ EXTENSIONS

Lots of nice ideas here.
I suspect we should just save them for a future paper and use the
space here to explain all the existing great ideas more clearly
and convincingly.
You're probably right.
I suppose I just thought some of these were cool.
I've left this section in for the moment, but if and when
we want it gone, just comment out this part of body.tex.

§.§ Confidentiality

§.§ Block Deletion

§.§ Compacting Attestations

§ RELATED WORK

Unchained blocks:

Integrity meets:

§ CONCLUSION

§ ADDITIONAL APPLICATIONS

§.§ Version Control

§.§ Medical Records

§ BITCOIN TRANSACTIONS IN TWO ACCOUNTS OR LESS