11institutetext: Univ. Grenoble Alpes, CNRS, Grenoble INP111Institute of
Engineering Univ. Grenoble Alpes, VERIMAG

# Specification and Validation of Autonomous Driving Systems: A Multilevel
Semantic Framework

Marius Bozga  Joseph Sifakis

###### Abstract

Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent
systems whose specification and validation raises extremely challenging
problems. The paper presents a multilevel semantic framework for the
specification of ADS and discusses associated validation problems. The
framework relies on a formal definition of maps modeling the physical
environment in which vehicles evolve. Maps are directed metric graphs whose
nodes represent positions and edges represent segments of roads. We study
basic properties of maps including their geometric consistency. Furthermore,
we study position refinement and segment abstraction relations allowing
multilevel representation from purely topological to detailed geometric. We
progressively define first order logics for modeling families of maps and
distributions of vehicles over maps. These are Configuration Logics, which in
addition to the usual logical connectives are equipped with a coalescing
operator to build configurations of models. We study their semantics and basic
properties. We illustrate their use for the specification of traffic rules and
scenarios characterizing sequences of scenes. We study various aspects of the
validation problem including run-time verification and satisfiability of
specifications. Finally, we show links of our framework with practical
validation needs for ADS and advocate its adequacy for addressing the many
facets of this challenge.

###### Keywords:

autonomous driving system, map modeling, configuration logic, traffic rule
specification, scene and scenario description, runtime verification,
simulation and validation in the large

##  1 Introduction

The validation of ADS raises challenges far beyond the current state of the
art because of their overwhelming complexity and the integration of non-
explainable AI components. Providing sufficient evidence that these systems
are safe enough is a hot and critical need, given the underlying economic and
societal stakes. This objective mobilizes considerable investments and efforts
by key players including big tech companies and car manufacturers. The efforts
focus on the development of efficient simulation technology and common
infrastructure for modelling the physical environment of ADS and their desired
properties. They led in particular to the definition of common formats such as
OpenDRIVE [1, 2] for the description of road networks, and OpenSCENARIO [3]
for the description of complex, synchronized maneuvers that involve multiple
entities like vehicles, pedestrians and other traffic participants.
Additionally, several open simulation environments such as CARLA [10] and
LGSVL [26] are available for modelling and validation.

As a rule, existing industrial simulation environments are built on top of
game engines. They privilege realism of modeling but allow poor semantic
awareness. Simulation tools are not rooted in rigorous semantics that could
provide a basis for analysis and reasoning about model properties. For
instance, they provide no support to check that a map obtained by composition
of road components e.g. using OpenDRIVE in CARLA, is consistent with its
geometric interpretation. Furthermore, lack of semantic awareness makes
impossible the development of convincing technical arguments regarding the
safety of the simulated systems. Accident-free simulation even for billions of
miles is not a conclusive safety evidence if it is not possible to explain how
simulated miles are related to real miles. Obviously, any technically sound
safety evaluation should be model-based and this is not possible under the
current state of the art.

The paper proposes a semantic framework for the specification and validation
of ADS. The framework provides a precise semantic model of the environment of
ADS based on maps. It also includes logics for the specification and
validation of properties of the semantic model and of the system dynamic
behavior.

Maps have been the object of numerous studies focusing on the formalization of
the concept and its use for the analysis of ADS. A key research issue is to
avoid monolithic representations and build maps by composition of components
and heterogeneous data. This motivated formalizations using ontologies and
logics with associated reasoning mechanisms to check consistency of
descriptions and their correctness with respect to desired properties [6, 4]
or to generate scenarios [4, 8]. Other works propose open source map
frameworks for highly automated driving [1, 2, 22].

A different research line focuses on the validation of ADS either to verify
satisfaction of safety and efficiency properties or even to check that
vehicles respect given traffic rules. Many works deal with safety verification
in a simple multilane setting. In [19] a dedicated Multi-Lane Spatial Logic
inspired by interval temporal logic is used to specify safety and provide
proofs for lane change controllers. The work in [24] presents a motion planner
formally verified in Isabelle/HOL. The planner is based on manoeuver automata,
a variant of hybrid automata, and properties are expressed in linear temporal
logic.

Other works deal with scenarios for modeling the behavior of ADS. OpenSCENARIO
[3] defines a data model and a derived file format for the description of
scenarios used in driving and traffic simulators, as well as in automotive
virtual development, testing and validation. The work in [9] proposes a visual
formal specification language for capturing scenarios inspired from Message
Charts and shows possible applications to specification and testing of
autonomous vehicles. In [27] a scenario-based methodology for functional
safety analysis is presented using the example of automated valet parking. The
work in [16] presents an approach to automated scenario-based testing of the
safety of autonomous vehicles, based on Metric Temporal Logic. Finally, the
probabilistic language Scenic for the design and analysis of cyber physical
systems allows the description of scenarios used to control and validate
simulated systems of self-driving cars. The Scenic programming environment
provides a big variety of constructs making possible modeling anywhere in the
spectrum from concrete scenes to broad classes of abstract scenarios [17, 15].

Other works focus on checking compliance of vehicles with traffic rules. A
formalization of traffic rules in linear temporal logic is proposed in [13].
Runtime verification is applied to check that maneuvers of a high-level
planner comply with the rules. Works in [25, 23] formalize a set of traffic
rules for highway scenarios in Isabelle/HOL; they show that traffic rules can
be used as requirements to be met by autonomous vehicles and propose a
verification procedure. A formalization of traffic rules for uncontrolled
intersections is provided in [21] using the CLINGO logic programming language.
Furthermore, the rules are applied by a simulator to safely control traffic
across intersections. The work in [14] proposes a methodology for the
formalization of traffic rules in Linear Temporal Logic; it is shown how
evaluation of formalized rules on recorded drives of humans provides insight
on what extent drivers respect the rules.

This work is an attempt to provide a minimal framework unifying the concepts
for the specification of ADS and the associated validation problems. The
proposed semantic framework clearly distinguishes between a static part
consisting of the road network with its equipment and a dynamic part involving
objects. The static part is a map described as a metric graph obtained as the
composition of subgraphs representing roads and junctions at different
abstraction levels. The vertices of the graph are positions and its edges are
road segments. Depending on the chosen level of abstraction, segments can be
simply the distance between the connected positions or curves or even two-
dimensional regions. The geometric interpretation of segments implies that
maps should meet consistency properties studied in the paper. It allows
multilevel representation using position refinement and segment abstraction.
The proposed concept of map is quite general encompassing compositional
multilevel description of traffic networks. The dynamic part of the ADS model
is a transition system whose state characterizes the distribution of objects
over a map with their positions, itineraries and attributes of their kinematic
state.

We progressively introduce three logics to express properties of the semantic
model at different levels. The _Metric Configuration Logic_ ($\mathit{MCL}$)
allows the compositional and parametric description of metric graphs. This is
a first order logic with variables ranging over positions and segments. It
uses in addition to logical connectives, a coalescing operator for the
compositional construction of maps from segments. A $\mathit{MCL}$ formula
represents configurations of maps sharing a common set of locations. We
discuss a specification methodology and show how various road patterns such as
roundabouts, intersections, mergers of roads can be specified in
$\mathit{MCL}$.

The Mobile Metric Configuration Logic (abbreviated $\mathit{M2CL}$) is an
extension of $\mathit{MCL}$ with additional object variables and primitives
for the specification of scenes as the distribution of objects over maps.
$\mathit{M2CL}$ formulas can be written as the conjunction of formulas
describing: i) static map contexts; ii) dynamic relations between objects;
iii) addressing relations between objects and maps. Last, we define Temporal
$\mathit{M2CL}$ (abbreviated $\mathit{TM2CL}$), a linear temporal logic whose
atomic propositions are formulas of $\mathit{M2CL}$. We illustrate the use of
these logics for the specification of safety properties including traffic
rules as well as the description of dynamic scenarios.

Additionally, we study the validation of properties expressed in the three
logics and provide a classification of problems showing that validation of
general dynamic properties boils down to constraint checking on metric graphs.
Checking that a finite model satisfies a formula of $\mathit{MCL}$ or
$\mathit{M2CL}$ amounts to eliminate quantifiers by adequate instantiation of
variables. We argue that satisfiability of $\mathit{M2CL}$ formulas can be
reduced to satisfiability of $\mathit{MCL}$ formulas which is an undecidable
problem. We identify a reasonably expressive decidable subset of
$\mathit{MCL}$ and propose a decision procedure. Furthermore, we discuss the
problem of runtime verification of $\mathit{TM2CL}$ formulas and sketch a
principle of solution inspired from a recent work with a similar configuration
logic [12]. We complete the presentation on ADS validation with an analysis of
practical needs for a rigorous validation methodology. We describe a general
validation environment and show how the proposed framework provides insight
into the different aspects of validation and related methodological issues.

The proposed framework allows a holistic treatment of all the aspects of ADS
modeling. It is not limited to specific contexts such as simple multilane
setting, intersection, roundabout, parking, etc. It fully encompasses both
dynamic and static aspects. Finally, the proposed concept of map allows
conciseness and precision not achievable by ontologies where semantic issues
are often overloaded and obscured by details that can be added to our model
without affecting its basic properties.

The paper is structured as follows. In section 2, we study metric graphs and
their relevant properties for the representation of map models as well as the
logic $\mathit{MCL}$, its main properties and application for map
specification. Section 3 deals with the study of logics $\mathit{M2CL}$ and
$\mathit{TM2CL}$ and their application to the specification of safety
properties and the description of scenarios. Then, section 4 discusses a
classification of validations problems, approaches for their solution and
their effective application. Section 5 concludes with a summary of main
results and a discussion about future developments.

##  2 Metric Graphs and Metric Configuration Logic

###  2.1 Segments and Metric Graphs

####  2.1.1 Segments.

We build contiguous road segments from a set ${\cal S}$ equipped with a
partial concatenation operator $\cdot:{\cal S}\times{\cal S}{}\rightarrow{\cal
S}\cup\\{\bot\\}$ and a length norm ${|\\!|.|\\!|}:{\cal
S}\rightarrow\mathbb{R}_{\geq 0}$ satisfying the following properties:

  1. (i)

_associativity:_ for any segments $s_{1}$, $s_{2}$, $s_{3}$ either both
$(s_{1}\cdot s_{2})\cdot s_{3}$ and $s_{1}\cdot(s_{2}\cdot s_{3})$ are defined
and equal, or both undefined;

  2. (ii)

_length additivity wrt concatenation:_ for any segments $s_{1}$, $s_{2}$
whenever $s_{1}\cdot s_{2}$ defined it holds ${|\\!|s_{1}\cdot
s_{2}|\\!|}={|\\!|s_{1}|\\!|}+{|\\!|s_{2}|\\!|}$;

  3. (iii)

_segment split:_ for any segment $s$ and non-negative $a_{1}$, $a_{2}$ such
that ${|\\!|s|\\!|}=a_{1}+a_{2}$ there exist unique $s_{1}$, $s_{2}$ such that
$s=s_{1}\cdot s_{2}$, ${|\\!|s_{1}|\\!|}=a_{1}$, ${|\\!|s_{2}|\\!|}=a_{2}$.

The last property allows us to define consistently a subsegment operation:
${s}[{a_{1}},{a_{2}}]$ is the unique segment of length $a_{2}-a_{1}$
satisfying $s=s_{1}\cdot{s}[{a_{1}},{a_{2}}]\cdot s_{2}$ where $s_{1}$,
$s_{2}$ are such that ${|\\!|s_{1}|\\!|}=a_{1}$,
${|\\!|s_{2}|\\!|}={|\\!|s|\\!|}-a_{2}$, for any $0\leq a_{1}\leq
a_{2}\leq{|\\!|s|\\!|}$. For brevity, we use the shorthand notation
${s}[{a},{\textrm{-}}]$ to denote the subsegment ${s}[{a},{{|\\!|s|\\!|}}]$.

Segments will be used to model building blocks of roads in maps considering
three different interpretations. Interval segments simply define the length of
a segment. Curve segments define the precise geometric form of the trajectory
of a mobile object along the segment. Region segments are 2D-regions of given
width around a center curve segment.

##### Interval Segments.

Consider ${\cal S}_{interval}\stackrel{{\scriptstyle
def}}{{=}}\\{[0,a]~{}|~{}a\in\mathbb{R}_{\geq 0}\\}$, that is, the set of
closed intervals on reals with lower bound 0, concatenation defined by
$[0,a_{1}]\cdot[0,a_{2}]\stackrel{{\scriptstyle def}}{{=}}[0,a_{1}+a_{2}]$ and
length ${|\\!|[0,a]|\\!|}\stackrel{{\scriptstyle def}}{{=}}a$.

##### Curve Segments.

Consider ${\cal S}_{curve}\stackrel{{\scriptstyle
def}}{{=}}\\{c:[0,1]\rightarrow\mathbb{R}^{2}~{}|~{}c(0)=(0,0),~{}c\mbox{
curve}\\}\cup\\{\epsilon\\}$ that is, the set of curves that are continuous
smooth222the derivative $\dot{c}$ exists and is continuous on $[0,1]$ and
uniformly progressing333the instantaneous speed ${|\dot{c}|}$, that is, the
Euclidean norm of the derivative is constant functions $c$, starting at the
origin, plus a designated single point curve $\epsilon$. The length is defined
by taking respectively the length of the curve
${|\\!|c|\\!|}\stackrel{{\scriptstyle def}}{{=}}\int_{0}^{1}{|\dot{c}(t)|}dt$
and ${|\\!|\epsilon|\\!|}=0$. The concatenation $c_{1}\cdot c_{2}$ of two
curves $c_{1}$ and $c_{2}$ is a partial operation that consists in joining the
final endpoint of $c_{1}$ with the initial endpoint of $c_{2}$ provided the
slopes at these points are equal. This condition preserves smoothness of the
curve $c_{1}\cdot c_{2}$ defined by $c_{1}\cdot
c_{2}:[0,1]\rightarrow\mathbb{R}^{2}$ where:

$(c_{1}\cdot c_{2})(t)\stackrel{{\scriptstyle
def}}{{=}}\left\\{\begin{array}[]{rcl}c_{1}(\frac{t}{\lambda})&\mbox{if}&t\in[0,\lambda]\\\\[3.0pt]
c_{1}(1)+c_{2}(\frac{t-\lambda}{1-\lambda})&\mbox{if}&t\in[\lambda,1]\end{array}\right.\mbox{
where }\lambda=\frac{{|\\!|c_{1}|\\!|}}{{|\\!|c_{1}|\\!|}+{|\\!|c_{2}|\\!|}}$

Note that in this definition, $c_{1}$ and $c_{2}$ are scaled on sub-intervals
of $[0,1]$ respecting their length ratio. We additionally take
$c\cdot\epsilon\stackrel{{\scriptstyle def}}{{=}}\epsilon\cdot
c\stackrel{{\scriptstyle def}}{{=}}c$, for any $c$. For practical reasons, one
can further restrict the set ${\cal S}_{curve}$ to curves of some form e.g,
finite concatenation of parametric line segments and circle arcs. That is, for
any $a,r\in\mathbb{R}_{\geq 0}^{*}$, $\varphi\in\mathbb{R}$,
$\theta\in\mathbb{R}^{*}$ the curves $line[a,\varphi]$,
$arc[r,\varphi,\theta]$ are defined as

$\begin{array}[]{rcl}line[a,\varphi](t)&\stackrel{{\scriptstyle
def}}{{=}}&(at\cos\varphi,at\sin\varphi)~{}~{}\forall t\in[0,1]\\\
arc[r,\varphi,\theta](t)&\stackrel{{\scriptstyle
def}}{{=}}&(r(\sin(\varphi+t\theta)-\sin\varphi),r(-\cos(\varphi+t\theta)+\cos\varphi))~{}~{}\forall
t\in[0,1]\end{array}$

Note that $a$ and $r$ are respectively the length of the line and the radius
of the arc, $\varphi$ is the slope of the curve at the initial endpoint and
$\theta$ is the degree of the arc. Fig. 1 illustrates the composition of three
segments of this parametric form.

$c_{2}=arc[1,10^{\circ},160^{\circ}]$$c_{1}=line[5,10^{\circ}]$$c_{3}=line[6,170^{\circ}]$$c_{1}\cdot
c_{2}\cdot c_{3}$

Figure 1: Curve segments and their composition

##### Region Segments.

Consider ${\cal S}_{region}\stackrel{{\scriptstyle def}}{{=}}{\cal
S}_{curve}\times\mathbb{R}_{\geq 0}^{*}$, that is, the set of pairs $(c,w)$
where $c$ is a curve and $w$ a positive number, denoting respectively the
region center curve and the region width. Region segments can be concatenated
iff their curves can be concatenated and if their widths are equal, that is,
$(c_{1},w)\cdot(c_{2},w)\stackrel{{\scriptstyle def}}{{=}}(c_{1}\cdot
c_{2},w)$ if $c_{1}\cdot c_{2}\not=\bot$. The length of a region segment is
defined as the length of its center curve,
${|\\!|(c,w)|\\!|}\stackrel{{\scriptstyle def}}{{=}}{|\\!|c|\\!|}$.

Region segments can be equally understood as subsets of points in
$\mathbb{R}^{2}$ defined by algebraic constraints. More precisely, for any
curve $c$ and width $w$ the region segment $(c,w)$ corresponds to the subset
of $\mathbb{R}^{2}$ defined as $\\{c(t)+\lambda\cdot\frac{\mbox{\small\it
ortho}(\dot{c}(t))}{{|\dot{c}(t)|}}~{}|~{}t\in[0,1],~{}\lambda\in[-\frac{w}{2},\frac{w}{2}]\\}$
where ortho is the orthogonal operator on $\mathbb{R}^{2}$ defined as
$ortho((a,b))\stackrel{{\scriptstyle def}}{{=}}(-b,a)$. In particular, the
above definition allows us to systematically derive parametric
characterizations for region segments constructed using line or arc curves.
The region generated by the curve $line[a,\varphi]$ is a rectangle containing
the set of points
$\\{(at\cos\varphi-\lambda\sin\varphi,at\sin\varphi+\lambda\cos\varphi)~{}|~{}t\in[0,1],\lambda\in[-\frac{w}{2},\frac{w}{2}]\\}$.
The region generated by the curve $arc[r,\varphi,\theta]$ is a ring sector
containing the set of points
$\\{((r+\lambda)(\sin(\varphi+t\theta)-r\sin\varphi,-(r+\lambda)\cos(\varphi+t\theta)+r\cos\varphi)~{}|~{}t\in[0,1],\lambda\in[-\frac{w}{2},\frac{w}{2}]\\}$.

####  2.1.2 Metric Graphs.

We use metric graphs $G\stackrel{{\scriptstyle def}}{{=}}(V,{\cal S},E)$ to
represent maps, where $V$ is a finite set of _vertices_ , ${\cal S}$ is a set
of segments and $E\subseteq V\times{\cal S}^{\star}\times V$ is a finite set
of _edges_ labeled by non-zero length segments in ${\cal S}^{\star}$. We also
denote an edge $e=(v,s,v^{\prime})\in E$ by
${v}\xrightarrow{s}_{G}{v^{\prime}}$ and we define
${}^{\bullet}\\!{e}\stackrel{{\scriptstyle def}}{{=}}v$,
${e}^{\bullet}\stackrel{{\scriptstyle def}}{{=}}v^{\prime}$,
${e}.s\stackrel{{\scriptstyle def}}{{=}}s$. For a vertex $v$, we define
${}^{\bullet}\\!{v}\stackrel{{\scriptstyle def}}{{=}}\\{e|{e}^{\bullet}=v\\}$
and ${v}^{\bullet}\stackrel{{\scriptstyle
def}}{{=}}\\{e|^{\bullet}\\!{e}=v\\}$. We denote by $E^{+}_{ac}$ the finite
set of non-empty _acyclic 444every edge occurs at most once in the path_
directed paths with edges from $E$. We call a metric graph _strongly_ (resp.
_weakly_) connected if a _directed_ (resp. _undirected_) path exists between
any pair of vertices. A metric graph is called _acyclic_ if at most one path,
directed or undirected, exist between any pairs of vertices.

We consider the set $\mathit{Pos}_{G}\stackrel{{\scriptstyle
def}}{{=}}V\cup\\{(e,a)~{}|~{}e\in E,~{}0<a<{|\\!|{e}.s|\\!|}\\}$ of
_positions_ defined by a metric graph. Note that $(e,0)$ and
$(e,{|\\!|{e}.s|\\!|})$ are respectively the positions ${}^{\bullet}\\!{e}$
and ${e}^{\bullet}$. Moreover, a $s$-labelled _ride_ between positions $(e,a)$
and $(e^{\prime},a^{\prime})$ is an acyclic path denoted by
${(e,a)}\stackrel{{\scriptstyle s}}{{\leadsto}}_{G}{(e^{\prime},a^{\prime})}$
and defined as follows:

  1. (i)

$e=e^{\prime}$, $0\leq a\leq a^{\prime}\leq{|\\!|{e}.s|\\!|}$,
$s={{e}.s}[{a},{a^{\prime}}]$

  2. (ii)

$e=e^{\prime}$, $0\leq a^{\prime}\leq a\leq{|\\!|{e}.s|\\!|}$,
${e}^{\bullet}=^{\bullet}\\!{e}$,
$s={{e}.s}[{a},{\textrm{-}}]\cdot{{e}.s}[{0},{a^{\prime}}]\not=\bot$

  3. (iii)

$e=e^{\prime}$, $0\leq a^{\prime}\leq a\leq{|\\!|{e}.s|\\!|}$, $w\in
E^{+}_{ac}$, $e\not\in w$, ${e}^{\bullet}=^{\bullet}\\!{w}$,
${w}^{\bullet}=^{\bullet}\\!{e}$,
$s={{e}.s}[{a},{\textrm{-}}]\cdot{w}.s\cdot{{e}.s}[{0},{a^{\prime}}]\not=\bot$

  4. (iv)

$e\not=e^{\prime}$, ${e}^{\bullet}=^{\bullet}\\!{e^{\prime}}$,
$s={{e}.s}[{a},{\textrm{-}}]\cdot{{e^{\prime}}.s}[{0},{a^{\prime}}]\not=\bot$

  5. (v)

$e\not=e^{\prime}$, $w\in E^{+}_{ac}$, $e,e^{\prime}\not\in w$,
${e}^{\bullet}=^{\bullet}\\!{w}$, ${w}^{\bullet}=^{\bullet}\\!{e^{\prime}}$,
$s={{e}.s}[{a},{\textrm{-}}]\cdot{w}.s\cdot{{e^{\prime}}.s}[{0},{a^{\prime}}]\not=\bot$

Fig. 2 illustrates the five cases of the above definition for a simple graph
with segments $s_{1}$, $s_{2}$ and $s_{3}$. Cases (i) and (ii) correspond to
rides on the same segment. Case (iii) corresponds to rides originating and
terminating in fragments of the same segment and also involving other segments
between them. Finally cases (iv) and (v) are rides originating and terminating
at different segments.

$p$$p^{\prime}$$p^{\prime}$$p$$p^{\prime}$$p^{\prime}$$p$$p$$p$$p^{\prime}$$u$$v$$s_{2}$$s_{1}$$s_{3}$

Figure 2:  Rides in metric graphs - cases (i)-(v) illustrated

We define the distance $d_{G}$ between positions $p$, $p^{\prime}$ as 0
whenever $p=p^{\prime}$ or the minimum length among all segments labeling
rides from $p$ to $p^{\prime}$ and otherwise $+\infty$ if no such ride exists.
It can be checked that $d_{G}$ is an _extended quasi-metric_ on the set
$\mathit{Pos}_{G}$ and therefore, $(\mathit{Pos}_{G},d_{G})$ is an extended
quasi-metric space.

###  2.2 Properties of Metric Graphs

####  2.2.1 Contraction/Refinement.

A metric graph $G^{\prime}=(V^{\prime},{\cal S},E^{\prime})$ is a
_contraction_ of a metric graph $G=(V,{\cal S},E)$ (or dually, $G$ is a
_refinement_ of $G^{\prime}$), denoted by $G\sqsubseteq G^{\prime}$, iff $G$
is obtained from $G^{\prime}$ by transformations replacing some of its edges
$e$ by acyclic sequences of interconnected edges $e_{1}e_{2}...e_{n}$ while
preserving the segment labeling i.e.,
${e}.s={e_{1}}.s\cdot{e_{2}}.s\cdot...\cdot{e_{n}}.s$.

###### Example 1

In Fig. 3, the graph on the right is a contraction of the one on the left iff
$s_{12}=s_{14}\cdot s_{45}\cdot s_{52}$, $s^{\prime}_{12}=s^{\prime}_{16}\cdot
s^{\prime}_{62}$ and $s_{31}=s_{37}\cdot s_{78}\cdot s_{81}$.

$v_{1}$$v_{2}$$s_{81}$$s_{14}$$s_{23}$$s_{78}$$v_{3}$$v_{5}$$v_{6}$$s^{\prime}_{31}$$s_{37}$$s^{\prime}_{16}$$s^{\prime}_{62}$$s_{52}$$v_{4}$$v_{7}$$v_{8}$$s_{45}$$v_{1}$$v_{2}$$v_{3}$$s_{12}$$s^{\prime}_{12}$$s^{\prime}_{31}$$s_{23}$$s_{31}$contractionrefinement

Figure 3:  Illustration of contraction/refinement on metric graphs

Note that metric graphs where all vertices have input or output degree greater
than one cannot be contracted. Such vertices correspond to _junctions_
(confluence of divergence of roads) when metric graphs represent maps. The
following proposition states some key properties on contraction/refinement of
metric graphs.

###### Proposition 1

Let $\mathit{Con}(G)\stackrel{{\scriptstyle
def}}{{=}}\\{G^{\prime}~{}|~{}G\sqsubseteq G^{\prime}\\}$,
$\mathit{Ref}(G)\stackrel{{\scriptstyle
def}}{{=}}\\{G^{\prime}~{}|~{}G^{\prime}\sqsubseteq G\\}$ be respectively the
set of contractions, refinements of a metric graph $G$.

  1. (i)

the refinement relation $\sqsubseteq$ is a partial order on the set of metric
graphs;

  2. (ii)

for any metric graph $G$, both $(\mathit{Con}(G),\sqsubseteq)$ and
$(\mathit{Ref}(G),\sqsubseteq)$ are complete lattices, moreover,
$(\mathit{Con}(G),\sqsubseteq)$ is finite;

  3. (iii)

for any metric graphs $G$, $G^{\prime}$ if $G\sqsubseteq G^{\prime}$ then (1)
the labelled transition systems $(\mathit{Pos}_{G},{\cal
S},{}\stackrel{{\scriptstyle}}{{\leadsto}}_{G}{)}$ and
$(\mathit{Pos}_{G^{\prime}},{\cal
S},{}\stackrel{{\scriptstyle}}{{\leadsto}}_{G^{\prime}}{)}$ are strongly
bisimilar and (2) the quasi-metric spaces $(\mathit{Pos}_{G},d_{G})$ and
$(\mathit{Pos}_{G^{\prime}},d_{G^{\prime}})$ are isometric;

###### Proof

(i) reflexivity, anti-symmetry and transitivity hold by definition of
$\sqsubseteq$ (ii) the least common contraction (resp. the greatest common
refinement) graph is obtained by taking the intersection (resp. the union) of
the sets of vertices and concatenating (resp. splitting) the set of edges
accordingly. Any contraction graph in $\mathit{Con}(G)$ is obtained from $G$
by removing a subset of its (finitely many) vertices with input and output
degree equal to one (iii) the sets of positions and the set of rides are
preserved by refinement, hence the labelled transition systems are bisimilar.
Consequently, distances are preserved so the metric spaces are isometric.

####  2.2.2 Abstraction/Concretization.

Consider ${\cal S}$, ${\cal S}^{\prime}$ be sets of segments associated with
respectively concatenation $\cdot$, $\cdot^{\prime}$, and length norm
${|\\!|.|\\!|}$, ${|\\!|.|\\!|}^{\prime}$. A function $\alpha:{\cal
S}\rightarrow{\cal S}^{\prime}$ is a _segment abstraction_ if it satisfies the
following properties:

  1. (i)

_length preservation_ : ${|\\!|s|\\!|}={|\\!|\alpha(s)|\\!|}^{\prime}$, for
all $s\in{\cal S}$

  2. (ii)

_homomorphism wrt concatenation_ : $\alpha(s_{1}\cdot
s_{2})=\alpha(s_{1})\cdot^{\prime}\alpha(s_{2})$ for all $s_{1},s_{2}\in{\cal
S}$ such that $s_{1}\cdot s_{2}\not=\bot$.

For example, the function $\alpha^{CI}:{\cal S}_{curve}\rightarrow{\cal
S}_{interval}$ defined by $\alpha^{CI}(s)\stackrel{{\scriptstyle
def}}{{=}}[0,{|\\!|s|\\!|}]$ for all $s\in{\cal S}_{curve}$ is a an
abstraction of curve segments as interval segments. Similarly, the function
$\alpha^{RC}:{\cal S}_{region}\rightarrow{\cal S}_{curve}$ defined by
$\alpha^{RC}((s,w))\stackrel{{\scriptstyle def}}{{=}}s$ for all $(s,w)\in{\cal
S}_{region}$ is an abstraction of region segments as curve segments.

Dually, we can define concretization functions $\gamma$ that go from intervals
to curves, and from curves to regions. For example, for any angles $\varphi$,
$\theta$ consider $\gamma^{IC}_{\varphi,\theta}:{\cal
S}_{interval}\rightarrow{\cal S}_{curve}$ where respectively,
$\gamma^{IC}_{\varphi,\theta}([0,a])\stackrel{{\scriptstyle
def}}{{=}}arc[\frac{a}{\theta},\varphi,\theta]$ if $\theta\not=0$ or
$\gamma^{IC}_{\varphi,\theta}([0,a])\stackrel{{\scriptstyle
def}}{{=}}line[a,\varphi]$ if $\theta=0$. Or, for any positive real $w$
consider $\gamma^{CR}_{w}:{\cal S}_{curve}\rightarrow{\cal S}_{regions}$ where
$\gamma^{CR}_{w}(s)\stackrel{{\scriptstyle def}}{{=}}(s,w)$.

Given a segment abstraction $\alpha:{\cal S}\rightarrow{\cal S}^{\prime}$, a
metric graph $G^{\prime}=(V,{\cal S}^{\prime},E^{\prime})$ is an
$\alpha$-_abstraction_ of a metric graph $G=(V,{\cal S},E)$, denoted by
$G^{\prime}=\alpha(G)$, iff $G^{\prime}$ is obtained from $G$ by replacing
segments $s$ by their abstractions $\alpha(s)$. That is, any edge
${u}\xrightarrow{s}_{G}{v}$ is transformed into an edge
${u}\xrightarrow{\alpha(s)}_{G^{\prime}}{v}$. In a similar way,
$\gamma$-concretization on metric graphs is defined for a segment
concretization $\gamma:{\cal S}^{\prime}\rightarrow{\cal S}$.

Fig. 4 illustrates the use of the three segment abstraction levels
(respectively as intervals, curves, regions) and their associated metric
graphs. Interval metric graphs are $\alpha^{CI}$-abstractions of curve metric
graphs, which in turn are $\alpha^{RC}$-abstractions of region metric graphs.
Proposition 2 states some key properties on abstraction on metric graphs.

abstraction

concretization

region metric graph$v_{1}$$v_{2}$$v_{3}$$v_{4}$directed graphcurve metric
graphinterval metric
graph$v_{2}$$v_{3}$$v_{4}$$v_{4}$$v_{3}$$v_{2}$$v_{1}$$v_{2}$$v_{3}$$v_{4}$$v_{1}$$v_{1}$$[0,a_{1}]$$[0,a_{2}]$$[0,a_{3}]$$c_{1}$$c_{2}$$c_{3}$$(c_{1},w)$$(c_{2},w)$$(c_{3},w)$

Figure 4:  Illustration of abstraction/concretization on metric graphs

###### Proposition 2

For a segment abstraction $\alpha:{\cal S}\rightarrow{\cal S}^{\prime}$ and
metric graphs $G$, $G^{\prime}$ such that $G^{\prime}=\alpha(G)$, the labelled
transition system $(\mathit{Pos}_{G^{\prime}},{\cal
S}^{\prime},{}\stackrel{{\scriptstyle}}{{\leadsto}}_{G^{\prime}}{)}$ simulates
the labelled transition system $(\mathit{Pos}_{G},{\cal
S},{}\stackrel{{\scriptstyle}}{{\leadsto}}_{G}{)}$ renamed by $\alpha$.

###### Proof

The set of positions are preserved up to homomorphism by $\alpha$-abstraction
and any $s$-labelled ride of $G$ can be simulated by an $\alpha(s)$-labelled
ride of $G^{\prime}$. Nonetheless, the reverse is not necessarily true as
segments $s_{1}$, $s_{2}$ that do not concatenate in $G$ may have abstractions
$\alpha(s_{1})$, $\alpha(s_{2})$ that concatenate in $G^{\prime}$ and
therefore, leading to strictly more rides in $G^{\prime}$ than $G$.

###### Proposition 3

Metric graph contraction and abstraction commute, that is, for any metric
graphs $G$, $G^{\prime}$, for any segment abstraction $\alpha$, if
$G\sqsubseteq G^{\prime}$ then $\alpha(G)\sqsubseteq\alpha(G^{\prime})$, as
depicted below.

$G$$\alpha(G)$contractioncontraction$\alpha$-abstraction$\alpha$-abstraction$G^{\prime}$$\alpha(G^{\prime})$

###### Proof

Recall that segment abstraction is an homomorphism wrt segment concatentation,
that is, for any $s_{1}$, $s_{2}$ such that $s_{1}\cdot s_{2}\not=\bot$ it
holds $\alpha(s_{1}\cdot s_{2})=\alpha(s_{1})\cdot\alpha(s_{2})$. Therefore,
contracting $s_{1}$ and $s_{2}$ into $s_{12}$ (from $G$ to $G^{\prime}$) then
abstracting $s_{12}$ as $\alpha(s_{12})$ (from $G^{\prime}$ to
$\alpha(G^{\prime})$) is the same as abstracting $s_{1}$, $s_{2}$ into
respectively $\alpha(s_{1})$, $\alpha(s_{2})$ (from $G$ to $\alpha(G)$) then
contracting $\alpha(s_{1})$ and $\alpha(s_{2})$ into
$\alpha(s_{1})\cdot\alpha(s_{2})$ (from $\alpha(G)$ to $\alpha(G^{\prime})$).

####  2.2.3 2D-geometric consistency.

The concept of _2D-geometric consistency_ is important when we use metric
graphs to represent 2D-maps. A curve metric graph $G=(V,{\cal S}_{curve},E)$
is 2D-geometrically consistent if it can be embedded in the 2D-plane, that is,
there exists an adressing mapping $\chi:V\rightarrow\mathbb{R}^{2}$ of
vertices to coordinates in the 2D-plane such that for any edge
$e=(v,s,v^{\prime})$ it holds $\chi(v)+s(1)=\chi(v^{\prime})$. 2D-geometric
consistency can be checked by combining the following results.

###### Proposition 4

Any acyclic weakly connected curve metric graph is 2D-geometrically
consistent.

###### Proof

Starting from the known coordinates $\chi(v_{0})$ for some designated vertex
$v_{0}$ it is possible to compute successively the coordinates of all the
other vertices as between two vertices there exists only a single undirected
path. So given the coordinates of any vertex of such a sequence we can compute
the coordinates of any others such that to ensure consistency.

###### Proposition 5

Any weakly connected curve metric graph is 2D-geometrically consistent iff for
any elementary circuit $\omega$ (directed or undirected) it holds
$\sum_{e\in\omega^{+}}{e}.s(1)=\sum_{e\in\omega^{-}}{e}.s(1)$ where
$\omega^{+}$ (resp. $\omega^{-}$) denote the sets of edges taken with their
direct (resp. reverted) orientation in $\omega$.

###### Proof

This is a necessary conditions because for given coordinates $\chi(v)$ of some
vertex $v$ from which starts a circuit $\omega$, the same coordinates are
reached by following $\omega$, that is,
$\chi(v)=\chi(v)+\sum_{e\in\omega^{+}}{e}.s(1)-\sum_{e\in\omega^{-}}{e}.s(1)$
holds. This condition is also sufficient because if we remove edges of the
graph so as to break all circuits, then by the previous proposition it is
possible to find consistent coordinate mappings.

###### Example 2

Consider the curve metric graph in Fig. 5 representing a 4-way regular
intersection with entrances $u_{1}$, $u_{2}$, $u_{3}$, $u_{4}$ and exits
$v_{1}$, $v_{2}$, $v_{3}$, $v_{4}$. The edges
$e_{ij}=({u_{i}}\xrightarrow{s_{ij}}{v_{j}})$ are defined by the relations:

$\begin{array}[]{l l
l}{u_{1}}\xrightarrow{line[2r+d,0]}{v_{3}}&{u_{1}}\xrightarrow{arc[r,0,-\frac{\pi}{2}]}{v_{2}}&{u_{1}}\xrightarrow{arc[r+d,0,\frac{\pi}{2}]}{v_{4}}\\\
{u_{2}}\xrightarrow{line[2r+d,\frac{\pi}{2}]}{v_{4}}&{u_{2}}\xrightarrow{arc[r,\frac{\pi}{2},-\frac{\pi}{2}]}{v_{3}}&{u_{2}}\xrightarrow{arc[r+d,\frac{\pi}{2},\frac{\pi}{2}]}{v_{1}}\\\
{u_{3}}\xrightarrow{line[2r+d,\pi]}{v_{1}}&{u_{3}}\xrightarrow{arc[r,\pi,-\frac{\pi}{2}]}{v_{4}}&{u_{3}}\xrightarrow{arc[r+d,\pi,\frac{\pi}{2}]}{v_{2}}\\\
{u_{4}}\xrightarrow{line[2r+d,-\frac{\pi}{2}]}{v_{2}}&{u_{4}}\xrightarrow{arc[r,-\frac{\pi}{2},-\frac{\pi}{2}]}{v_{1}}&{u_{4}}\xrightarrow{arc[r+d,-\frac{\pi}{2},\frac{\pi}{2}]}{v_{3}}\end{array}$

Note that to prove the 2D-geometric consistency we need to check the
identities defined for elementary circuits as stated in Proposition 5. For
instance, the circuit visiting the vertices $u_{2},v_{4},u_{1},v_{3},u_{2}$
traverses forwards the edges $e_{24}$, $e_{13}$ and backwards the edges
$e_{14}$, $e_{23}$. Henceforth, one must check:

$\begin{array}[]{ccccccc}{e_{24}}.s(1)&+&{e_{13}}.s(1)&=&{e_{14}}.s(1)&+&{e_{23}}.s(1)\\\
line[2r+d,\frac{\pi}{2}](1)&+&line[2r+d,0](1)&=&arc[r+d,0,\frac{\pi}{2}](1)&+&arc[r,\frac{\pi}{2},-\frac{\pi}{2}](1)\\\
(0,2r+d)&+&(2r+d,0)&=&(r+d,r+d)&+&(r,r)\end{array}$

$u^{\prime}_{3}$$u_{3}$$v^{\prime}_{3}$$v_{3}$$u^{\prime}_{1}$$v_{1}$$v^{\prime}_{1}$$u_{2}$$v_{2}$$v^{\prime}_{2}$$v_{4}$$v^{\prime}_{4}$$u^{\prime}_{4}$$u_{4}$$u^{\prime}_{2}$$u_{1}$

Figure 5: Curve metric graph representing a 4-way intersection

###  2.3 The Metric Configuration Logic

####  2.3.1 Syntax.

Let consider a fixed set of segments ${\cal S}$ and assume there exists a
finite set ${\cal S}^{T}$ of segment constructors $s^{T}$ (or segment types),
that is, partial functions $s^{T}:\mathbb{R}^{m}\rightarrow{\cal S}^{\bot}$
for some natural $m$. For example, we can take ${\cal
S}^{T}_{curve}=\\{line:\mathbb{R}^{2}\rightarrow{\cal
S}^{\bot},arc:\mathbb{R}^{3}\rightarrow{\cal S}^{\bot}\\}$ as the set of
constructor curve segments ${\cal S}_{curve}$.

Let $K$, $Z$, $X$ be distinct finite sets of _variables_ denoting respectively
reals, segments and vertices of a metric graph. The syntax of the _metric
configuration logic_ ($\mathit{MCL}$) is defined in Table 1.

$\begin{array}[]{rcll}\hline\cr t&::=&a\in\mathbb{R}~{}|~{}k\in
K~{}|~{}t+t~{}|~{}t\cdot t&\mathit{arithmetic~{}terms}\\\ \psi_{K}&::=&t\leq
t^{\prime}&\mathit{arithmetic~{}constraints}\\\\[5.0pt]
s&::=&s^{T}(t_{1},...,t_{m})~{}|~{}z\in Z~{}|~{}s\cdot
s&\mathit{segment~{}terms}\\\
\psi_{S}&::=&s=s^{\prime}~{}|~{}{|\\!|s|\\!|}=t&\mathit{segment~{}constraints}\\\\[5.0pt]
p&::=&x\in X~{}|~{}(x,s,t)~{}|~{}(t,s,x)&\mathit{position~{}terms}\\\
\psi_{G}&::=&{x}\xrightarrow{s}{x^{\prime}}~{}|~{}p=p^{\prime}~{}|~{}{p}\stackrel{{\scriptstyle
s}}{{\leadsto}}{p^{\prime}}~{}|~{}d(p,p^{\prime})=t{}{}{}&\mathit{metric~{}graph~{}constraints}\\\\[5.0pt]
\phi&::=&\psi_{K}~{}|~{}\psi_{S}~{}|~{}\psi_{G}&\mathit{atomic~{}formula}\\\
&|&\phi+\phi~{}|~{}\phi\vee\phi~{}|~{}\neg\phi&\mathit{non\textrm{-}atomic~{}formula}\\\
&|&\exists k.~{}\phi(k)~{}|~{}\exists z.~{}\phi(z)~{}|~{}\exists
x.~{}\phi(x)&\mathit{quantifiers}\\\ \hline\cr\end{array}$ Table 1:
$\mathit{MCL}$ Syntax

####  2.3.2 Semantics.

Let $G=(V,{\cal S},E)$ be a metric graph fixed in the context, and let
$\sigma$ be an assignment of variables $K$, $Z$, $X$ to respectively reals
$\mathbb{R}$, segments ${\cal S}$, vertices $V$. As usual, we extend $\sigma$
for evaluation of arithmetic terms (with variables from $K$) into reals.
Moreover, we extend $\sigma$ for the partial evaluation of segment terms (with
variables from $Z$) and position terms (with variables from $Z$ and $X$) into
respectively segments ${\cal S}$ and positions $\mathit{Pos}_{G}$ as defined
by the rules in Table 2.

$\begin{array}[]{rclrcl}\\\ \hline\cr\sigma
s^{T}(t_{1},...,t_{m})&\stackrel{{\scriptstyle def}}{{=}}&s^{T}(\sigma
t_{1},...,\sigma t_{m})&\sigma(x,s,t)&\stackrel{{\scriptstyle
def}}{{=}}&\mathit{pos}_{G}^{fwd}(\sigma x,\sigma s,\sigma t)\\\
\sigma~{}s\cdot s^{\prime}&\stackrel{{\scriptstyle def}}{{=}}&\sigma
s\cdot\sigma s^{\prime}&~{}~{}~{}~{}~{}\sigma(t,s,x)&\stackrel{{\scriptstyle
def}}{{=}}&\mathit{pos}_{G}^{bwd}(\sigma x,\sigma s,\sigma t)\end{array}$

where $\mathit{pos}_{G}^{fwd}$, $\mathit{pos}_{G}^{bwd}:V\times{\cal
S}\times\mathbb{R}\rightarrow\mathit{Pos}_{G}^{\bot}$ are defined as

$\begin{array}[]{rcll}\mathit{pos}_{G}^{fwd}(v,s,a)&\stackrel{{\scriptstyle
def}}{{=}}&(e,a)&\mbox{ only if }\exists!~{}e=(v,s,v^{\prime})\in
E,~{}0<a<{|\\!|s|\\!|}\\\
\mathit{pos}_{G}^{bwd}(v,s,a)&\stackrel{{\scriptstyle
def}}{{=}}&(e,{|\\!|s|\\!|}-a)&\mbox{ only if
}\exists!~{}e=(v^{\prime},s,v)\in E,~{}0<a<{|\\!|s|\\!|}\\\
\hline\cr\end{array}$

Table 2:  Evaluation of $\mathit{MCL}$ terms

We tacitly restrict to terms which evaluate successfully in their respective
domains. The semantics of the metric configuration logic is defined by the
rules in Table 3. Note that a formula represents a configuration of metric
graphs sharing common characteristics. Besides the logic connectives with the
usual set-theoretic meaning, the coalescing operator $+$ allows building
graphs by grouping elementary constituents characterized by atomic formulas
relating positions via segments. Hence, the formula $\phi_{1}+\phi_{2}$
represents the graph configurations obtained as the union of configurations
satisfying $\phi_{1}$ and $\phi_{2}$ respectively. It differs from
$\phi_{1}\vee\phi_{2}$ in that this formula satisfies configurations that
satisfy either $\phi_{1}$ or $\phi_{2}$.

$\begin{array}[]{rclcl}\hline\cr\sigma,G&\models&t\leq
t^{\prime}&~{}~{}\mbox{iff}{}{}&\sigma t\leq\sigma t^{\prime}\\\
\sigma,G&\models&s=s^{\prime}&\mbox{iff}&\sigma s=\sigma s^{\prime}\\\
\sigma,G&\models&{|\\!|s|\\!|}=t&\mbox{iff}&{|\\!|\sigma s|\\!|}=\sigma t\\\
\sigma,G&\models&{x}\xrightarrow{s}{x^{\prime}}&\mbox{iff}&E=\\{(\sigma
x,\sigma s,\sigma x^{\prime})\\}\\\
\sigma,G&\models&p=p^{\prime}&\mbox{iff}&\sigma p=\sigma p^{\prime}\\\
\sigma,G&\models&{p}\stackrel{{\scriptstyle
s}}{{\leadsto}}{p^{\prime}}&\mbox{iff}&{\sigma p}\stackrel{{\scriptstyle\sigma
s}}{{\leadsto}}_{G}{\sigma p^{\prime}}\\\
\sigma,G&\models&d(p,p^{\prime})=t&\mbox{iff}&d_{G}(\sigma p,\sigma
p^{\prime})=\sigma t\\\
\sigma,G&\models&\phi_{1}+\phi_{2}&\mbox{iff}&\sigma,(V,E_{1})\models\phi_{1}\mbox{
and }\sigma,(V,E_{2})\models\phi_{2}\\\ &&&&\mbox{for some }E_{1},E_{2}\mbox{
such that }E_{1}\cup E_{2}=E\\\
\sigma,G&\models&\phi_{1}\vee\phi_{2}&\mbox{iff}&\sigma,G\models\phi_{1}\mbox{
or }\sigma,G\models\phi_{2}\\\
\sigma,G&\models&\neg\phi&\mbox{iff}&\sigma,G\not\models\phi\\\
\sigma,G&\models&\exists k.~{}\phi&\mbox{iff}&\sigma[k\mapsto
a],G\models\phi\mbox{ for some }a\in\mathbb{R}\\\ \sigma,G&\models&\exists
z.~{}\phi&\mbox{iff}&\sigma[z\mapsto s],G\models\phi\mbox{ for some }s\in{\cal
S}\\\ \sigma,G&\models&\exists x.~{}\phi&\mbox{iff}&\sigma[x\mapsto
v],G\models\phi\mbox{ for some }v\in V\\\ \hline\cr\end{array}$ Table 3:
$\mathit{MCL}$ Semantics

####  2.3.3 Properties.

$\begin{array}[]{lrcl}\hline\cr(A.i)&(\phi_{1}+\phi_{2})+\phi_{3}&\equiv&\phi_{1}+(\phi_{2}+\phi_{3})\\\
(A.ii)&\phi_{1}+\phi_{2}&\equiv&\phi_{2}+\phi_{1}\\\
(A.iii)&\phi+\mbox{false}&\equiv&\mbox{false}\\\
(A.iv)&\phi+\phi&\not\equiv&\phi~{}~{}(\mathit{in~{}general})\\\
(A.v)&\phi_{1}+(\phi_{2}\vee\phi_{3})&\equiv&(\phi_{1}+\phi_{2})\vee(\phi_{1}+\phi_{3})\\\\[4.0pt]
(B.i)&\sim\\!\\!{\sim\\!\\!{\phi}}&\equiv&\sim\\!\\!{\phi}\\\
(B.ii)&\phi&\implies&\sim\\!\\!{\phi}\\\
(B.iii)&\sim\\!\\!{(\phi_{1}\vee\phi_{2})}&\equiv&\sim\\!\\!{\phi_{1}}\vee\sim\\!\\!{\phi_{2}}\\\
(B.iv)&\sim\\!\\!{(\phi_{1}+\phi_{2})}&\equiv&\sim\\!\\!{\phi_{1}}+\sim\\!\\!{\phi_{2}}~{}~{}\equiv~{}~{}\sim\\!\\!{\phi_{1}}\wedge\sim\\!\\!{\phi_{2}}\\\\[4.0pt]
(C.i)&{x}\xrightarrow{s}{x^{\prime}}\wedge(\phi_{1}+\phi_{2})&\equiv&({x}\xrightarrow{s}{x^{\prime}}\wedge\phi_{1})+({x}\xrightarrow{s}{x^{\prime}}\wedge\phi_{2})\\\
(C.ii)&\mbox{true}&\equiv&({x}\xrightarrow{s}{x^{\prime}}+\neg(\sim\\!\\!{{x}\xrightarrow{s}{x^{\prime}}}))\vee\neg(\sim\\!\\!{{x}\xrightarrow{s}{x^{\prime}}})\\\\[4.0pt]
(D.i)&d(p,p^{\prime})=t\wedge{p}\stackrel{{\scriptstyle
s}}{{\leadsto}}{p^{\prime}}&\implies&t\leq{|\\!|s|\\!|}\\\
(D.ii)&d(p,p^{\prime})=t\wedge
d(p^{\prime},p^{\prime\prime})=t^{\prime}&\implies&\exists
k.~{}d(p,p^{\prime\prime})=k\wedge k\leq t+t^{\prime}\\\ \hline\cr\end{array}$
Table 4: $\mathit{MCL}$ Theorems

Table 4 provides a set of theorems giving insight into the characteristic
properties of the logic. Theorems $(A.i)\mbox{-}(A.v)$ illustrate important
properties of the $+$ operator that is associative and commutative but not
idempotent. As explained below, of particular interest for writing
specifications are formulas of the form
$\sim\\!\\!{}\phi\stackrel{{\scriptstyle def}}{{=}}\phi+\mathit{true}$. These
are satisfied by configurations with graphs that contain a subgraph satisfying
$\phi$. Hence, while the formula ${x}\xrightarrow{s}{x^{\prime}}$
characterizes the graphs with two vertices and a single edge labeled by $s$,
the formula $\sim\\!\\!{{x}\xrightarrow{s}{x^{\prime}}}$ characterizes the set
of graphs containing such an edge. Thus $\sim\\!\\!{}$ is a closure operator
which moreover satisfies theorems $(B.i)\mbox{-}(B.iv)$. Finally, theorems
$(C.i)\mbox{-}(C.ii)$ relate the atomic formula
${x}\xrightarrow{s}{x^{\prime}}$ to coalescing and the complement of their
closure. The two last theorems $(D.i)\mbox{-}(D.ii)$ differ from the others in
that they express specific properties of segment and metric graph constraints.

###### Proposition 6

Metric graph constraints not involving edge constraints of the form
${x}\xrightarrow{s}{x^{\prime}}$ are insensitive to metric graph contraction
and refinement.

###### Proof

This is an immediate consequence of Proposition 1, point (iii), guaranteeing
preservation of structural properties by contraction and refinement
(bisimilarity, isometry).

Note that stronger preservation results for (even simple fragments of)
$\mathit{MCL}$ are hard to obtain because the domain of vertex variables is a
fixed set of vertices. This makes $\mathit{MCL}$ sensitive to both contraction
and refinement. For example, the formula $\exists x.~{}\exists
y.~{}{x}\stackrel{{\scriptstyle s}}{{\leadsto}}{y}$ may not hold before and
hold after refinement i.e., if a pair of vertices $u$, $v$ satisfying the
constraint is added by refinement.

We provide below abstraction preservation results for MCL formulas. Any
segment abstraction $\alpha:{\cal S}\rightarrow{\cal S}^{\prime}$ can be
lifted to segment terms by taking respectively
$\alpha(s^{T}(t_{1},...,t_{m}))\stackrel{{\scriptstyle def}}{{=}}(\alpha
s^{T})(t_{1},...,t_{n})$, $\alpha(s_{1}\cdot s_{2})\stackrel{{\scriptstyle
def}}{{=}}\alpha(s_{1})\cdot^{\prime}\alpha(s_{2})$,
$\alpha(z)\stackrel{{\scriptstyle def}}{{=}}z$. Moreover, $\alpha$ can be
further lifted to $\mathit{MCL}$ formulas on ${\cal S}$. We denote by
$\alpha(\phi)$ the $\mathit{MCL}$ formula on ${\cal S}^{\prime}$ obtained by
rewriting all the segment terms $s$ occuring in $\phi$ by $\alpha(s)$. The
following proposition relates abstractions on formulas to abstractions on
metric graphs.

###### Proposition 7

Let $\phi$ be an existential positive $\mathit{MCL}$ formula. Then
$G\models\phi$ implies $\alpha(G)\models\alpha(\phi)$ whenever:

  1. (i)

$\phi$ does not contain distance constraints or

  2. (ii)

for any connected edges $e_{1}$, $e_{2}$ such that
${e_{1}}^{\bullet}=^{\bullet}\\!{e_{2}}$ their segments compose, that is,
${e_{1}}.s\cdot{e_{2}}.s\not=\bot$.

###### Proof

On one hand, the satisfiability of positive segment and graph constraints
(except path constraints) are preserved by segment abstraction. For example,
if $s_{1}=s_{2}$ holds then $\alpha(s_{1})=\alpha(s_{2})$ holds, if
${x}\xrightarrow{s}{y}$ holds in $G$ then ${x}\xrightarrow{\alpha(s)}{y}$
holds in $\alpha(G)$, etc. On the other hand, path constraints rely on an
implicit universal quantification over segments labeling acyclic rides in $G$.
Therefore, they are preserved only if, the set of acyclic rides is not
augmented by abstraction. This is indeed the case if the condition (ii) holds.

####  2.3.4 Modeling styles.

Configuration logics allow the characterization of configurations of graphs by
adopting two different and complementary styles. The bottom-up style consists
in building graphs as the coalescing of atomic formulas specifying
connectivity relations between vertices. The top-down style consists in giving
the specification as the conjunction of formulas. Hence, the meaning of the
specification is the intersection of the meanings of its conjuncts.

$arc[r,\varphi,\pi]$$v_{4}$$v_{3}$$line[a,\varphi+\pi]$$line[a,\varphi]$$v_{1}$$v_{2}$$arc[r,\varphi+\pi,\pi]$

Figure 6:  A ring map

For example, consider the ring map of Fig. 6 with four vertices and edges
labeled by corresponding segments. The bottom-up specification $\zeta_{ring}$
describes the ring as the coalescing of the four segments as shown below (left
side) whereas the top-down specification $\xi_{ring}$ is the conjunction of a
set of rules whose application defines a ring map (right side):

$\begin{array}[]{l | c l}\exists a.~{}\exists r.~{}\exists\varphi.~{}\exists x_{1}.~{}\exists x_{2}.~{}\exists x_{3}.~{}\exists x_{4}.&&\exists a.~{}\exists r.~{}\forall\varphi.~{}\forall x_{1}.~{}\forall x_{2}.~{}\exists x_{3}\\\ ~{}~{}{x_{1}}\xrightarrow{line[a,\varphi]}{x_{2}}+{x_{2}}\xrightarrow{arc[r,\varphi,\pi]}{x_{3}}~{}+&&~{}~{}\sim\\!\\!{{x_{1}}\xrightarrow{line[a,\varphi]}{x_{2}}}\Rightarrow\sim\\!\\!{{x_{2}}\xrightarrow{arc[r,\varphi,\pi]}{x_{3}}}~{}\wedge\\\ ~{}~{}{x_{3}}\xrightarrow{line[a,\varphi+\pi]}{x_{4}}+{x_{4}}\xrightarrow{arc[r,\varphi+\pi,\pi]}{x_{1}}&&~{}~{}\sim\\!\\!{{x_{1}}\xrightarrow{arc[r,\varphi,\pi]}{x_{2}}}\Rightarrow\sim\\!\\!{{x_{2}}\xrightarrow{line[a,\varphi+\pi]}{x_{3}}}\\\ \end{array}$

It is possible to define a meaning-preserving correspondence between top-down
and bottom-up specifications as follows. We consider that bottom up
specifications are built by coalescing atomic formulas $\zeta_{k}$ of the form
${x}\xrightarrow{s}{x^{\prime}}$. Denote by $\xi_{k}$ the formula
$\xi_{k}\stackrel{{\scriptstyle def}}{{=}}\sim\\!\\!{\zeta_{k}}$.

Given a formula $\sum_{k}\zeta_{k}$ the strongest corresponding top-down
specification is defined by the homomorphism:
$\sim\\!\\!{\sum_{k}\zeta_{k}}=\bigwedge_{k}\sim\\!\\!{\zeta_{k}}=\bigwedge_{k}\xi_{k}$.
A weaker top-down specification that admits an interesting interpretation as a
conjunction of implications is the formula
$(\bigwedge_{k}\neg\xi_{k})\vee(\bigwedge_{k}\xi_{k})$. Note that the
conjunction $\bigwedge_{k}\neg\xi_{k}$ is satisfied by models that do not
contain any of the segments of the bottom-up specification. The following
properties are useful as they provide insight into to the way we can write
top-down weak specifications as a conjunction of “causality rules” expressed
by implications:

$\begin{array}[]{c c c c
c}\textstyle{\bigwedge_{k=1}^{m}}\neg\xi_{k}\vee\textstyle{\bigwedge_{k=1}^{m}}\xi_{k}&~{}~{}\equiv{}{}&\textstyle{\bigwedge_{1\leq
k,k^{\prime}\leq m}}~{}(\xi_{k}\Leftrightarrow\xi_{k^{\prime}})\\\
&\equiv&\textstyle{\bigwedge_{1\leq k,k^{\prime}\leq
m}}~{}(\xi_{k}\Rightarrow\xi_{k^{\prime}})&~{}~{}\equiv{}{}&\textstyle{\bigwedge_{k=1}^{m}}~{}(\xi_{k}\Rightarrow\xi_{k\oplus
1})\end{array}$

Note that
$\bigwedge_{k}\xi_{k}=(\mathit{true}\Rightarrow\xi_{1})\wedge(\bigwedge_{k=1}^{m}\xi_{k}\Rightarrow\xi_{k\oplus
1})$. As an application of these results let us re-consider the example of
Fig. 6 and write the bottom-up specification $\zeta_{ring}$ (making
abstraction of quantifiers) as the formula
$\zeta_{12}+\zeta_{23}+\zeta_{34}+\zeta_{41}$. The corresponding weak top-down
specification is then
$(\xi_{12}\Rightarrow\xi_{23})\wedge(\xi_{23}\Rightarrow\xi_{34})\wedge(\xi_{34}\Rightarrow\xi_{41})\wedge(\xi_{41}\Rightarrow\xi_{12})$.
Note that the formula above can be simplified given that the implications
$\xi_{12}\Rightarrow\xi_{23}$, $\xi_{34}\Rightarrow\xi_{41}$ and respectively
$\xi_{23}\Rightarrow\xi_{34}$, $\xi_{41}\Rightarrow\xi_{12}$ are of the same
form. Hence, they can be replaced by two parametric implications by adequately
changing quantification. In that manner, we obtain precisely the weak top-down
specification corresponding to the top-down specification $\xi_{ring}$.

##  3 ADS Specification

The results of the previous section provide a basis for the definition of both
a dynamic model for ADS and of logics for the expression of their properties.
The model is a timed transition system with states defined as the distribution
of objects over of a metric graph representing a map. Objects may be mobile
such as vehicles and pedestrians or static such as signaling equipment. The
logics are two extensions of $\mathit{MCL}$, one for the specification of
predicates representing sets of states and the other for the specification of
its behavior.

We introduce first the concept of map and its properties. Then we define the
dynamic model and the associated logics. Finally, we discuss the validation
problem and its possible solutions.

###  3.1 Map specification

A weakly connected metric graph $G=(V,{\cal S},E)$ can be interpreted as a map
with a set of roads $R$ and a set of junctions $J$, defined in the following
manner:

  * •

a _road_ $r$ of $G$ is a maximal directed path
$r={v_{0}}\xrightarrow{s_{1}}_{G}{v_{1}}$,
${v_{1}}\xrightarrow{s_{2}}_{G}{v_{2}}$, …,
${v_{n-1}}\xrightarrow{s_{n}}_{G}{v_{n}}$ where all the vertices $v_{1}$, …,
$v_{n-1}$ have indegree and outdegree equal to one. We say that $v_{0}$ is the
_entrance_ and $v_{n}$ is the _exit_ of $r$. Let $R=\\{r_{i}\\}_{i\in I}$ be
the set of roads of $G$.

  * •

a junction $j$ of $G$ is any maximal weakly connected sub-graph $G^{\prime}$
of $G$, obtained from $G$ by removing from its roads all the vertices (and
connecting edges) except their entrances and exits. Note that for a junction,
its set of vertices of indegree one are exits of some road and its set of
vertices of outdegree one are entrances of some road. Let
$J=\\{j_{\ell}\\}_{\ell\in L}$ be the set of junctions of $G$.

Note that $G$ is the union of the subgraphs representing its roads and
junctions. For every junction, the strong connectivity of $G$ implies that
from any entrance there exists at least one path leading to an exit.
Additionally, we assume that maps include information about features of roads,
junctions that are relevant to traffic regulations:

  * •

roads and junctions are _typed_ : road types can be highway, built-up area
roads, carriage roads, etc. Junctions types can be roundabouts, crossroads,
highway exit, highway entrance, etc. We use standard notation associating a
road or junction to its type e.g., $r:\mathit{highway}$,
$j:\mathit{roundabout}$.

  * •

roads, junctions and their segments have _attributes_. We use the dot notation
$a.\mathit{x}$ and $a.\mathit{X}$ to denote respectively the attribute $x$ or
the set of attributes $X$ of $a$. In particular, we denote by $r.\mathit{en}$
and $r.\mathit{ex}$ respectively the entrance and the exit of a road $r$ and
by $j.\mathit{En}$ and $j.\mathit{Ex}$ the sets of entrances and exits of a
junction $j$. Similarly, $r.\mathit{lanes}$ is the number of lanes of the road
$r$.

Note that contraction and refinement transform maps into maps. A road may be
refined into a road while a junction may be decomposed into a set of roads and
junctions. Furthermore, abstraction and concretization transform maps into
maps as they preserve their connectivity.

Given a map with sets of roads and junctions $R$ and $J$ respectively, it is
possible to derive compositionally its bottom-up and top-down specifications.
We show first how we can get formulas $\zeta_{j}$, $\zeta_{r}$ and $\xi_{j}$,
$\xi_{r}$ for the bottom-up and top-down specifications of $j$ and $r$,
respectively. Let us consider the junctions illustrated in Fig. 7:

  * •

if $ra$ is a roundabout with $n$ entrances
$ra.\mathit{En}=\\{en_{k}\\}_{k\in[1,n]}$ alternating with $n$ exits
$ra.\mathit{Ex}=\\{ex_{k}\\}_{k\in[1,n]}$ then its bottom-up specification is
$\zeta_{ra}\stackrel{{\scriptstyle
def}}{{=}}\sum_{k=1}^{n}\zeta_{k}+\sum_{k=1}^{n}\zeta_{k,k+1}$, where
$\zeta_{k}\stackrel{{\scriptstyle
def}}{{=}}{ex_{k}}\xrightarrow{s_{k}}{en_{k}}$ and
$\zeta_{k,k+1}\stackrel{{\scriptstyle
def}}{{=}}{en_{k}}\xrightarrow{s_{k,k+1}}{ex_{k+1}}$. The top-down
specification is $\xi_{ra}\stackrel{{\scriptstyle
def}}{{=}}\bigwedge_{k=1}^{n}\xi_{k}\wedge\bigwedge_{k=1}^{n}\xi_{k,k+1}$
where $\xi_{k}\stackrel{{\scriptstyle def}}{{=}}\sim\\!\\!{\zeta_{k}}$ and
$\xi_{k,k+1}\stackrel{{\scriptstyle def}}{{=}}\sim\\!\\!{\zeta_{k,k+1}}$.

  * •

if $in$ is an intersection with $n$ entrances
$in.\mathit{En}=\\{en_{k}\\}_{k=1,n}$ and $n$ exits
$in.\mathit{Ex}=\\{ex_{k}\\}_{k\in[1,n]}$ then its bottom-up specification is
$\zeta_{in}\stackrel{{\scriptstyle def}}{{=}}\sum_{k=1}^{n}\zeta_{k}$ with
$\zeta_{k}\stackrel{{\scriptstyle def}}{{=}}\sum_{j\in
J_{k}}{en_{k}}\xrightarrow{s_{k,j}}{ex_{j}}$ and $J_{k}$ is the set of indices
of the exits of $j.\mathit{Ex}$ connected to the entrance $en_{k}$. Hence, the
top-down specification is $\xi_{in}\stackrel{{\scriptstyle
def}}{{=}}\bigwedge_{k=1}^{n}\xi_{k}$ where $\xi_{k}\stackrel{{\scriptstyle
def}}{{=}}\sim\\!\\!{\zeta_{k}}$.

  * •

the formulas for a merger $mg$ and a fork $fk$ with respectively $n$ entrances
and $n$ exits and unique exit and entrance respectively, can be obtained as a
particular case of an intersection.

  * •

finally, for a road $r$ the corresponding specifications are $\zeta_{r}$ and
$\xi_{r}\stackrel{{\scriptstyle def}}{{=}}\sim\\!\\!{\psi_{r}}$ with
$\zeta_{r}\stackrel{{\scriptstyle
def}}{{=}}{r.\mathit{en}}\xrightarrow{s_{r}}{r.\mathit{ex}}$.

$ex_{k}$$en_{k}$$s_{k,k+1}$roundabout$ex_{k+1}$$en_{k+1}$$s_{1}$$s_{n}$$s_{1}$$s_{n}$$en_{1}$$en_{n}$$ex$fork$ex_{n}$$ex_{1}$$en$merger$en$$ex$$s$road$s_{k,l}$$s_{k,j}$$ex_{l}$$ex_{j}$$en_{k}$$en_{j}$$ex_{k}$$en_{l}$intersection$s_{k}$$s_{k+1}$

Figure 7:  Junctions and roads

Note that a map can be characterized by $R=\\{r_{i}\\}_{i\in I}$,
$J=\\{j_{\ell}\\}_{\ell\in L}$, and a set of connectivity equations
$E\subseteq\\{r_{i}.en=j_{\ell}.ex_{k}~{}|~{}r_{i}\in R,j_{\ell}\in
J,ex_{k}\in
j_{\ell}.\mathit{Ex}\\}\cup\\{r_{i}.ex=j_{\ell}.en_{k}~{}|~{}r_{i}\in
R,j_{\ell}\in J,en_{k}\in j.\ell.\mathit{En}\\}$ indicating how the road
entrances/exits are connected to junction exits/entrances (see Fig. 8). Let
$\zeta_{j}$, $\xi_{j}$ and $\zeta_{r}$, $\xi_{r}$ be the formulas
corresponding to the bottom-up and top-down specifications of a junction $j$
and a road $r$. Then the global map specifications are
$\zeta_{M}\stackrel{{\scriptstyle def}}{{=}}\sum_{i\in
I}\zeta_{r_{i}}+\sum_{\ell\in L}\zeta_{j_{\ell}}[E/j_{\ell}.\mathit{En}\cup
j_{\ell}.\mathit{Ex}]$ where in $\zeta_{j_{\ell}}$ the entrance and exit names
of $j_{\ell}$ are replaced by the corresponding road endpoints.

$j_{3}$$j_{1}$$j_{2}$$r_{1}$$r_{3}$$j_{1}.en_{1}=r_{1}.ex$$j_{1}.ex_{1}=r_{2}.en$$j_{1}.en_{2}=r_{3}.ex$$j_{2}.ex_{1}=r_{3}.en$$j_{2}.ex_{2}=r_{5}.en$$r_{5}$$r_{4}$$j_{3}.ex_{2}=r_{4}.en$$r_{2}$$j_{3}.ex_{1}=r_{1}.en$$j_{3}.en_{2}=r_{5}.ex$$j_{2}.en_{1}=r_{4}.ex$

Figure 8: Map specification

###  3.2 Dynamic ADS Model

Given a metric graph $G$ representing a map, the state of an ADS is a tuple
$\mathbf{s}\stackrel{{\scriptstyle
def}}{{=}}\langle\mathbf{s}_{o}\rangle_{o\in{\cal O}}$ representing the
distribution of a finite set of objects ${\cal O}$ with their relevant dynamic
attributes on the map $G$. The set of objects ${\cal O}$ includes a set of
vehicles ${\cal C}$ and sets of immobile equipment used to enforce traffic
rules such as lights, road signs, gates, etc.

For a vehicle $c$, its state $\mathbf{s}_{c}\stackrel{{\scriptstyle
def}}{{=}}\langle\mathit{it,pos,sp,wt,ln,...}\rangle$ includes respectively
its _itinerary_ (from the set of segments ${\cal S}$), its _position_ on the
map (from $\mathit{Pos}_{G}$), its _speed_ (from $\mathbb{R}_{\geq 0}$), the
_waiting time_ (from $\mathbb{R}_{\geq 0}$) which is the time elapsed since
the speed of $c$ became zero, the _lane_ it is traveling (from
$\mathbb{R}_{\geq 0}$), etc. For a traffic light $lt$, its state
$\mathbf{s}_{lt}\stackrel{{\scriptstyle
def}}{{=}}\langle\mathit{pos,cl,...}\rangle$ includes respectively its
position on the map (from $\mathit{Pos}_{G}$), and its _color_ (with values
_red_ and _green_), etc.

For a given set of vehicles ${\cal C}$, we define below the transition
relation of the dynamic model on tuples of vehicle states
$\langle\mathbf{s}_{c}\rangle_{c\in{\cal C}}$ labeled by time increments
$\Delta t$. For this purpose, we assume that each vehicle $c$ is equipped with
a function $c.\mathit{ctrl}$ that determines its dynamics continuously
pursuing two goals: 1) keep the vehicle on the trajectory defined by its
itinerary; and 2) safety goals e.g., avoid collision with obstacles in its
neighborhood and respect traffic rules. Then, the evolution of some key state
variables is defined as follows:

$\begin{array}[]{rcl}c.\mathit{sp}(t+\Delta t)&\stackrel{{\scriptstyle
def}}{{=}}&c.\mathit{sp}(t)+c.\mathit{ctrl}(\mathbf{s}(t))\cdot\Delta t\\\
c.\mathit{pos}(t+\Delta t)&\stackrel{{\scriptstyle
def}}{{=}}&(c.\mathit{pos}(t),c.\mathit{it}(t),c.\mathit{sp}(t)\cdot\Delta
t)\\\ c.\mathit{it}(t+\Delta t)&\stackrel{{\scriptstyle
def}}{{=}}&{c.\mathit{it}}[{c.\mathit{sp}(t)\cdot\Delta
t},{{|\\!|c.\mathit{it}|\\!|}}]\end{array}$

That is, the vehicle $c$ travels at constant speed $c.\mathit{sp}(t)$ for time
$\Delta t$ and

  1. (i)

its speed during the next interval $\Delta t$ is computed using the speed
control function $c.\mathit{ctrl}$ depending on system global state $s(t)$.

  2. (ii)

its next position is obtained from $c.\mathit{pos}(t)$ following the itinerary
$c.\mathit{it}(t)$ for the distance $c.\mathit{sp}(t)\cdot\Delta t$.

  3. (iii)

