11institutetext: Univ. Grenoble Alpes, CNRS, Grenoble INP111Institute of
Engineering Univ. Grenoble Alpes, VERIMAG, 38000 Grenoble, France 11email:
<EMAIL_ADDRESS>
http://www-verimag.imag.fr/

# Correct by Design Coordination of Autonomous Driving Systems

Marius Bozga  0000-0003-4412-5684 Joseph Sifakis  0000-0003-2447-7981

###### Abstract

The paper proposes a method for the correct by design coordination of
autonomous driving systems (_ADS_). It builds on previous results on collision
avoidance policies and the modeling of _ADS_ by combining descriptions of
their static environment in the form of maps, and the dynamic behavior of
their vehicles.

An _ADS_ is modeled as a dynamic system involving a set of vehicles
coordinated by a _Runtime_ that based on vehicle positions on a map and their
kinetic attributes, computes free spaces for each vehicle. Vehicles are
bounded to move within the corresponding allocated free spaces.

We provide a correct by design safe control policy for an _ADS_ if its
vehicles and the _Runtime_ respect corresponding assume-guarantee contracts.
The result is established by showing that the composition of assume-guarantee
contracts is an inductive invariant that entails _ADS_ safety.

We show that it is practically possible to define speed control policies for
vehicles that comply with their contracts. Furthermore, we show that traffic
rules can be specified in a linear-time temporal logic, as a class of formulas
that constrain vehicle speeds. The main result is that, given a set of traffic
rules, it is possible to derive free space policies of the _Runtime_ such that
the resulting system behavior is safe by design with respect to the rules.

###### Keywords:

Autonomous driving systems Traffic rule specification Map specification
Collision avoidance policy Assume-guarantee contract Correctness by design.

##  1 Introduction

Autonomous driving systems (_ADS_) are probably the most difficult systems to
design and validate, because the behavior of their agents is subject to
temporal and spatial dynamism. They are real-time distributed systems
involving components with partial knowledge of their environment, pursuing
specific goals while the collective behavior must meet given global goals.

Development of trustworthy _ADS_ is an urgent and critical need. It poses
challenges that go well beyond the current state of the art due to their
overwhelming complexity. These challenges include, on the one hand, modeling
the system and specifying its properties, usually expressed as traffic rules;
on the other hand, building the system and verifying its correctness with
respect to the desired system properties.

Modeling involves a variety of issues related to the inherent temporal and
spatial dynamics as well as to the need for an accurate representation of the
physical environment in which vehicles operate. Much work focuses on
formalizing and standardizing a concept of map that is central to semantic
awareness and decision-making. Maps should be semantically rich, i.e., their
structure should provide all relevant semantic information such as road type,
junction type, signaling information, etc. Given their importance for the
modeling _ADS_ , maps have been the subject of many studies focused on their
compositional description and formalization. These studies often use
ontologies and logics with associated reasoning mechanisms to check the
consistency of descriptions and their accuracy with respect to desired
properties [4, 3]. Other works propose open source mapping frameworks for
highly automated driving [1, 2, 16]. Finally, the SOCA method [7] proposes an
abstraction of maps called zone graph, and uses this abstraction in a
morphological behavior analysis.

There is an extensive literature on _ADS_ validation that involves two
interrelated problems: the specification of system properties and the
application of validation techniques. The specification of properties requires
first-order temporal logics because parameterization and genericity are
essential for the description of situations involving a varying number of
vehicles and types of traffic patterns. The work in [19, 17] formalizes a set
of traffic rules for highway scenarios in Isabelle/HOL. It shows that traffic
rules can be used as requirements to be met by autonomous vehicles and
proposes a verification procedure. A formalization of traffic rules for
uncontrolled intersections is provided in [12], which shows how the rules can
be used by a simulator to safely control traffic at intersections. The work in
[10] proposes a methodology for formalizing traffic rules in linear temporal
logic; it shows how the evaluation of formalized rules on recorded human
behaviors provides insight into how well drivers follow the rules.

Many works deal with the formal verification of controllers that perform
specific maneuvers. For example, in [11], a dedicated multi-way spatial logic
inspired by interval temporal logic is used to specify safety and provide
proofs for lane change controllers. The work in [18] presents a formally
verified motion planner in Isabelle/HOL. The planner uses maneuver automata, a
variant of hybrid automata, and linear temporal logic to express properties.
In [10], runtime verification is applied to check that the maneuvers of a
high-level planner conform to traffic rules expressed in linear temporal
logic.

Of particular interest for this work are correct by construction techniques
where system construction is guided by a set of properties that the system is
guaranteed to satisfy. They involve either the application of monolithic
synthesis techniques or compositional reasoning throughout a component-based
system design process. There is considerable work on controller synthesis from
a set of system properties usually expressed in linear temporal logic, see for
example [13, 27, 28, 21, 26]. These are algorithmic techniques extensively
studied in the field of control. They consist of restricting the controllable
behavior of a system interacting with its environment so that a set of
properties are satisfied. Nonetheless, their application is limited due to
their high computational cost, which depends in particular on the type of
properties and the complexity of the system behavior.

An alternative to synthesis is to achieve correctness by design as a result of
composing the properties of the system components. Component properties are
usually "assume-guarantee" contracts characterizing a causal relationship
between a component and its environment: if the environment satisfies the
"assume" part of the contract, the state of the component will satisfy the
"guarantee" part, e.g. [5, 15, 8]. The use of contracts in system design
involves a decomposition of overall system requirements into contracts that
provide a basis for more efficient analysis and validation. In addition,
contract-based design is advocated as a method for achieving correctness by
design, provided that satisfactory implementations of the system can be found
[23]. There are a number of theoretical frameworks that apply mainly to
continuous or synchronous systems, especially for analysis and verification
purposes [22, 14, 20]. They suffer computational limitations because, in the
general case, they involve the symbolic solution of fixed-point equations,
which restricts the expressiveness of the contracts [14]. Furthermore, they
are only applicable to systems with a static architecture, which excludes
dynamic reconfigurable systems, such as autonomous systems.

The paper builds on previous results [6] on a logical framework for parametric
specification of _ADS_ combining models of the system’s static environment in
the form of maps, and the dynamic properties of its vehicles. Maps are metric
graphs whose vertices represent locations and edges are labeled with segments
that can represent roads at different levels of abstraction, with
characteristics such as length or geometric features characterizing their
shape and size.

An _ADS_ model is a dynamic system consisting of a map and a set of vehicles
moving along specific routes. Its state can be conceived as the distribution
of vehicles on a map with their positions, speeds and other kinematic
attributes. For its movement, each vehicle has a safe estimate of the free
space in its neighborhood, according to predefined visibility rules. We assume
that vehicle coordination is performed by a _Runtime_ that, for given vehicle
positions and speeds on the map, can compute the free spaces on each vehicle’s
itinerary in which it can safely move.

We consider without loss of generality, _ADS_ with a discretized execution
time step $\Delta t$. Knowing its free space, each vehicle can move by
adapting its speed in order to stay in this space, braking if necessary in
case of emergency. At the end of each cycle, taking into account the movements
of the vehicles, the _Runtime_ updates their positions on the map. The cycle
iterates by calculating the free spaces from the new state.

We study a safe control policy for _ADS_ , which is correct by design. It
results from the combination of two types of assume-guarantee contracts: one
contract for each vehicle and another contract for the _Runtime_ taking into
account the positions of the vehicles on the map.

The contract for a vehicle states that, assuming that initially the dynamics
of the vehicle allow it to stay in the allocated free space, it will stay in
this free space. Note that the details of the contract implementation are
irrelevant; only the I/O relationship between free space and vehicle speed
matters. The _Runtime_ assume-guarantee contract asserts that if the free
spaces allocated to vehicles at the beginning of a cycle are disjoint, then
they can be allocated new disjoint free spaces provided they have fulfilled
their contract. The combination of these two contracts leads to a control
policy that satisfies an inductive invariant, implying system safety.

We build on this general result by specializing its application in two
directions. First, we show that it is possible to define speed policies for
vehicles that satisfy their assume-guarantee contract. Second, we show that it
is possible to define free space policies for the _Runtime_ enforcing safety
constraints of a given set of traffic rules. We formalize traffic rules as a
class of properties of a linear temporal logic. Each rule applicable to a
vehicle $c$, is an implication whose conclusion involves two types of
constraints on the speed of $c$: speed regulation and speed limitation
constraints. We provide a method that derives from a given set of traffic
rules, constraints on the free spaces chosen by the _Runtime_ such that the
resulting system behavior is safe with respect to these rules. This is the
main result of the paper establishing correctness by design of general _ADS_ ,
provided that their components comply with their respective contracts.

The paper is structured as follows. In Section 2, we establish the general
framework by introducing the basic models and concepts for the representation
of maps. In Section 3, we introduce the dynamic model of _ADS_ involving a set
of vehicles and a _Runtime_ for their coordination. We show how a correct by
design safe control policy is obtained by combining assume-guarantee contracts
for the vehicles and the _Runtime_. In Section 4, we study the principle of
speed policies respecting the vehicle contract and show its application
through an example. In Section 5, we formalize traffic rules as a class of
formulas of a linear temporal logic and show how it is possible to generate
from a set of traffic rules free space policies such that the system is safe
by design. In Section 6, we briefly describe the implementation of the
approach and experiments underway. Section 7 concludes with a discussion of
the significance of the results, future developments and applications.

##  2 Map Representation

