11institutetext:  Computer Science Department
Carnegie Mellon University, Pittsburgh, USA
11email<EMAIL_ADDRESS>11email<EMAIL_ADDRESS>
# Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and
Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars

Megan Strauss  0009-0009-6769-2404 Stefan Mitsch  0000-0002-3194-9759

###### Abstract

Technology advances give us the hope of driving without human error, reducing
vehicle emissions and simplifying an everyday task with the future of self-
driving cars. Making sure these vehicles are safe is very important to the
continuation of this field. In this paper, we formalize the Responsibility-
Sensitive Safety model (RSS) for self-driving cars and prove the safety and
optimality of this model in the longitudinal direction. We utilize the hybrid
systems theorem prover KeYmaera X to formalize RSS as a hybrid system with its
nondeterministic control choices and continuous motion model, and prove
absence of collisions. We then illustrate the practicality of RSS through
refinement proofs that turn the verified nondeterministic control envelopes
into deterministic ones and further verified compilation to Python. The
refinement and compilation are safety-preserving; as a result, safety proofs
of the formal model transfer to the compiled code, while counterexamples
discovered in testing the code of an unverified model transfer back. The
resulting Python code allows to test the behavior of cars following the motion
model of RSS in simulation, to measure agreement between the model and
simulation with monitors that are derived from the formal model, and to report
counterexamples from simulation back to the formal model.

###### Keywords:

differential dynamic logic, refinement, testing, self-driving cars, collision
avoidance, theorem proving

##  1 Introduction and Motivation

As technology advances, it becomes both more appealing and feasible to
automate everyday tasks. In doing this, there is a higher need for robust
formal verification and testing strategies to ensure that these automated
systems are safe. Formal verification ensures that all situations encountered
in a model of physics are safe, while testing provides evidence that the
formal model works as expected and can give insight to bugs in a yet-to-be-
verified model. To this end, a testing strategy analyzes some (representative)
situations that an automated system may encounter. This paper develops a
formal framework to link modeling, offline verification, online monitoring,
and testing, sketched in Fig. 1 and illustrated throughout the paper with an
example in autonomous driving.

Formalize HP Create HP $\alpha$ Refinement Prove $D(\alpha)\leq\alpha$ Python
Test $\textsf{Py}(D(\alpha))$ Safety Proof (dL) $[\alpha]P$ Safety Transfer
(dRL) $[\alpha]P\rightarrow[D(\alpha)]P$ Code Correctness
$(\textsf{Py}(D(\alpha)),\nu)\rightarrow(\perp,\omega)$ then
$(\nu,\omega)\in\llbracket D(\alpha)\rrbracket$ deterministic $D(\alpha)$
compile $D(\alpha)\vartriangleright Py(D(\alpha))$ Safety
PreservationCounterexample Transfer Figure 1: Proof and testing structure with
relationships to each other

We use hybrid systems to describe the dynamic components of a car, with the
goal of creating discrete computer controllers which prevent collisions and
other unsafe situations. Analyzing such a system requires two components: a
differential equation modeling the cars’ motion and a car control algorithm.
For the differential equation, we follow [13] and describe the longitudinal
motion of a car in response to acceleration/deceleration inputs. For the
discrete controller, we follow the Responsibility-Sensitive Safety (RSS) model
[24]. Its discrete control choices influence the continuous motion of the car,
and are given in terms of a nondeterministic control envelope that allows for
many different ways of deterministic control implementation. In the resulting
hybrid systems model, we prove the safety (defined by absence of collision) of
all possible implementations within the control envelope. This proof step
replaces the need to test through simulation whether the model is safe, i.e.
checking if cars collide in any implementation of the system, but simulation
can help in debugging unverified models. We also want the ability to analyze
concrete (deterministic) controller implementations and motion models and
determine whether they follow the general verified model. We do this through
refinement proofs in differential refinement logic [14] to a deterministic
hybrid program followed by a verified compilation to Python which allows us to
further analyze the behavior of a system. This way, we can analyze concrete
behavior for concrete parameter choices in the formal model, and simulate
behavior for analysis in select driving situations. In order to transfer the
safety proof to _all encountered situations_ , the remaining question after a
safety proof is then to detect at runtime when the proof applies and when it
does not. We answer this by applying ModelPlex [17] to generate monitors that
are able to validate unverified code and motion model alike. We utilize the
same monitors in testing and simulation to measure the robustness of control
choices, or in other words, the safety-criticality of test scenarios. The
proof, refinement, and compilation framework is set up in such a way that, if
a proof step fails, compiling the formal model and analyzing it for
counterexamples through testing is still possible.

##  2 Background

###  2.1 Responsibility-Sensitive Safety

We briefly summarize Responsibility-Sensitive Safety (RSS, [24]) that we use
as a case study throughout this paper. The general purpose of RSS is to
describe a safe algorithm for the interaction of (semi-)autonomous cars, with
safety being defined as the avoidance of collision. RSS defines a lane-based
coordinate system which describes the position of cars with a longitudinal and
lateral coordinate relative to the lane they are in on a road. The
longitudinal coordinate measures the distance relative to a starting position
along the road, which abstracts from road geometry. The lateral position
describes the distance from the center of the road. The lane-based coordinate
system simplifies the motion model into a linear differential equation system
as in [13].

Table 1: RSS variables and model parameters Parameter |  Description
---|---
$x_{1},x_{2}$ |  positions in lateral or longitudinal direction of car 1 and 2
$v_{1},v_{2}$ |  velocities in lateral or longitudinal direction of car 1 and car 2
$a_{1},a_{2}$ |  acceleration in lateral or longitudinal direction of car 1 and car 2
$a_{minBrake}$ |  minimum deceleration during evasion maneuver
$a_{maxBrake}$ |  maximum deceleration
$a_{minBrakeCorrect}$ |  minimum deceleration during evasion maneuver in the correct direction (only used for cars driving in opposite directions)
$a_{maxAccel}$ |  maximum acceleration (positive constant, used in both directions)
$\rho$ |  reaction time for starting evasion maneuver

The general idea behind the RSS control envelope is that two cars should
maintain a safe distance between them, which is a function of the current
speeds of the two cars. If at a safe distance, they are allowed to drive at
any acceleration or deceleration within their cars’ maximum acceleration and
maximum braking bounds. Otherwise, if not at a safe distance, they must
respond with a predefined evasion maneuver called _proper response_ within a
specified reaction time horizon in order to remain safe. The safe distance is
specified as a function of (relative) vehicle speed and vehicle parameters, as
summarized in Table 1 [24].

###  2.2 Differential Dynamic Logic and Notation

We use differential dynamic logic (dL) [21] to create models of car control
and motion, and to express correctness and optimality properties of RSS.
Differential dynamic logic supports modeling hybrid systems complete with
support for continuous dynamics expressed using differential equations. Within
the RSS model, we utilize discrete dynamics to describe the control options in
terms of instantly changing the acceleration or deceleration that the car is
following. We use differential equations to model the resulting motion change
in speed and position of the cars with respect to this chosen acceleration. dL
comes with a proof calculus [21], which is supported in the automated theorem
prover KeYmaera X [6]. For the scope of this paper, the following informal
understanding, summarized in Table 2 suffices. Assignment of a variable
$x\coloneqq\theta$ instantly assigns the value of $\theta$ to $x$,
nondeterministic assignment $x\coloneqq\ast$ assigns any real value to $x$
(e.g. choosing an arbitrary acceleration value). Continuous evolution
$\\{x{{}^{\prime}}=\theta~{}\&~{}Q\\}$ evolves $x$ along the differential
equation $x{{}^{\prime}}=\theta$ for an arbitrary duration while $Q$ is true
throughout (e.g. change position of cars along kinematic equations, but
prevent moving backwards). The test $?P$ checks that formula $P$ is true and
continues running if it is, and if not aborts the program (possibly
backtracking to other nondeterministic options). Sequential composition
$\alpha\texttt{;}\beta$ first runs hybrid program $\alpha$ and subsequently
runs hybrid program $\beta$ from the resulting states of $\alpha$ (e.g. first
choose acceleration, then follow motion). A nondeterministic choice of
operations allows for the choice of two separate hybrid programs,
$\alpha\,\cup\,\beta$ (e.g. running $\alpha$ if there is a safe distance
between two cars and running emergency braking $\beta$ otherwise).
Nondeterministic repetition $\alpha^{\ast}$ repeats hybrid program $\alpha$
some $n\geq 0$ times (e.g. repeatedly running control and motion).

Table 2: Syntax and informal semantics of hybrid programs Program |  Meaning
---|---
$x\coloneqq\theta$ |  Assigns the value of $\theta$ to $x$
$x\coloneqq*$ |  Assigns any real value to $x$
$\\{x{{}^{\prime}}=\theta~{}\&~{}Q\\}$ |  Evolves $x$ along $\theta$ for any duration $t\geq 0$ while $Q$ is true throughout
$?P$ |  Tests formula $P$ and continues if true, aborts if false
$\alpha;\beta$ |  Follows program $\alpha$ and subsequently follows program $\beta$
$\alpha\,\cup\,\beta$ |  Follows either program $\alpha$ or program $\beta$, nondeterministically
$\alpha^{\ast}$ |  Repeats program $\alpha$ a nondeterministic $n\geq 0$ number of times

The set of dL formulas is generated by the following grammar, where
$\sim\,\in\\{<,\leq,=,\neq,\geq,>\\}$ and terms $f,g$ in $+,-,\cdot,/$ are
over the reals, contain number literals, variables and $n$-ary rigid function
symbols, plus support interpreted minimum, maximum, absolute value and
trigonometric functions [7]:

$P,Q\coloneqq f\sim g\mid P\land Q\mid P\lor Q\mid P\rightarrow Q\mid
P\leftrightarrow Q\mid\forall x\,P\mid\exists
x\,P\mid\left[\alpha\right]P\mid\langle\alpha\rangle P\enspace.$

We use $f\sim g\sim h$ as shorthand for $f\sim g\land g\sim h$ where $f,g$.
Arithmetic operations, comparisons, Boolean connectives, and quantifiers are
as usual. Formulas of the form $\left[\alpha\right]P$ and
$\langle\alpha\rangle P$ express properties about programs:
$\left[\alpha\right]P$ is true when in all states reachable through
transitions of program $\alpha$ the property $P$ is true (used for safety);
$\langle\alpha\rangle P$ is true when there exists a state reachable by the
program $\alpha$ in which $P$ is true (used for liveness, optimality, and
runtime monitoring).

The semantics of dL [21] is a Kripke semantics in which the states of the
Kripke model are the states of the hybrid system. A state is a map
$\omega:\mathcal{V}\rightarrow\mathbb{R}$, assigning a real value $\omega(x)$
to each variable $x\in\mathcal{V}$ in the set of variables $\mathcal{V}$. We
write $\llbracket P\rrbracket$ to denote the set of states in which formula
$P$ is true, $\omega\in\llbracket P\rrbracket$ or equivalently $\omega\models
P$ if formula $P$ is true at state $\omega$, $\models P$ for $P$ being valid
(true in all states), and $\omega\llbracket e\rrbracket$ to denote the real
value of term $e$ in state $\omega$. The semantics of hybrid programs is
expressed as a transition relation
$\llbracket\alpha\rrbracket\subseteq\mathcal{S}\times\mathcal{S}$ of initial
and final states in $\mathcal{S}$ [21] and we write
$(\omega,\nu)\in\llbracket\alpha\rrbracket$ to express that program $\alpha$
reaches state $\nu$ when starting in state $\omega$. dL is decidable relative
to either an oracle for the continuous first-order logic of differential
equations or an oracle for the discrete fragment of dL [20, Theorem 11].

###  2.3 Differential Refinement Logic

Differential refinement logic dRL [14] defines a relationship between two
hybrid programs $\alpha\leq\beta$ that tells us that all the states reachable
from program $\alpha$ are also reachable by operations of $\beta$. This allows
us to transfer safety properties between programs: safety properties about a
hybrid program also hold for all refinements of this program. In this paper,
we refine the RSS control envelopes to create deterministic controllers, which
are guaranteed to inherit the verified safety properties of the original
control envelopes.

###  2.4 ModelPlex

A proof of $\left[\alpha\right]P$ gives us confidence in the safety of the
model $\alpha$. The remaining question is now whether $\alpha$ represents a
useful real (driving) behavior, and whether an implementation is faithful to
the conditions of the verified model. ModelPlex [17] combines an offline
safety proof of the shape $A\rightarrow\left[\alpha\right]P$ with a runtime
monitor checking whether two concrete states $\omega,\nu$ are connected by a
program $\alpha$, i.e., semantically whether
$(\omega,\nu)\in\llbracket\alpha\rrbracket$. The safety proof witnesses that,
starting from states satisfying $A$, _all_ states reachable by model $\alpha$
satisfy $P$, while satisfying the runtime monitor witnesses that the two
concrete states $\omega,\nu$ are connected by the program $\alpha$, and so
state $\nu$ inherits the safety proof, i.e., $\nu\models P$ if $\omega\models
A$. The semantic runtime monitor is equivalently phrased in dL as a monitor
specification
$\langle\alpha\rangle\bigwedge_{x\in\textsf{BV}(\alpha)}(x=x^{+})$ with fresh
variables $x^{+}$ not occurring in $\alpha$ [17]. The dL monitor specification
allows ModelPlex, in contrast to online reachability analysis, to shift
computation offline by using theorem proving in order to translate a hybrid
systems model into a formula $\phi\in\mathcal{M}$ where $\mathcal{M}$ is the
set of quantifier-free, modality-free formulas over real arithmetic. Note that
the dL monitor specification is not provable offline, since it introduces
fresh variables $x^{+}$. Instead, the proof can be finished at runtime for two
concrete states (a state $\omega$ providing values for $x$ and a state $\nu$
providing values for $x^{+}$) by plugging in concrete measurements for all
variables of the runtime monitor. When a runtime monitor $\phi$ is satisfied
over states $\omega,\nu$, we write $(\omega,\nu)\in\llbracket\phi\rrbracket$.

##  3 Formalization of RSS Safety and Optimality