its next itinerary is obtained by erasing the initial sub-segment of the same
distance from $c.\mathit{it}(t)$.

$c_{1}$$c_{2}$$c_{3}$$c_{1}.it$$c_{2}.it$$c_{3}.it$update statenext
statecomputevariables$\Delta t$$c_{2}.ctrl$$c_{3}.ctrl$$c_{1}.ctrl$EXECUTION
ENGINE$\mathbf{s}(t),\Delta t$$\mathbf{s}(t+\Delta t)$OBJECTDISTRIBUTION

Figure 9:  ADS Execution Principle

Fig. 9 depicts the execution principle by an engine that cyclically updates
the vehicle distribution on a map representing their environment and
coordinates the movement of components representing each one a vehicle by
choosing an adequate execution step $\Delta t$. Of course, in this abstract
execution we do not take into account various aspects of dynamism and
reconfiguration discussed in [12].

For a map $G$ and an initial state $\mathbf{s}^{(t_{0})}$ we define a _run_ as
a sequence of consecutive states $[\mathbf{s}^{(t_{i})}]_{i\geq 0}$
parameterized by an increasing sequence of time points
$t_{i}\in\mathbb{R}_{\geq 0}$, equal to the sum of the time intervals elapsed
for reaching the $i$-th state.

###  3.3 Mobile $\mathit{MCL}$ and Scenario Description for ADS