Following the idea presented in [6], 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\\}$, a length norm
$|\\!|.|\\!|:{\cal S}\rightarrow\mathbb{R}_{\geq 0}$ and a partial subsegment
extraction operator ${.}{[.,.]}:{\cal S}\times\mathbb{R}_{\geq
0}\times\mathbb{R}_{\geq 0}\rightarrow{\cal S}\cup\\{\bot\\}$. Thus, given a
segment $s$, $|\\!|s|\\!|$ represents its length and ${s}{[a,b]}$ for $0\leq
a<b\leq|\\!|s|\\!|$, represents the sub-segment starting at length $a$ from
its origin and ending at length $b$. Segments can be used to represent roads
at different levels of abstraction, from intervals to regions. As an example,
we consider ${\cal S}$ as the set of curves obtained by concatenation of
parametric line segments and circle arcs. More precisely, 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\mathit{def}}}{{=}}&(at\cos\varphi,at\sin\varphi)~{}~{}\forall
t\in[0,1]\\\
arc[r,\varphi,\theta](t)&\stackrel{{\scriptstyle\mathit{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
curves of this parametric form.

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

Figure 1: Curve segments and their composition

We use metric graphs $G\stackrel{{\scriptstyle\mathit{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 (denoted ${\cal
S}^{\star}$). For an edge $e=(v,s,v^{\prime})\in E$ we denote
${{}^{\bullet}\\!{e}}\stackrel{{\scriptstyle\mathit{def}}}{{=}}v$,
${{e}^{\bullet}}\stackrel{{\scriptstyle\mathit{def}}}{{=}}v^{\prime}$,
${e}.s\stackrel{{\scriptstyle\mathit{def}}}{{=}}s$. For a vertex $v$, we
define
${{}^{\bullet}\\!{v}}\stackrel{{\scriptstyle\mathit{def}}}{{=}}\\{e~{}|~{}{{e}^{\bullet}}=v\\}$
and
${{v}^{\bullet}}\stackrel{{\scriptstyle\mathit{def}}}{{=}}\\{e~{}|~{}{{}^{\bullet}\\!{e}}=v\\}$.
We call a metric graph _connected_ (resp. _weakly connected_) if a path (resp.
an undirected path) exists between any pair of vertices.

We consider the set
$\mathit{Pos}_{G}\stackrel{{\scriptstyle\mathit{def}}}{{=}}V\cup\\{(e,a)~{}|~{}e\in
E,~{}0\leq a\leq|\\!|{e}.s|\\!|\\}$ of _positions_ defined by a metric graph.
Note that positions $(e,0)$ and $(e,|\\!|{e}.s|\\!|)$ are considered equal
respectively to positions ${{}^{\bullet}\\!{e}}$ and ${{e}^{\bullet}}$. We
denote by ${p}\xrightarrow{{s}}_{G}{p^{\prime}}$ the existence of an
$s$-labelled _edge ride_ between succeeding positions $p=(e,a)$ and
$p^{\prime}=(e,a^{\prime})$ in the same edge $e$ whenever $0\leq
a<a^{\prime}\leq|\\!|{e}.s|\\!|$ and $s={{e}.s}{[a,a^{\prime}]}$. Moreover, we
denote by ${p}\stackrel{{\scriptstyle s}}{{\rightsquigarrow}}_{G}{p^{\prime}}$
the existence of an $s$-labelled _ride_ between arbitrary positions $p$,
$p^{\prime}$, that is,
${}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}_{G}{}\stackrel{{\scriptstyle\mathit{def}}}{{=}}({}\xrightarrow{{}}_{G}{})^{+}$
the transitive closure of edge rides. Finally, we define the distance $d_{G}$
from position $p$ to position $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. Whenever $G$ is fixed in the
context, we will omit the subscript $G$ for positions $\mathit{Pos}_{G}$,
distance $d_{G}$, and rides ${}\xrightarrow{{}}_{G}{}$ or
${}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}_{G}{}$.

A connected metric graph $G=(V,{\cal S},E)$ can be interpreted as a map,
structured into roads and junctions, subject to additional assumptions:

  * •

we restrict to metric graphs which are 2D-consistent [6], meaning intuitively
they can be drawn in the 2D-plane such that the geometric properties of the
segments are compatible with the topological properties of the graph. In
particular, if two distinct paths starting from the same vertex $v$, meet at
another vertex $v^{\prime}$, the coordinates of $v^{\prime}$ calculated from
each path are identical. For the sake of simplicity, we further restrict to
graphs where distinct vertices are located at distinct points in the plane,
and moreover, where no edge is self-crossing (meaning actually that distinct
positions $(e,a)$ of the same edge $e$ are located at distinct points).

  * •

the map is equipped with a symmetric junction relationship $\crossing$ on
edges $E$ which abstracts the geometric crossing (or the proximity) between
edges at positions other than the edge end points. This relationship is used
to define the _junctions_ of the map, that is, as any non-trivial equivalence
class in the transitive closure of $\crossing$. Actually, junctions need
additional signalisation to regulate the traffic on their edges (e.g., traffic
lights, stop signs, etc). In addition, we assume a partial ordering
$\prec_{j}$ on the set of vertices to reflect their static priorities as
junction entries.

  * •

to resolve conflicts at merger vertices, i.e., vertices with two or more
incident segments which do not belong to a junction, we assume that the map is
equipped with a static priority relationship. Specifically, for a vertex $v$,
there is a total priority order $\prec_{v}$ on the set of edges
${{}^{\bullet}\\!{v}}$. This order reflects an abstraction of the static
priority rules associated with each of the merging edges (e.g., right-of-way,
yield-priority, etc).

  * •

every edge $e$ is associated with a maximal speed limit
$e.\mathit{v}\in\mathbb{R}_{\geq 0}$.

\begin{picture}(4293.0,1843.0)(-233.0,-1873.0)\end{picture}

Figure 2: A map with junctions (blue edges) and a merger vertices (red edges)

In the remainder of the paper, we consider a fixed metric graph $G=(V,{\cal
S},E)$ altogether with the junction relationship $\crossing$, static
priorities $\prec_{v}$ and edge speed limits as discussed above. Also, we
extend the junction and priority relationships from edges to their associated
positions, that is, consider
$(e_{1},a_{1})\sim(e_{2},a_{2})\stackrel{{\scriptstyle\mathit{def}}}{{=}}e_{1}\sim
e_{2}$ for any relation $\sim\in\\{\crossing,(\prec_{v})_{v\in V}\\}$.
Finally, we denote by $r_{1}\uplus r_{2}$ the property that rides $r_{1}$,
$r_{2}$ in $G$ are _non-crossing_ , that is, their sets of positions are
disjoint and moreover not belonging to the same junction(s), except for
endpoints.

##  3 The _ADS_ Dynamic Model

###  3.1 General _ADS_ Architecture

Given a metric graph $G$ representing a map, the state of an _ADS_ is a tuple
$\langle st_{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 fixed equipment such as lights, road signs, gates, etc. For a vehicle $c$,
its state $st_{c}\stackrel{{\scriptstyle\mathit{def}}}{{=}}\langle
c.\mathit{p},c.\mathit{\delta},c.\mathit{v},c.\mathit{wt},c.\mathit{it}\dots\rangle$
includes respectively its _position_ on the map (from $\mathit{Pos}$), its
_displacement_ traveled since $c.\mathit{p}$ (from $\mathbb{R}_{\geq 0}$), 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, its _itinerary_ (from the set of segments ${\cal S}$) which labels a
ride starting at $c.\mathit{p}$, etc. For a traffic light $lt$, its state
$st_{lt}\stackrel{{\scriptstyle\mathit{def}}}{{=}}\langle\mathit{lt.\mathit{p},lt.\mathit{cl},\dots}\rangle$
includes respectively its position on the map (from $\mathit{Pos}$), and its
_color_ (with values _red_ and _green_), etc.

The general _ADS_ model is illustrated in Fig. 3 and consists of a set of
vehicle models ${\cal C}$ and a _Runtime_ that interact cyclically with period
$\Delta t$. The _Runtime_ calculates free space values for each vehicle $c$
which are lenghts $c.\mathit{f}$ of initial rides on their itineraries
$c.\mathit{it}$ whose positions are free of obstacles. In turn, the vehicles
adapt their speed to stay within the allocated free space. Specifically, the
interaction proceeds as follows:

  * •

each vehicle $c$ applies a _speed policy_ for period $\Delta t$ respecting its
free space $c.\mathit{f}$ received from the _Runtime_. During $\Delta t$, it
travels a distance $c.\mathit{\delta}^{\prime}$ to some new position
$c.\mathit{p}^{\prime}$, and at the end of the period its speed is
$c.\mathit{v}^{\prime}$, its itinerary $c.\mathit{it}^{\prime}$, etc. The new
state is then communicated to the _Runtime_.

  * •

the _Runtime_ updates the system state on the map taking into account the new
vehicle states and time-dependent object attributes. Then it applies a _free
space policy_ computing the tuple $\langle
c.\mathit{f}^{\prime}\rangle_{c\in{\cal C}}$, the new free space for all
vehicles based on the current system state. The corresponding free spaces are
then communicated to vehicles and the next cycle starts.

$\langle c.\mathit{f},...\rangle_{c\in{\cal C}},~{}\langle
st_{o}\rangle_{o\in{\cal O}\setminus{\cal C}}$$\langle
c.\mathit{f}\rangle_{c\in{\cal C}},\Delta t$Map$\langle
c.\mathit{p},c.\mathit{\delta},c.\mathit{v},c.\mathit{it},...\rangle_{c\in{\cal
C}}$Runtime$st_{c}=$$\langle
c.\mathit{p},c.\mathit{\delta},c.\mathit{v},c.\mathit{it},...\rangle$Vehicle c

Figure 3:  General _ADS_ architecture

Note that the coordination principle described is independent of the type of
segments used in the map, e.g. intervals, curves or regions. For simplicity,
we take the free spaces to measure the length of an initial ride without
obstacles on the vehicle itinerary. This abstraction is sufficient to state
the basic results. We discuss later how they can be generalized for richer
interpretations of the map.

###  3.2 Assume-Guarantee for Safe Control Policies

We give below the principle of a safe control policy for vehicles, which
respects their allocated free space, applying assume-guarantee reasoning.

We consider the following two hypotheses. For a vehicle $c$, there exists a
function $B_{c}:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}_{\geq 0}$ that gives
the minimum braking distance $c$ needs to stop from speed $v$, in case of
emergency. Furthermore, for a non-negative distance $f$, let
$\mathit{Ahead}_{c}(f)$ denote the ride consisting of the positions reachable
on the itinerary $c.\mathit{it}$ from the current vehicle position
$c.\mathit{p}$ within distance $f$, formally
$\mathit{Ahead}_{c}(f)\stackrel{{\scriptstyle\mathit{def}}}{{=}}\\{p^{\prime}\in\mathit{Pos}~{}|~{}\exists\delta\leq
f.~{}{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta]}}}{{\rightsquigarrow}}{p^{\prime}}\\}$.

The following definition specifies a safe control policy using assume-
guarantee reasoning on the components of the _ADS_ architecture. We consider
assume-guarantee contracts on components defined as pairs of properties $A/G$
specifying respectively the input-output component behavior for a cycle, i.e.,
respectively, what the component guarantees ($G$) provided its environment
conforms to given assumption ($A$).

The policy is the joint enforcement of safe speed policies for vehicles and
safe free space policies for the _Runtime_. Vehicle safe speed policies
require that if a vehicle can brake safely by moving forward within its
allocated free space at the beginning of a cycle, then it can adapt its speed
moving forward within this space. _Runtime_ safe free space policies require
that if the free spaces of the vehicles are non-crossing at the beginning of a
cycle, then it is possible to find new non-crossing free spaces for the
vehicles provided they move forward in their allocated free space.

######  Definition 1 (safe control policy)

A control policy is safe if

  * •

each vehicle $c\in{\cal C}$ respects the assume-guarantee contract:

$\displaystyle 0\leq c.\mathit{v},~{}B_{c}(c.\mathit{v})\leq c.\mathit{f}$
$\displaystyle\big{/}$ $\displaystyle 0\leq c.\mathit{v}^{\prime},~{}0\leq
c.\mathit{\delta}^{\prime},~{}c.\mathit{\delta}^{\prime}+B_{c}(c.\mathit{v}^{\prime})\leq
c.\mathit{f},~{}$
$\displaystyle{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,c.\mathit{\delta}^{\prime}]}}}{{\rightsquigarrow}}{c.\mathit{p}^{\prime}},~{}c.\mathit{it}^{\prime}={c.\mathit{it}}{[c.\mathit{\delta}^{\prime},-]}$

  * •