In this section we begin our case study on RSS. We first formalize the RSS
guidelines and verify the safety of the model. We then propose a way to verify
that the RSS model drives optimally. After this we create deterministic
controllers which we show are refinements of the general verified model and
utilize these to illustrate RSS behavior in simulation.

###  3.1 Formalization and Verification of RSS Safety

Models in the subsequent sections follow the same structure. To capture this
common structure, we introduce a safety template in Model 1. All subsequent
safety proofs for the longitudinal motion regardless of direction (same or
opposite direction of motion), follow this template, but with specific
formulas and programs to fill in the placeholders for the safety distance
safeDist, evolution domain constraint edc, free driving program freeDriving,
and evasion maneuver program properResponse.

Model 1 Model template for longitudinal motion collision avoidance
$\texttt{longitudinal}(\texttt{safeDist},\texttt{edc},\texttt{freeDriving},\texttt{properResponse})$
init $\displaystyle\left|\begin{aligned} &{\ltx@label{line:first-
init}}\quad\text{\scriptsize{1}}\quad\phantom{\land}~{}x_{1}\leq
x_{2}\land\texttt{safeDist}(v_{1},v_{2})\leq x_{1}-x_{2}\\\
&{\ltx@label{line:second-init}}\quad\text{\scriptsize{2}}\quad\land
0<a_{minBrake}<a_{maxBrake}\land 0<a_{maxAccel}\\\ &{\ltx@label{line:third-
init}}\quad\text{\scriptsize{3}}\quad\land\rho>0\\\ &{\ltx@label{line:last-
init}}\quad\text{\scriptsize{4}}\quad\land\texttt{edc}\end{aligned}\right.$
$\displaystyle\,\phantom{\bigl{|}}{\ltx@label{line:implication}}\quad\text{\scriptsize{5}}\quad\rightarrow$
$\displaystyle\,\phantom{\bigl{|}}{\ltx@label{line:first-
loopstart}}\quad\text{\scriptsize{6}}\quad\bigl{[}\bigl{(}$ ctrl
$\displaystyle\left|\begin{aligned} &{\ltx@label{line:first-
ctrl-1}}\quad\text{\scriptsize{7}}\quad\quad\phantom{\bigl{(}}\bigl{(}?\texttt{safeDist}(v_{1},v_{2})\leq
x_{2}-x_{1};\ (a_{1},a_{2})\coloneqq\texttt{freeDriving}\\\
&{\ltx@label{line:first-
ctrl-2}}\quad\text{\scriptsize{8}}\quad\quad\phantom{\bigl{(}\bigl{(}}\cup\,\\\
&{\ltx@label{line:first-
ctrl-3}}\quad\text{\scriptsize{9}}\quad\quad\phantom{\bigl{(}\bigl{(}}?\texttt{safeDist}(v_{1},v_{2})\geq
x_{2}-x_{1};\ (a_{1},a_{2})\coloneqq\texttt{properResponse}\bigl{)};\\\
&{\ltx@label{line:first-
ctrl-3}}\quad\text{\scriptsize{10}}\quad\quad\phantom{\bigl{(}}t\coloneqq
0;\end{aligned}\right.$ motion $\displaystyle\left|\begin{aligned}
&{\ltx@label{line:first-
ode}}\quad\text{\scriptsize{11}}\quad\phantom{\bigl{(}}\quad\\{x_{1}{{}^{\prime}}=v_{1},\,x_{2}{{}^{\prime}}=v_{2},\,v_{1}{{}^{\prime}}=a_{1},\,v_{2}{{}^{\prime}}=a_{2},\,t{{}^{\prime}}=1~{}\&~{}\texttt{edc}\land
t\leq\rho\\}\end{aligned}\right.$ safe
$\displaystyle\,\Bigl{|}{\ltx@label{line:first-
safe}}\quad\text{\scriptsize{12}}\quad\phantom{\Bigl{[}\,}\bigr{)}^{\ast}\bigr{]}\left(x_{1}\leq
x_{2}\right)$

The template defines preconditions (Line LABEL:line:first-
init–LABEL:line:last-init) under which all runs of the hybrid program in Line
LABEL:line:first-loopstart–LABEL:line:first-ode are expected to establish the
safety condition in Line LABEL:line:first-safe. The preconditions init set
parameter bounds for acceleration, deceleration, and reaction time $\rho$,
make sure that the cars are oriented correctly (driving in the expected
direction and car 1 is closer to the lane origin than car 2), and are at a
safe distance initially. The ctrl program implements the RSS control envelope
by setting the accelerations of the cars based on whether the distance between
them is safe: the nondeterministic choice in Line LABEL:line:first-ctrl-2
expresses the two options of executing freeDriving when at a safe distance and
evasion maneuver properResponse otherwise (we use notation
$(a_{1},a_{2})\coloneqq\texttt{prg}$ to emphasize that the program prg chooses
acceleration values $a_{1}$ and $a_{2}$). At the boundary, either choice is
possible. The motion program uses a differential equation to model the
continuous dynamics of driving in response to the chosen acceleration, modeled
through kinematics. Subsequent sections utilize this template to create
specific dL models to prove several aspects of RSS safety. First we start with
cars driving in the same longitudinal direction.

###  3.2 Longitudinal Safety

In the longitudinal direction, two cars may either drive in the same direction
(a follower car following at a safe distance behind a lead car), or in
opposite directions (a narrow road with two-way traffic, or a lead car backing
up). We describe both models as instances of the template Model 1, using the
sign of their respective longitudinal velocities to determine driving
direction. We analyze these driving situations in isolation, under the
assumption that a gear change when fully stopped is necessary to transition
between these situations, which also allows for switching between the formal
models that guide runtime safety.

##### Same Longitudinal Direction.

For two cars driving in the same longitudinal direction, RSS [24] defines a
safe distance between these cars with respect to their velocities: if the cars
were to drive with worst-case behavior (rear car with the maximum possible
acceleration and lead car with the maximum possible deceleration) for the
entire reaction time $\rho$, there would still be enough space for the rear
car to come to a full stop before the stopping point of the lead car, i.e.,
before colliding, see (1).

$\texttt{safeDist}_{s}\triangleq\max(v_{1}\rho+\frac{1}{2}a_{\text{maxAccel}}+\frac{(v_{1}+\rho
a_{\text{maxAccel}})^{2}}{2a_{\text{minBrake}}}-\frac{v_{2}^{2}}{2a_{\text{maxBrake}}},0)$
(1)

Whenever the cars are not satisfying the safe distance (1), the cars must
execute the proper response behavior as an evasion maneuver. In a leader and
follower setup, the follower car is responsible for not hitting the lead car.
As a consequence, the proper response allows the lead car to continue with any
acceleration or deceleration that does not exceed maximum braking, but
requires the follower car to decelerate at rate at least $a_{\text{minBrake}}$
[24]. We will now fill in Model 1 with formulas and programs (2)–(4), which
gives [13, Model 1].

$\displaystyle\texttt{freeDriving}_{s}$ $\displaystyle\triangleq
a_{1}\coloneqq\ast;?{-}a_{\text{maxBrake}}\leq a_{1}\leq a_{\text{maxAccel}};$
(2)
$\displaystyle\phantom{\triangleq}~{}~{}a_{2}\coloneqq\ast;?{-}a_{\text{maxBrake}}\leq
a_{2}\leq a_{\text{maxAccel}}$ $\displaystyle\texttt{properResponse}_{s}$
$\displaystyle\triangleq\bigl{(}a_{1}\coloneqq\ast;?a_{1}\leq-
a_{\text{minBrake}}\,\cup\,?v_{1}=0;a_{1}\coloneqq 0\bigl{)};$ (3)
$\displaystyle\phantom{\triangleq}~{}~{}\bigl{(}a_{2}\coloneqq*;?a_{2}\geq
a_{\text{maxBrake}}\,\cup\,?v_{2}=0;a_{2}\coloneqq 0\bigl{)}$
$\displaystyle\texttt{edc}_{s}$ $\displaystyle\triangleq v_{1}\geq 0\land
v_{2}\geq 0$ (4)

The definition of properResponse includes a choice of $a_{1,2}\coloneqq 0$ if
$v_{1,2}=0$ in order to allow time to pass in the ODE if one or both cars are
stopped.

######  Theorem 3.1 (Same Longitudinal Safety)

Model 1 with safeDist as per (1), freeDriving as per (2), properResponse as
per (3), and edc as per (4) is valid.

###### Proof

The key insight to this proof is the loop invariant $J\equiv x_{1}\leq
x_{2}\land x_{1}+\frac{v_{1}^{2}}{2a_{\text{minBrake}}}\leq
x_{2}+\frac{v_{1}^{2}}{2a_{\text{maxBrake}}}$ for proving inductive safety
using the loop invariant (LI) rule.

$\Gamma\vdash[\alpha*]P,\Delta\lx@proof@logical@and\Gamma\vdash J,\Delta
J\vdash PJ\vdash[\alpha]J$

The loop invariant $J$ summarizes that the cars maintain sufficient distance
to stop before colliding. The resulting real arithmetic proof obligations
become tractable by relating terms of the safe distance formula to terms in
the solution of the differential equations using a series of cuts. The details
of this proof are in Appendix 0.B. ∎

##### Opposite Longitudinal Direction.

The responsibility for collision avoidance is shared among the cars when they
drive towards each other (in opposite longitudinal direction on the same
lane). Similar to the same longitudinal direction, the safe distance to be
maintained in opposite direction driving considers the worst-case behavior for
the full reaction time $\rho$ followed by the collision avoidance proper
response. In opposite direction, the worst-case behavior is accelerating
towards each other with acceleration of $a_{\text{maxAccel}}$ for $a_{1}$ and
$-a_{\text{maxAccel}}$ for $a_{2}$ in the opposing direction. For two cars
driving with opposite longitudinal velocity signs, let $v_{1,\rho}=v1+\rho
a_{\text{maxAccel}}$ and $v_{2,\rho}=|v_{2}|+\rho a_{\text{maxAccel}}$. Then,
[24] defines the safe distance in longitudinal opposite direction as in (5).

$\texttt{safeDist}_{o}=\frac{v_{1}+v_{1,\rho}}{2}\rho+\frac{(v_{1,\rho})^{2}}{2a_{\text{minBrake}}}+\frac{v_{2}+v_{2,\rho}}{2}\rho+\frac{(v_{2,\rho})^{2}}{2a_{\text{minBrake}}}$
(5)

In this case, we assume the cars drive towards each other (car 1 driving
“forward”, i.e., away from the lane origin, car 2 driving “backward”, i.e.,
towards the lane origin), and want both of them to decelerate in the proper
response. This differs from the same longitudinal direction case, where only
the follower car reacts. In this case, the car driving forward reacts to
imminent collision with deceleration $a_{1}\leq-a_{\text{minBrake}}$, and the
car driving backward reacts with deceleration $a_{2}\geq a_{\text{minBrake}}$,
formalized in (6)–(8).

$\displaystyle\texttt{freeDriving}_{o}$ $\displaystyle\triangleq
a_{1}\coloneqq\ast;?-a_{\text{maxBrake}}\leq a_{1}\leq a_{\text{maxAccel}};$
(6)
$\displaystyle\phantom{\triangleq}~{}~{}a_{2}\coloneqq\ast;?-a_{\text{maxAccel}}\leq
a_{2}\leq a_{\text{maxBrake}}$ $\displaystyle\texttt{properResponse}_{o}$
$\displaystyle\triangleq\bigl{(}(a_{1}\coloneqq\ast;?a_{1}\leq-
a_{\text{minBrake}})\,\cup\,(?v_{1}=0;a_{1}\coloneqq 0)\bigl{)};$ (7)
$\displaystyle\phantom{\triangleq}~{}~{}\bigl{(}(a_{2}\coloneqq\ast;?a_{2}\geq
a_{\text{minBrake}})\,\cup\,(?v_{2}=0;a_{2}\coloneqq 0)\bigl{)}$
$\displaystyle\texttt{edc}_{o}$ $\displaystyle\triangleq v_{1}\geq 0\land
v_{2}\leq 0$ (8)

######  Theorem 3.2 (Opposite Longitudinal Safety)

Model 1 with $\texttt{safeDist}_{o}$ (5), $\texttt{freeDriving}_{o}$ (6),
$\texttt{properResponse}_{o}$ (7), and $\texttt{edc}_{o}$ (8) is valid.

###### Proof

The proof of this model follows a similar structure to the proof of Theorem
3.1 in the same longitudinal direction. The key insight again is a loop
invariant: $J\equiv x_{1}\leq x_{2}\land
x_{2}-\frac{v_{2}^{2}}{2a_{\text{minBrake}}}\geq
x_{1}+\frac{v_{1}^{2}}{2a_{\text{minBrake}}}$. Details of this proof are in
Appendix 0.B. ∎

###  3.3 Formalization and Verification of RSS Optimality

This section analyzes whether the safe distance is the minimal safe distance
needed to avoid collision. To this end, we encode the rationale behind
$\texttt{safeDist}_{s}$ and $\texttt{safeDist}_{o}$ as a hybrid program, and
ask if we were to follow a smaller safe distance, would there exist collisions
(which is a liveness property of the shape $P\rightarrow\langle\alpha\rangle
Q$). Recall that in both cases, the safe distance was determined by one
iteration of worst-case behavior of duration $\rho$, followed by executing the
proper response until both cars are stopped. Model 2 captures this intuition
behind the safe distance formulas in a hybrid program: first, the worst-case
behavior in Line LABEL:line:mindist-ctrl-1–LABEL:line:mindist-ode-1 is
executed, followed by any number and duration of proper response in Line
LABEL:line:mindist-proper-1–LABEL:line:mindist-ode-2. We show that starting
from an initial separation of $\texttt{safeDist}-\varepsilon$ for any
arbitrarily small $\varepsilon$, leads to collisions, i.e., we can reach
states in which $x_{1}>x_{2}$.

Model 2 Minimum Distance Same Direction init
$\displaystyle\left|\begin{aligned} &{\ltx@label{line:mindist-
init}}\quad\text{\scriptsize{1}}\quad\phantom{\land}\texttt{init}~{}\text{per
Model\,\ref{model:safetyProofTemplate}}\\\ &{\ltx@label{line:mindist-
epsilon}}\quad\text{\scriptsize{2}}\quad\land\varepsilon>0\\\
&{\ltx@label{line:mindist-
safedist}}\quad\text{\scriptsize{3}}\quad\land\texttt{safeDist}(v_{1},v_{2})-\varepsilon=x2-x1\rightarrow\\\
\end{aligned}\right.$
$\displaystyle\,\phantom{\bigl{|}}{\ltx@label{line:mindist-
loopstart}}\quad\text{\scriptsize{4}}\quad\bigl{<}\bigl{(}$ worst case
$\displaystyle\left|\begin{aligned} &{\ltx@label{line:mindist-
ctrl-1}}\quad\text{\scriptsize{5}}\quad\quad\phantom{\bigl{(}}\texttt{freeDriving};\\\
&{\ltx@label{line:mindist-
ctrl-2}}\quad\text{\scriptsize{6}}\quad\quad\phantom{\bigl{(}}t\coloneqq 0;\\\
&{\ltx@label{line:mindist-
ode-1}}\quad\text{\scriptsize{7}}\quad\phantom{\bigl{(}}\quad\\{x_{1}{{}^{\prime}}=v_{1},\,x_{2}{{}^{\prime}}=v_{2},\,v_{1}{{}^{\prime}}=a_{1},\,v_{2}{{}^{\prime}}=a_{2},\,t{{}^{\prime}}=1~{}\&~{}t\leq\rho\land\texttt{edc}\\}\end{aligned}\right.$
attempt evade $\displaystyle\left|\begin{aligned} &{\ltx@label{line:mindist-
proper-1}}\quad\text{\scriptsize{8}}\quad\phantom{\bigl{\langle}\bigl{(}~{}}\bigl{(}\texttt{properResponse;}\\\
&{\ltx@label{line:mindist-
ode-2}}\quad\text{\scriptsize{9}}\quad\phantom{\bigl{\langle}\bigl{(}\bigl{(}~{}}\\{x_{1}{{}^{\prime}}=v_{1},\,x_{2}{{}^{\prime}}=v_{2},\,v_{1}{{}^{\prime}}=a_{1},\,v_{2}{{}^{\prime}}=a_{2},\,t{{}^{\prime}}=1~{}\&~{}\texttt{edc}\\}\bigl{)}^{\ast}\end{aligned}\right.$
unsafe $\displaystyle\,\Bigl{|}{\ltx@label{line:mindist-
safe}}\quad\text{\scriptsize{10}}\quad\phantom{\Bigl{[}\,}\bigr{)}\bigr{>}\left(x_{1}>x_{2}\right)$

######  Theorem 3.3 (Same Longitudinal Optimality)

Model 2 with safeDist as per (1), freeDriving as per (2), properResponse as
per (3), and edc as per (4) is valid.

###### Proof

The proof strategy for this case simulates worst case behavior, choosing
$a_{1}=a_{\text{maxAccel}}$, $a_{2}=-a_{\text{minBrake}}$. Unrolling the loop
twice enables both cars to come to a complete stop and stay stopped by picking
$a_{1,2}=0$ once stopped. The choice of accelerations and loop unrolling
results in a collision. Note that two iterations are necessary in the case
that one car stops before the other one does, in order to allow for the
stopped car to change its deceleration to $a_{1,2}=0$ so that the differential
equation can be followed without violating the evolution domain constraint
$v_{1,2}\geq 0$ until the second car stops. The proof strategy again
simplifies arithmetic proof obligations by matching terms in the safe distance
formula with terms in the solution of the differential equation. Since the
distance between the cars is initially equal to safe distance reduced by an
arbitrarily small $\varepsilon$, using Theorem 3.1 we conclude that the
minimum safe distance between the two cars is characterized by (1). ∎

######  Theorem 3.4 (Opposite Longitudinal Optimality)

Model 2 with safeDist as per (5), freeDriving as per (6), properResponse as
per (7), and edc as per (8) is valid.

###### Proof

The proof strategy follows Lemma 3: we again choose worst case behaviors of
both cars, namely both cars driving toward each other at maximum acceleration.
∎

##  4 Refinement from dL to Python

The previous section proves correctness of control decisions in all situations
using dL under an assumed model of car dynamics. Increased model fidelity
often comes at the price of higher verification effort. For example, if we
wanted to consider tire friction, the dynamical motion model would no longer
have symbolic closed-form solutions, but would require advanced differential
equation reasoning [22]. In order to determine whether a model is sufficiently
realistic, and to test concrete implementation behavior in specific situations
(e.g., how abruptly a car would brake when encountering obstacles), we now
discuss refinement to deterministic implementation and simulation. This
provides a way of showing fidelity evidence for models to complement the
safety evidence, and to debug unverified models.

In formal models, nondeterminism is beneficial to model a large variety of
concrete implementations at an abstract level: nondeterministic choice of
acceleration in the controllers, nondeterministic number of loop iterations,
and nondeterministic duration of ODEs within each loop iteration capture
variation in total driving time and behavior. For execution and testing
purposes, deterministic behavior is beneficial to produce repeatable,
predictable, and comprehensible results. In order to generate control code,
integrate with testing, and ensure that a simulation of a system follows its
formal model, we select a deterministic subset of hybrid programs to introduce
an intermediate language that can then be directly compiled to Python. This
language, det-HP, supports assignment, deterministic choice (defined from
nondeterministic choice and tests), and loops (defined from nondeterministic
repetition and tests). The deterministic subset det-HP of hybrid programs is
generated by the grammar below, where $\theta$ is an arithmetic term in
$+,-,\cdot,/$ and $P$ is a quantifier-free formula in real arithmetic:

$\alpha,\beta\coloneqq
x\coloneqq\theta\mid\alpha;\beta\mid\underbrace{(?P;\alpha)\,\cup\,(?\lnot
P;\beta)}_{\text{if}~{}P~{}\alpha~{}\text{else}~{}\beta}\mid\underbrace{(?P;\alpha)^{\ast};?\lnot
P}_{\text{while}~{}P~{}\alpha}$

Starting from the formal models in Section 3, we need a way of resolving the
following points of nondeterminism when examining the behavior of these
models: First, the nondeterministic choice between free driving and proper
response at the boundary of the safe distance region needs to be resolved
(e.g., aggressively by favoring freeDriving, or conservatively by favoring
properResponse). Second, the nondeterministic choice of acceleration value in
both freeDriving and properResponse must be resolved with a deterministic
computation of acceleration within the acceleration bounds (e.g., a bang-bang
controller implementation will only choose the values of
$a_{\text{maxAccel}},a_{\text{minBrake}},$ and $a_{\text{maxBrake}}$). Third,
the nondeterministic duration of differential equations and hence the
nondeterministic control cycle time must be resolved (e.g., conservatively by
picking the maximum reaction time $\rho$, but not violating the remaining
conditions of the evolution domain constraint). Fourth, the nondeterministic
number of repetitions must be resolved (e.g., by picking a test length or a
finite amount of time to be followed). Note that the model parameter choices
and initial values for variables are not sources of nondeterminism as they are
symbolically defined and preset.

We now illustrate det-HP with a deterministic controller freeDriving-det that
chooses the same acceleration for every iteration of freeDriving below:

$\texttt{freeDriving-det}\triangleq a_{1}\coloneqq
a_{\text{maxAccel}};a_{2}\coloneqq-a_{\text{maxBrake}}$

In order to inherit Theorem 3.1, we use dRL to prove that freeDriving-det
reaches a subset of the states of $\texttt{freeDriving}_{s}$ (2).

######  Theorem 4.1 (Refinement)

The deterministic free driving controller refines the RSS free driving control
envelope, i.e., $\texttt{freeDriving-det}\leq\texttt{freeDriving}_{s}$ (2) is
valid under assumptions $\Gamma\equiv a_{\text{maxAccel}}>0\land
a_{\text{maxBrake}}>0$.

###### Proof

We prove by refinement in dRL. Let $P\equiv-a_{\text{maxBrake}}\leq a_{1}\leq
a_{\text{maxAccel}}$ and $Q\equiv-a_{\text{maxBrake}}\leq a_{2}\leq
a_{\text{maxAccel}}$:

$\Gamma\vdash a_{1}\coloneqq a_{\text{maxAccel}};a_{2}\coloneqq-
a_{\text{maxBrake}}\leq
a_{1}\coloneqq\ast;?P;a_{2}\coloneqq\ast;?Q\textbf{B1}\qquad\Gamma\vdash[a_{1}\coloneqq
a_{\text{maxAccel}};a_{2}\coloneqq-a_{\text{maxBrake}}]?\top\leq
P\Gamma,a_{1}=a_{\text{maxAccel}},a_{2}=-a_{\text{maxBrake}}\vdash?\top\leq
P\Gamma,a_{1}=a_{\text{maxAccel}},a_{2}=-a_{\text{maxBrake}}\vdash\top\rightarrow
P\ast$ $\textbf{B1}\Gamma\vdash\\{a_{1}\coloneqq
a_{\text{maxAccel}};a_{2}\coloneqq-
a_{\text{maxBrake}}\\}\leq\\{a_{1}\coloneqq\ast;a_{2}\coloneqq\ast\\}\Gamma\vdash
a_{1}\coloneqq a_{\text{maxAccel}}\leq a_{1}\coloneqq\ast\ast\ \
\Gamma\vdash[a_{1}\coloneqq a_{\text{maxAccel}}](a_{2}\coloneqq-
a_{\text{maxBrake}}\leq
a_{2}\coloneqq\ast)\Gamma,a_{1}=a_{\text{maxAccel}}\vdash a_{2}\coloneqq-
a_{\text{maxBrake}}\leq a_{2}\coloneqq\ast\ast$

In this proof we utilize the test, sequential and assignment rules [14] to
show that each step that the deterministic controller takes is within the
bounds that the nondeterministic controller sets. The main insight is that
deterministic assignments are refinements of unguarded nondeterministic
assignments. ∎

The intermediate language det-HP serves as a stepping stone towards
compilation to Python. We introduce the compilation rules in Fig. 2, where we
use the following subset of the Python expression and statement syntax [9]
(for simplicity, we will ignore the difference between $\mathbb{R}$ and Float,
which can be addressed with interval arithmetic [3]):

pexpr $\displaystyle\coloneqq\text{true}\mid\text{false}\mid
z\in\mathbb{Z}\mid x\in\text{Float}$
$\displaystyle\phantom{\coloneqq}\mid-\text{pexpr}\mid\text{pexpr}\circ\text{pexpr}\mid\text{pexpr}\bullet\text{pexpr}$
$\displaystyle\phantom{\coloneqq}\mid\texttt{not}~{}\text{pexpr}\mid\text{pexpr}~{}\texttt{and}~{}\text{pexpr}\mid\text{pexpr}~{}\texttt{or}~{}\text{pexpr}$
pprg
$\displaystyle\coloneqq\texttt{x=}\text{pexpr}\mid\texttt{if}~{}\text{pexpr}\text{:}~{}\text{pprg}~{}\texttt{else:}~{}\text{pprg}\mid\texttt{while}~{}\text{pexpr}\texttt{:}~{}\text{pprg}\mid\text{pprg};\text{pprg}$

The simplified syntax uses arithmetic operators
$\circ\in\\{\texttt{+},\texttt{-},\texttt{*},\texttt{/},\texttt{**}\\}$ and
comparison operators
$\bullet\in\\{\texttt{<},\texttt{<=},\texttt{>=},\texttt{>},\texttt{==},\texttt{!=}\\}$.

Programs $\displaystyle\textsf{Py}(x\coloneqq\theta)$
$\displaystyle\vartriangleright\textsf{Py}(x)\texttt{=}\textsf{Py}(\theta)$
$\displaystyle\textsf{Py}(?P;\alpha\,\cup\,?\lnot P;\beta)$
$\displaystyle\vartriangleright\texttt{if}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else:}~{}\textsf{Py}(\beta)$
$\displaystyle\textsf{Py}(\\{?P;\alpha\\}^{\ast};?\lnot P)$
$\displaystyle\vartriangleright\texttt{while}~{}\textsf{Py}(P):~{}\textsf{Py}(\alpha)~{}\texttt{else
pass}$ Arithmetic $\displaystyle\textsf{Py}(z)$
$\displaystyle\vartriangleright\texttt{z}$ for number literal $z$
$\displaystyle\textsf{Py}(x)$ $\displaystyle\vartriangleright\texttt{x}$ for
variable $x$ $\displaystyle\textsf{Py}(\theta+\eta)$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{+}\textsf{Py}(\eta)$
$\displaystyle\textsf{Py}(\theta-\eta)$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{-}\textsf{Py}(\eta)$
$\displaystyle\textsf{Py}(\theta\cdot\eta)$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{*}\textsf{Py}(\eta)$
$\displaystyle\textsf{Py}(\frac{\theta}{\eta})$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{/}\textsf{Py}(\eta)$
$\displaystyle\textsf{Py}(\theta^{\eta})$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{**}\textsf{Py}(\eta)$
Boolean $\displaystyle\textsf{Py}(\top)$
$\displaystyle\vartriangleright\texttt{True}$ $\displaystyle\textsf{Py}(\bot)$
$\displaystyle\vartriangleright\texttt{False}$
$\displaystyle\textsf{Py}(\theta<\eta)$
$\displaystyle\vartriangleright\textsf{Py}(\theta)\texttt{<}\textsf{Py}(\eta)$
$\displaystyle\text{similar for}~{}\leq,=,\neq,\geq,>$
$\displaystyle\textsf{Py}(\lnot P)$
$\displaystyle\vartriangleright\texttt{not}~{}\textsf{Py}(P)$
$\displaystyle\textsf{Py}(P\land Q)$
$\displaystyle\vartriangleright\textsf{Py}(P)~{}\texttt{and}~{}\textsf{Py}(Q)$
$\displaystyle\textsf{Py}(P\lor Q)$
$\displaystyle\vartriangleright\textsf{Py}(P)~{}\texttt{or}~{}\textsf{Py}(Q)$
Figure 2: det-HP to Python compilation rules

The compilation from deterministic hybrid programs to the restricted Python
syntax preserves safety, see Lemmas 2–4 and Theorem 4. We abbreviate
arithmetic evaluation [9] as
$\textsf{eval}(\textsf{Py}(\theta))_{\nu}\rightarrow u$ to real value $u$ and
Boolean evaluation as $\nu(\textsf{bool}~{}\textsf{Py}(\theta))\rightarrow v$
to Boolean value $v$.

[end,restate,category=compilation,text link=]lemma[Term compilation is
correct] Assuming Float=$\mathbb{R}$, terms evaluate equivalently, i.e., if
$\textsf{eval}(\textsf{Py}(\theta))_{\nu}\rightarrow u$ then
$\nu\llbracket\theta\rrbracket=u$.

###### Proof

By structural induction over dL terms, see Appendix 0.A. ∎

Structural induction over dL terms as follows:

Number literals

$\textsf{eval}(n)_{\nu}\rightarrow n$ for all states $\nu$ and $\nu\llbracket
n\rrbracket=n$

Variables

$\textsf{eval}(v)_{\nu}\rightarrow\nu(v)$ and dL variable valuation
$\nu\llbracket v\rrbracket=\nu(v)$

Negation

$\textsf{eval}(-\theta)_{\nu}\rightarrow-c$ for
$\textsf{eval}(\theta)_{\nu}=c$ and dL negation
$\nu\llbracket-\theta\rrbracket=-\nu\llbracket\theta\rrbracket$

Arithmetic operator

for terms $\theta,\eta$ and arithmetic operator $\sim$, in Python
$\textsf{eval}(\theta\sim\eta)_{\nu}\rightarrow c\sim d$ for
$\textsf{eval}(\theta)_{\nu}\rightarrow c$ and
$\textsf{eval}(\eta)_{\nu}\rightarrow d$ and dL
$\nu\llbracket\theta\sim\eta\rrbracket=\nu\llbracket\theta\rrbracket\sim\nu\llbracket\eta\rrbracket$
∎

[end,restate,category=compilation,text link=]lemma[Formula compilation is
correct] Formulas evaluate equivalently, i.e., $\nu\models\phi$ iff
$\nu(\textsf{bool}~{}\textsf{Py}(\phi))\rightarrow\texttt{true}$.

###### Proof

By structural induction over dL formulas, see Appendix 0.A. ∎

Structural induction over dL formulas as follows:

Comparisons

for terms $\theta,\eta$ and comparison operators
$\sim\in\\{<,\leq,=,\neq,\geq,>\\}$, in Python
$\nu(\textsf{bool}~{}\textsf{Py}(\theta<\eta))\rightarrow c~{}\texttt{<}~{}d$
(accordingly for $\leq,=\neq,\geq,>$) for
$\textsf{eval}(\textsf{Py}(\theta))_{\nu}\rightarrow c$ and
$\textsf{eval}(\textsf{Py}(\eta))_{\nu}\rightarrow d$ and in dL
$\nu\llbracket\theta\sim\eta\rrbracket=\nu\llbracket\theta\rrbracket\sim\nu\llbracket\eta\rrbracket$

Logical connectives

for formulas $\phi,\psi$ and operators $\lnot,\land,\lor$, in
Python$\nu(\textsf{bool}~{}\textsf{Py}(\phi\land\psi))\rightarrow
p~{}\texttt{and}~{}q$ for $\nu(\textsf{bool}~{}\textsf{Py}(\phi))\rightarrow
p$ and $\nu(\textsf{bool}~{}\textsf{Py}(\psi))\rightarrow q$ and in dL
$\nu\llbracket\phi\land\psi\rrbracket=\nu\llbracket\phi\rrbracket\land\nu\llbracket\psi\rrbracket$,
accordingly for $\lnot,\lor$ ∎

[end,restate,category=compilation,text link=]thm[Compilation of det-HP to
Python is correct] All states reachable with the compiled Python program are
also reachable by the source HP program, i.e.
$(\textsf{Py}(\alpha),\nu)\rightarrow(\perp,\omega)$ then
$(\nu,\omega)\in\llbracket\alpha\rrbracket$.

###### Proof

By structural induction over hybrid programs, see Appendix 0.A. ∎

By structural induction over hybrid programs. Recall that states in Python [9]
have the form $\nu=(S,H,M)$ (each mapping variables to values), which for
simplicity we restrict to programs operating only on the stack. As a result,
we consider states in Python $S:\mathcal{V}\rightarrow\mathbb{R}$ the same as
states in dL mapping variables to reals
$\nu:\mathcal{V}\rightarrow\mathbb{R}$. The induction base case is
$(\perp,\nu)$ so $(\nu,\nu)\in\llbracket?\top\rrbracket$ and induction
hypothesis $(\textsf{Py}(\alpha),\nu)\rightarrow(\perp,\omega)$ then
$(\nu,\omega)\in\llbracket\alpha\rrbracket$.

If statement $\textsf{Py}(\bm{?P;\alpha\,\cup\,?\lnot
P;\beta})\vartriangleright\texttt{if}~{}\textsf{Py}(\bm{P})\texttt{:}~{}\textsf{Py}(\bm{\alpha})~{}\texttt{else:}~{}\textsf{Py}(\bm{\beta})$

Let$(\texttt{if}~{}\textsf{Py}(P)\texttt{:}\textsf{Py}(\alpha)~{}\texttt{else:}~{}\textsf{Py}(\beta),\nu)\rightarrow(\perp,\omega)$.
We have to show that $(\nu,\omega)\in\llbracket?P;\alpha\,\cup\,?\lnot
P;\beta\rrbracket$.

Case $\bm{\nu\models P}$:

We have $\nu(\textsf{bool}~{}\textsf{Py}(P))\xrightarrow{}\texttt{true}$ by
bool-eval and bool-true [9, p. 83] and thus
$(\nu,\nu)\in\llbracket?P\rrbracket$ by Lemma 4 and dL. By rule if-true
therefore
$(\texttt{if}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else:}~{}\textsf{Py}(\beta),\nu)\rightarrow(\textsf{Py}(\alpha),\nu)$
and in turn $(\textsf{Py}(\alpha),\nu)\rightarrow(\perp,\omega)$. Now
$(\nu,\omega)\in\llbracket\alpha\rrbracket$ by I.H. and thus
$(\nu,\omega)\in\llbracket?P;\alpha\rrbracket$ by dL.

Case $\bm{\nu\not\models P}$:

We have $\nu(\textsf{bool}~{}\textsf{Py}(P))\xrightarrow{}\texttt{false}$ by
bool-eval and bool-false and thus $(\nu,\nu)\in\llbracket?\lnot P\rrbracket$
by Lemma 4 and dL. By rule if-false therefore
$(\texttt{if}~{}\textsf{Py}(P)~{}\textsf{Py}(\alpha)~{}\texttt{else:}\textsf{Py}(\beta),\nu)\rightarrow(\textsf{Py}(\beta),\nu)$
and in turn $(\textsf{Py}(\beta),\nu)\rightarrow(\perp,\omega)$. Now
$(\nu,\omega)\in\llbracket\beta\rrbracket$ by I.H. and thus
$(\nu,\omega)\in\llbracket?\neg P;\beta\rrbracket$ by dL.

Now we have that either $(\nu,\omega)\in\llbracket?P;\alpha\rrbracket$ or
$(\nu,\omega)\in\llbracket?\lnot P;\beta\rrbracket$ and thus we conclude
$(\nu,\omega)\in\llbracket?P;\alpha\,\cup\,?\lnot P;\beta\rrbracket$ by dL.

Sequential composition
$\textsf{Py}(\bm{\alpha;\beta})\vartriangleright\textsf{Py}(\bm{\alpha})\texttt{;}\textsf{Py}(\bm{\beta})$

We have to show $(\nu,\omega)\in\llbracket\alpha;\beta\rrbracket$. Let
$(\textsf{Py}(\alpha;\beta),\nu)\rightarrow(\perp,\omega)$. By sequence-first
and sequence-elim [9, p. 91], there exists state $\mu$ such that
$(\textsf{Py}(\alpha),\nu)\rightarrow(\perp,\mu)$ and
$(\textsf{Py}(\beta),\mu)\rightarrow(\perp,\omega)$. This means that
$(\nu,\mu)\in\llbracket\alpha\rrbracket$ and
$(\mu,\omega)\in\llbracket\beta\rrbracket$ by I.H and we conclude
$(\nu,\omega)\in\llbracket\alpha;\beta\rrbracket$ by dL.

Assignment
$\textsf{Py}(\bm{x\coloneqq\theta})\vartriangleright\textsf{Py}(\bm{x})\bm{=}\textsf{Py}(\bm{\theta})$

We have to show that $(\nu,\omega)\in\llbracket x\coloneqq\theta\rrbracket$.
From assign-exec we know
$(\textsf{Py}(x)=\textsf{Py}(\theta),\nu)\rightarrow(\perp,\nu[x\mapsto u])$
for $\textsf{eval}(\textsf{Py}(\theta))_{\nu}\rightarrow u$. As a result,
there is some state $\omega$ that agrees with all values of $\nu$ except for
the value of $\textsf{Py}(x)$, so
$\omega(\textsf{Py}(x))=\nu\llbracket\textsf{Py}(\theta)\rrbracket$ and we
conclude $(\nu,\omega)\in\llbracket x\coloneqq\theta\rrbracket$ by dL from
Lemma 2.

While loop $\textsf{Py}(\bm{(?P;\alpha)^{\ast};?\neg
P})\vartriangleright\texttt{\bf
while}~{}\textsf{Py}(\bm{P}):~{}\textsf{Py}(\bm{\alpha})~{}\texttt{\bf else
pass}$

We have to show that $(\nu,\omega)\in\llbracket(?P;\alpha)^{\ast};?\lnot
P\rrbracket$. Let

$(\texttt{while}~{}\textsf{Py}(P):~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\nu)\rightarrow(\perp,\omega)\enspace.$

We prove by induction on the loop iterations. The induction base case is
$\nu\models\lnot P$ and therefore
$(\texttt{while}~{}\textsf{Py}(P):~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\nu)\rightarrow(\perp,\nu)$ by while-eval [9, p. 94], while-false [9, p.
94], and pass [9, p. 92] and in turn $(\nu,\nu)\in\llbracket?\top\rrbracket$.
Assume
$(\texttt{while}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\nu)\rightarrow(\perp,\mu)$ then
$(\nu,\mu)\in\llbracket(?P;\alpha)^{\ast};?\lnot P\rrbracket$.

Case $\bm{\mu\models P}$

We have $\mu(\textsf{bool}~{}\texttt{true})$ by while-eval. Then,

$(\texttt{while}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\mu)\rightarrow\\\
(\textsf{Py}(\alpha);\texttt{while}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\mu)$

by while-true. By sequential composition there exists state $\tilde{\mu}$ such
that $(\textsf{Py}(\alpha),\mu)\rightarrow(\perp,\tilde{\mu})$ and
$(\texttt{while}~{}\textsf{Py}(P)\texttt{:}~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\tilde{\mu})\rightarrow(\perp,\omega)$. Now
$(\mu,\tilde{\mu})\in\llbracket\alpha\rrbracket$ by outer I.H. and
$(\tilde{\mu},\omega)\in\llbracket(?P;\alpha)^{\ast};?\lnot P\rrbracket$ by
inner I.H. and we conclude $(\nu,\omega)\in\llbracket(?P;\alpha)^{\ast};?\lnot
P\rrbracket$ by dL.

Case $\bm{\mu\not\models P}$

Then $(\texttt{while}~{}\textsf{Py}(P):~{}\textsf{Py}(\alpha)~{}\texttt{else
pass},\mu)\rightarrow(\texttt{pass},\mu)$ by while-eval and while-false and in
turn $(\texttt{pass},\mu)\rightarrow(\perp,\omega)$ by pass. Now
$(\mu,\omega)\in\llbracket(?P;\alpha)^{\ast};?\lnot P\rrbracket$ by outer I.H.
and we conclude $(\nu,\omega)\in\llbracket(?P;\alpha)^{\ast};?\lnot
P\rrbracket$ by inner I.H. ∎

Theorem 4 ensures that any state reached in a compiled Python program will
also be reachable in the source det-HP program. Together with the refinement
step from our original model, we therefore know that any counterexample found
in the compiled simulation will also be a counterexample of the original
formal dL model.

##  5 Testing and Monitoring by Example

The previous sections introduced safety verification and refinement proofs
that eliminate the need for correctness testing. These two steps, if
completed, assure that the system is safe under all implementations. In this
section, we consider testing and simulation as a method to provide insight for
correcting the formal model and/or an implementation when either of these
steps fails, and as a way to assess the fidelity of the formal model and
experiment with model parameter selection once the proofs are completed.

###  5.1 Monitor Structure

In order to assess whether the simulation and the formal model agree and flag
differences, we utilize ModelPlex [17]. ModelPlex monitors are formally
verified and derived automatically from a hybrid systems model; they flag
whenever states encountered at runtime (e.g., in simulation) disagree with the
expectations of the formal model. For this, the monitors collect the
relationship between starting and final states along all possible execution
paths of the formal model. For example, a monitor derived from the discrete
statements of Model 1 as instantiated in Theorem 3.1 is illustrated below
(variables of the initial state are $x,y,z$, variables of the final state are
$x^{+},y^{+},z^{+}$).

$\displaystyle(\texttt{safeDist}_{s}(v_{1},v_{2})\leq x_{2}-x_{1}\land-
a_{\text{maxBrake}}\leq a_{1}^{+}\leq a_{\text{maxAccel}}$
$\displaystyle\qquad\land-a_{\text{maxBrake}}\leq a_{2}^{+}\leq
a_{\text{maxAccel}}\land t^{+}=0\land\texttt{edc}_{s})$ $\displaystyle\lor$
$\displaystyle(\texttt{safeDist}_{s}(v_{1},v_{2})\geq
x_{2}-x_{1}\land(a_{1}^{+}\leq-a_{\text{minBrake}}\lor(v_{1}=0\land
a_{1}^{+}=0))$ $\displaystyle\qquad\land(a_{2}^{+}\geq
a_{\text{maxBrake}}\lor(v_{2}=0\land a_{2}^{+}=0))\land
t^{+}=0\land\texttt{edc}_{s})$

###  5.2 Examples of Monitor Usage

##### Monitoring for faulty implementation.

Our first example illustrates the use of testing and monitoring when the
refinement proof cannot be completed due to an incorrect implementation. With
user-defined test scenarios, ModelPlex monitors in simulation highlight the
vulnerabilities of the controller implementation as an intermediate step
towards finding implementation fixes and completing the refinement proof. In
this case, counterexamples found in simulation represent control decisions of
the unverified controller implementation that violate the expectations of the
formal model.

Figure 3: Leader-follower same direction test scenario, with rear car control
implementation violating the conditions of RSS. Plots from top to bottom are:
ModelPlex monitor verdict, car positions $x_{1},x_{2}$, car speeds
$v_{1},v_{2}$, and accelerations $a_{1},a_{2}$.

In Fig. 3, a front and a rear car are driving in the same direction, while the
rear car follows a faulty controller. The user-defined test scenario is an
example of a boundary test by picking worst case behavior where the rear car
is accelerating at maximum acceleration whenever allowed by its control
guards. The ModelPlex monitor derived from Model 1 with the formulas and
programs of Theorem 3.1 fails at the point of violating RSS: executing the
proper response instead of the faulty controller at time time of the monitor
alarm would have prevented collision, but following the faulty controller
makes the rear car exceed the front car’s position (i.e., cause a collision).
The monitor verdict (“ModelPlex ID” in Fig. 3) flags the violated condition of
the monitor, which directly relates to a path through the formal model: the
faulty controller allowed to continue accelerating forward for one more time
step when it should have been following the proper response already. In this
case, a boundary test reveals the controller implementation flaw, but other
implementation bugs are more subtle and require extensive search. For future
work, we envision integration of monitors with falsification techniques.

##### Monitoring for modeling flaws.

With a setup similar to monitoring for faulty implementations, we address
modeling flaws in unverified models. User-defined test scenarios allow us to
examine the behavior of the formal model through monitors: the formal model is
faulty when finding scenarios that end in collision without a prior ModelPlex
monitor alarm. In this case, the insight for fixing the bug is not merely the
(missing) monitor alarm itself, but the sequence of control actions that lead
up to the collision.

##### Parameter selection.

The last example we include illustrates how to use tests for parameter
selection once the formal model and the refinement to a concrete controller
implementation is proved. The concrete choices for the symbolic parameters,
such as $a_{\text{maxBrake}}$, $a_{\text{minBrake}}$, $a_{\text{maxAccel}}$,
and $\rho$, heavily influence the specific behavior of the controller
implementation. Simulation with specific parameter choices is a useful
technique to inspect the expected real-world behavior, and completes the
circle of interaction between formal methods and testing. Formal methods
guarantee correctness in a model of physics, refinement proofs and correct
compilation guarantee correctness of implementations, and simulation and
testing allow for inspecting the fidelity of the formal model and the concrete
behavior of the implementation under specific parameter choices.

Figure 4: Car behavior in opposite direction model at $\rho=1$ (left) and
$\rho=6$ (right).

In Fig. 4 we consider parameter selection and its effect on the behavior of
cars in the opposite direction scenario. The controllers of both cars in free
driving accelerate towards each other at maximum acceleration and in proper
response they both brake at minimum rate. With a “short” response horizon of
$\rho=1$, the final distance between the cars once fully stopped is much lower
than when a response $\rho=6$.

##  6 Related Work

RSS introduced in [24] has been deployed by the Mobileye research group as the
basis for their self-driving car and analyzed extensively from different
aspects for its safety and reliablity: [18] considers parameter analysis and
concrete behavior of RSS on German highways; [10] extends RSS fidelity by
applying Newtonian mechanics to analyze car behavior on slopes and in varying
road conditions.

Related work within formal verification of driving models is extensive: [16]
utilize a formula equivalent to the same direction safe distance formula
introduced by RSS for an adaptive cruise control system, [15] analyze
collision avoidance while following Dubin’s paths, [4] and [11] formally
verify waypoint navigation, [1] verify swerving maneuvers to avoid collision,
[23] develops a formally verified motion planner, [2, 12] use reachability
analysis in highway settings and introduce a toolbox to create simulated
driving environments to determine reachable sets, [8] is close to our work in
that it uses falsification to find mistakes in motion plans of autonomous
vehicles. We complement these approaches by providing proofs of optimality of
the RSS safety conditions and proofs of opposite driving direction, combined
with refinement proofs and correct compilation to Python for testing.

##  7 Conclusion and Future Work

In this paper we formalized and proved safety and optimality of the
Responsibility-Sensitive Safety control envelopes in both longitudinal
directions. The safety proofs discover loop invariants, which concisely
document design properties of the system. These properties of the longitudinal
cases do not transfer to the lateral case in a straightforward way, because
velocity direction changes do not require an intermediate stop such as a gear
change; formalizing and verifying the lateral case is an area of future
research.

To complement the safety guarantees of formal verification with practical
tools to test and debug unverified models, as well as to assess the fidelity
of verified models in specific driving situations and under specific parameter
choices, we introduce refinement proofs and correct compilation from
nondeterministic models to deterministic implementations in Python. Formal
methods guarantee correctness in a model of physics, refinement proofs and
correct compilation guarantee correctness of implementations, and simulation
and testing allow for inspecting the fidelity of the formal model and the
concrete behavior of the implementation under specific parameter choices.
Future research includes combination with falsification methods to provide a
systematic automated approach to testing of unverified models in differential
dynamic logic.

#### Acknowledgements

This material is based upon work supported by the National Science Foundation
under Grant No. CCF2220311.

## References

  * [1] Abhishek, A., Sood, H., Jeannin, J.: Formal verification of swerving maneuvers for car collision avoidance. In: 2020 American Control Conference, ACC 2020, Denver, CO, USA, July 1-3, 2020. pp. 4729–4736 (2020). https://doi.org/10.23919/ACC45564.2020.9147679
  * [2] Althoff, M., Koschi, M., Manzinger, S.: Commonroad: Composable benchmarks for motion planning on roads. In: 2017 IEEE Intelligent Vehicles Symposium (IV). pp. 719–726 (2017). https://doi.org/10.1109/IVS.2017.7995802
  * [3] Bohrer, R., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: Veriphy: verified controller executables from verified cyber-physical system models. In: PLDI. pp. 617–630 (2018). https://doi.org/10.1145/3192366.3192406
  * [4] Bohrer, R., Tan, Y.K., Mitsch, S., Sogokon, A., Platzer, A.: A formal safety net for waypoint-following in ground robots. IEEE Robotics Autom. Lett. 4(3), 2910–2917 (2019). https://doi.org/10.1109/LRA.2019.2923099
  * [5] Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential 5(1), 29–35. https://doi.org/10.1016/S0747-7171(88)80004-X
  * [6] Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: Keymaera X: an axiomatic tactical theorem prover for hybrid systems. In: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. pp. 527–538 (2015). https://doi.org/10.1007/978-3-319-21401-6_36
  * [7] Gallicchio, J., Tan, Y.K., Mitsch, S., Platzer, A.: Implicit definitions with differential equations for keymaera x. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Automated Reasoning. pp. 723–733. Springer International Publishing, Cham (2022)
  * [8] Klischat, M., Althoff, M.: Falsifying motion plans of autonomous vehicles with abstractly specified traffic scenarios. IEEE Trans. Intell. Veh. 8(2), 1717–1730 (2023). https://doi.org/10.1109/TIV.2022.3191179
  * [9] Kohl, M.A.: An Executable Structural Operational Formal Semantics for Python. Ph.D. thesis (2020)
  * [10] Koopman, P., Osyk, B., Weast, J.: Autonomous vehicles meet the physical world: Rss, variability, uncertainty, and proving safety. In: Romanovsky, A., Troubitsyna, E., Bitsch, F. (eds.) Computer Safety, Reliability, and Security. pp. 245–253. Springer International Publishing, Cham (2019)
  * [11] Kopylov, A., Mitsch, S., Nogin, A., Warren, M.: Formally verified safety net for waypoint navigation neural network controllers. In: Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. pp. 122–141 (2021). https://doi.org/10.1007/978-3-030-90870-6_7
  * [12] Liu, E.I., Würsching, G., Klischat, M., Althoff, M.: Commonroad-reach: A toolbox for reachability analysis of automated vehicles. In: 25th IEEE International Conference on Intelligent Transportation Systems, ITSC 2022, Macau, China, October 8-12, 2022. pp. 2313–2320 (2022). https://doi.org/10.1109/ITSC55140.2022.9922232
  * [13] Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: 2011 14th International IEEE Conference on Intelligent Transportation Systems (ITSC). pp. 1181–1186. IEEE. https://doi.org/10.1109/ITSC.2011.6083138
  * [14] Loos, S.M., Platzer, A.: Differential refinement logic. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. pp. 505–514 (2016). https://doi.org/10.1145/2933575.2934555
  * [15] Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robotics Res. 36(12), 1312–1340 (2017). https://doi.org/10.1177/0278364917733549
  * [16] Mitsch, S., Loos, S.M., Platzer, A.: Towards formal verification of freeway traffic control. In: 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, ICCPS 2012, Beijing, China, April 17-19, 2012. pp. 171–180 (2012). https://doi.org/10.1109/ICCPS.2012.25
  * [17] Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models 49(1), 33–74. https://doi.org/10.1007/s10703-016-0241-z
  * [18] Naumann, M., Wirth, F., Oboril, F., Scholl, K., Elli, M.S., Alvarez, I., Weast, J., Stiller, C.: On responsibility sensitive safety in car-following situations - a parameter analysis on german highways. In: 2021 IEEE Intelligent Vehicles Symposium (IV). pp. 83–90. https://doi.org/10.1109/IV48863.2021.9575420
  * [19] Platzer, A.: Differential dynamic logics: Automated theorem proving for hybrid systems 24(1), 75–77. https://doi.org/10.1007/s13218-010-0014-6
  * [20] Platzer, A.: The complete proof theory of hybrid systems. In: LICS. pp. 541–550. IEEE (2012). https://doi.org/10.1109/LICS.2012.64
  * [21] Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–265 (2017). https://doi.org/10.1007/s10817-016-9385-1
  * [22] Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM 67(1), 6:1–6:66 (2020). https://doi.org/10.1145/3380825
  * [23] Rizaldi, A., Immler, F., Schürmann, B., Althoff, M.: A formally verified motion planner for autonomous vehicles. In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. pp. 75–90 (2018). https://doi.org/10.1007/978-3-030-01090-4_5
  * [24] Shalev-Shwartz, S., Shammah, S., Shashua, A.: On a formal model of safe and scalable self-driving cars
  * [25] Tarski, A.: A decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. pp. 24–84. Texts and Monographs in Symbolic Computation, Springer. https://doi.org/10.1007/978-3-7091-9459-1_3

##  Appendix 0.A Correctness of det-HP to Python Compilation

For the proof of det-HP compilation we utilize the dL semantics described in
[19]. We also use the subset in Fig. 5 of the semantic rules found in [9].

$(\texttt{if True then a else b})\rightarrow a$

$(\texttt{if False then a else b})\rightarrow b$

$[\texttt{False}]c\texttt{while P: a else b}\rightarrow b$

$[\texttt{True}]c\texttt{while P: a else b}\rightarrow[\alpha]\ a\ \
\texttt{while P: a else b}$

$(\texttt{s ; s'})\rightarrow(\texttt{t ; s'})\texttt{s ; t}$

$(\perp\texttt{; s})\rightarrow\texttt{s}$

$(\texttt{x = u},\nu)\rightarrow(\perp,\nu[x\mapsto u])$

Figure 5: Semantic rules of Python [9]

[compilation]

##  Appendix 0.B Case Study Details

###  0.B.1 Same Longitudinal Direction Safety

In this section we describe in detail the strategy behind proving the safety
of the same longitudinal direction RSS model. Since the basis of this model is
a loop, we utilize a loop invariant to aid in proving this. The invariant $J$
expresses that at each iteration of the loop in Model 1, we know two facts:
(1) that car 1 stays behind car 2 and (2) that the latest stopping position of
car 1 when applying $-a_{minBrake}$ deceleration is behind the earliest
stopping position of car 2 when applying $-a_{maxBrake}$ deceleration.
Formally, our loop invariant is

$J\equiv x_{1}\leq x_{2}\land x_{1}+\frac{v_{1}^{2}}{2a_{\text{minBrake}}}\leq
x_{2}+\frac{v_{1}^{2}}{2a_{\text{maxBrake}}}$

The induction step of the proof requires us to show
$J\rightarrow\left[\text{\ref{model:safetyProofTemplate}}\right]J$. Our proof
proceeds by cases according to Model 1: $\texttt{safeDist}(v_{1},v_{2})\leq
x_{2}-x_{1}$ and $\texttt{safeDist}(v_{1},v_{2})\geq x_{2}-x_{1}$.

Case $\texttt{safeDist}(v_{1},v_{2})\leq x_{2}-x_{1}$

We need to show the free driving case

$\displaystyle J\rightarrow[$
$\displaystyle?\texttt{safeDist}(v_{1},v_{2})\leq x_{2}-x_{1};$
$\displaystyle(a_{1},a_{2})\coloneqq\texttt{freeDriving};$ $\displaystyle
t\coloneqq 0;$ $\displaystyle\text{motion}]J\enspace.$

In this case, we know from freeDriving that the chosen acceleration for both
cars is within the overall bounds, which include positive and negative values
between the maximum braking parameter and maximum acceleration parameter. We
recall the fact that the differential equation can run for any amount of time
such that the evolution domain constraints are satisfied, i.e., before
exceeding time $\rho$. We solve the differential equation to obtain the usual
kinematic constraints:

$\displaystyle\tilde{x}_{1}$
$\displaystyle=x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}$
$\displaystyle\tilde{x}_{2}$
$\displaystyle=x_{2}+v_{2}t+\frac{1}{2}a_{2}t^{2}$
$\displaystyle\tilde{v}_{1}$ $\displaystyle=v_{1}+a_{1}t\land\tilde{v}_{1}\geq
0$ $\displaystyle\tilde{v}_{2}$
$\displaystyle=v_{2}+a_{2}t\land\tilde{v}_{2}\geq 0$ $\displaystyle 0\leq
t\leq\rho$

and thus we need to show

$\displaystyle\phantom{\land~{}}\tilde{J}=x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}\leq
x_{2}+v_{2}t+\frac{1}{2}a_{2}t^{2}$ $\displaystyle\land
x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}+\frac{(v_{1}+a_{1}t)^{2}}{2a_{\text{minBrake}}}\leq
x_{2}+v_{2}t+\frac{1}{2}a_{2}t^{2}+\frac{(v_{2}+a_{2}t)^{2}}{2a_{\text{maxBrake}}}$

In principle, since quantifier elimination for real arithmetic is decidable
[25, 5], the proof could be finished automatically; in practice, however, the
proof obligations above are too complicated to terminate in reasonable time.
In order to split the proof into multiple more tractable subproblems, we
relate terms in the loop invariant and the safeDist condition. The loop
invariant $J$ follows the shape of safeDist closely, with $\rho$ replaced by
$t$, $a_{\text{maxAccel}}$ replaced by $a_{1}$ and $a_{\text{maxBrake}}$
replaced by $a_{2}$. We consider that we substitute the most extreme cases for
choice of acceleration in the safe distance formula, which is the case that
the two cars are driving towards each other in the most extreme case possible,
meaning that these are easily relatable. For the time parameter, the position
functions of the two cars are monotonic, meaning that we prove a lemma that is
equivalent to the safe distance formula with $\rho$ replaced with $t$.
Specifically, we use a cut to provide the following lemma (9):

$\max(v_{1}t+\frac{1}{2}a_{maxAccel}+\frac{(v_{1}+ta_{maxAccel})^{2}}{2a_{minBrake}}-\frac{v_{2}^{2}}{2a_{maxBrake}},0)\leq
x2-x1$ (9)

Finally, with the following additional lemmas, which all follow from the fact
that $0\leq t\leq\rho$, $v1\geq 0$, $v2\geq 0$, $-a_{\text{maxBrake}}\leq
a_{1}\leq a_{\text{maxAccel}}$, and $-a_{\text{maxBrake}}\leq a_{2}\leq
a_{\text{maxAccel}}$, we align subterms of safeDist and lemma (9):

  * •

$x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}\leq v_{1}t+\frac{1}{2}a_{maxAccel}$

  * •

$\frac{(v_{1}+a_{1}t)^{2}}{2a_{\text{minBrake}}}\leq\frac{(v_{1}+ta_{maxAccel})^{2}}{2a_{minBrake}}$

  * •

$\frac{(v_{2}+a_{2}t)^{2}}{2a_{\text{maxBrake}}}+v_{2}t+\frac{1}{2}a_{2}t^{2}\geq\frac{v_{2}^{2}}{2a_{maxBrake}}$

Case $\texttt{safeDist}(v_{1},v_{2})\geq x_{2}-x_{1}$

For the proper response branch we utilize the loop invariant stopping distance
constraints that we know are true at the start of the iteration. The stopping
distance portion of the loop invariant solves for the position that each car
will be at when it reaches a full stop if the $-a_{\text{minBrake}}$ is
applied in car 1 and car 2 stays within its maximum braking (the assumed worst
case). This is exactly what the proper response does, as it assigns an
acceleration to each car, where car 1 has to brake at least as hard as
$-a_{\text{minBrake}}$ and car 2 has to apply some acceleration greater than
$-a_{\text{maxBrake}}$. This case closes by solution of the differential
equation and quantifier elimination. ∎

###  0.B.2 Opposite Longitudinal Direction Proof Details

For the model of cars driving in opposite directions, we use a similar proof
strategy to the cars driving in the same direction. We define a loop invariant
to encode the information that at each iteration the cars will not pass each
other, and that if both cars apply minimum braking, they will not collide.
This is to say that if after an iteration of the loop, the cars would follow
the proper response, they would not collide. Formally the invariant states
that

$J\equiv x_{1}\leq x_{2}\land x_{2}-\frac{v_{2}^{2}}{2a_{\text{minBrake}}}\geq
x_{1}+\frac{v_{1}^{2}}{2a_{\text{minBrake}}}$

Consider at the end of an iteration of the loop, we get the proof obligation:

$\displaystyle\phantom{\land~{}}x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}\leq
x_{2}+v_{2}t+\frac{1}{2}a_{2}t^{2}$ $\displaystyle\land
x_{1}+v_{1}t+\frac{1}{2}a_{1}t^{2}+\frac{(v_{1}+a_{1}t)^{2}}{2a_{\text{minBrake}}}\leq
x_{2}+v_{2}t-\frac{1}{2}a_{2}t^{2}+\frac{(v_{2}+a_{2}t)^{2}}{2a_{\text{minBrake}}}$

for $0\leq t\leq\rho$. As in the same direction case, there is a free driving
and proper response program to the model. In the free driving case, we relate
terms in the loop invariant to terms in safeDist as follows:

  * •

$v_{1}t+\frac{1}{2}a_{1}t^{2}\leq v_{1}\rho+\frac{1}{2}a_{maxAccel}$

  * •

$v_{2}t+\frac{1}{2}a_{1}t^{2}\geq v_{2}\rho-\frac{1}{2}a_{maxAccel}$

  * •

$\frac{(v_{1}+a_{1}t)^{2}}{2a_{\text{minBrake}}}\leq\frac{(v_{1}+ta_{maxAccel})^{2}}{2a_{minBrake}}$

  * •

$\frac{(v_{2}+a_{2}t)^{2}}{2a_{\text{minBrake}}}+v_{2}t+\frac{1}{2}a_{2}t^{2}\geq\frac{v_{2}^{2}}{2a_{minBrake}}$

Using these cuts, we are able to show that the distance the cars will travel
if needing to come to a complete stop will not cause a collision. Formally,
this is the second term in the loop invariant. For the first term, using the
fact that the distance that the front car travels is always less or equal to
the distance that would be travelled at full acceleration for $\rho$ time and
the distance that car 2 travels will always be greater or equal to it
travelling at full negative acceleration for $\rho$ time, we are able to show
that the new positions of the cars do not collide, i.e. $x_{1}\leq x_{2}$. The
proper response case again follows by quantifier elimination automatically. ∎


# MAD Families of Gowers’ Infinite Block Sequences

Clement Yung

###### Abstract.

Call a subset of $\mathbf{FIN}_{k}$ _small_ if it does not contain a copy of
$\left\langle P\right\rangle$ for some infinite block sequence
$P\in\mathbf{FIN}_{k}^{[\infty]}$. Gowers’ $\mathbf{FIN}_{k}$ theorem asserts
that the set of small subsets of $\mathbf{FIN}_{k}$ forms an ideal, so it is
sensible to consider almost disjoint families of $\mathbf{FIN}_{k}$ with
respect to the ideal of small subsets of $\mathbf{FIN}_{k}$. We shall show
that $\mathfrak{a}_{\mathbf{FIN}_{k}}$, the smallest possible cardinality of
an infinite mad family of $\mathbf{FIN}_{k}$, is uncountable.

##  1\. Introduction

For each $k\in\omega\setminus\\{0\\}$, let $\mathbf{FIN}_{k}$ denote the set
of all mappings $p:\omega\to\\{0,\dots,k\\}$ such that
$\operatorname{supp}(p)$ is finite and $k\in\operatorname{ran}(p)$. For two
such maps $p,q$ of disjoint support, we may define a partial binary operation
$+$ on $\mathbf{FIN}_{k}$ by stipulating that:

$\displaystyle(p+q)(n)=\begin{cases}p(n),&\text{if
$n\in\operatorname{supp}(p)$}\\\ q(n),&\text{if
$n\in\operatorname{supp}(q)$}\\\ 0,&\text{otherwise}\end{cases}$

Thus, $(\mathbf{FIN}_{k},+)$ forms a partial semigroup. Define the tetris
operation $T:\mathbf{FIN}_{k}\to\mathbf{FIN}_{k-1}$ by stipulating that
$T(p)(n):=\max\\{p(n)-1,0\\}$. These mappings are also known as blocks, and a
block sequence is defined as a sequence $(p_{n})_{n<\alpha}$, such that
$\max\operatorname{supp}(p_{n})<\min\operatorname{supp}(p_{n+1})$ (abbreviated
as $p_{n}<p_{n+1}$) for all $n$, where $0\leq\alpha\leq\omega$. For each such
$\alpha$, the space of block sequences of length $\alpha$ is denoted by
$\mathbf{FIN}_{k}^{[\infty]}$. Given a finite block sequence
$P=(p_{n})_{n<N}$, the partial subsemigroup generated by $P$ is:

$\displaystyle\left\langle P\right\rangle$ $\displaystyle:=\left\langle
p_{0},\dots,p_{N-1}\right\rangle$
$\displaystyle:=\\{T^{j_{0}}(p_{n_{0}})+\cdots+T^{j_{m}}(p_{n_{m}}):m<\omega,n_{0}<\cdots<n_{m}<N,$
$\displaystyle\phantom{{}={}}j_{0},\dots,j_{m}<k,\min{j_{i}}=0\\}$

If $P=(p_{n})_{n<\omega}$ is an infinite block sequence, then:

$\displaystyle\left\langle P\right\rangle:=\bigcup_{N<\omega}\left\langle
p_{0},\dots,p_{N-1}\right\rangle$

Given another block sequence $Q=(q_{n})_{n<\beta}$, where $\beta\leq\alpha$,
we say that $Q$ is a subsequence of $P$ (written $Q\leq P$) if
$q_{n}\in\left\langle P\right\rangle_{k}$ for all $n<\beta$. Finally, write
$\left\langle P\right\rangle^{[\beta]}$ to be the set of all block
subsequences of $P$ of length $\beta$. We let $\mathbf{FIN}_{k}^{[\infty]}$
denote the space of all infinite block sequences.

The Ramsey theory of $\mathbf{FIN}_{k}$ was first explored by Gowers [2] in
proving the oscillation stability of uniformly continuous functions
$f:S_{c_{0}}\to\mathbb{R}$, where $S_{c_{0}}$ is the unit sphere in $c_{0}$.
The current formulation of infinite block sequences is also due to Todorčević
in [3].

######  Theorem 1.1 (Gowers $\mathbf{FIN}_{k}$ Theorem).

For any $X\subseteq\mathbf{FIN}_{k}$ and $P\in\mathbf{FIN}_{k}^{[\infty]}$,
there exists some $Q\leq P$ such that $\left\langle Q\right\rangle\subseteq X$
or $\left\langle Q\right\rangle\subseteq X^{c}$.

Call a subset of $X\subseteq\mathbf{FIN}_{k}$ _small_ if there does not exist
some $P\in\mathbf{FIN}_{k}^{[\infty]}$ such that $\left\langle
P\right\rangle\subseteq X$. This theorem implies that the set of small subsets
of $\mathbf{FIN}_{k}$ forms an ideal: Indeed, if $X\cup
Y\subseteq\mathbf{FIN}_{k}$ is not small, say $\left\langle
P\right\rangle\subseteq X\cup Y$, then by the above theorem there exists some
$Q\leq P$ such that $\left\langle Q\right\rangle\subseteq X$ or $\left\langle
Q\right\rangle\subseteq X^{c}$. In the latter case, $\left\langle
Q\right\rangle\subseteq Y$. Consequently, it is reasonable to discuss almost
disjoint families with respect to the ideal of small subsets of
$\mathbf{FIN}_{k}$.

######  Definition 1.2.

  1. (1)

Two subsets $X,Y\subseteq\mathbf{FIN}_{k}$ are _almost disjoint_ (or simply
_ad_) if $X\cap Y$ is small.

  2. (2)

Two infinite block sequences $P,Q\in\mathbf{FIN}_{k}^{[\infty]}$ are _almost
disjoint_ if $\left\langle P\right\rangle,\left\langle Q\right\rangle$ are
almost disjoint.

  3. (3)

A family $\cal{A}\subseteq\mathbf{FIN}_{k}^{[\infty]}$ is an _almost disjoint
family_ if for all $P\neq Q$ in $\cal{A}$, $P$ and $Q$ are almost disjoint. If
$\cal{A}$ is maximal under inclusion, then $\cal{A}$ is called a _maximal
almost disjoint family_ , or simply a _mad family_.

For $k=1$, $P,Q\in\mathbf{FIN}^{[\infty]}$ are almost disjoint iff
$\left\langle P\right\rangle\cap\left\langle Q\right\rangle$ are finite, so
the uncountability of the cardinal $\mathfrak{a}_{\mathbf{FIN}}$ is immediate.
This particular cardinal was studied in [1], where it was shown that the
inequality $\operatorname{non}(\mathcal{M})\leq\mathfrak{a}_{\mathbf{FIN}}$.
Consequently, $\mathfrak{a}<\mathfrak{a}_{\mathbf{FIN}}$ in the random model.

The uncountability of the cardinal $\mathfrak{a}_{\mathbf{FIN}_{k}}$ is less
apparent for $k\geq 2$. Unlike the case of $\mathbf{FIN}$, it is not true that
if $P,Q\in\mathbf{FIN}_{k}^{[\infty]}$ are almost disjoint, then $\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ is finite.

######  Example 1.3.

Fix $k\geq 2$. Consider the following blocks
$p_{n},q_{n},r\in\mathbf{FIN}_{k}$, where $n<\omega$:

  1. (1)

$\operatorname{supp}(r)=\\{0\\}$, $r(0)=k$.

  2. (2)

$\operatorname{supp}(p_{n})=\\{n\\}$, $p_{n}(n)=k$, $p_{n}(n+1)=0$.

  3. (3)

$\operatorname{supp}(q_{n})=\\{n,n+1\\}$, $q_{n}(n)=k$, $q_{n}(n+1)=1$.

Let $P:=r^{\frown}(p_{2n+1})_{n<\omega}$ and
$Q:=r^{\frown}(q_{2n+1})_{n<\omega}$. We first show that $\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ is infinite. For each $m$,
define $s_{m}\in\mathbf{FIN}_{k}$ by
$\operatorname{supp}(s_{m})=\\{0\\}\cup\\{2n+1:n<m\\}$, $s_{m}(0)=k$ and
$s_{m}(2n+1)=k-1$ for $n<m$. Then we see that:

$\displaystyle s_{m}=r+\sum_{n<m}T(p_{2n+1})=r+\sum_{n<m}T(q_{2n+1})$

so $s_{m}\in\left\langle P\right\rangle\cap\left\langle Q\right\rangle$ for
all $m<\omega$. Clearly, the $s_{m}$’s are all distinct, so $\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ is infinite.

We now show that $\left\langle P\right\rangle\cap\left\langle Q\right\rangle$
is small. Suppose on the contrary that $[R]\subseteq\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ for some
$R=(t_{n})_{n<\omega}\in\mathbf{FIN}_{k}^{[\infty]}$. Let $t_{n}>r$, and
suppose $t_{n}(l)=k$ for some $0\neq l\in\operatorname{supp}(t_{n})$. We may
write:

$\displaystyle
t_{n}=T^{i^{\prime}}(r)+T^{i_{0}^{\prime}}(q_{2i_{0}+1})+\cdots+T^{i_{m-1}^{\prime}}(q_{2i_{m-1}+1})$

Since $t_{n}(l)=k$, we must have that $q_{2i_{j}+1}=q_{l}$ for some $l<m-1$,
and $i_{j}^{\prime}=0$ as $T^{i_{j}^{\prime}}(q_{2i_{j}^{\prime}+1})=q_{l}$.
This is because for $g\neq j$, $l\notin\operatorname{supp}(q_{2i_{g}+1})$.
This implies that $t_{n}(l+1)=q_{2i_{j}+1}(l+1)=q_{l}(l+1)=1$. However, on the
other hand for all $n$, if $l$ is odd then $p_{n}(l+1)=0$, so any element
generated by $A$ must also have no support on $l+1$, a contradiction.

The main theorem of this paper is thus the following:

######  Theorem 1.4.

For all $k\geq 1$, $\mathfrak{a}_{\mathbf{FIN}_{k}}\geq\aleph_{1}$.

##  2\. Valuation and Diagonalisation

Fix some $k\geq 1$. Define a function $f:\mathbf{FIN}_{k}\to\mathbb{N}$ by
stipulating that:

$\displaystyle f(p):=\max\\{n<\omega:p(n)=k\\}$

We then extend $f$ to a function
$F:\cal{P}(\mathbf{FIN}_{k})\to\mathbb{N}\cup\\{\infty\\}$ by:

$\displaystyle F(X):=\sup_{p\in X}f(p)$

######  Lemma 2.1.

The function $F$ satisfies the following two properties:

  1. (1)

For all $P,Q\in\mathbf{FIN}_{k}^{[\infty]}$, $F(\left\langle
P\right\rangle\cap\left\langle Q\right\rangle)<\infty$ iff $P$ and $Q$ are
almost disjoint.

  2. (2)

For $X_{0},X_{1},\dots\in\cal{P}(\mathbf{FIN}_{k})$, we have that:

$\displaystyle F\left(\bigcup_{n<\omega}X_{n}\right)=\sup_{n<\omega}F(X_{n})$

We also say that $F$ satisfies the criteria of being a _valuation_. We
postpone the proof of Lemma 2.1 to the next section. Intuitively, this lemma
shows that the function $F$ accurately measures the almost disjointness of two
infinite block sequences $P$ and $Q$.

The valuation $F$ was introduced to help us with the diagonalisation argument
when showing that $\mathfrak{a}_{\mathbf{FIN}_{k}}$ is uncountable.

###### Proof of Theorem 1.4.

Let $\cal{A}:=\\{P_{n}:n<\omega\\}$ be a countable almost disjoint family of
infinite block sequences. We shall show that $\cal{A}$ is not maximal by
constructing some $Q=(q_{n})_{n<\omega}$ that is almost disjoint from $P_{n}$
for all $n<\omega$. Write $P_{n}=(p_{l}^{(n)})_{l<\omega}$. Let
$q_{0}\in\left\langle P_{0}\right\rangle$ be any element, and suppose that
$q_{0},\dots,q_{n-1}$ have been chosen. Recall that $P_{n}$ is almost disjoint
from $P_{i}$ for all $i<n$.

######  Claim.

There exists some $q_{n}\in\left\langle P_{n}\right\rangle$ such that for all
$i<n$:

$\displaystyle F(\left\langle q_{0},\dots,q_{n}\right\rangle\cap\left\langle
P_{i}\right\rangle)=F(\left\langle
q_{0},\dots,q_{n-1}\right\rangle\cap\left\langle P_{i}\right\rangle)$

Assuming the claim, we can finish the proof as follows: By induction, we have
that for all $k<\omega$:

$\displaystyle F\left(\left\langle Q\right\rangle\cap\left\langle
P_{i}\right\rangle\right)$
$\displaystyle=F\left(\bigcup_{n<\omega}\left\langle
q_{0},\dots,q_{n-1}\right\rangle\cap\left\langle P_{i}\right\rangle\right)$
$\displaystyle=\sup_{n<\omega}F(\left\langle
q_{0},\dots,q_{n-1}\right\rangle\cap\left\langle P_{i}\right\rangle)$
$\displaystyle\leq F(\left\langle
q_{0},\dots,q_{i}\right\rangle\cap\left\langle P_{i}\right\rangle)$
$\displaystyle<\infty$

so $Q$ is almost disjoint from $P_{k}$ for all $k<\omega$.

We now prove the claim. For each $i<n$, let $N_{i}:=F(\left\langle
P_{n}\right\rangle\cap\left\langle P_{i}\right\rangle)$. Let
$q_{n}\in\left\langle P_{n}\right\rangle$ such that
$q_{n}>p_{J}^{(n)}>q_{n-1}$ for some $J$, and $f(q_{n})>N_{i}$ for all $i$. We
shall show that this $q_{n}$ works. Let $r\in\left\langle
q_{0},\dots,q_{n}\right\rangle\cap\left\langle P_{i}\right\rangle$, so we may
write:

$\displaystyle
r=T^{i_{0}}(q_{0})+\cdots+T^{i_{n-1}}(q_{n-1})+T^{i_{n}}(q_{n})=\sum_{l<\omega}T^{j_{l}}(p_{l}^{(i)})$

Now observe that by the choice of $q_{n}$ and $p_{J}^{(i)}$, we must have:

$\displaystyle\operatorname{supp}\left(T^{i_{0}}(q_{0})+\cdots+T^{i_{n-1}}(q_{n-1})\right)=\operatorname{supp}\left(\sum_{l<J}T^{j_{l}}(p_{l}^{(i)})\right)$
$\displaystyle\operatorname{supp}\left(T^{i_{n}}(q_{n})\right)=\operatorname{supp}\left(\sum_{l>J}T^{j_{l}}(p_{l}^{(i)})\right)$

Therefore, we must have that:

$\displaystyle
T^{i_{0}}(q_{0})+\cdots+T^{i_{n-1}}(q_{n-1})=\sum_{l<J}T^{j_{l}}(p_{l}^{(i)})$
$\displaystyle T^{i_{n}}(q_{n})=\sum_{l>J}T^{j_{l}}(p_{l}^{(i)})$

If $i_{n}=0$, then $q_{n}\in\left\langle P_{i}\right\rangle\cap\left\langle
P_{n}\right\rangle$, which is not possible as $f(q_{n})>N_{i}$. Thus,
$i_{n}>0$. Therefore, $T^{i_{n}}(q_{n})(m)<k$ for all $m$, so:

$\displaystyle f(r)$
$\displaystyle=f\left(T^{i_{0}}(q_{0})+\cdots+T^{i_{n-1}}(q_{n-1})+T^{i_{n}}(q_{n})\right)$
$\displaystyle=f\left(T^{i_{0}}(q_{0})+\cdots+T^{i_{n-1}}(q_{n-1})\right)$
$\displaystyle\leq F(\left\langle
q_{0},\dots,q_{n-1}\right\rangle\cap\left\langle P_{i}\right\rangle)$

so the desired equality holds. ∎

##  3\. Proof of Lemma 2.1

Note that (2) of Lemma 2.1 follows immediately from the definition of $F$.
Also, the $\implies$ direction of (1) is easy: If $\left\langle
R\right\rangle\subseteq\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$ and $R=(r_{n})_{n<\omega}$, then $r_{n}\in\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ for all $n$ and
$\\{f(r_{n}):n<\omega\\}$ is unbounded, so $F(\left\langle
P\right\rangle\cap\left\langle Q\right\rangle)=\infty$. Therefore, the only
non-trivial part of Lemma 2.1 is thus the $\impliedby$ direction of (1).

######  Lemma 3.1.

Let $P,Q\in\mathbf{FIN}_{k}^{[\infty]}$. Then $\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ is small iff there exists some
$n$ such that $\left\langle P/n\right\rangle\cap\left\langle
Q\right\rangle=\emptyset$.

###### Proof.

$\impliedby$: Suppose $\left\langle R\right\rangle\subseteq\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$ for some
$R\in\mathbf{FIN}_{k}^{[\infty]}$. Write $R=(r_{n})_{n<\omega}$. Then, for any
$n\geq 1$, there exists some $m$, such that $r_{m}>p_{n-1}$. Therefore,
$r_{n}\in\left\langle P/n\right\rangle\cap\left\langle
Q\right\rangle\neq\emptyset$.

$\implies$: Suppose on the contrary that $\left\langle
P/n\right\rangle\cap\left\langle Q\right\rangle\neq\emptyset$ for all $n$.
Write $P=(p_{n})_{n<\omega}$. We define $r_{n}\in\mathbf{FIN}_{k}$ inductively
as follows: Let $r_{0}\in\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$ be any block. If $r_{n}$ has been defined, then let $m$ be
large enough so that $p_{m}>r_{n}$, and let $r_{n+1}\in\left\langle
P/m\right\rangle\cap\left\langle Q\right\rangle$. We have $r_{n+1}>r_{n}$, so
if $R=(r_{n})_{n<\omega}\in\mathbf{FIN}_{k}^{[\infty]}$, then $\left\langle
R\right\rangle\subseteq\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$, as desired. ∎

We shall give a quick outline of the proof. Assume that $F(\left\langle
P\right\rangle\cap\left\langle Q\right\rangle)=\infty$. By Lemma 3.1, it
suffices to show that $F(\left\langle P/n\right\rangle\cap\left\langle
Q\right\rangle)=\infty$ for all $n$. To do this, we follow the following
steps:

  1. (1)

We introduce a binary operation $\star$ on $\mathbf{FIN}_{k}$ which allows us
to “stack” blocks together, and that $\left\langle P\right\rangle$ is closed
under $\star$.

  2. (2)

We introduce a notion of an _intertwined block_ $p\in\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$, and show that such blocks do
exist.

  3. (3)

We shall show that intertwined blocks cannot be stacked any higher - that is,
for any $q\in\left\langle P\right\rangle\cap\left\langle Q\right\rangle$,
$p\star q=s+p+r$ for some $r,s\in\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$ (if non-empty) such that $s<p<r$ if they are not empty.

  4. (4)

Since $f(r)=f(s+p+r)=f(p\star q)\geq f(q)$ can be chosen arbitrarily large,
and $r\in\left\langle P/n\right\rangle\cap\left\langle Q\right\rangle$,
$F(\left\langle P/n\right\rangle\cap\left\langle Q\right\rangle)=\infty$.

For the first step, given $p,q\in\mathbf{FIN}_{k}$ we shall define $p\star q$
to be the function such that for all $n$:

$\displaystyle(p\star q)(n)=\max\\{p(n),q(n)\\}$

We have that $\operatorname{supp}(p\star
q)=\operatorname{supp}(p)\cup\operatorname{supp}(q)$, which is finite, and if
$p(n)=k$ or $q(n)=k$, then $(p\star q)(n)=k$. Therefore, $p\star
q\in\mathbf{FIN}_{k}$. Furthermore, $\left\langle P\right\rangle$ is closed
under $\star$ for any $P=(p_{n})_{n<\omega}\in\mathbf{FIN}_{k}^{[\infty]}$, as
it’s easy to check that if $p=\sum_{n<\omega}T^{i_{n}}(p_{n})$ and
$q=\sum_{n<\omega}T^{j_{n}}(p_{n})$, then:

$\displaystyle p\star q=\sum_{n<\omega}T^{\min\\{i_{n},j_{n}\\}}(p_{n})$

We remark as well that $\star$ is commutative and associative.

We now consider intertwined blocks for a fixed pair of
$P,Q\in\mathbf{FIN}_{k}^{[\infty]}$, where $P=(p_{n})_{n<\omega}$ and
$Q=(q_{m})_{m<\omega}$. For each $p\in\left\langle
P\right\rangle\cap\left\langle Q\right\rangle$, we may write:

$\displaystyle
p=T^{i_{0}^{\prime}}(p_{i_{0}})+\cdots+T^{i_{n-1}^{\prime}}(p_{i_{n-1}})=T^{j_{0}^{\prime}}(q_{j_{0}})+\cdots+T^{j_{m-1}^{\prime}}(q_{j_{m-1}})$

such that $i_{0},\dots,i_{n-1},j_{0},\dots,j_{m-1}<k$. Let
$V_{1}:=\\{i_{0},\dots,i_{n-1}\\}$, $V_{2}:=\\{j_{0},\dots,j_{m-1}\\}$. We
consider the bipartite graph $G_{p}:=(V_{1}\sqcup V_{2},E)$ such that:

$\displaystyle(i_{g},j_{h})\in
E\iff\operatorname{supp}(T^{i_{g}^{\prime}}(p_{i_{g}}))\cap\operatorname{supp}(T^{j_{h}^{\prime}}(q_{j_{h}}))\neq\emptyset$

######  Definition 3.2.

A block $p$ is _intertwined_ if the graph $G_{p}$ is connected.

######  Example 3.3.

Let $P,Q$ be the pair of infinite block sequences in Example 1.3. For any $n$,
$r+T(p_{2n+1})=r+T(q_{2n+1})$, but it is not intertwined as
$\operatorname{supp}(r)<\operatorname{supp}(T(p_{2n+1}))=\operatorname{supp}(T(q_{2n+1}))$.
However, we can “extract” the part on the left to get the block $r$, which is
intertwined. This “extraction” paves the proof that an intertwined block
always exist.

######  Lemma 3.4.

If $N$ is the least number such that $\left\langle
p_{0},\dots,p_{N-1}\right\rangle\cap\left\langle Q\right\rangle\neq\emptyset$,
then there exists an intertwined block $p\in\left\langle
p_{0},\dots,p_{N-1}\right\rangle\cap\left\langle Q\right\rangle$.

###### Proof.

Fix any $p\in\left\langle p_{0},\dots,p_{N-1}\right\rangle\cap\left\langle
Q\right\rangle$. Write:

$\displaystyle
p=T^{i_{0}^{\prime}}(p_{i_{0}})+\cdots+T^{i_{n-1}^{\prime}}(p_{i_{n-1}})=T^{j_{0}^{\prime}}(q_{j_{0}})+\cdots+T^{j_{m-1}^{\prime}}(q_{j_{m-1}})$

Note that by the minimality of $N$, $i_{n-1}=N-1$. Let $H\subseteq G_{p}$ be
the connected component containing $i_{n-1}$. We make two observations:

  1. (1)

The graph $G_{p}$ contains no isolated points.

  2. (2)

If $(i_{g},j_{h})\in E$, $(i_{g^{\prime}},j_{h^{\prime}})\in E$ and
$g<g^{\prime}$, then $h\leq h^{\prime}$.

Consequently, $V(H)$ is “upward-closed”, i.e. we have that
$V(H)=\\{i_{\alpha},\dots,i_{n-1}\\}\sqcup\\{j_{\beta},\dots,j_{m-1}\\}$ for
some $\alpha\leq n-1$ and $\beta\leq m-1$. Therefore, we may “split” $p$ as
follows:

$\displaystyle
p=\underbrace{T^{i_{0}^{\prime}}(p_{i_{0}})+\cdots+T^{i_{\alpha-1}^{\prime}}(p_{i_{\alpha-1}})}_{=:q_{0}}+\underbrace{T^{i_{\alpha}^{\prime}}(p_{i_{\alpha}})+\cdots+T^{i_{n-1}^{\prime}}(p_{i_{n-1}})}_{=:r_{0}}$
$\displaystyle
p=\underbrace{T^{j_{0}^{\prime}}(q_{j_{0}})+\cdots+T^{j_{\beta-1}^{\prime}}(q_{j_{\beta-1}})}_{=:q_{1}}+\underbrace{T^{j_{\beta}^{\prime}}(q_{j_{\beta}})+\cdots+T^{j_{m-1}^{\prime}}(q_{j_{m-1}})}_{=:r_{1}}$

Since $(i_{\alpha},j_{\beta-1})\notin E$, we must have that
$T^{j_{\beta-1}^{\prime}}(q_{j_{\beta-1}})<T^{i_{\alpha}^{\prime}}(p_{i_{\alpha}})$.
Similarly, we also have
$T^{i_{\alpha-1}^{\prime}}(p_{i_{\alpha-1}})<T^{j_{\beta}^{\prime}}(q_{j_{\beta}})$.
Therefore, $q_{0},q_{1}<r_{0},r_{1}$, so this separation of support implies
that $q_{0}=q_{1}$ and $r_{0}=r_{1}$. However, if $q_{0}$ is a block (i.e.
$q_{0}(M)=k$ for some $M\in\operatorname{supp}(q_{0})$), then
$q_{0}\in\left\langle
p_{0},\dots,p_{i_{\alpha-1}}\right\rangle\cap\left\langle Q\right\rangle$,
contradicting the minimality of $N$. Since $p(N)=k$ for some
$N\in\operatorname{supp}(p)$, we must have that $r_{0}(N)=k$ for some
$N\in\operatorname{supp}(r_{0})$. Thus, $r_{0}$ is an intertwined block in
$\left\langle P/n\right\rangle\cap\left\langle Q\right\rangle$. ∎

This finishes the second step. The following lemma completes the third step.

######  Definition 3.5.

  1. (1)

A _subblock_ is a function $T^{i}(p)$ for some $p\in\mathbf{FIN}_{k}$.

  2. (2)

Given $p_{0}<\cdots<p_{n-1}$, we define:

$\displaystyle\left\langle
p_{0},\dots,p_{n-1}\right\rangle^{*}:=\\{T^{i}(p):p\in\left\langle
p_{0},\dots,p_{n-1}\right\rangle\wedge i\geq 0\\}$

  3. (3)

Given $P=(p_{n})_{n<\omega}\in\mathbf{FIN}_{k}^{[\infty]}$, we define:

$\displaystyle\left\langle P\right\rangle^{*}:=\bigcup_{n<\omega}\left\langle
p_{0},\dots,p_{n-1}\right\rangle^{*}$

Similar to blocks, for subblocks $p,q$, we write $p<q$ if either
$\max(\operatorname{supp}(p))<\min(\operatorname{supp}(q))$, or
$\operatorname{supp}(p)=\emptyset$ or $\operatorname{supp}(q)=\emptyset$.

######  Lemma 3.6.

If $p\in\left\langle P\right\rangle\cap\left\langle Q\right\rangle$ is
intertwined, then for all $q\in\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$, $p\star q=s+p+r$ for some subblocks $s,r\in\left\langle
P\right\rangle^{*}\cap\left\langle Q\right\rangle^{*}$ such that $s<p<r$.

###### Proof.

We first write:

$\displaystyle
p=T^{i_{0}^{\prime}}(p_{i_{0}})+\cdots+T^{i_{n-1}^{\prime}}(p_{i_{n-1}})=T^{j_{0}^{\prime}}(q_{j_{0}})+\cdots+T^{j_{m-1}^{\prime}}(q_{j_{m-1}})$

Write
$q:=\sum_{\alpha<\omega}T^{g_{\alpha}}(p_{\alpha})=\sum_{\beta<\omega}T^{h_{\beta}}(q_{\beta})$,
so we have that:

$\displaystyle p\star
q=\sum_{\alpha<\omega}T^{g_{\alpha}^{\prime}}(p_{\alpha})=\sum_{\beta<\omega}T^{h_{\beta}^{\prime}}(q_{\beta})$

######  Claim.

For all $\min(\operatorname{supp}(p))\leq N\leq\max(\operatorname{supp}(p))$,
$(p\star q)(N)=p(N)$.

###### Proof.

Suppose not, so there exists some $N\in\operatorname{supp}(p)$ such that
$(p\star q)(N)>p(N)$. We consider two cases.

  1. (1)

Suppose $N\in\operatorname{supp}(p_{i_{\gamma}})$ for some $\gamma$. Then
$g_{i_{\gamma}}^{\prime}<i_{\gamma}^{\prime}$.

  2. (2)

Suppose $N\in\operatorname{supp}(p_{\alpha})$ and
$i_{\gamma}<\alpha<i_{\gamma+1}$. We claim that there exists some $\delta$
such that
$\operatorname{supp}(T^{i_{\gamma}^{\prime}}(p_{i_{\gamma}}))\cap\operatorname{supp}(T^{j_{\delta}^{\prime}}(q_{j_{\delta}}))\neq\emptyset$
and
$\operatorname{supp}(T^{i_{\gamma+1}^{\prime}}(p_{i_{\gamma+1}}))\cap\operatorname{supp}(T^{j_{\delta}^{\prime}}(q_{j_{\delta}}))\neq\emptyset$.
Otherwise, let $\delta_{1}$ be the largest number such that
$(i_{\gamma},j_{\delta_{1}})\in E$ (where $E$ is the edge set of the graph
$G_{p}$), and let $\delta_{2}$ be the smallest number such that
$(i_{\gamma},j_{\delta_{2}})\in E$. By observation (2) in the proof of Lemma
3.4, for any $\delta<m$, we have that:

$\displaystyle(i_{\xi},j_{\delta})\in
E\implies\begin{cases}\xi\leq\gamma,&\text{if $\delta\leq\delta_{1}$}\\\
\xi\geq\gamma+1,&\text{if $\delta\geq\delta_{2}$}\end{cases}$

But this implies that there is no path from $i_{\gamma}$ to $i_{\gamma+1}$,
contradicting that $G_{p}$ is connected. Therefore, we have that:

$\displaystyle\min(\operatorname{supp}(T^{j_{\delta}^{\prime}}(q_{j_{\delta}})))\leq\max(\operatorname{supp}(T^{i_{\gamma}^{\prime}}(p_{i_{\gamma}})))$
and
$\displaystyle\min(\operatorname{supp}(T^{i_{\gamma+1}^{\prime}}(p_{i_{\gamma+1}})))\leq\max(\operatorname{supp}(T^{j_{\delta}^{\prime}}(q_{j_{\delta}})))$

This implies that:

$\displaystyle\min(\operatorname{supp}(q_{j_{\delta}}))\leq\max(\operatorname{supp}(p_{i_{\gamma}}))$
and
$\displaystyle\min(\operatorname{supp}(p_{i_{\gamma+1}}))\leq\max(\operatorname{supp}(q_{j_{\delta}}))$

Since $p_{i_{\gamma}}<p_{\alpha}<p_{i_{\gamma+1}}$, we must have that
$N\in\operatorname{supp}(q_{j_{\delta}})$. Since $(p\star q)(N)>p(N)$,
$h_{j_{\delta}}^{\prime}<h_{\delta}^{\prime}$.

However, in either case, it leads to a contradiction: We prove the first case,
and the second case follows similarly. Suppose
$g_{i_{\gamma}}^{\prime}<i_{\gamma}^{\prime}$. If $(i_{\gamma},j_{\delta})\in
E$, then let
$N\in\operatorname{supp}(T^{i_{\gamma}^{\prime}}(p_{i_{\gamma}}))\cap\operatorname{supp}(T^{j_{\delta}^{\prime}}(q_{j_{\delta}}))$.
Then:

$\displaystyle
T^{h_{j_{\delta}}^{\prime}}(q_{j_{\delta}})(N)=T^{g_{i_{\gamma}}^{\prime}}(p_{i_{\gamma}})(N)>T^{i_{\gamma}^{\prime}}(p_{i_{\gamma}})(N)=T^{j_{\delta}^{\prime}}(q_{j_{\delta}})(N)$

Therefore $h_{j_{\delta}}^{\prime}<j_{\delta}^{\prime}$. Let $\xi<n$ be such
that $i_{\xi}^{\prime}=0$, which exists as $p$ is a block. Since $G_{p}$ is
connected, consider a path in $G_{p}$ from $i_{\gamma}$ to $i_{\xi}$. By
repeating the above argument on this path, we conclude that
$g_{i_{\xi}}^{\prime}<i_{\xi}^{\prime}=0$, which is a contradiction. ∎

Consequently, we may write:

$\displaystyle
p*q=\underbrace{\sum_{\alpha<i_{0}}T^{g_{\alpha}^{\prime}}(p_{\alpha})}_{s}+\sum_{l=0}^{n-1}T^{i_{l}^{\prime}}(p_{i_{l}})+\underbrace{\sum_{\alpha>i_{n}}T^{g_{\alpha}^{\prime}}(p_{\alpha})}_{r}$
$\displaystyle
p*q=\underbrace{\sum_{\beta<j_{0}}T^{h_{\alpha}^{\prime}}(q_{\alpha})}_{s^{\prime}}+\sum_{l=0}^{m-1}T^{j_{l}^{\prime}}(q_{j_{l}})+\underbrace{\sum_{\alpha>j_{m}}T^{h_{\alpha}^{\prime}}(q_{\beta})}_{r^{\prime}}$

The two terms in the middle are equal to $p$. Since
$s,s^{\prime}<p<r,r^{\prime}$, by separation of support, we must have that
$s=s^{\prime}$ and $r=r^{\prime}$, and $s,r\in\left\langle
P\right\rangle^{*}\cap\left\langle Q\right\rangle^{*}$. ∎

We can now finish the proof of Lemma 2.1. Assume that $F(\left\langle
P\right\rangle\cap\left\langle Q\right\rangle)=\infty$. Let $n$ be minimal
such that $\left\langle p_{0},\dots,p_{n-1}\right\rangle\cap\left\langle
Q\right\rangle\neq\emptyset$, and let $p\in\left\langle
p_{0},\dots,p_{n-1}\right\rangle\cap\left\langle Q\right\rangle$ be an
intertwined block. Since $F(\left\langle P\right\rangle\cap\left\langle
Q\right\rangle)=\infty$, let $q\in\left\langle P\right\rangle\cap\left\langle
Q\right\rangle$ be such that $f(p\star q)>f(p)$. By Lemma 3.6, $p\star
q=s+p+r$ for some $r,s\in\left\langle P\right\rangle^{*}\cap\left\langle
Q\right\rangle^{*}$. If $r$ is not a block, then $f(p\star q)=f(p)$,
contradicting our assumption. Therefore, $r$ is a block, and
$f(r)=f(s+p+r)=f(p\star q)\geq f(q)$ with $r\in\left\langle
P/n\right\rangle\cap\left\langle Q\right\rangle$. Since $f(q)$ may be chosen
to be arbitrarily large, we conclude that $F(\left\langle
P/n\right\rangle\cap\left\langle Q\right\rangle)=\infty$. Repeat this argument
for arbitrarily large $n$, we have in particular that $\left\langle
P/n\right\rangle\cap\left\langle Q\right\rangle\neq\emptyset$ for all $n$, so
by Lemma 3.1, $P$ and $Q$ are not almost disjoint.

## References

  * [1] J. Brendle and L.. García-Ávila  “Forcing-theoretic aspects of Hindman’s Theorem”  In _Journal of the Mathematical Society of Japan_ 69.3 Mathematical Society of Japan, 2017, pp. 1247–1280  DOI: 10.2969/jmsj/06931247
  * [2] W.. Gowers  “Lipschitz functions on classical spaces”  In _European J. Combin._ 13.3, 1992
  * [3] Stevo Todorčević  “Introduction to Ramsey Spaces” 174, Annals of Mathematics Studies  Princeton University Press, 2010