Mobile $\mathit{MCL}$ (shorthand $\mathit{M2CL}$) is an extension of
$\mathit{MCL}$ for the specification of states of dynamic ADS models as
distributions of objects over maps. It is equipped with object variables $Y$
with attributes allowing to express constraints on object states. Object
variables in $Y$ are typed and denote objects from a finite set ${\cal O}$.
Constraints are obtained by extending the syntax of $\mathit{MCL}$ to include
object attribute terms. For example, if $y$ is a ”vehicle” variable then
$y.\mathit{it}$ is a segment term, $y.\mathit{pos}$ is a position term, and
$y.\mathit{ln}$, $y.\mathit{sp}$, $y.\mathit{wt}$ are arithmetic terms of
$\mathit{M2CL}$. Moreover, $\mathit{M2CL}$ allows for equality $y=y^{\prime}$
and existential quantification $\exists y$ of object variables.

The semantics of $\mathit{M2CL}$ formulas is defined on distributions
$\langle\sigma,G,\mathbf{s}\rangle$ where $\sigma$ provides an interpretation
of variables (including object variables) to their respective domains, $G$ is
a metric graph representing the map, and $\mathbf{s}$ is the system state
vector for objects in ${\cal O}$. The evaluation of terms is extended to
include object attributes, that is, for any object variable $y$ with attribute
$\mathit{attr}$ we define $\sigma~{}y.\mathit{attr}\stackrel{{\scriptstyle
def}}{{=}}\mathbf{s}_{\sigma y}(\mathit{attr})$. Equality and existential
elimination on objects variables are interpreted with the usual meaning, that
is, $y=y^{\prime}$ holds on $\langle\sigma,G,\mathbf{s}\rangle$ iff $\sigma
y=\sigma y^{\prime}$ and respectively $\exists y.~{}\psi$ holds on
$\langle\sigma,G,\mathbf{s}\rangle$ iff $\psi$ holds on
$\langle\sigma[y\mapsto o],G,\mathbf{s}\rangle$ for some object $o\in{\cal
O}$.

From a methodological perspective, we restrict to $\mathit{M2CL}$ formulas
that can be written as boolean combinations of three categories of sub-
formulas:

  1. (i)

$\psi_{map}$ describing map specifications characterizing the static
environment in which a dynamic system evolves,

  2. (ii)

$\psi_{dyn}$ describing relations between distributions of the objects of a
dynamic system,

  3. (iii)

$\psi_{add}$ linking itinerary attributes of objects involved in $\psi_{dyn}$
to position addresses of maps described by $\psi_{map}$.

The following set of primitives used respectively in sub-formulas of the above
categories is needed to express ADS scenarios and specifications:

  1. (i)

for $x$, $x^{\prime}$ vertex variables, $X$ set of vertex variables,
$[x~{}\mbox{\it right-of}~{}x^{\prime}~{}\mbox{\it in}~{}X]$, $[x~{}\mbox{\it
opposite}~{}x^{\prime}~{}\mbox{\it in}~{}X]$ express constraints on the
positioning of $x$, $x^{\prime}$ with respect to the map restricted to
vertices in $X$ (typically a junction):
$\small[x~{}\mbox{\it right-of}~{}x^{\prime}~{}\mbox{\it
in}~{}X]\stackrel{{\scriptstyle def}}{{=}}\exists a.\exists
r.\exists\varphi.~{}\bigvee_{x^{\prime\prime}\in
X}{x^{\prime}}\xrightarrow{line[a,\varphi]}{x^{\prime\prime}}\wedge{x}\xrightarrow{arc[r,\varphi+\frac{\pi}{2},-\frac{\pi}{2}]}{x^{\prime\prime}}$
$\small[x~{}\mbox{\it opposite}~{}x^{\prime}~{}\mbox{\it
in}~{}X]\stackrel{{\scriptstyle def}}{{=}}\exists
a.\exists\varphi.~{}\bigvee_{x^{\prime\prime},x^{\prime\prime\prime}\in
X}{x}\xrightarrow{line[a,\varphi]}{x^{\prime\prime}}\wedge{x^{\prime}}\xrightarrow{line[a,\varphi+\pi]}{x^{\prime\prime\prime}}$

  2. (ii)

for $c$, $o$ respectively vehicle, object variables, $d$ arithmetic term,
$[{c}~{}\mathit{meets}(d)~{}o]$ means that $c$ reaches the position of $o$ at
distance $d$:
$\small[{c}~{}\mathit{meets}(d)~{}o]\stackrel{{\scriptstyle def}}{{=}}\exists
z,z^{\prime}.~{}{c.\mathit{pos}}\stackrel{{\scriptstyle
z}}{{\leadsto}}{o.\mathit{pos}}\wedge c.\mathit{it}=z\cdot
z^{\prime}\wedge{|\\!|z|\\!|}=d$

  3. (iii)

a) for $c$ a vehicle variable, $X$ a set of vertex variables, $[c~{}\mbox{\it
go-straight}~{}X]$, $[c~{}\mbox{\it turn-right}~{}X]$, $[c~{}\mbox{\it turn-
left}~{}X]$ express constraints on the itinerary of $c$ within the map
restricted to vertices in $X$ (typically, a junction):
$\small\begin{array}[]{lcl}[c~{}\mbox{\it go-
straight}~{}X]&\stackrel{{\scriptstyle def}}{{=}}&\exists
a.\exists\varphi.\exists z.~{}\bigvee_{x,x^{\prime}\in
X}c.\mathit{pos}=x\wedge{x}\xrightarrow{line[a,\varphi]}{x^{\prime}}\wedge
c.\mathit{it}=line[a,\varphi]\cdot z\\\\[3.0pt] [c~{}\mbox{\it turn-
right}~{}X]&\stackrel{{\scriptstyle def}}{{=}}&\exists
r.\exists\varphi.\exists z.~{}\bigvee_{x,x^{\prime}\in
X}c.\mathit{pos}=x\wedge{x}\xrightarrow{arc[r,\varphi,-\frac{\pi}{2}]}{x^{\prime}}\wedge
c.\mathit{it}=arc[r,\varphi,-\frac{\pi}{2}]\cdot z\\\\[3.0pt] [c~{}\mbox{\it
turn-left}~{}X]&\stackrel{{\scriptstyle def}}{{=}}&\exists
r.\exists\varphi.\exists z.~{}\bigvee_{x,x^{\prime}\in
X}c.\mathit{pos}=x\wedge{x}\xrightarrow{arc[r,\varphi,+\frac{\pi}{2}]}{x^{\prime}}\wedge
c.\mathit{it}=arc[r,\varphi,+\frac{\pi}{2}]\cdot z\end{array}$

b) for $o$ an object variable, $X$ a set of vertex variables, $l$ an optional
arithmetic term, $[{o}\mathit{@}{X,l}]$ means that the position of $o$ belongs
to the map subgraph restricted to vertices in $X$ and the lane of $o$ is $l$:
$\small[{o}\mathit{@}{X,l}]\stackrel{{\scriptstyle def}}{{=}}\left(\exists
d.\exists s.\bigvee_{x,x^{\prime}\in X}{x}\xrightarrow{s}{x^{\prime}}\wedge
o.\mathit{pos}=(x,s,d)\vee o.\mathit{pos}=x\right)\\!\wedge\\!o.\mathit{ln}=l$

####  3.3.1 Scenario Description for ADS.

We define a scene as a triplet
$\langle\psi_{map},\psi_{add},\psi_{dyn}\rangle$ of $\mathit{M2CL}$ formulas
without universal quantifiers where $\psi_{add}$ defines the addresses of the
objects involved in $\psi_{dyn}$ in the map specified by $\psi_{map}$. As for
maps, a scene can have a top-down and a bottom-up specification defined
respectively by the formulas,
$\sim\\!\\!{\psi}_{map}\Rightarrow\psi_{add}\wedge\psi_{dyn}$ and
$\psi_{map}\wedge\psi_{add}\wedge\psi_{dyn}$.

A scenario is a sequence of scenes sharing a common map context and intended
to describe relevant partial states of an ADS run. There are several proposals
for scenario description languages [3, 9, 17, 15]. Figure 10 presents a
scenario of two scenes taken from [3]. The initial scene is defined by:

$\small\begin{array}[]{rcl}\psi_{map}&=&[r:road(x,s,y)]\wedge[s.\mathit{lanes}=2]\\\
\psi_{add}&=&[{ego}\mathit{@}{r,1}]\wedge[{c_{1}}\mathit{@}{r,1}]\wedge[{c_{2}}\mathit{@}{r,2}]\\\
\psi_{dyn}&=&[{ego}~{}\mathit{meets}(84)~{}c_{1}]\wedge[{c_{2}}~{}\mathit{meets}(100)~{}ego]\wedge[ego.\mathit{sp}=c_{1}.\mathit{sp}=100\wedge
c_{2}.\mathit{sp}=110]\end{array}$

The second scene after the vehicle $c_{2}$ passes the $ego$ vehicle is:

$\small\begin{array}[]{rcl}\psi^{\prime}_{map}&=&[r:road(x,s,y)]\wedge[s.\mathit{lanes}=2]\\\
\psi^{\prime}_{add}&=&[{ego}\mathit{@}{r,1}]\wedge[{c_{1}}\mathit{@}{r,1}]\wedge[{c_{2}}\mathit{@}{r,1}]\\\
\psi^{\prime}_{dyn}&=&[{ego}~{}\mathit{meets}(20)~{}c_{2}]\wedge[{c_{2}}~{}\mathit{meets}(64)~{}c_{1}]\wedge[ego.\mathit{sp}=c_{1}.\mathit{sp}=100\wedge
c_{2}.\mathit{sp}=110]\end{array}$

Note that from a semantic point of view, a scene is characterized by minimal
models of $\mathit{M2CL}$ $\langle\sigma,G,\mathbf{s}\rangle$ that satisfy the
formula and where all irrelevant components of $\mathbf{s}$ are omitted. For
instance, in the minimal models of the two scenes only the components of
$\mathbf{s}$ corresponding to $c_{1}$, $c_{2}$ and $ego$ are taken.

$c_{2}$$ego$$c_{1}$$100km/h$$100km/h$$110km/h$$20m$$84m$$100m$

Figure 10: A scenario

Of particular practical relevance are dynamic scenarios [15, 16] used to
control the execution of objects of an ADS model. These can be described as
sequences of guarded commands of the form
$sc\boldsymbol{\rightarrow}c_{1}.\mathit{act_{1}}\&\cdots\&c_{n}.\mathit{act_{n}}$
where the guard is a scene $sc$ involving a set of vehicles $c_{1},\cdots
c_{n}$ and the command is a list of control actions to be executed by the
vehicles. The control action $c.\mathit{act}$ is an action to be performed by
vehicle $c$ and affecting its own state variables. Hence,
$sc\boldsymbol{\rightarrow}c_{1}.\mathit{act_{1}}\&\cdots\&c_{n}.\mathit{act_{n}}$
describes a transition of an ADS from a scene $sc$ to a new scene obtained by
collateral modification of the state variables of the involved vehicles after
execution of the corresponding actions. We define two control actions for a
vehicle $c$ and an interval constraint $cnt$ of the form $speed_{1}\leq
c.\mathit{sp}\leq speed_{2}$ :

  * •

$c.\mathit{move}(cnt\mbox{ at }d)$ means that $c$ should travel to a position
at distance $d$ and $c.\mathit{sp}$ satisfies $cnt$ at this position. That is
after executing $c.\mathit{move}(cnt\mbox{ at }d)$ from state $sc$ with
$c.\mathit{pos}=p$ the new state will have $c.\mathit{pos}=p+d$ and the speed
$c.\mathit{sp}$ will satisfy $cnt$.

  * •

$c.\mathit{move}(cnt\mbox{ to }p)$ means that $c$ should travel to position
$p$ while $c.\mathit{sp}$ continuously satisfies $cnt$. That is after
executing $c.\mathit{move}(cnt\mbox{ at }d)$ from state $sc$ the new state
will have $c.\mathit{pos}=p$ and the speed $c.\mathit{sp}$ will satisfy
satisfy $cnt$ at any position between the current position and $p$.

We provide below few action rules enforcing ADS properties and traffic rules:

  1. (i)

$[{c}~{}\mathit{meets}(d)~{}st]\boldsymbol{\rightarrow}c.\mathit{move}(\mbox{0
at $d$})$ i.e., $c$ should brake to stop exactly before a stop sign;

  2. (ii)

<EMAIL_ADDRESS>$\wedge$ $[\neg\exists
<EMAIL_ADDRESS>$\wedge$ [$j.\mathit{ex}\in c.\mathit{it}]$ $\boldsymbol{\rightarrow}$
$c.\mathit{move}(\mbox{$v$ to $j.\mathit{ex}$})$ i.e., if $c$ has been waiting
longer than any other car at the entrance of a junction $j$, then it can move
to the exit intersecting its itinerary reaching speed $v$;

  3. (iii)

<EMAIL_ADDRESS>c.\mathit{it}]\boldsymbol{\rightarrow}c.\mathit{move}(\mbox{$v$ to
$j.\mathit{ex}$})$ i.e., if a vehicle $c$ is in a junction $j$ then it will
move to its exit intersecting its itinerary;

  4. (iv)