the _Runtime_ respects the assume-guarantee contract:

$\displaystyle\wedge_{c}0\leq c.\mathit{\delta}\leq
c.\mathit{f},~{}\uplus_{c}\mathit{Ahead}_{c}(c.\mathit{f}-c.\mathit{\delta})$
$\displaystyle\big{/}$ $\displaystyle\wedge_{c\in{\cal
C}}c.\mathit{f}^{\prime}\geq
c.\mathit{f}-c.\mathit{\delta},~{}\uplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f}^{\prime})$

###### Theorem 3.1

Safe control policies preserve the following invariants:

  * •

the speed is positive and compliant to the free space, for all vehicles, that
is,
$\bigwedge_{c\in{\cal C}}0\leq c.\mathit{v}\wedge B(c.\mathit{v})\leq
c.\mathit{f}$,

  * •

the free spaces are non-crossing, that is, $\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f})$.

###### Proof

Consider the usual notation for Hoare triples $\\{\phi\\}P\\{\psi\\}$ denoting
that whenever the precondition $\phi$ is met, executing the program $P$
establishes the postcondition $\psi$. Let $A_{P}(X)/G_{P}(X,X^{\prime})$ be a
contract for a program $P$ whose initial state $X$ satisfies the assumption
$A_{P}(X)$ and which when it terminates guarantees the relation
$G_{P}(X,X^{\prime})$ between $X$ and the final state $X^{\prime}$. Then,
Hoare triples are established by the proof rule:

$\begin{array}[]{c}\phi(X)\implies A_{P}(X)~{}~{}~{}~{}\exists
X.~{}\phi(X)\wedge G_{P}(X,X^{\prime})\implies\psi(X^{\prime})\\\
\hline\cr\\{\phi\\}P\\{\psi\\}\end{array}$

We now prove that the conjunction of two assertions in the theorem is an
inductive invariant, holding at the beginning of every cycle. First, using the
rule above for the assume-guarantee contract on _all_ vehicles we establish
the following triple, where $||_{c\in{\cal C}}c$ represents the program
executed by the vehicle controllers in one cycle:

$\begin{array}[]{l}\\{\bigwedge_{c\in{\cal C}}0\leq c.\mathit{v}\wedge
B(c.\mathit{v})\leq c.\mathit{f}\wedge\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f})\\}\\\ \hskip 28.45274pt||_{c\in{\cal
C}}~{}c\\\ \\{\bigwedge_{c\in{\cal C}}0\leq c.\mathit{v}\wedge 0\leq
c.\mathit{\delta}\wedge c.\mathit{\delta}+B(c.\mathit{v})\leq
c.\mathit{f}\wedge\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f}-c.\mathit{\delta})\\}\\\ \end{array}$

The arithmetic constraints on the speed, distance traveled and free space are
implied from the guarantee. The constraint on the free space takes into
account the update of the vehicle positions, that is, moving ahead into their
free space by the distance traveled. Second, using the assume-guarantee
contract on the _Runtime_ we establish the triple

$\begin{array}[]{l}\\{\bigwedge_{c\in{\cal C}}0\leq c.\mathit{v}\wedge 0\leq
c.\mathit{\delta}\wedge c.\mathit{\delta}+B(c.\mathit{v})\leq
c.\mathit{f}\wedge\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f}-c.\mathit{\delta})\\}\\\ \hskip
28.45274pt\mbox{\emph{Runtime}}\\\ \\{\bigwedge_{c\in{\cal C}}0\leq
c.\mathit{v}\wedge B(c.\mathit{v})\leq c.\mathit{f}\wedge\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f})\\}\\\ \end{array}$

That is, the _Runtime_ re-establishes the invariant essentially by providing
at least the same free space as in the previous cycle.∎

Note that this theorem guarantees the safety of the coordination insofar as
the vehicles respecting their contracts remain in their allocated free spaces
which are non-crossing by construction. Nevertheless, the result leaves a lot
of freedom to vehicles and the _Runtime_ to choose speeds and non-crossing
free spaces. In particular, two questions arise concerning these choices. The
first question is wether the system can reach states where no progress is
possible. One can imagine traffic jam situations, for example when vehicles do
not have enough space to move. The second question is whether free space
choices can be determined by traffic rules that actually enforce fairness in
resolving conflicts between vehicles. This question is discussed in detail in
Section 5.

We show below that it is possible to compute non-blocking control policies by
strengthening the contracts satisfied by the vehicles and the _Runtime_ with
additional conditions. For vehicles, we require that they move in a cycle if
their free space is greater than a minimum free space $f_{min}$. This constant
should take into account the dimensions of the vehicles and their dynamic
characteristics, e.g., the minimum space needed to safely reach a non-negative
speed from a stop state. Additional conditions for the contract of the
_Runtime_ are that if all vehicles are stopped, then it can find at least one
free space greater than $f_{min}$.

######  Definition 2 (non-blocking control policy)

A control policy is non-blocking if there exists non-negative $f_{min}$ such
that:

  * •

each vehicle $c\in C$ respects the $A/G$ contract: $c.\mathit{f}\geq
f_{min}~{}\big{/}~{}c.\mathit{v}^{\prime}>0$,

  * •

the _Runtime_ respects the $A/G$ contract:
$\bigwedge_{c}c.\mathit{v}=0~{}\big{/}~{}\max_{c}c.\mathit{f}^{\prime}\geq
f_{min}$.

###### Theorem 3.2

Non-blocking control policies ensure progress i.e., there is always a vehicle
whose speed is positive.

###### Proof

The proof is an immediate consequence of the two contracts of Def. 2. If all
vehicles stop moving during a cycle, the _Runtime_ will necessarily find at
least $f_{\min}$ free space for at least one of them. Then, at the next cycle,
at least one vehicle will move again with positive speed, which concludes the
proof. ∎

##  4 Speed Policies abiding by the Vehicle Contract

In this section, we show that it is possible for vehicles to compute speed
policies in accordance with their contract.

The behavior of each vehicle is defined by a controller, which given its
current speed and its free space, computes the displacement for $\Delta t$ so
that it can safely move in the free space. Such safe speed policies have been
studied in [24, 25].

We illustrate the principle of safe speed policy with respect to $f$
considering that each vehicle is equipped with a controller that receives a
free space value and adjusts its speed adequately. For the sake of simplicity,
assume the controller can select among three different constant acceleration
values $\\{-b_{max},0,a_{max}\\}\in\mathbb{R}$ respectively, the negative
value $-b_{max}$ for decreasing, the zero value for maintaining and the
positive value $a_{max}$ for increasing the speed. At every cycle, the
controller will select the highest acceleration value for which the vehicle
guarantee holds as defined by its contract in Def. 1. Nonetheless, an
exception applies for the very particular case where the vehicle stops within
the cycle, which cannot be actually handled with constant acceleration.

The proposed speed policy defines the new speed $v^{\prime}$ and displacement
$\delta^{\prime}$ using a region decomposition of the safe $v\times f$ space
(that is, where $v\geq 0$ and $f\geq B(v)$) as follows:

$v^{\prime},~{}\delta^{\prime}\stackrel{{\scriptstyle\mathit{def}}}{{=}}\left\\{\begin{array}[]{l
l}0,~{}f&\mbox{if }f\geq B(v),f-v\Delta t<B(v),v-b_{max}\Delta t<0\\\\[5.0pt]
\lx@intercol v-b_{max}\Delta t,~{}v\Delta t-b_{max}\Delta
t^{2}/2\hfil\lx@intercol\\\ &\mbox{if }f\geq B(v),f-v\Delta
t<B(v),v-b_{max}\Delta t\geq 0\\\\[5.0pt] v,~{}v\Delta t&\mbox{if }f-v\Delta
t\geq B(v),f-v\Delta t-a_{max}\Delta t^{2}/2<B(v+a_{max}\Delta t)\\\\[5.0pt]
\lx@intercol v+a_{max}\Delta t,~{}v\Delta t+a_{max}\Delta
t^{2}/2\hfil\lx@intercol\\\ &\mbox{if }f-v\Delta t-a_{max}\Delta t^{2}/2\geq
B(v+a_{max}\Delta t)\end{array}\right.$ (1)

Intuitively, the regions are defined such that, when the corresponding
acceleration is constantly applied for $\Delta t$ time units, the guarantee on
the vehicle is provable given the assumptions and the region boundary
conditions. For illustration, the regions are depicted in Fig. 4 for some
concrete values of $\Delta t=1~{}sec$, $a_{max}=2.5m/s^{2}$ and
$b_{max}=-3.4m/s^{2}$.

Figure 4:  Region decomposition for safe speed policy

Moreover, the vehicle position and the itinerary are updated according to the
travelled distance by taking $c.\mathit{p}^{\prime}$ such that
${c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,c.\mathit{\delta}^{\prime}]}}}{{\rightsquigarrow}}{c.\mathit{p}^{\prime}}$
and $c.\mathit{it}^{\prime}={c.\mathit{it}}{[c.\mathit{\delta}^{\prime},-]}$.
Furthermore, the waiting time $c.\mathit{wt}$ is updated bt taking
$c.\mathit{wt}^{\prime}\stackrel{{\scriptstyle\mathit{def}}}{{=}}c.\mathit{wt}+\Delta
t$ if $c.\mathit{v}=c.\mathit{v}^{\prime}=0$ and
$c.\mathit{wt}^{\prime}\stackrel{{\scriptstyle\mathit{def}}}{{=}}0$ otherwise.

###### Proposition 1

The region-based speed policy respects the safety contract for vehicles if the
braking function is $B(v)=v^{2}/2b_{max}$.

###### Proof

According to Def. 1 let assume that $0\leq v$ and $B(v)\leq f$. The policy
must guarantee that $0\leq v^{\prime}$, $0\leq\delta^{\prime}$,
$\delta^{\prime}+B(v^{\prime})\leq f$,
${c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,c.\mathit{\delta}^{\prime}]}}}{{\rightsquigarrow}}{c.\mathit{p}^{\prime}}$,
$c.\mathit{it}^{\prime}={c.\mathit{it}}{[c.\mathit{\delta}^{\prime},-]}$.
Obviously, the last two constraints are explicitely enforced. For the
remaining constraints, the proof is made on a case by case basis for the four
regions:

  1. (i)

Immediate as $v^{\prime}=0$, $\delta^{\prime}=f$ in this case.

  2. (ii)