$[{c}~{}\mathit{meets}(d)~{}lt]\wedge[d\leq
d_{min}]\boldsymbol{\rightarrow}c.\mathit{move}(\mbox{0 at $d$})$ i.e., it $c$
is approaching a light and the distance is less than a distance $d_{min}$ then
$c$ should start braking to stop at $d$;

  5. (v)

<EMAIL_ADDRESS>d_{min}]\wedge[lt.\mathit{cl}=\mbox{\it green}]\wedge[j.\mathit{ex}\in
c.\mathit{it}]\boldsymbol{\rightarrow}c.\mathit{move}(\mbox{$v$ to
$j.\mathit{ex}$})$

###  3.4 Temporal $\mathit{M2CL}$ and Specification of ADS

_Temporal_ -$\mathit{M2CL}$ (shorthand $\mathit{TM2CL}$) is defined as the
linear time temporal extension of $\mathit{M2CL}$. The syntax is as follows:

$\Phi::=\phi~{}|~{}\mathbf{N}~{}\Phi~{}|~{}\Phi~{}\mathbf{U}~{}\Phi~{}|~{}\Phi\wedge\Phi~{}|~{}\exists
c.~{}\Phi~{}|~{}\neg\Phi$

where $\phi$ is $\mathit{M2CL}$ formula. The semantics of $\mathit{TM2CL}$ is
defined on triples $(\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq 0})$ containing
respectively an assignment of vehicle variables defined in the
$\mathit{TM2CL}$ context, a map $G$ and a run $[\mathbf{s}^{(t_{i})}]_{i\geq
0}$ on $G$ for a finite set of objects ${\cal O}$. The semantic rules are
defined in Table 5.

$\begin{array}[]{rclcl}\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}&\models&\phi&\mbox{iff}&\sigma,G,\mathbf{s}^{(t_{0})})\models\phi\\\
\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}&\models&\mathbf{N}~{}\Phi&\mbox{iff}&\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
1}\models\Phi\\\ \sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}&\models&\Phi_{1}~{}\mathbf{U}~{}\Phi_{2}&\mbox{iff}&\exists k\geq
0.~{}\forall j\in[0,k-1].~{}\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
j}\models\Phi_{1}\\\ &&&&\mbox{and }\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
k}\models\Phi_{2}\\\ \sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}&\models&\Phi_{1}\wedge\Phi_{2}&\mbox{iff}&\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}\models\Phi_{1}\mbox{ and }\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}\models\Phi_{2}\\\ \sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq 0}&\models&\exists
o.~{}\Phi&\mbox{iff}&\sigma[o\mapsto u],G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}\models\Phi,\mbox{ for some }u\in{\cal O}\\\
\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}&\models&\neg\Phi&\mbox{iff}&\sigma,G,[\mathbf{s}^{(t_{i})}]_{i\geq
0}\not\models\Phi\end{array}$ Table 5:  Semantics of $\mathit{TM2CL}$

We use $\mathit{TM2CL}$ for both the specification of system properties and
traffic rules. The difference between the two concepts is not clear-cut
although it is implicit in many works. System properties characterize the
desired ADS behavior in terms of relations between speeds and distances taking
into account relevant dynamic characteristics. These include properties such
as keeping safe distance or keeping acceleration and deceleration rates
between some bounds.

Traffic rules are higher-level specifications for enhanced safety and
efficiency that usually depend on the driving context. They deal not only with
obligations such as yielding right of way and traffic control at junctions but
also advice on how to drive sensibly and safely in situations disrupting
traffic flow such as congestion, accidents and works in progress. We provide
below a formalization of system properties and traffic rules showing the
expressiveness of our modeling framework. We rather focus on the specification
of traffic rules because it is context sensitive and nicely illustrates the
intricacy of the combination of static and dynamic aspects.

Specifications related to junctions (i.e., intersections, roundabouts, etc)
are written as implications $\sim\\!\\!{\zeta}(j)\Rightarrow\Phi(j)$ where
$\zeta(j)$ is a $\mathit{MCL}$ formula characterizing a junction $j$ (cf.
section 3.1, see example 2 for illustration) and $\Phi(j)$ is a
$\mathit{TM2CL}$ formula specifying the temporal property holding in the
context of $j$.

System Properties: We provide examples of general properties that should be
respected for vehicles for any type or road or junction.

  1. (i)

keep safe distance, on the same lane or during overtaking:
$\begin{array}[]{l}\forall c_{1}.~{}\forall c_{2}.~{}\Box~{}\left[\forall
d.~{}[{c_{1}}~{}\mathit{meets}(d)~{}c_{2}]\wedge[abs(c_{1}.\mathit{ln}-c_{2}.\mathit{ln})<1]\right.\left.\Rightarrow[d\geq\mathit{safe\textrm{-}dist}(c_{1},c_{2})]\right]\end{array}$
where $\mathit{safe\textrm{-}dist}(c_{1},c_{2})$ is the minimal distance for
safe braking computed as a function of the speeds of the two vehicles/objects
$c_{1}$, $c_{2}$ and the maximal braking force of $c_{1}$;

  2. (ii)

reduce speed at proximity of a _stop_ sign:
$\forall c.~{}\forall st.~{}\Box~{}\left[\forall
d.~{}[{c}~{}\mathit{meets}(d)~{}st]\Rightarrow[d\geq\mathit{safe\textrm{-}dist}(c,st)]\right]$

  3. (iii)

whenever moving along arc segments, maintain the centrifugal force below some
constant threshold $C$:
$\forall c.~{}\Box~{}\left[\forall
r.~{}\forall\varphi.~{}\forall\theta.~{}\forall
z^{\prime}.~{}[c.\mathit{it}=arc[r,\varphi,\theta]\cdot
z^{\prime}]\Rightarrow[c.\mathit{weight}\cdot(c.\mathit{sp})^{2}/r\leq
C]\right]$

Traffic rules for intersection $j$ with all-way stop: We formalize a set
traffic rules provided in [29]:

  1. (iv)

“If a driver arrives at the intersection and no other vehicles are present,
then the driver can proceed”:
$\forall c.\forall
st.~{}\Box~{}[{st}\mathit{<EMAIL_ADDRESS>c^{\prime}.~{}c^{\prime}\not=c\wedge[{c^{\prime}}\mathit{@}{j}]]\Rightarrow\Diamond[{c}\mathit{@}{j}]$

  2. (v)

“If, on approach of the intersection, there are one or more cars already
there, let them proceed, then proceed yourself”:
$\begin{array}[]{l}\forall c.\forall
st.~{}\Box~{}[{st}\mathit{@}{j.\mathit{en}}]\wedge[{c}~{}\mathit{meets}(d)~{}st]\wedge[d\leq
d_{min}]\Rightarrow\\\ \hskip
56.9055pt[\neg[{c}\mathit{@}{j}]]~{}\mathbf{U}~{}[\neg\exists
c^{\prime}.c^{\prime}\not=c\wedge[{c^{\prime}}\mathit{@}{j}]]\end{array}$

  3. (vi)

“If a driver arrives at the same time as another vehicle, the vehicle on the
right has the right-of-way”:
$\begin{array}[]{l}\forall c.\forall
c^{\prime}.~{}\Box~{}[{c}\mathit{<EMAIL_ADDRESS>right-of}~{}j.\mathit{en^{\prime}}~{}\mbox{\it in}~{}j]\Rightarrow\\\ \hskip
56.9055pt[{c^{\prime}}\mathit{@}{j.\mathit{en^{\prime}}}]~{}\mathbf{U}~{}[{c}\mathit{@}{j}]\end{array}$

  4. (vii)

“(a) If two vehicles arrive opposite each other at the same time, and no
vehicles are on the right, then they may proceed at the same time if they are
going straight ahead. (b) If one vehicle is turning and one is going straight,
the right-of-way goes to the car going straight:”
$\begin{array}[]{l}\forall c.\forall
c^{\prime}.~{}\Box~{}[{c}\mathit{<EMAIL_ADDRESS>opposite}~{}j.\mathit{en^{\prime}}~{}\mbox{\it in}~{}j]\wedge\\\ \hskip
28.45274pt\neg[\exists
<EMAIL_ADDRESS>right-of}~{}j.\mathit{en}~{}\mbox{\it
in}~{}j]\vee[j.\mathit{en^{\prime\prime}}~{}\mbox{\it right-
of}~{}j.\mathit{en^{\prime}}~{}\mbox{\it in}~{}j]]\wedge\\\ \hskip
28.45274pt[c~{}\mbox{\it go-straight}~{}j]\wedge[c^{\prime}~{}\mbox{\it go-
straight}~{}j]~{}\Rightarrow~{}\Diamond[{c}\mathit{<EMAIL_ADDRESS>\forall c.\forall
c^{\prime}.~{}\Box~{}[{c}\mathit{<EMAIL_ADDRESS>opposite}~{}j.\mathit{en^{\prime}}~{}\mbox{\it in}~{}j]\wedge\\\ \hskip
28.45274pt\neg[\exists
<EMAIL_ADDRESS>right-of}~{}j.\mathit{en}]\vee[j.\mathit{en^{\prime\prime}}~{}\mbox{\it right-
of}~{}j.\mathit{en^{\prime}}]]\wedge\\\ \hskip 28.45274pt[c~{}\mbox{\it go-
straight}~{}j]\wedge\neg[c^{\prime}~{}\mbox{\it go-
straight}~{}j]~{}\Rightarrow~{}\Diamond[{c}\mathit{@}{j}]\end{array}$

  5. (viii)

“If two vehicles arrive opposite each other at the same time and one is
turning right and one is turning left, the right-of-way goes to the vehicle
turning right. Since they are both trying to turn into the same road, priority
should be given to the vehicle turning right as they are closest to the lane”:
$\begin{array}[]{l}\forall c.\forall
c^{\prime}.~{}\Box~{}[{c}\mathit{<EMAIL_ADDRESS>opposite}~{}j.\mathit{en^{\prime}}~{}\mbox{\it in}~{}j]\wedge\\\ \hskip
28.45274pt[c~{}\mbox{\it turn-right}~{}j]\wedge[c^{\prime}~{}\mbox{\it turn-
left}~{}j]~{}\Rightarrow~{}\Diamond[{c}\mathit{@}{j}]\end{array}$

Traffic rules for roundabout $j$: We formalize two traffic rules provided in
[30]:

  1. (ix)

“Continue toward the roundabout and look to your left as you near the yield
sign and dashed yield line at the entrance to the roundabout. Yield to traffic
already in the roundabout”:
$\forall
c.~{}\Box~{}[{c}\mathit{<EMAIL_ADDRESS>c^{\prime}.\exists
d.~{}[{c^{\prime}}\mathit{@}{j}]\wedge[{c^{\prime}}~{}\mathit{meets}(d)~{}c]\wedge[d\leq
d_{left}\right]]$

  2. (x)

“Once you see a gap in traffic, enter the circle and proceed to your exit. If
there is no traffic in the roundabout, you may enter without yielding”:
$\forall<EMAIL_ADDRESS>c^{\prime}.\exists
d.~{}[{c^{\prime}}\mathit{@}{j}]\wedge[{c^{\prime}}~{}\mathit{meets}(d)~{}c]\wedge[d\leq
d_{left}]]\Rightarrow~{}\Diamond[{c}\mathit{@}{j}]$

Traffic rules for intersection $j$ with traffic lights $lt$:

  1. (xi)

reduce speed at proximity of a traffic _light_ :
$\forall c.~{}\forall lt.~{}\Box~{}\left[\forall
d.~{}[{c}~{}\mathit{meets}(d)~{}lt]\wedge[d\leq
d_{min}]\Rightarrow[d\geq\mathit{safe\textrm{-}dist}(c,lt)]\right]$

  2. (xii)

eventually enter junction $j$ if the traffic _light_ on the entry is _green_ :
$\begin{array}[]{l}\forall c.~{}\forall lt.~{}\Box~{}\left[\forall
d.~{}[{c}~{}\mathit{meets}(d)~{}lt]\wedge[d\leq
d_{min}]\wedge[{lt}\mathit{@}{j.\mathit{En}}]\right.\left.\wedge~{}[lt.\mathit{cl}=\mathit{green}]\Rightarrow\Diamond[{c}\mathit{@}{j}]\right]\end{array}$

##  4 ADS Validation

###  4.1 Classification of validation problems

The following categories of validation problems can arise in our framework:

####  4.1.1 $\mathit{MCL}$ and $\mathit{M2CL}$ model-checking:

(i) given a map specification $\phi$ as a closed $\mathit{MCL}$ formula and a
metric graph $G$ decide if $G$ is a model of $\phi$. The problem boils down to
checking satisfiability of a segment logic ($\mathit{SL}$) formula obtained by
quantifier elimination of vertex variables and partial evaluation of graph
constraints in $\phi$ according to $G$. We present later in this section a
decision procedure for $\mathit{SL}$. (ii) Similarly, given a distribution
specification $\phi$ as a closed $\mathit{M2CL}$ formula, a map $G$ and a
state $\mathbf{s}$ for a _finite_ set of objects ${\cal O}$, decide if
$\langle G,\mathbf{s}\rangle$ is a model of $\phi$. Again, the problem boils
down to checking satisfiability of a $\mathit{SL}$ formula obtained by
quantifier elimination of vertex and object variables an and partial
evaluation of attribute terms.

####  4.1.2 $\mathit{TM2CL}$ runtime verification:

given a temporal specification $\Phi$ as a $\mathit{TM2CL}$ formula, a map $G$
and a run $[\mathbf{s}^{(t_{i})}]_{i\geq 0}$ of an ADS, check if
$G,[\mathbf{s}^{(t_{i})}]_{i\geq 0}$ is a model of $\Phi$. This problem boils
down to evaluating the semantics of $\Phi$ on the run. In [12] we consider a
similar runtime verification problem for temporal configuration logic and runs
of dynamic reconfigurable systems. We have shown that the evaluation of
linear-time temporal operators and the model-checking of state/configuration
specifications can be dealt separately. The same idea can be applied here: on
one hand, the temporal formulas can be handled by LamaConv [20] to generate
FSM monitors and on the other hand, the model-checking of distribution
specifications can be handled by a SMT solver (such as Z3) by using an
encoding into a decidable theory.

####  4.1.3 $\mathit{MCL}$ and $\mathit{M2CL}$ satisfiability checking:

(i) given a map specification $\phi$ as closed $\mathit{MCL}$ formula decide
if $\phi$ is satisfiable, that is, it has at least one model. We show next in
this section that the problem can be effectively solved for a significant
fragment of $\mathit{MCL}$ including a restricted form of bottom-up map
specifications. Notice that entailment checking, that is, deciding validity of
$\forall\mathbf{x}.~{}\phi_{1}\Rightarrow\phi_{2}$ for map specifications
$\phi_{1}$, $\phi_{2}$ where $fv(\phi_{1})=fv(\phi_{2})=\mathbf{x}$, boils
down to checking satisfiability of
$\exists\mathbf{x}.~{}\phi_{1}\wedge\neg\phi_{2}$, and can be solved under the
same restrictions. (ii) Similarly, given a distribution specification $\phi$
as a closed $\mathit{M2CL}$ formula decides if $\phi$ is satisfiable, that is,
it has at least one model. The problem can be reduced to the satisfiability
checking of $\mathit{MCL}$ specifications whenever $\phi$ is of the restricted
form $\exists y_{1}...\exists y_{k}.~{}\phi^{\prime}$ where $y_{1}$, … $y_{k}$
are the only object variables occurring in $\phi^{\prime}$. In this case,
every object variable $y$ can be _substituted_ by a finite number of
$\mathit{MCL}$ variables $y_{attr}$ encoding its identity and attributes. As
example, for a vehicle variable $y$ consider an identity (real) variable
$y_{id}$, a segment variable $y_{it}$, a position variable $y_{pos}$, real
variables $y_{ln}$, $y_{sp}$, $y_{wt}$, etc. After replacement, we obtain an
equisatisfiable $\mathit{MCL}$ formula by enforcing the additional constraints
that state attributes are consistently assigned (e.g.,
$(y_{id}=y^{\prime}_{id})\Rightarrow y_{it}=y^{\prime}_{it})$ for all pairs
$y$, $y^{\prime}$ of vehicle variables among $y_{1}$, …, $y_{k}$. Finally,
notice also that entailment checking between distributed specifications can be
solved as well, by reduction to satisfiability checking as explained above.

###  4.2 Satisfiability checking

####  4.2.1 Satisfiability checking of $\mathit{MCL}$.

The satisfiability checking for $\mathit{MCL}$ formula is undecidable in
general. Actually, the combined use of edge constraints
${x}\xrightarrow{s}{x^{\prime}}$, equalities on vertex positions
$x=x^{\prime}$, boolean operators and quantifiers leads to undecidability, as
it allows the embedding of first order logic on directed graphs.

Nevertheless, for a significant class of $\mathit{MCL}$ formula, their
satisfiability checking can be reduced to satisfiability checking of _segment
logic_ ($\mathit{SL}$), that is, the fragment of $\mathit{MCL}$ without vertex
variables, which is a first order logic combining only arithmetic and segment
constraints.

A complete metric graph specification $\psi^{*}$ is a $\mathit{MCL}$ formula
of the form:

$\begin{array}[]{c}(\wedge_{1\leq i<j\leq n}~{}x_{i}\not=x_{j})\wedge(\forall
y.\vee_{i=1}^{n}~{}y=x_{i})~{}\wedge\\\
(\textstyle{\sum_{i=1}^{n}\sum_{j=1}^{n}\sum_{h=1}^{m_{ij}}~{}{x_{i}}\xrightarrow{s_{ijh}}{x_{j}}})\wedge(\wedge_{i=1}^{n}\wedge_{j=1}^{n}\wedge_{1\leq
h<h^{\prime}\leq m_{ij}}~{}s_{ijh}\not=s_{ijh^{\prime}})\end{array}$

that is, where the set of free vertex variables is
$\mathbf{x}=\\{x_{1},....,x_{n}\\}$. Note that a complete metric specification
characterizes precisely a metric graph with precisely $n$ vertices (in
correspondence with vertex variables $x_{1}$, $\dots$, $x_{n}$) and, with
precisely $m_{ij}$ distinct edges (that is, defined by the constraints
${x_{i}}\xrightarrow{s_{ijh}}{x_{j}}$ for $h=1,m_{ij}$), for every pair of
vertices $x_{i}$, $x_{j}$.

###### Theorem 4.1

Let $\psi^{*}$ be a complete metric graph specification with free variables
$\mathbf{x}\uplus\mathbf{z}\uplus\mathbf{k}$. For any $\mathit{MCL}$ formula
$\phi$ with $fv(\phi)\subseteq\mathbf{x}\uplus\mathbf{z}\uplus\mathbf{k}$ it
holds

  1. 1.

the closed $\mathit{MCL}$ formula
$\exists\mathbf{x}.~{}\exists\mathbf{z}.~{}\exists\mathbf{k}.~{}\psi^{*}\wedge\phi$
is satisfiable iff

  2. 2.

the closed $\mathit{SL}$ formula

$\begin{array}[]{c}\exists\mathbf{z}.~{}\exists\mathbf{k}.~{}(\wedge_{i=1}^{n}\wedge_{j=1}^{n}\wedge_{1\leq
h<h^{\prime}\leq m_{ij}}~{}s_{ijh}\not=s_{ijh^{\prime}})\wedge\\\ \hskip
85.35826pt(\wedge_{i=1}^{n}\wedge_{j=1}^{n}\wedge_{h=1}^{m_{ij}}~{}{|\\!|s_{ijh}|\\!|}>0)\wedge
tr(n,E^{*},\mu^{*},\phi)\end{array}$

is satisfiable, where $n=card~{}\mathbf{x}$,
$E^{*}=\cup_{i=1}^{n}\cup_{j=1}^{n}\\{(i,s_{ijh},j)\\}_{h=1,m_{ij}}$,
$\mu^{*}=\\{x_{i}\mapsto i\\}_{i=1,n}$ and the translation $tr(n,E,\mu,\phi)$
is defined in table 6.

###### Proof

($1.\rightarrow 2.$) If the formula $\psi^{*}\wedge\phi$ is satisfiable, then
it has a metric graph model isomorphic to the (unique up to edge labeling)
metric graph $G_{\psi^{*}}$ specified by $\psi^{*}$. The translated formula
$tr(n,E^{*},\mu^{*},\phi)$ represents the evaluation of the semantics of
$\phi$ on the metric graph $G_{\psi^{*}}$ according to the rules defined in
Table 3. It must be therefore satisfiable as well, as initially
$\psi^{*}\wedge\phi$ is satisfiable. ($2.\Rightarrow 1.$) If the conjunction
of the translated formula $tr(n,E^{*},\mu^{*},\phi)$ and the additional
constraints has a model, ones can use it to build a metric graph, isomorphic
to $G_{\psi^{*}}$, satisfying both $\psi^{*}$ and $\phi$. In particular the
additional constraints ensure that the metric graph is well formed, that is,
all edges are labeled by non-zero length segments, and there are no replicated
edges between any pairs of vertices.

$\begin{array}[]{rcl}\hline\cr tr(n,E,\mu,\psi_{K})&\stackrel{{\scriptstyle
def}}{{=}}&\psi_{K}\\\ tr(n,E,\mu,\psi_{S})&\stackrel{{\scriptstyle
def}}{{=}}&\psi_{S}\\\
tr(n,E,\mu,{x}\xrightarrow{s}{y})&\stackrel{{\scriptstyle
def}}{{=}}&\left\\{\begin{array}[]{ll}s=s_{ijh}&\mbox{if
}E=\\{(i,s_{ijh},j)\\},~{}\mu x=i,~{}\mu y=j\\\ \mbox{\it
false}&\mbox{otherwise}\end{array}\right.\\\
tr(n,E,\mu,p=p^{\prime})&\stackrel{{\scriptstyle def}}{{=}}&\mbox{\bf eq-
pos}(n,E,\mu,p,p^{\prime})\\\ tr(n,E,\mu,{p}\stackrel{{\scriptstyle
s}}{{\leadsto}}{p^{\prime}})&\stackrel{{\scriptstyle def}}{{=}}&\mbox{\bf
acyclic-path}(n,E,\mu,p,s,p^{\prime})\\\
tr(n,E,\mu,\phi_{1}+\phi_{2})&\stackrel{{\scriptstyle
def}}{{=}}&\bigvee_{E_{1}\cup E_{2}=E}tr(n,E_{1},\mu,\phi_{1})\wedge
tr(n,E_{2},\mu,\phi_{2})\\\
tr(n,E,\mu,\phi_{1}\vee\phi_{2})&\stackrel{{\scriptstyle
def}}{{=}}&tr(n,E,\mu,\phi_{1})\vee tr(n,E,\mu,\phi_{2})\\\
tr(n,E,\mu,\neg\phi)&\stackrel{{\scriptstyle def}}{{=}}&\neg
tr(n,E,\mu,\phi)\\\ tr(n,E,\mu,\exists k.~{}\phi)&\stackrel{{\scriptstyle
def}}{{=}}&\exists k.~{}tr(n,E,\mu,\phi)\\\ tr(n,E,\mu,\exists
z.~{}\phi)&\stackrel{{\scriptstyle def}}{{=}}&\exists z.~{}tr(n,E,\mu,\phi)\\\
tr(n,E,\mu,\exists x.~{}\phi)&\stackrel{{\scriptstyle
def}}{{=}}&\bigvee_{i=1}^{n}tr(n,E,\mu[x\mapsto i],\phi)\\\
\hline\cr\end{array}$ Table 6:  Translation rules for Theorem 4.1

The complete definition of eq-pos and acyclic-path is provided in the
appendix. Also, notice that distance constraints of the form
$d(p,p^{\prime})=t$ have not been considered as they are equivalent to

$(p=p^{\prime}\wedge t=0)\vee((\exists z.~{}{p}\stackrel{{\scriptstyle
z}}{{\leadsto}}{p^{\prime}}\wedge{|\\!|z|\\!|}=t)\wedge(\forall
z.~{}{p}\stackrel{{\scriptstyle
z}}{{\leadsto}}{p^{\prime}}\Rightarrow{|\\!|z|\\!|}\geq t))$

####  4.2.2 Satisfiability checking of $\mathit{SL}$.

If segments ${\cal S}$ are restricted to particular interpretations, the
satisfiability checking of formula of $\mathit{SL}$ can be further reduced to
satisfiability checking of formula of extended arithmetics on reals.

###### Theorem 4.2

If segments ${\cal S}$ are defined as intervals

  1. 1.

the closed $\mathit{SL}$ formula $\phi$ is satisfiable iff

  2. 2.

the closed real arithmetic formula $tr_{1}(\phi)$ is satisfiable, where the
translation $tr_{1}(\phi)$ is defined in Table 7.

###### Proof

With interval interpretation, segments are precisely determined by their
length and all segment operations and constraints boil down to operations and
constraints on reals. Moreover, we remark that the transformation does not
require multiplication555except if needed for encoding the length of segment
types on real terms, henceforth, the translated formula $tr_{1}(\phi)$ belongs
to linear arithmetic iff all arithmetic constraints $\psi_{K}$ within $\phi$
were linear.

$\begin{array}[]{rcl rcl}\hline\cr tr_{1}({|\\!|s^{T}(t_{1},\cdots
t_{m})|\\!|})&\stackrel{{\scriptstyle
def}}{{=}}&len\mbox{-}s^{T}(t_{1},...,t_{m})&tr_{1}(s=s^{\prime})&\stackrel{{\scriptstyle
def}}{{=}}&tr_{1}({|\\!|s|\\!|})=tr_{1}({|\\!|s^{\prime}|\\!|})\\\
tr_{1}({|\\!|z|\\!|})&\stackrel{{\scriptstyle
def}}{{=}}&k_{z}&tr_{1}({|\\!|s|\\!|}=t)&\stackrel{{\scriptstyle
def}}{{=}}&tr_{1}({|\\!|s|\\!|})=t\\\ tr_{1}({|\\!|s\cdot
s^{\prime}|\\!|})&\stackrel{{\scriptstyle
def}}{{=}}&tr_{1}({|\\!|s|\\!|})+tr_{1}({|\\!|s^{\prime}|\\!|}))&~{}~{}~{}tr_{1}(\phi_{1}\vee\phi_{2})&\stackrel{{\scriptstyle
def}}{{=}}&tr_{1}(\phi_{1})\vee tr_{1}(\phi_{2})\\\
&&&tr_{1}(\neg\phi)&\stackrel{{\scriptstyle def}}{{=}}&\neg tr_{1}(\phi)\\\
&&&tr_{1}(\exists k.~{}\phi)&\stackrel{{\scriptstyle def}}{{=}}&\exists
k.~{}tr_{1}(\phi)\\\ &&&tr_{1}(\exists z.~{}\phi)&\stackrel{{\scriptstyle
def}}{{=}}&\exists k_{z}.~{}tr_{1}(\phi)\\\ \hline\cr\end{array}$ Table 7:
Translation rules for Theorem 4.2

###  4.3 Validation in the large - Catching up with the needs

There is a big gap between the state of the art and needs for validation of
ADS achievable only through simulation and testing due to overwhelming
complexity. How existing results can be integrated into a rigorous validation
methodology intended to provide conclusive trustworthiness evidence? We bring
elements of an answer to the above question and show how the proposed
framework provides insight into the different aspects of validation and
related methodological and technical issues.

Fig. 11 depicts the architecture of a general validation environment
integrating three tools: i) a Simulator; ii) a dynamic Scenario Execution
Engine; and iii) a Monitor. Simulation is driven by actions generated by the
Scenario Execution Engine. It consists in executing the model of some ADS and
generating runs checked online by the Monitor. The three tools collaborate to
implement an efficient and rigorous validation methodology as discussed below.

  * •

The Simulator executes a dynamic ADS model obtained as the composition of two
entities: 1) a model of the world represented by maps and the distribution of
the objects with their kinematic attributes; 2) behavioral models of objects
and their possible interactions. Following the execution principle presented
in 3.2, the Simulator exhibits cyclic behavior alternating between concurrent
actions of the objects for a lapse of time and computation of the resulting
state of the world. We assume that the Simulator exports to the other tools
implementations of basic predicates, variables and actions via an interface
e.g., in the form of an API. The rigorous definition of the interface should
rely on a semantic model of the simulated system with well-defined concept of
state and execution step, as described in Section 3.2.

  * •

The Scenario Execution Engine drives the simulation process by executing
dynamic scenarios and providing sequences of actions executed by vehicles in
the Simulator. Scenarios are chosen following an adaptive test strategy [7].
The purpose is to lead the simulated system to specific configurations e.g. to
explore corner cases and high-risk situations or to meet specific coverage
criteria as discussed below.

  * •

The Monitor continuously receives relevant state changes of the global system
behavior and applies run-time verification techniques checking online that the
ADS runs satisfy a given set of specifications including traffic rules and
specific properties. Furthermore, the Monitor provides diagnostics and KPIs
used by the Scenario Execution Engine in its test strategy.

SCENARIOEXEC.
ENGINESIMULATORstateSemanticModelaction$o_{1}$$o_{n}$$o_{2}$behaviorobjectworldmodelmapsobjectstest
strategiesparametric scenariostraffic rulesSpecificationsMONITORspecific
properties-verdicts-diagnostics-coverage-KPIsscenarioapplicationruns
(sequences of ADS states)resultsSpecificationand ScenarioDescriptionLanguage

Figure 11:  Architecture of Validation Environment

Note that in the proposed architecture, scenarios should be consistent with
the behavior of the objects specified in the Simulator and the execution
context. For instance, if a scenario requires that a vehicle accelerate, this
should be compatible with its collision avoidance policy (if there is any).
Furthermore, if the scenario enforces a left turn for a vehicle this should be
possible in the current execution context. Many works focus on testing a
particular “ego” vehicle with respect to the collective behavior other mobile
objects specified by scenarios. Hence, while the behavior of the tested ego
vehicle is integrated in the Simulator, the (often-rudimentary) behavior of
the other objects may ignore the particular execution context possibly leading
to inconsistency.

The described architecture is an adaptive testing environment. Using common
terminology, the Simulator corresponds to a _Unit Under Test_ , the Monitor is
an _Oracle_ and the Scenario Execution Engine plays the role of a _Test Case
Generator_ [16]. To what extent is it possible to extend to ADS conventional
testing techniques? The application of a test strategy should aim at
optimizing criteria such as coverage and KPI’s. If for software systems
coverage can be defined as the ratio of source code exercised when we run test
sequences, it is not clear how a similar criterion could be defined for ADS
models.

To reduce the complexity of the space of situations to be explored by test
strategies, we need structuring criteria for scenarios. One way for achieving
this aim is to define an equivalence relation on scenes and by extension on
scenarios preserving correctness for the considered specifications. This idea
that is also adopted by metamorphic testing [31], may allow a drastic
reduction of the test cases to be considered. Executions driven by equivalent
scenarios should be indistinguishable by the Monitor. Furthermore, testing one
scenario per class could provide coverage for all its scenarios.

The efficiency of exploration can be further improved if the equivalence is
defined by symmetrizing a risk pre-order on scenes and by extension on
scenarios. Intuitively, given a scene $sc$ and a set of traffic rules $TR$ we
can compute the set of active rules for $sc$, i.e., the subset of rules of
$TR$ that are applicable to $sc$. We can consider the number of active rules
for a scene $sc$ as a factor of potential risk. Then for the same map context
and the same car distribution over roads and junction segments, a scene $sc$
is deemed more risky than another $sc^{\prime}$ if the set of active rules of
$sc$ contains the set of active rules of $sc^{\prime}$.

This idea can be further refined taking the approach applied in [11, 12] for
the analysis of dynamic reconfigurable systems. Given a set $TR$ of traffic
rules, we can model the risk of a scene $sc$ as a labeled hypergraph whose
vertices are its objects with their state attributes and the hyper-edges are
traffic rules. In this hypergraph, each object $o$ of $sc$ is connected to all
the traffic rules of $TR$ that are applicable to $o$. The degree of $o$
measures somehow the risk induced by interactions with other objects from the
application of the rules of $TR$. The risk hypergraph thus constructed for a
given scene $sc$, can provide a basis for the evaluation of the risk involved
in $sc$ as a function of its complexity and other state attributes. We can
define a preorder relation on risk hypergraphs such that if a hypergraph $hg$
contains another hypergraph $hg^{\prime}$ and all the kinematic attributes
agree, then the risk involved in the scene of $hg$ is higher.

Clearly, any risk hypergraph that is the union of disjoint hypergraphs can be
decomposed into hypergraphs that can be evaluated independently. This often
happens because of the locality of the traffic rules; a rule is applicable to
a set of objects that are geographically close in a certain map context.

Hence, a test strategy could be progressive following the three steps:

  1. (i)

Consider scenarios involving scenes arising in simple traffic patterns such as
junctions and road types. Such scenarios could generate sequences of scenes
for roundabout, intersection, merger, overtaking etc.

  2. (ii)

For a given traffic pattern, guide the simulation to produce higher-risk
scenes e.g. by creating scenes with increasing number of active traffic rules.

  3. (iii)

Embed the tested simple high-risk traffic patterns in a map and progressively
apply scenarios leading to new higher-risk scenes.

##  5 Discussion

The proposed framework relies on a minimal set of semantically integrated
concepts. It is expressive and modular as it introduces progressively the
basic concepts and carefully separates concerns. It supports a well-defined
specification and validation methodology without semantic gaps. Using
configuration logic allows the specification of behavioral properties taking
into account map contexts. This is a main difference from approaches relying
on temporal logics that cannot account for map configurations and where
formulas characterize sets of runs in some implicit map environment, usually a
simple multi-lane setting. Configuration logic specifies scenes as
conjunctions of formulas describing map configurations and vehicle
distributions linked by an addressing relation. It enables enhanced
expressiveness by combining static and dynamic aspects while retaining the
possibility to consider them separately. It considers maps as the central
concept of the semantic model and emphasizes the needs for multilevel
representation depending on the type of goals to be met including long-term
mission goals, mid-term maneuver goals and short-term safety and trajectory
tracking goals. Among the three abstraction levels, curve segment models play
a central role. Interval segment models can account for simple properties
depending only on relative distances between the involved mobiles. For
properties depending on topological and geometric relations, curve segment
models are needed. The expression of such properties involves primitives such
as go-straight, turn-right, turn-left, right-of and opposite. Region segment
models are needed for low level properties taking into account the dimensions
of the objects and their movement in the 2D space.