The constraint $v^{\prime}\geq 0$ is equivalent to $v-b_{max}\Delta t\geq 0$
which is one of the region boundaries. The constraint $\delta^{\prime}\geq 0$
holds as $\delta^{\prime}=v\Delta t-b_{max}\Delta t^{2}=\Delta
t(v-b_{max}\Delta t/2)$. Consider the constraint
$\delta^{\prime}+B(v^{\prime})\leq f$. The term
$\delta^{\prime}+B(v^{\prime})$ can be successively rewritten as follows:

$\begin{array}[]{rcl}\delta^{\prime}+B(v^{\prime})&=&v\Delta t-b_{max}\Delta
t^{2}/2+B(v-b_{max}\Delta t)\\\ &=&v\Delta t-b_{max}\Delta
t^{2}/2+(v-b_{max}\Delta)^{2}/2b_{max}\\\ &=&v\Delta t-b_{max}\Delta
t^{2}/2+v^{2}/2b_{max}-v\Delta t+b_{max}\Delta t^{2}/2\\\
&=&v^{2}/2b_{max}=B(v)\end{array}$

Henceforth, $\delta^{\prime}+B(v^{\prime})\leq f$ is equivalent to $B(v)\leq
f$ and holds from the assumption.

  3. (iii)

The constraint $v^{\prime}\geq 0$ holds because $v^{\prime}=v$. The constraint
$\delta^{\prime}\geq 0$ holds because $\delta^{\prime}=v\cdot\Delta t$. The
constraint $\delta^{\prime}+B(v^{\prime})\leq f$ is equivalent to $v\Delta
t+B(v)\leq f$ which is one of the region boundaries.

  4. (iv)

The constraint $v^{\prime}\geq 0$ holds because $v^{\prime}=v+a_{max}\Delta t$
and $v$, $a_{max}$, $\Delta t$ are all positive. Similarly, the constraint
$\delta^{\prime}\geq 0$ holds as $\delta^{\prime}=v\Delta t+a_{max}\Delta
t^{2}/2$. The constraint $\delta^{\prime}+B(v^{\prime})\leq f$ is equivalent
to $v\Delta t+a_{max}\Delta t^{2}/2+B(v+a_{max}\Delta t)\leq f$ and is the
region boundary.∎

###### Proposition 2

The region-based policy respects the non-blocking contract for vehicles for
any $f_{min}\geq B(a_{max}\Delta t)+a_{max}\Delta t^{2}/2$.

###### Proof

Actually, the value $B(a_{max}\Delta t)+a_{max}\Delta t^{2}/2$ represents the
minimal amount of space for which the policy will select acceleration
$a_{max}$ when the speed is zero, as defined by the condition of the 4th
region. ∎

Note that the speed policy works independently of the value of the parameter
$\Delta t$, which is subject only to implementation constraints, e.g., it must
be large enough to allow the controlled electromechanical system to realize
the desired effect. A large $\Delta t$ may imply low responsiveness to changes
and jerky motion, but will never compromise the safety of the system.

The proposed implementation of the speed policy is "greedy" in the sense that
it applies maximum acceleration to move as fast as possible in the available
space. We could have "lazy" policies that do not move as fast as possible, and
simply extend the travel time. We have shown in [24] that the region-based
speed policy approaches the optimal safety policy, i.e., the one that gives
the shortest travel time, when we refine the choice of acceleration and
deceleration rates in the interval $[-b_{max},a_{max}]$.

##  5 Free Space Policies implied by Traffic Rules

In this section, we study free space safety policies for a given set of global
system properties describing traffic rules. We formalize traffic rules as a
class of linear temporal logic formulas and provide a method for computing
free space values for vehicles that allow them to meet a given set of traffic
rules.

###  5.1 Writing Specifications of Traffic Rules

Traffic rules are a special class of properties that can be reliably applied
by humans. They involve the responsibility of a driver who can control the
speed and direction of a vehicle on the basis of an approximate knowledge of
its kinetic state. They do not include conditions that are difficult to assess
by the subjective judgment of human drivers, whereas they could be verified by
properly instrumented computers. Thus, traffic rules are based on topological
considerations rather than on quantitative information, such as an accurate
comparison of vehicle speeds. Furthermore, they can be formulated as
implications where the implicant is a condition that is easy to check by a
driver and the conclusion is a constraint on controllable variables that call
for a possible corrective action by the driver.

Given a map $G$ and a set of objects ${\cal O}$, we specify traffic rules as
formulas of a linear time logic of the following form, where $\Box$ is the
_always_ time modality and $\mathsf{N}~{}$ is the _next_ time modality:

$\Box~{}\forall c_{1}.~{}\forall o_{2}...\forall
o_{k}.~{}\phi(c_{1},o_{2},\dots,o_{k})\implies\mathsf{N}~{}\psi(c_{1},o_{2},\dots,o_{k})$
(2)

A rule says that for any run of the system, the satisfaction of the
precondition $\phi$ implies that the postcondition $\psi$ holds at the next
state. Both $\phi$ and $\psi$ are boolean combinations of state predicates as
defined below. Furthermore, we assume that $\psi$ constrains the speed of a
single vehicle $c_{1}$ for which the property is applicable, and which we call
for convenience the _ego_ vehicle.

The rules involve state predicates $\phi$ in the form of first-order
assertions built from variables and object attributes (denoting map positions,
segments, reals, etc) using available primitives on map positions (e.g., rides
${}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{}$, edge rides
${}\xrightarrow{{}}{}$, distance $d$, equality $=$), on segments (e.g.,
concatenation and subsegment extraction), in addition to real arithmetic and
boolean operators.

Moreover, we define auxiliary non-primitive _location_ and _itinerary_
predicates proven useful for the expression of traffic rules. For a vehicle
$c\in{\cal C}$ and $x$ either an object $o\in{\cal O}$, a vertex $u$ or an
edge $e$ of the map, we define the predicates $\and{c}{x}$ ($c$ _is at_ $x$),
${{c}}\xrightarrow{{}}{{x}}$ ($c$ _meets_ $x$ _along the same edge_),
${{c}}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{{x}}$ ($c$ _meets_ $x$) as
in Table 1. Furthermore, for a vehicle $c\in{\cal C}$ and non-negative
$\delta$ let $c.\mathit{p}\oplus_{c}\delta$ denote the future position of $c$
after traveling distance $\delta$, that is, either $c.\mathit{p}$ if
$\delta=0$ or the position $p^{\prime}$ such that
${c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta]}}}{{\rightsquigarrow}}{p^{\prime}}$.
We extend $\oplus_{c}$ to arbitrary future positions of $c$ by taking
$(c.\mathit{p}\oplus_{c}\delta)\oplus_{c}\delta^{\prime}\stackrel{{\scriptstyle\mathit{def}}}{{=}}c.\mathit{p}\oplus_{c}(\delta+\delta^{\prime})$
and we consider the total ordering $\leq_{c}$ defined as
$c.\mathit{p}\oplus_{c}\delta\leq_{c}c.\mathit{p}\oplus_{c}\delta^{\prime}$ if
and only if $\delta\leq\delta^{\prime}$.

$\begin{array}[]{c|c|c|c}\hline\cr&\and{c}{x}&{{c}}\xrightarrow{{}}{{x}}&{{c}}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{{x}}\\\
\hline\cr
x=o&c.\mathit{p}=o.\mathit{p}&\exists\delta.~{}{c.\mathit{p}}\xrightarrow{{{c.\mathit{it}}{[0,\delta]}}}{o.\mathit{p}}&\exists\delta.~{}{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta]}}}{{\rightsquigarrow}}{o.\mathit{p}}\\\
x=u&c.\mathit{p}=u&\exists\delta.~{}{c.\mathit{p}}\xrightarrow{{{c.\mathit{it}}{[0,\delta]}}}{u}&\exists\delta.~{}{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta]}}}{{\rightsquigarrow}}{u}\\\
x=e&\exists a.~{}c.\mathit{p}=(e,a)&\exists\delta.~{}\exists
a>0.~{}{c.\mathit{p}}\xrightarrow{{{c.\mathit{it}}{[0,\delta]}}}{{{}^{\bullet}\\!{e}}}\wedge&\exists\delta.~{}\exists
a>0.~{}{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta]}}}{{\rightsquigarrow}}{{{}^{\bullet}\\!{e}}}\wedge\\\
&&{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta+a]}}}{{\rightsquigarrow}}{(e,a)}&{c.\mathit{p}}\stackrel{{\scriptstyle{c.\mathit{it}}{[0,\delta+a]}}}{{\rightsquigarrow}}{(e,a)}\\\
\hline\cr\end{array}$ Table 1:  Location and itinerary predicates.

We define the semantics of state predicates $\phi$ in the usual way, by
providing a satisfaction relation $\sigma,st\vdash\phi$, where $\sigma$ is an
assignment of free variables of $\phi$ and $st$ is a system state. A complete
formal definition can be found in [6]. The semantics of rules is defined on
pairs $\sigma,[st^{(t_{i})}]_{i\geq 0}$ consisting of a function $\sigma$
assigning objects instances to object variables of the formulas and a run
$[st^{(t_{i})}]_{i\geq 0}$ for a finite set of objects ${\cal O}$. For initial
state $st^{(t_{0})}$ we define _runs_ as sequences of consecutive states
$[st^{(t_{i})}]_{i\geq 0}$ obtained along the cyclic _ADS_ execution as
described in section 3.1 and parameterized by the increasing sequence of time
points $t_{i}\stackrel{{\scriptstyle\mathit{def}}}{{=}}t_{0}+i\cdot\Delta
t\in\mathbb{R}_{\geq 0}$, that is, equal to the time for reaching the $i^{th}$
system state.

$\begin{array}[]{cl}\\\ \hline\cr 1&\mbox{enforcing safety distance between
following vehicles $c_{1}$ and $c_{2}$:}\\\ &\Box~{}\forall c_{1}.~{}\forall
c_{2}.~{}{{c_{1}}}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{{c_{2}}}\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},c_{2}.\mathit{p})\\\\[5.0pt] 2&\mbox{coordination within
all-way-stop junctions:}\\\ (i)&\mbox{safe braking of vehicle $c_{1}$
approaching a stop $so_{1}$}\\\ &\Box~{}\forall c_{1}.~{}\forall
so_{1}.~{}{{c_{1}}}\xrightarrow{{}}{{so_{1}}}\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},so_{1}.\mathit{p})\\\ (ii)&\mbox{vehicle $c_{1}$ obeys a
stop sign when another vehicle $c_{2}$ crosses the junction}\\\
&\Box~{}\forall c_{1}.~{}\forall so_{1}.~{}\forall
c_{2}.~{}\and{c_{1}}{so_{1}}\wedge c_{1}.\mathit{v}=0\wedge
c_{2}.\mathit{v}>0\wedge c_{1}.\mathit{p}\crossing
c_{2}.\mathit{p}\implies\mathsf{N}~{}c_{1}.\mathit{v}=0\\\ (iii)&\mbox{if two
vehicles $c_{1}$, $c_{2}$ are waiting before the respective stops $so_{1}$,
$so_{2}$}\\\ &\mbox{and $c_{2}$ waited longer than $c_{1}$ then $c_{1}$ has to
stay stopped}\\\ &\Box~{}\forall c_{1}.~{}\forall so_{1}.~{}\forall
c_{2}.~{}\forall so_{2}.~{}\and{c_{1}}{so_{1}}\wedge
c_{1}.\mathit{v}=0\wedge\and{c_{2}}{so_{2}}\wedge
c_{2}.\mathit{v}=0~{}\wedge\\\ &\hskip 28.45274ptc_{1}.\mathit{p}\crossing
c_{2}.\mathit{p}\wedge
c_{1}.\mathit{wt}<c_{2}.\mathit{wt}\implies\mathsf{N}~{}c_{1}.\mathit{v}=0\\\
(iv)&\mbox{if two vehicles $c_{1}$, $c_{2}$ are waiting before the respective
stops $so_{1}$, $so_{2}$ the same}\\\ &\mbox{amount of time and $c_{2}$ is at
an entry with higher priority then $c_{1}$ has to stay stopped}\\\
&\Box~{}\forall c_{1}.~{}\forall so_{1}.~{}\forall c_{2}.~{}\forall
so_{2}.~{}\and{c_{1}}{so_{1}}\wedge
c_{1}.\mathit{v}=0\wedge\and{c_{2}}{so_{2}}\wedge
c_{2}.\mathit{v}=0~{}\wedge\\\ &\hskip 28.45274ptc_{1}.\mathit{p}\crossing
c_{2}.\mathit{p}\wedge c_{1}.\mathit{wt}=c_{2}.\mathit{wt}\wedge
so_{1}.\mathit{p}\prec_{j}so_{2}.\mathit{p}\implies\mathsf{N}~{}c_{1}.\mathit{v}=0\\\\[5.0pt]
3&\mbox{coordination using traffic-lights:}\\\ &\mbox{if vehicle $c_{1}$ meets
a red traffic light $lt_{1}$, it will remain in safe distance}\\\
&\Box~{}\forall c_{1}.~{}\forall
lt_{1}.~{}{{c_{1}}}\xrightarrow{{}}{{lt_{1}}}\wedge
lt_{1}.\mathit{color}=red\wedge B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},lt_{1}.\mathit{p})\\\ &\hskip
28.45274pt\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},lt_{1}.\mathit{p})\\\\[5.0pt] 4&\mbox{priority-based
coordination of two vehicles $c_{1}$ and $c_{2}$ whose itineraries }\\\
&\mbox{meet at merger vertex $u$:}\\\ (i)&\mbox{if $c_{2}$ cannot stop at $u$
then $c_{1}$ must give way}\\\ &\Box~{}\forall c_{1}.~{}\forall
c_{2}.~{}\forall u.~{}{{c_{1}}}\xrightarrow{{}}{{u}}\wedge
B_{c_{1}}(c_{1}.\mathit{v})\leq d(c_{1}.\mathit{p},u)~{}\wedge\\\ &\hskip
28.45274pt{{c_{2}}}\xrightarrow{{}}{{u}}\wedge
B_{c_{2}}(c_{2}.\mathit{v})>d(c_{2}.\mathit{p},u)\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},u)\\\ (ii)&\mbox{if $c_{1}$, $c_{2}$ are reaching $u$ and
$c_{1}$ has less priority than $c_{2}$ then $c_{1}$ must give way}\\\
&\Box~{}\forall c_{1}.~{}\forall c_{2}.~{}\forall
u.~{}{{c_{1}}}\xrightarrow{{}}{{u}}\wedge
B_{c_{1}}(c_{1}.\mathit{v})=d(c_{1}.\mathit{p},u)\wedge
c_{1}.\mathit{p}\prec_{u}c_{2}.\mathit{p}~{}\wedge\\\ &\hskip
28.45274pt{{c_{2}}}\xrightarrow{{}}{{u}}\wedge
B_{c_{2}}(c_{2}.\mathit{v})=d(c_{2}.\mathit{p},u)\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},u)\\\\[5.0pt] 5&\mbox{enforcing speed limits for vehicle
$c_{1}$:}\\\ (i)&\mbox{if $c_{1}$ is traveling in an edge $e$ then its speed
should be lower than the speed limit}\\\ &\Box~{}\forall c_{1}.~{}\forall
e.~{}\and{c_{1}}{e}\implies\mathsf{N}~{}c_{1}.\mathit{v}\leq e.\mathit{v}\\\
(ii)&\mbox{if $c_{1}$ is approaching an edge $e$ then it controls its speed so
that it complies}\\\ &\mbox{ with the speed limit at the entrance of $e$}\\\
&\Box~{}\forall c_{1}.~{}\forall
e.~{}{{c_{1}}}\xrightarrow{{}}{{e}}\implies\mathsf{N}~{}B_{c_{1}}(c_{1}.\mathit{v})\leq
d(c_{1}.\mathit{p},{{}^{\bullet}\\!{e}})+B_{c_{1}}(e.\mathit{v})\\\
\hline\cr\end{array}$ Table 2:  Traffic rules

We provide examples of traffic rules in Table 2. We restrict ourselves to
safety rules that characterize boundary conditions that should not be violated
by the driver controlling the vehicle speed. Therefore, the preconditions
characterize potential conflict situations occurring at intersections as well
as other constraints implied by the presence of obstacles or speed rules,
e.g., traffic lights or speed limit signals. The preconditions may involve
various itinerary and location predicates and constraints on the speed of the
ego vehicle. Moreover, the latter are limited to constraints maintained by the
vehicle and involving braking functions in the form
$B_{c}(c.\mathit{v})~{}\\#~{}k$ where $k$ is a distance with respect to a
reference position on the map and $\\#$ is a relational symbol
$\\#\in\\{<,\leq,=,\geq,>\\}$. Furthermore, the postconditions involve two
types of constraints on the speed of the ego vehicle: either speed regulation
constraints that limit the distance to full stop, that is
$B_{c_{1}}(c_{1}.\mathit{v})$, or speed limitation constraints requiring that
the speed $c_{1}.\mathit{v}$ does not exceed a given limit value.

Note the difference with other approaches using unrestricted linear temporal
logic, with "eventually" and "until" operators, to express traffic rules, e.g.
[6]. We have adopted the above restrictions because they closely characterize
the vehicle safety obligations in the proposed model. Furthermore, as we show
below, traffic rules of this form can be translated into free space rules that
can reinforce the policy managed by the _Runtime_.

###  5.2 Deriving Free Space Rules from Traffic Rules

We show that we can derive from traffic rules limiting the speed of vehicles,
rules on free space variables controlled by the _Runtime_ as illustrated in
Fig. 5) such that both the traffic rules and the free space contract hold.

$\langle c.\mathit{f},...\rangle_{c\in{\cal C}},~{}\langle
st_{o}\rangle_{o\in{\cal O}\setminus{\cal C}}$$\langle
c.\mathit{f}\rangle_{c\in{\cal C}},\Delta t$Map$\langle
c.\mathit{p},c.\mathit{\delta},c.\mathit{v},c.\mathit{it},...\rangle_{c\in{\cal
C}}$Runtime$st_{c}=$$\langle
c.\mathit{p},c.\mathit{\delta},c.\mathit{v},c.\mathit{it},...\rangle$Vehicle
cTraffic RulesFree SpaceRules

Figure 5: Refined _ADS_ architecture

To express constraints on the free space variables $c.\mathit{f}$, we use, for
vehicles $c$, auxiliary _limit position_ variables $\langle
c.\mathit{\pi}\rangle_{c\in{\cal C}}$ such that
$c.\mathit{\pi}=c.\mathit{p}\oplus_{c}c.\mathit{f}$. In other words, the limit
position $c.\mathit{\pi}$ defines the position beyond which a vehicle should
not be according to its contract. It is clear that for given $c.\mathit{\pi}$
and $c.\mathit{p}$, $c.\mathit{f}$ is defined as the distance from
$c.\mathit{p}$ to $c.\mathit{\pi}$.

Using the limit position variables $\langle c.\mathit{\pi}\rangle_{c\in{\cal
C}}$ we can transform structurally any state formula $\phi$ into a free space
formula $\phi_{\pi}$ by replacing constraints on speeds by induced constraints
on limit positions as follows, for $\\#\in\\{<,\leq,=,\geq,>\\}$ and $t$ a
non-negative real constant:

$\begin{array}[]{rcl c
rcrcl}B_{c}(c.\mathit{v})&\\#&d(c.\mathit{p},x)+t&\hskip
28.45274pt\mapsto&c.\mathit{\pi}&\\#_{c}&x&\oplus_{c}&t\\\
c.\mathit{v}&\\#&t&\mapsto&c.\mathit{\pi}&\\#_{c}&c.\mathit{p}&\oplus_{c}&B_{c}(t)\end{array}$

The first case concerns speed regulation constraints bounding the limit
position $c.\mathit{\pi}$ relatively to the position $x$ of a fixed or moving
obstacle ahead of $c$, that is, a stop or traffic light sign, a vehicle, etc.
The second case concerns speed limitation constraints bounding
$c.\mathit{\pi}$ relatively to the current vehicle position $c.\mathit{p}$ and
the allowed speed.

Given a state formula $\phi$, let $\phi_{\pi}$ be the derived formula obtained
by replacing constraints on speeds by constraints on limit positions. The
following theorem guarantees preservation between properties involving speed
constraints and properties involving limit positions, in relation to the
vehicle speed contracts.

###### Theorem 5.1

The following equivalences hold:

$\begin{array}[]{rrcl}(i)&\phi&\Longleftrightarrow&(\exists~{}c.\mathit{\pi})_{c}~{}\phi_{\pi}\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
(ii)&\swarrow\\!\\!\\!{\phi}&\Longleftrightarrow&(\exists~{}c.\mathit{\pi})_{c}~{}\phi_{\pi}\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})\leq
d(c.\mathit{p},c.\mathit{\pi})\end{array}$

where $\swarrow\\!\\!\\!{\phi}$ is the speed-lower closure of $\phi$, that is,
$\phi$ where speed constraints of the form $c.\mathit{v}~{}\\#~{}t$,
$B_{c}(c.\mathit{v})~{}\\#~{}d(c.\mathit{p},x))+t$ for $\\#\in\\{\geq,>\\}$
are removed.

###### Proof

(i) Assuming $B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})$ the
following equivalences between constraints on speed $c.\mathit{v}$ and derived
constraints on limit position $c.\mathit{\pi}$ hold trivially, for any
$\\#\in\\{<,\leq,=,\geq,>\\}$:

$\begin{array}[]{rrcl}&B_{c}(c.\mathit{v})~{}\\#~{}d(c.\mathit{p},x)+t&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\Longleftrightarrow&d(c.\mathit{p},c.\mathit{\pi})~{}\\#~{}d(c.\mathit{p},x)+t&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\Longleftrightarrow&c.\mathit{\pi}~{}\\#~{}x\oplus_{c}t&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\\[5.0pt]
&c.\mathit{v}~{}\\#~{}t&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\Longleftrightarrow&B_{c}(c.\mathit{v})~{}\\#~{}B_{c}(t)&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\Longleftrightarrow&d(c.\mathit{p},c.\mathit{\pi})~{}\\#~{}B_{c}(t)&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\Longleftrightarrow&c.\mathit{\pi}~{}\\#~{}c.\mathit{p}\oplus_{c}B_{c}(t)&\wedge&B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
\end{array}$

This implies, assuming
$\bigwedge_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})$ that any
state formula $\phi$ is equivalent to the derived constraint $\phi_{\pi}$ on
limit positions, that is:

$\phi\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\Longleftrightarrow\phi_{\pi}\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})$

Then, as $\phi$ does not involve limit positions we have:

$\begin{array}[]{rcr}\phi&\Longleftrightarrow&\phi\wedge(\exists
c.\mathit{\pi})_{c}~{}\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
&\Longleftrightarrow&(\exists
c.\mathit{\pi})_{c}~{}\phi\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\\\
&\Longleftrightarrow&(\exists
c.\mathit{\pi})_{c}~{}\phi_{\pi}\wedge\bigwedge\nolimits_{c}B_{c}(c.\mathit{v})=d(c.\mathit{p},c.\mathit{\pi})\end{array}$

(ii) Immediate consequence of (i) by applying $\swarrow$ on both sides.

Re-calling Thm. 3.1 in section 3.2, notice that $B_{c}(c.\mathit{v})\leq
d(c.\mathit{p},c.\mathit{\pi})$ is enforced by safe control policies as
$d(c.\mathit{p},c.\mathit{\pi})=c.\mathit{f}$. Therefore, any property $\phi$
is preserved through equivalence only when all the vehicles run with the
maximal allowed speed by the distance to their limit positions. Otherwise, the
speed-lower closure $\swarrow\\!\\!\\!{\phi}$ is preserved through
equivalence, that is, only the upper bounds on speeds as derived from
corresponding bounds on limit positions.

Therefore, all traffic rules of form (2) which, for states satisfying the
precondition $\phi$, constrain the speed of vehicle $c_{1}$ at the next cycle
according to constraint $\psi$, are transformed into free space rules on limit
positions of the form:

$\Box~{}\forall c_{1}.\forall o_{2}...\forall
o_{k}.~{}\phi_{\pi}(c_{1},o_{2},\dots,o_{k})\implies\mathsf{N}~{}\psi_{\pi}(c_{1},o_{2},\dots,o_{k})$
(3)

Notice that the postcondition $\psi_{\pi}$ is of the form
$c_{1}.\mathit{\pi}\leq_{c_{1}}b_{\psi}(c_{1},o_{2},\dots,o_{k})$ for a
position term $b_{\psi}$ obtained by the transformation of $\psi$.

For example, the traffic rule $1$ is transformed into the free space rule:
$\Box\forall c_{1}.~{}\forall c_{2}.$
${{c_{1}}}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{{c_{2}}}$ $\implies$
$\mathsf{N}~{}c_{1}.\mathit{\pi}\leq_{c_{1}}c_{2}.\mathit{p}$. The traffic
rule $4(ii)$ is transformed into the free space rule: $\Box\forall
c_{1}.~{}\forall c_{2}.~{}\forall
u.~{}{{c_{1}}}\xrightarrow{{}}{{u}}\wedge{{c_{2}}}\xrightarrow{{}}{{u}}\wedge
c_{1}.\mathit{\pi}=u\wedge c_{2}.\mathit{\pi}=u\wedge
c_{1}.\mathit{p}\prec_{u}c_{2}.\mathit{p}\implies\mathsf{N}~{}c_{1}.\mathit{\pi}\leq_{c_{1}}u$.

We are now ready to define the _Runtime_ free space policy based on traffic
rules. Let ${\cal R}$ denotes the set of traffic rules of interest e.g., the
ones defined in Table 2. For a current _ADS_ state $st$ and current limit
positions and free spaces $\langle
c.\mathit{\pi},c.\mathit{f}\rangle_{c\in{\cal C}}$ the policy computes new
limit positions and new free spaces $\langle
c.\mathit{\pi}^{\prime},c.\mathit{f}^{\prime}\rangle_{c\in{\cal C}}$ as
follows:

$\displaystyle c.\mathit{\pi}^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\mathit{def}}}{{=}}$
$\displaystyle\min_{\leq c}~{}\\{~{}\sigma b_{\psi}~{}|~{}[\forall
c_{1}.\forall o_{2}...\forall o_{k}.~{}\phi\implies N\psi]\in{\cal
R},~{}~{}\sigma[c/c_{1}],st\vdash\phi_{\pi}\\}$ (4) $\displaystyle\hskip
22.76228pt\cup~{}\\{~{}{{e}^{\bullet}}~{}|~{}\exists
a<|\\!|e|\\!|,~{}c.\mathit{\pi}=(e,a),~{}{{c}}\stackrel{{\scriptstyle}}{{\rightsquigarrow}}{{e}}~{}\\}$
$\displaystyle c.\mathit{f}^{\prime}$
$\displaystyle\stackrel{{\scriptstyle\mathit{def}}}{{=}}$
$\displaystyle\delta\mbox{ such that
}c.\mathit{p}\oplus_{c}\delta=c.\mathit{\pi}^{\prime}$ (5)

Actually, that means computing for every vehicle $c$ the new limit position
$c.\mathit{\pi}^{\prime}$ as the nearest position with respect to $\leq_{c}$
from two sets of bounds. The first set contains the bounds $\sigma b_{\psi}$
computed for all the free space rules derived from the traffic rules in ${\cal
R}$ and applicable for $c$ at the given state $st$. The second set contains
the endpoint ${{e}^{\bullet}}$ of the edge $e$ where the current limit
position $c.\mathit{\pi}$ is located. It is needed to avoid "jumping" over
${{e}^{\bullet}}$, even though this is allowed by application of the rules, as
${{e}^{\bullet}}$ may be a merger node and should be considered for solving
potential conflicts. Then, we define the new free space
$c.\mathit{f}^{\prime}$ as the distance $\delta$ from the current position
$c.\mathit{p}$ to the new limit position $c.\mathit{\pi}^{\prime}$ measured
along the itinerary of $c$.

Note that if the free space policy respects the assume-guarantee contract of
the _Runtime_ from Def. 1 then it will moreover guarantees the satisfaction of
all traffic rules from ${\cal R}$ where both the pre- and the postcondition
$\phi$ and $\psi$ are speed-lower closed formulas. First, conformance with
respect to the contract is needed to obtain the invariants
$B_{c}(c.\mathit{v})\leq c.\mathit{f}=d(c.\mathit{p},c.\mathit{\pi})$
according to Thm. 3.1. Second, these invariants ensure preservation through
equivalence between speed-lower closed formula and derived formula on limit
positions, according to Thm. 5.1. Third, the free space policy ensures the
satisfaction of the derived free space rules, that is, by construction it
chooses limit positions ensuring postconditions $\psi_{\pi}$ hold whenever
preconditions $\phi_{\pi}$ hold. As these formulas are preserved through
equivalence, it leads to the satisfaction of the original traffic rule.

###  5.3 Correctness with respect to the Free Space Contract

We prove correctness, that is, conformance with the assume-guarantee contract
of Def. 1, of the free space policy obtained by the application of the traffic
rules from Table. 2 excluding the one concerning traffic lights. For this rule
we need additional assumptions taking into account the light functioning and
the behavior of the crossing vehicles.

First, we assume that the vehicle braking dynamics are compatible with the
speed limits associated with the map segments, that means:

  * •

for any edge $e$ leading to a junction (and henceforth a stop sign) or a
merger vertex holds $B_{c}(e.\mathit{v})\leq|\\!|e|\\!|$, for any vehicle
$c\in{\cal C}$ (see Figure 6(a)),

  * •

for any consecutive edges $e_{1}$, $e_{2}$ holds
$B_{c}(e_{1}.\mathit{v})\leq|\\!|e_{1}|\\!|+B_{c}(e_{2}.\mathit{v})$, for any
vehicle $c\in{\cal C}$ (see Figure 6(b)) i.e., between two consecutive speed
limit changes, there is sufficient space to adapt the speed.

$B_{c}(v)$$e$$v$(a)$e_{1}$$e_{2}$$v_{1}$$v_{2}$$B_{c}(v_{1})$$B_{c}(v_{2})$(b)

Figure 6: Explaining restrictions on speed limits

We call an _ADS_ state $\langle st_{o}\rangle_{o\in{\cal O}}$ _consistent with
limit positions_ $\langle c.\mathit{\pi}\rangle_{c\in{\cal C}}$ iff for every
vehicle $c\in{\cal C}$:

  * •

the limit position is ahead of the current vehicle position, that is,
$c.\mathit{p}\leq_{c}c.\mathit{\pi}$,

  * •

there is no stop sign located strictly between the current vehicle position
and the limit position, that is,
$c.\mathit{p}<_{c}so.\mathit{p}<_{c}c.\mathit{\pi}$ does not hold for any stop
$so$,

  * •

the limit position conforms to the speed limits of the current edge ($e_{1}$)
and next edge ($e_{2}$) on the itinerary of $c$, that is,
$d(c.\mathit{p},c.\mathit{\pi})\leq B_{c}(e_{1}.\mathit{v})$ and
$d(c.\mathit{p},c.\mathit{\pi})\leq
d(c.\mathit{p},{{}^{\bullet}\\!{e_{2}}})+B_{c}(e_{2}.\mathit{v})$.

For vehicle $c$ and position $p$ located ahead of $c$ on its itinerary we
further denote by
$\mathit{ahead}_{c}(p)\stackrel{{\scriptstyle\mathit{def}}}{{=}}\mathit{Ahead}_{c}(f)$
for $f=d(c.\mathit{p},p)$, that is, the space ahead of $c$ until position $p$.
In particular,
$\mathit{ahead}_{c}(c.\mathit{\pi})=\mathit{Ahead}_{c}(c.\mathit{f})$ holds as
$c.\mathit{\pi}=c.\mathit{p}\oplus_{c}c.\mathit{f}$. The following lemma
provides the basic conditions that guarantee the correctness of the free space
policy.

###### Lemma 1

Let $st$ be an _ADS_ state and $\langle c.\mathit{\pi}\rangle_{c\in{\cal C}}$
be limit positions such that:

  * •

the state $st$ is consistent with the limit positions $\langle
c.\mathit{\pi}\rangle_{c\in{\cal C}}$,

  * •