The paper is the culmination of work developed over the past three years both
on foundations of autonomous systems [18, 28] and on modelling and validation
of reconfigurable dynamic systems using the DR-BIP component framework [5,
12]. We plan to extend this work in two directions. The first is to leverage
on the DR-BIP execution semantics and formalize ADS dynamics as the
composition of object behavior acting on maps. The second is to extend our
work on runtime verification of dynamic reconfigurable systems [12] by
developing adaptive validation techniques driven by adequate model coverage
criteria. These techniques should provide model-based evidence that a good
deal of the many and diverse driving situations are covered (e.g. different
types of roads, of junctions, of traffic conditions, etc). Finally, we will
investigate diagnostics generation techniques linking failures to their causes
emerging from risk factors such as violations of traffic regulations and
unpredictable events.

## References

  * [1] OpenDRIVE® Format Specification. Tech. Rep. V 1.4 ©2006-2015, VIRES Simulationstechnologie GmbH (2015), retrieved from https://www.asam.net/standards/detail/opendrive
  * [2] ASAM OpenDRIVE® - Open Dynamic Road Information for Vehicle Environment. Tech. Rep. V 1.6.0, ASAM e.V. (Mar 2020), retrieved from https://www.asam.net/standards/detail/opendrive
  * [3] ASAM OpenScenario® - Dynamic content in driving simulation, UML Modeling Rules. Tech. Rep. V 1.0.0, ASAM e.V. (Mar 2020), retrieved from https://www.asam.net/standards/detail/openscenario
  * [4] Bagschik, G., Menzel, T., Maurer, M.: Ontology based scene creation for the development of automated vehicles. In: 2018 IEEE Intelligent Vehicles Symposium, IV 2018, Changshu, Suzhou, China, June 26-30, 2018. pp. 1813–1820. IEEE (2018). https://doi.org/10.1109/IVS.2018.8500632, https://doi.org/10.1109/IVS.2018.8500632
  * [5] Ballouli, R.E., Bensalem, S., Bozga, M., Sifakis, J.: Four exercises in programming dynamic reconfigurable systems: Methodology and solution in DR-BIP. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11246, pp. 304–320. Springer (2018)
  * [6] Beetz, J., Borrmann, A.: Benefits and limitations of linked data approaches for road modeling and data exchange. In: Smith, I.F.C., Domer, B. (eds.) Advanced Computing Strategies for Engineering - 25th EG-ICE International Workshop 2018, Lausanne, Switzerland, June 10-13, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10864, pp. 245–261. Springer (2018). https://doi.org/10.1007/978-3-319-91638-5_13, https://doi.org/10.1007/978-3-319-91638-5_13
  * [7] Bloem, R., Fey, G., Greif, F., Könighofer, R., Pill, I., Riener, H., Röck, F.: Synthesizing adaptive test strategies from temporal logic specifications. Formal Methods Syst. Des. 55(2), 103–135 (2019)
  * [8] Chen, W., Kloul, L.: An ontology-based approach to generate the advanced driver assistance use cases of highway traffic. In: Aveiro, D., Dietz, J.L.G., Filipe, J. (eds.) Proceedings of the 10th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, IC3K 2018, Volume 2: KEOD, Seville, Spain, September 18-20, 2018. pp. 73–81. SciTePress (2018). https://doi.org/10.5220/0006931700730081, https://doi.org/10.5220/0006931700730081
  * [9] Damm, W., Kemper, S., Möhlmann, E., Peikenkamp, T., Rakow, A.: Using traffic sequence charts for the development of HAVs. In: ERTS 2018, Toulouse, France, Jan 2018, Proceedings (2018)
  * [10] Dosovitskiy, A., Ros, G., Codevilla, F., López, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: 1st Annual Conference on Robot Learning, CoRL 2017, Mountain View, California, USA, November 13-15, 2017, Proceedings. Proceedings of Machine Learning Research, vol. 78, pp. 1–16. PMLR (2017)
  * [11] El-Hokayem, A., Bensalem, S., Bozga, M., Sifakis, J.: A layered implementation of DR-BIP supporting run-time monitoring and analysis. In: de Boer, F.S., Cerone, A. (eds.) Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14-18, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12310, pp. 284–302. Springer (2020)
  * [12] El-Hokayem, A., Bozga, M., Sifakis, J.: A temporal configuration logic for dynamic reconfigurable systems. In: Hung, C., Hong, J., Bechini, A., Song, E. (eds.) SAC ’21: The 36th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, Republic of Korea, March 22-26, 2021. pp. 1419–1428. ACM (2021)
  * [13] Esterle, K., Aravantinos, V., Knoll, A.C.: From specifications to behavior: Maneuver verification in a semantic state space. In: 2019 IEEE Intelligent Vehicles Symposium, IV 2019, Paris, France, June 9-12, 2019. pp. 2140–2147. IEEE (2019). https://doi.org/10.1109/IVS.2019.8814241, https://doi.org/10.1109/IVS.2019.8814241
  * [14] Esterle, K., Gressenbuch, L., Knoll, A.C.: Formalizing traffic rules for machine interpretability. In: 3rd IEEE Connected and Automated Vehicles Symposium, CAVS 2020, Victoria, BC, Canada, November 18 - December 16, 2020\. pp. 1–7. IEEE (2020). https://doi.org/10.1109/CAVS51000.2020.9334599, https://doi.org/10.1109/CAVS51000.2020.9334599
  * [15] Fremont, D.J., Kim, E., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: A language for scenario specification and data generation. CoRR abs/2010.06580 (2020), https://arxiv.org/abs/2010.06580
  * [16] Fremont, D.J., Kim, E., Pant, Y.V., Seshia, S.A., Acharya, A., Bruso, X., Wells, P., Lemke, S., Lu, Q., Mehta, S.: Formal scenario-based testing of autonomous vehicles: From simulation to the real world. In: 23rd IEEE International Conference on Intelligent Transportation Systems, ITSC 2020, Rhodes, Greece, September 20-23, 2020. pp. 1–8. IEEE (2020). https://doi.org/10.1109/ITSC45102.2020.9294368, https://doi.org/10.1109/ITSC45102.2020.9294368
  * [17] Fremont, D.J., Yue, X., Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: Language-based scene generation. CoRR abs/1809.09310 (2018), http://arxiv.org/abs/1809.09310
  * [18] Harel, D., Marron, A., Sifakis, J.: Autonomics: In search of a foundation for next-generation autonomous systems. Proc. Natl. Acad. Sci. USA 117(30), 17491–17498 (2020)
  * [19] Hilscher, M., Linker, S., Olderog, E., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6991, pp. 404–419. Springer (2011). https://doi.org/10.1007/978-3-642-24559-6_28, https://doi.org/10.1007/978-3-642-24559-6_28
  * [20] Institute for Software Engineering and Programming Languages, University of Lübeck: LamaConv - Logics and Automata Converter Library (2020), https://www.isp.uni-luebeck.de/lamaconv
  * [21] Karimi, A., Duggirala, P.S.: Formalizing traffic rules for uncontrolled intersections. In: 11th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2020, Sydney, Australia, April 21-25, 2020. pp. 41–50. IEEE (2020). https://doi.org/10.1109/ICCPS48487.2020.00012, https://doi.org/10.1109/ICCPS48487.2020.00012
  * [22] Poggenhans, F., Pauls, J., Janosovits, J., Orf, S., Naumann, M., Kuhnt, F., Mayr, M.: Lanelet2: A high-definition map framework for the future of automated driving. In: Zhang, W., Bayen, A.M., Medina, J.J.S., Barth, M.J. (eds.) 21st International Conference on Intelligent Transportation Systems, ITSC 2018, Maui, HI, USA, November 4-7, 2018. pp. 1672–1679. IEEE (2018). https://doi.org/10.1109/ITSC.2018.8569929, https://doi.org/10.1109/ITSC.2018.8569929
  * [23] Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015, Gran Canaria, Spain, September 15-18, 2015\. pp. 1658–1665. IEEE (2015). https://doi.org/10.1109/ITSC.2015.269, https://doi.org/10.1109/ITSC.2015.269
  * [24] Rizaldi, A., Immler, F., Schürmann, B., Althoff, M.: A formally verified motion planner for autonomous vehicles. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 75–90. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4_5, https://doi.org/10.1007/978-3-030-01090-4_5
  * [25] Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E., Nipkow, T.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. In: Polikarpova, N., Schneider, S.A. (eds.) Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10510, pp. 50–66. Springer (2017). https://doi.org/10.1007/978-3-319-66845-1_4, https://doi.org/10.1007/978-3-319-66845-1_4
  * [26] Rong, G., Shin, B.H., Tabatabaee, H., Lu, Q., Lemke, S., Mozeiko, M., Boise, E., Uhm, G., Gerow, M., Mehta, S., Agafonov, E., Kim, T.H., Sterner, E., Ushiroda, K., Reyes, M., Zelenkovsky, D., Kim, S.: LGSVL simulator: A high fidelity simulator for autonomous driving. CoRR abs/2005.03778 (2020), https://arxiv.org/abs/2005.03778
  * [27] Schönemann, V., Winner, H., Glock, T., Otten, S., Sax, E., Boeddeker, B., Verhaeg, G., Tronci, F., Padilla, G.G.: Scenario-based functional safety for automated driving on the example of valet parking. In: Arai, K., Kapoor, S., Bhatia, R. (eds.) Advances in Information and Communication Networks. pp. 53–64. Springer International Publishing, Cham (2019)
  * [28] Sifakis, J.: Autonomous systems - an architectural characterization. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, vol. 11665, pp. 388–410. Springer (2019)
  * [29] Wikipedia: https://en.wikipedia.org/wiki/All-way_stop
  * [30] WS Dept. of Transportation: https://wsdot.wa.gov/Safety/roundabouts
  * [31] Zhou, Z.Q., Sun, L.: Metamorphic testing of driverless cars. Commun. ACM 62(3), 61–67 (2019)

##  Appendix 0.A $\mathit{MCL}$ Satisfiability: Translation Rules

$\mbox{\bf eq-pos}(n,E,\mu,p,p^{\prime})\stackrel{{\scriptstyle def}}{{=}}$

$\left\\{\begin{array}[]{ll}\mbox{\it true}&\mbox{if
}p=x,~{}p^{\prime}=x^{\prime},\mu x=\mu x^{\prime}\\\\[5.0pt] \lx@intercol
s=s^{\prime}\wedge t=t^{\prime}\wedge 0<t<{|\\!|s|\\!|}\wedge\mbox{\bf
unique}(s,S)\hfil\lx@intercol\\\ &\mbox{if
}p=(x,s,t),~{}p^{\prime}=(x^{\prime},s^{\prime},t^{\prime}),~{}\mu x=\mu
x^{\prime},\\\ &~{}~{}~{}S=\\{s_{ijh}~{}|~{}(i,s_{ijh},j)\in E,~{}\mu
x=i\\}\\\\[5.0pt] \lx@intercol s=s^{\prime}\wedge t=t^{\prime}\wedge
0<t<{|\\!|s|\\!|}\wedge\mbox{\bf unique}(s,S)\hfil\lx@intercol\\\ &\mbox{if
}p=(t,s,x),~{}p^{\prime}=(t^{\prime},s^{\prime},x^{\prime}),~{}\mu x=\mu
x^{\prime},\\\ &~{}~{}~{}S=\\{s_{ijh}~{}|~{}(i,s_{ijh},j)\in E,~{}\mu
x=j\\}\\\\[5.0pt] \lx@intercol s=s^{\prime}\wedge
t+t^{\prime}={|\\!|s|\\!|}\wedge 0<t<{|\\!|s|\\!|}\wedge\mbox{\bf
unique}(s,S)\wedge\mbox{\bf unique}(s^{\prime},S^{\prime})\hfil\lx@intercol\\\
&\mbox{if }p=(x,s,t),~{}p^{\prime}=(t^{\prime},s^{\prime},x^{\prime}),\\\
&~{}~{}~{}S=\\{s_{ijh}~{}|~{}(i,s_{ijh},j)\in E,~{}\mu x=i\\}\\\
&~{}~{}~{}S^{\prime}=\\{s_{ijh}~{}|~{}(i,s_{ijh},j)\in E,~{}\mu
x^{\prime}=j\\}\\\ &\mbox{/* and the symmetric case */}\\\\[5.0pt] \mbox{\it
false}&\mbox{otherwise}\end{array}\right.$

Remark: in the above, $S$, $S^{\prime}$ are multisets.

Remark: $x$ denotes a vertex position, $(x,s,t)$, $(t,s,x)$ denotes edge
positions as $t$ must be strictly between 0 and ${|\\!|s|\\!|}$

$\mbox{\bf unique}(s,\\{s_{1},...,s_{m}\\})\stackrel{{\scriptstyle
def}}{{=}}(\vee_{h=1}^{m}s=s_{h})\wedge(\neg\vee_{1\leq h<h^{\prime}\leq
m}s=s_{h}\wedge s=s_{h^{\prime}})$

$\mbox{\bf acyclic-path}(n,E,\mu,p,s,p^{\prime})\stackrel{{\scriptstyle
def}}{{=}}$

$\begin{array}[]{l}\exists k.\exists k^{\prime}.\exists z.\exists
z^{\prime}.\\\ \bigvee_{e=(i,s_{ijh},j)\in E}\mbox{\bf at-
pos}(n,E,\mu,p,e,k)\wedge\mbox{\bf at-
pos}(n,E,\mu,p^{\prime},e,k^{\prime})~{}\wedge\\\ \hskip 14.22636pt(0\leq
k\leq k^{\prime}\leq{|\\!|s_{ijh}|\\!|}\wedge\mbox{\bf
subseg}(s_{ijh},k,k^{\prime},z)\wedge s=z)~{}\vee\\\\[5.0pt]
\bigvee_{e=(i,s_{ijh},j)\in E}\mbox{\bf at-pos}(n,E,\mu,p,e,k)\wedge\mbox{\bf
at-pos}(n,E,\mu,p^{\prime},e,k^{\prime})~{}\wedge\\\ \hskip
14.22636pt\big{(}0\leq k^{\prime}\leq k\leq{|\\!|s_{ijh}|\\!|}\wedge\mbox{\bf
subseg}(s_{ijh},k,{|\\!|s_{ijh}|\\!|},z)\wedge\mbox{\bf
subseg}(s_{ijh},0,k^{\prime},z^{\prime})~{}\wedge\\\ \hskip
28.45274pt((j=i\wedge s=z\cdot z^{\prime})~{}\vee\\\ \hskip
28.45274pt(\bigvee_{w\in(E\setminus{e})^{+}_{ac}}~{}^{\bullet}\\!{w}=j\wedge{w}^{\bullet}=i\wedge
s=z\cdot{w}.s\cdot z^{\prime}))\big{)}\\\\[5.0pt] \bigvee_{e=(i,s_{ijh},j)\in
E}\bigvee_{e^{\prime}=(i^{\prime},s_{i^{\prime}j^{\prime}h^{\prime}},j^{\prime})\in
E\setminus{e}}\mbox{\bf at-pos}(n,E,\mu,p,e,k)\wedge\mbox{\bf at-
pos}(n,E,\mu,p^{\prime},e^{\prime},k^{\prime})~{}\wedge\\\ \hskip
14.22636pt\big{(}0\leq k\leq{|\\!|s_{ijh}|\\!|}\wedge 0\leq
k^{\prime}\leq{|\\!|s_{i^{\prime}j^{\prime}h^{\prime}}|\\!|}\wedge\mbox{\bf
subseg}(s_{ijh},k,{|\\!|s_{ijh}|\\!|},z)\wedge\mbox{\bf
subseg}(s_{i^{\prime}j^{\prime}h^{\prime}},0,k^{\prime},z)~{}\wedge\\\ \hskip
28.45274pt((j=i^{\prime}\wedge s=z\cdot z^{\prime})~{}\vee\\\ \hskip
28.45274pt(\bigvee_{w\in(E\setminus(e,e^{\prime}))^{+}_{ac}}~{}^{\bullet}\\!{w}=j\wedge{w}^{\bullet}=i^{\prime}\wedge
s=z\cdot{w}.s\cdot z^{\prime}))\big{)}\end{array}$

$\mbox{\bf at-pos}(n,E,\mu,p,(i,s_{ijh},j),k)\stackrel{{\scriptstyle
def}}{{=}}$

$\mbox{\bf eq-pos}(n,E,\mu,p,p)\wedge\left\\{\begin{array}[]{ll}k=0&\mbox{if
}p=x,~{}\mu x=i\\\\[5.0pt] k={|\\!|s_{ijh}|\\!|}&\mbox{if }p=x,~{}\mu
x=j\\\\[5.0pt] s=s_{ijh}\wedge k=t&\mbox{if }p=(x,s,t),~{}\mu x=i\\\\[5.0pt]
s=s_{ijh}\wedge k+t={|\\!|s_{ijh}|\\!|}&\mbox{if }p=(t,s,x),~{}\mu
x=j\\\\[5.0pt] \mbox{\it false}&\mbox{otherwise}\end{array}\right.$

$\mbox{\bf subseg}(s,t_{1},t_{2},s^{\prime})\stackrel{{\scriptstyle
def}}{{=}}$

$0\leq t_{1}\leq t_{2}\leq{|\\!|s|\\!|}\wedge\exists z_{1}.~{}\exists
z_{2}.~{}{|\\!|z_{1}|\\!|}=t_{1}\wedge{|\\!|z_{2}|\\!|}+t_{2}={|\\!|s|\\!|}\wedge
s=z_{1}\cdot s^{\prime}\cdot z_{2}$