the spaces ahead up to the limit positions are non-crossing, that is,
$\biguplus_{c\in{\cal C}}\mathit{ahead}_{c}(c.\mathit{\pi})$.

Let $\langle c.\mathit{\pi}^{\prime}\rangle_{c\in{\cal C}}$ be the new limit
positions computed for state $st$ and $\langle
c.\mathit{\pi}\rangle_{c\in{\cal C}}$ according to the free space policy.
Then, the following hold:

  1. (a)

$c.\mathit{\pi}\leq_{c}c.\mathit{\pi}^{\prime}$, for every vehicle $c\in{\cal
C}$,

  2. (b)

the state $st$ is consistent with the new limit positions $\langle
c.\mathit{\pi}^{\prime}\rangle_{c\in{\cal C}}$,

  3. (c)

the spaces ahead up to the new limit positions are non-crossing, that is,
$\biguplus_{c\in{\cal C}}\mathit{ahead}_{c}(c.\mathit{\pi}^{\prime})$.

###### Proof

(a) Let fix an arbitrary vehicle $c$. According to the free space policy the
limit position $c.\mathit{\pi}^{\prime}$ is defined as the nearest position
among several bounds on the itinerary of $c$. We will show that, in all
situations, these bounds $b$ are at least as far as the current limit position
$c.\mathit{\pi}$, that is $c.\mathit{\pi}\leq_{c}b$ and hence the result.
First, consider all applicable traffic rules and their associated bounds:

  * •

rule $1$: The bound $b$ is defined as the position $c_{2}.\mathit{p}$ of the
heading vehicle $c_{2}$. The constraint
$c.\mathit{\pi}\leq_{c}c_{2}.\mathit{p}$ holds because the spaces ahead to the
limit positions are assumed non-crossing,

  * •

rule $2(i)$: The bound $b$ is defined as the position $so.\mathit{p}$ of the
stop sign located ahead of $c$. The constraint
$c.\mathit{\pi}\leq_{c}so.\mathit{p}$ holds because the state $st$ is assumed
consistent, that is, no stop sign between the vehicle and the current limit
position,

  * •

rules $2(ii,iii,iv)$: The bound $b$ is defined as the current position
$c.\mathit{p}$, which is equal to the current limit $c.\mathit{\pi}$ due to
the constraint $c.\mathit{v}=0$ in their respective preconditions, therefore
obviously $c.\mathit{\pi}\leq_{c}c.\mathit{\pi}$,

  * •

rules $4(i,ii)$: The bound $b$ is defined as the merger node $u$ and the
preconditions of the rules contain respectively $c.\mathit{\pi}\leq_{c}u$ and
$c.\mathit{\pi}=u$,

  * •

rules $5(i,ii)$: Assume $c$ is located on some edge $e_{1}$ and the next edge
is $e_{2}$. As $st$ is consistent with current limit positions, this implies
$d(c.\mathit{p},c.\mathit{\pi})\leq B(e_{1}.\mathit{v})$ and
$d(c.\mathit{p},c.\mathit{\pi})\leq
d(c.\mathit{p},{{}^{\bullet}\\!{e_{2}}})+B_{c}(e_{2}.\mathit{v})$. This is
equivalent to
$c.\mathit{\pi}\leq_{c}c.\mathit{p}\oplus_{c}B_{c}(e_{1}.\mathit{v})$ and
$c.\mathit{\pi}\leq_{c}{{}^{\bullet}\\!{e_{2}}}\oplus_{c}B_{c}(e_{2}.\mathit{v})$
which are the constraints for speed limit rules.

Second, we consider the position ${{e}^{\bullet}}$, where the edge $e$
contains the limit position $c.\mathit{\pi}$. That is, $c.\mathit{\pi}=(e,a)$
for some $a<|\\!|e|\\!|$ and hence
$c.\mathit{\pi}\leq_{c}(e,|\\!|e|\\!|)={{e}^{\bullet}}$.

(b) We know that $c.\mathit{p}\leq_{c}c.\mathit{\pi}$ for all vehicles $c$.
Then, from (a) above we obtain immediately that
$c.\mathit{p}\leq_{c}c.\mathit{\pi}^{\prime}$ for all vehicles $c$. Moreover,
according to traffic rule $2(i)$, new limit positions
$c.\mathit{\pi}^{\prime}$ cannot move over a stop sign $so$ unless the vehicle
$c$ is at $so$. That means, stop signs cannot be inserted between a vehicle
and their limit positions. Finally, according to traffic rules $5(i,ii)$, the
new limit positions are at most as far as the bounds for the current and next
edge speed limits. The restriction on speed limits from Figure 6(b) is needed
whenever vehicles are located at vertices, because of the transition from the
current to the next edge.

(c) We have seen that limit positions can either stay unchanged or move
forward on the itineraries of their respective vehicles. In order to show that
spaces until the new limit positions are non-crossing, we need to focus on
moving limit positions. We prove the following facts, which guarantee that
these spaces remain indeed non-crossing:

  * •

_no limit position exceeds the current position of a vehicle_. Actually, this
is explicitly excluded by the traffic rule $1$. Therefore, no space is
extended so as to overlap with an existing space,

  * •

_two limit positions never move simultaneously so that the corresponding
spaces cross each other_. First, crossing may happen at junctions i.e., if two
limit positions will simultaneously enter the same junction. Such situations
are excluded by traffic rules $2(i,ii,iii,iv)$ which force vehicles to stop
and then solve conflicts between them in a deterministic manner. Second,
crossing may happen at merger nodes i.e., if two limit positions will
simultaneously move over a merger node. These situations are explicitly
excluded by traffic rule $4(i,ii)$ which solve conflicts at merger nodes based
on priorities, plus the extra rule forbidding limit positions to jump over map
vertices. ∎

###### Proposition 3

The free space policy respects the safety contract for the _Runtime_ provided
the initial _ADS_ state is consistent with initial limit positions.

###### Proof

Let consider a state $st$ consistent with limit positions $\langle
c.\mathit{\pi}\rangle_{c\in{\cal C}}$ and satisfying the assumptions stated in
Def. 1. We are therefore satisfying the premises of Lemma 1 and consequently
the new limit positions $\langle c.\mathit{\pi}^{\prime}\rangle_{c\in{\cal
C}}$ will satisfy the conclusions (a)-(c) as stated by the Lemma 1.

Then, for any vehicle $c$, using (a) we know that the new limit position
satisfies $c.\mathit{\pi}\leq_{c}c.\mathit{\pi}^{\prime}$. Consequently, the
new free space $c.\mathit{f}^{\prime}$ which is the distance from the current
vehicle position to the next limit position satisfies
$c.\mathit{f}^{\prime}\geq c.\mathit{f}-c.\mathit{\delta}$, that is, the first
assertion of the _Runtime_ guarantee in Def. 1. This inequality can be
understood from Fig. 7 which depicts the generic situation for a vehicle $c$.

$c.\mathit{p}$$c.\mathit{\pi}$$c.\mathit{\pi}^{\prime}$$c.\mathit{f}$$c.\mathit{\delta}$$c.\mathit{f}^{\prime}$

Figure 7: Update of limit position and free space along the itinerary of $c$

Moreover, using (c) we obtain immediately the second assertion of the
_Runtime_ guarantee, that is, $\biguplus_{c\in{\cal
C}}\mathit{Ahead}_{c}(c.\mathit{f}^{\prime})$.

Finally, using (b) we know that the state $st$ is consistent with new limit
positions $\langle c.\mathit{\pi}^{\prime}\rangle_{c\in{\cal C}}$. Then, as
long as the vehicles move forward into their free spaces according to their
contract, the system state $st^{\prime}$ is consistent with respect to these
new limit positions. So, eventually, at the beginning of the next _Runtime_
cycle we are back to the initial situation considered for $st$ and limit
positions $\langle c.\mathit{\pi}\rangle_{c\in{\cal C}}$. That means
essentially that state consistency with respect to limit positions is an
inductive invariant in the system, so it can be safely assumed to hold at any
time provided it holds initially. ∎

###  5.4 Non-blocking Free Space Policies

The free space policy based on traffic rules is not non-blocking. While
continuously meeting traffic rules, an _ADS_ can potentially evolve into a
blocking state. For example, when a subset of vehicles is blocked in a
roundabout so that none of them can move further and eventually exit the
roundabout and all other vehicles are waiting to enter the same roundabout.
The non-blocking contract can be however fulfilled if the _Runtime_ monitors
the traffic from a global point of view and prevents situations as described
above.

Let consider that there exists a constant $f_{min}$ such that for all map
edges $e$, $|\\!|e|\\!|>f_{min}$ and $e.\mathit{v}>B^{-1}(f_{min})$.
Furthermore, let $E_{\crossing}\subseteq E$ be the subset of edges belonging
to junctions. An elementary directed path $\gamma=e_{1}e_{2}\dots e_{m}\in
E^{*}$ is _critical_ either if (i) it is a circuit visiting at most once every
junction or (ii) it ends and returns at the same junction, while visiting at
most once every other junction. Let $\\#_{j}(\gamma)$ be the number of
distinct junctions of a critical path $\gamma$. We define the capacity
$\mathit{w}({\gamma})$ of a critical path $\gamma$ as the least number of
vehicles that could "block" the critical path $\gamma$ minus one:

$\mathit{w}({\gamma})\stackrel{{\scriptstyle\mathit{def}}}{{=}}\\#_{j}(\gamma)+\left(\sum\nolimits_{e\in\gamma\setminus
E_{\crossing}}\big{\lfloor}|\\!|e|\\!|~{}/~{}f_{min}\big{\rfloor}\right)-1$
(6)

That is, we assume that a junction can be blocked by one vehicle, and a non-
junction edge $e$ can be blocked by $\lfloor|\\!|e|\\!|~{}/~{}f_{min}\rfloor$
vehicles.

###### Proposition 4

The free space policy derived from traffic rules respects the non-blocking
contract for the _Runtime_ as long as the number of vehicles on every critical
path $\gamma$ is lower than the path capacity $\mathit{w}({\gamma})$.

###### Proof

Consider a state where all vehicles are stopped. Consider an arbitrary vehicle
$c_{0}$. Two situations can happen, respectively (i) $c_{0}$ is waiting at an
entry of a junction since another vehicle is already in or (ii) $c_{0}$ is
waiting behind another stopped vehicle. That means, in both cases, some other
vehicle $c_{1}$ is actually blocking $c_{0}$. We continue the same reasoning
for $c_{1}$, and can find another vehicle $c_{2}$ blocking it and so on. As
the number of vehicles is finite, we finally find a circular chain $c_{i}$,
$c_{i+1}$, $\dots$, $c_{n}$, $c_{i}$ of vehicles that block each other
successively.

Any chain of vehicles as above is located on some critical path $\gamma$, that
is, either a circuit or a path going twice through the same junction of the
map. Assume the number of vehicles on the path $\gamma$ is lower than the path
capacity $\mathit{w}({\gamma})$. We distinguish two situations:

  * •

_the critical path contains only junction edges:_ Then, as the path capacity
is $\\#_{j}(\gamma)-1$ at least one of the junctions must be clear of
vehicles. Therefore, at least one of the vehicles waiting at that junction
entries will obtain the free space to proceed. That is, the vehicle in the
preceding junction or another one waiting at some other entry, depending on
the applicable traffic rules.

  * •

_the critical path contains both junction and non-junction edges:_ If at least
one of the junctions is not empty, we can reason as in the previous case and
find a vehicle that can proceed. Otherwise, as every junction contains one
vehicle, then the number of vehicles on the remaining non-junction edges is at
most $\sum\nolimits_{e\in\gamma\setminus
E_{\crossing}}\big{\lfloor}|\\!|e|\\!|/f_{min}\big{\rfloor}-1$. That means,
one can find a non-junction edge with more than $f_{min}$ unused space. That
space is eventually allocated to either one of the vehicles waiting on the
edge, or to a vehicle waiting to enter the edge (that is, exiting from a
junction, entering through a merger node, etc), depending on applicable
rules.∎

##  6 Experiments

We are currently developing a prototype for _ADS_ simulation implementing the
speed and free space policies introduced. It takes as inputs (i) a map defined
as an annotated metric graph with segments that are parametric lines or arcs
and (ii) an initial state containing the positions, the initial speeds and the
itineraries of a number of vehicles. The simulation proceeds then as explained
in section 3 by using the specific control policies from sections 4 and 5. The
prototype uses the SFML222Simple and Fast Multimedia Library,
https://www.sfml-dev.org/ library for graphical rendering of states. Fig. 8
presents simulation snapshots for two simple examples running respectively 5
and 18 vehicles. Note that performance scales up smoothly as the number of
vehicles increases because each rule is applied on a linear finite horizon
structure. Furthermore, compared to simulators that particularize an _ego_
vehicle, the _Runtime_ treats all vehicles the same and ignores their speed
control policy as long as they fulfill their contract.

Figure 8: Snapshots of _ADS_ simulation

##  7 Discussion

The paper studies results for the correct by design coordination of _ADS_
based on assume-guarantee contacts. The coordination follows a two-step
synchronous interaction protocol between vehicles and a _Runtime_ that, based
on the distribution of vehicles on a map, computes the corresponding free
spaces. A first result characterizes safe control policies as the combination
of assume-guarantee contracts for vehicles and the _Runtime_. This result is
then specialized by showing how policies consistent with their respective
contracts can be defined for vehicles and the _Runtime_. In particular, for
vehicles, we provide a principle for defining speed policies and, for the
_Runtime_ , we compute free space policies that conform to a set of traffic
rules. The results are general and overcome the limitations of a posteriori
verification. They can be applied to _ADS_ involving a dynamically changing
number of vehicles. In addition, they rely on a general map-based environment
model, which has been extensively studied in [6]. Control policies for
vehicles and the runtime can be implemented efficiently. In particular, the
speed policy has been tested in various implementations [24, 25] and found to
be not only safe, but also closer to the optimum when refining the space of
possible accelerations.

Note that the results can be extended with slight modifications to maps where
the segments are curves or regions to express traffic rules involving
properties of two-dimensional space, for example for passing maneuvers. For
example, if we consider region maps, their segments will be regions of
constant width centered on curves. Itineraries, free spaces and $B(v)$ will be
regions. The relationship $B(v)\leq f$ becomes $B(v)\subseteq f$ and the
addition of lengths of segments should be replaced by the disjoint union of
the regions they represent. The speed control policy will remain unchanged in
principle but will need a function computing the distance travelled in a
region. Finally, the runtime verification of the disjointness of free spaces
may incur a computational cost depending on the accuracy of the region
representation.

The presented results provide a basis for promising developments in several
directions. One direction is to extend the results to achieve correctness by
design for general properties. We have shown that traffic rules, which are
declarative properties of vehicles, can be abstracted into safety constraints
on free spaces. In this way, we solved a simple synthesis problem by
transforming a “static” constraint on vehicle speed into a “dynamic”
constraint on shared resources.

An interesting question that should be further investigated, is whether the
method can be extended to more general properties involving the joint
obligation of many vehicles. For example, we can require that for any pair of
vehicles $c_{1}$ and $c_{2}$ that are sufficiently close, the absolute value
of the difference between their speeds is less than a constant $k$, i.e.,
$|c_{1}.\mathit{v}-c_{2}.\mathit{v}|\leq k$. This can be achieved by a free
space constraint that gives more free space to the vehicle with the lower
speed, assuming that vehicle speed policies are not "lazy" and use as soon as
possible the available space.

For general properties involving more than one vehicle, it seems realistic to
translate them directly into free space constraints that will enforce the
constraints processed by the _Runtime_ to ensure the safe control policy. In
particular, in addition to safety properties, we could devise free space
policies that optimize criteria such as road occupancy and uniform separation
for a given group of vehicles e.g. platoon systems studied in [9]. Note that
achieving non-blocking control is such a property that involves the
application of occupancy criteria.

Another direction is to move from centralized to distributed coordination with
many runtimes. It seems possible to partition traffic rules according to the
geometric scope of their application, e.g., a specific runtime could control
access to each junction. Finally, the _Runtime_ can be used as a monitor to
verify that the vehicle speed policies of an _ADS_ are safe and respect the
given traffic rules.

## References

  * [1] OpenDRIVE® Format Specification. Tech. Rep. V 1.4 ©2006-2015, VIRES Simulationstechnologie GmbH (2015), 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), https://www.asam.net/standards/detail/opendrive
  * [3] Bagschik, G., Menzel, T., Maurer, M.: Ontology based scene creation for the development of automated vehicles. In: 2018 IEEE Intelligent Vehicles Symposium, IV 2018, Proceedings. pp. 1813–1820. IEEE (2018), https://doi.org/10.1109/IVS.2018.8500632
  * [4] 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, Proceedings, Part II. LNCS, vol. 10864, pp. 245–261. Springer (2018), https://doi.org/10.1007/978-3-319-91638-5_13
  * [5] Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J., Reinkemeier, P., Sangiovanni-Vincentelli, A.L., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2-3), 124–400 (2018)
  * [6] Bozga, M., Sifakis, J.: Specification and validation of autonomous driving systems: A multilevel semantic framework. CoRR abs/2109.06478 (2021), https://arxiv.org/abs/2109.06478
  * [7] Butz, M., Heinzemann, C., Herrmann, M., Oehlerking, J., Rittel, M., Schalm, N., Ziegenbein, D.: SOCA: domain analysis for highly automated driving systems. In: ITSC. pp. 1–6. IEEE (2020)
  * [8] Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: TACAS. Lecture Notes in Computer Science, vol. 4424, pp. 261–275. Springer (2007)
  * [9] 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, Proceedings. LNCS, vol. 12310, pp. 284–302. Springer (2020)
  * [10] Esterle, K., Gressenbuch, L., Knoll, A.C.: Formalizing traffic rules for machine interpretability. In: 3rd IEEE Connected and Automated Vehicles Symposium, CAVS 2020, Proceedings. pp. 1–7. IEEE (2020), https://doi.org/10.1109/CAVS51000.2020.9334599
  * [11] 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.) 13th International Conference on Formal Engineering Methods, ICFEM 2011, Proceedings. LNCS, vol. 6991, pp. 404–419. Springer (2011), https://doi.org/10.1007/978-3-642-24559-6_28
  * [12] Karimi, A., Duggirala, P.S.: Formalizing traffic rules for uncontrolled intersections. In: 11th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2020, Proceedings. pp. 41–50. IEEE (2020), https://doi.org/10.1109/ICCPS48487.2020.00012
  * [13] Kress-Gazit, H., Pappas, G.J.: Automatically synthesizing a planning and control subsystem for the DARPA urban challenge. In: CASE. pp. 766–771. IEEE (2008)
  * [14] Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: Compositional realizability analysis in FRET. In: FM. Lecture Notes in Computer Science, vol. 13047, pp. 503–523. Springer (2021)
  * [15] Meyer, B.: Applying "design by contract". Computer 25(10), 40–51 (1992)
  * [16] Poggenhans, F. et al: Lanelet2: A high-definition map framework for the future of automated driving. In: 21st International Conference on Intelligent Transportation Systems, ITSC 2018, Proceedings. pp. 1672–1679. IEEE (2018), https://doi.org/10.1109/ITSC.2018.8569929
  * [17] Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015, Proceedings. pp. 1658–1665. IEEE (2015), https://doi.org/10.1109/ITSC.2015.269
  * [18] 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, Proceedings. LNCS, vol. 11138, pp. 75–90. Springer (2018), https://doi.org/10.1007/978-3-030-01090-4_5
  * [19] Rizaldi A. et al: 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, Proceedings. LNCS, vol. 10510, pp. 50–66. Springer (2017), https://doi.org/10.1007/978-3-319-66845-1_4
  * [20] Saoud, A., Girard, A., Fribourg, L.: Assume-guarantee contracts for continuous-time systems. Autom. 134, 109910 (2021)
  * [21] Schwarting, W., Alonso-Mora, J., Rus, D.: Planning and decision-making for autonomous vehicles. Annual Review of Control, Robotics, and Autonomous Systems 1, 187–210 (2018)
  * [22] Sharf, M., Besselink, B., Molin, A., Zhao, Q., Johansson, K.H.: Assume/guarantee contracts for dynamical systems: Theory and computational tools. CoRR abs/2012.12657 (2020)
  * [23] Sun, M., Bakirtzis, G., Jafarzadeh, H., Fleming, C.: Correct-by-construction: a contract-based semi-automated requirement decomposition process. CoRR abs/1909.02070 (2019)
  * [24] Wang, Q., Li, D., Sifakis, J.: Safe and efficient collision avoidance control for autonomous vehicles. In: 18th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2020, Proceedings. pp. 1–6. IEEE (2020). https://doi.org/10.1109/MEMOCODE51338.2020.9315034, https://doi.org/10.1109/MEMOCODE51338.2020.9315034
  * [25] Wang, Q., Zheng, X., Zhang, J., Sifakis, J.: A hybrid controller for safe and efficient collision avoidance control. CoRR abs/2103.15484 (2021), https://arxiv.org/abs/2103.15484
  * [26] Waqas, M., Murtaza, M.A., Nuzzo, P., Ioannou, P.: Correct-by-construction design of adaptive cruise control with control barrier functions under safety and regulatory constraints (2022). https://doi.org/10.48550/ARXIV.2203.14110, https://arxiv.org/abs/2203.14110
  * [27] Wongpiromsarn, T., Karaman, S., Frazzoli, E.: Synthesis of provably correct controllers for autonomous vehicles in urban environments. In: ITSC. pp. 1168–1173. IEEE (2011)
  * [28] Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Autom. Control. 57(11), 2817–2830 (2012)