#  Relational Differential Dynamic Logic ††thanks:  Thanks are due to Kenji
Kamijo, Yoshiyuki Shinya, and Takamasa Suetomi from Mazda Motor Corporation
for helpful discussions. The authors are supported by ERATO HASUO
Metamathematics for Systems Design Project (No. JPMJER1603), JST. I.H. is
supported by Grants-in-Aid No. 15KT0012, JSPS. The work is done during J.K.’s
internship at National Institute of Informatics, Tokyo, Japan.

Juraj Kolčák12, Ichiro Hasuo13, Jérémy Dubut14, Shin-ya Katsumata1, David
Sprunger1 and Akihisa Yamada1  1 National Institute of Informatics, Tokyo,
Japan  2 LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, France  3 The
Graduate University for Advanced Studies (SOKENDAI), Tokyo, Japan  4 Japanese-
French Laboratory for Informatics, Tokyo, Japan

###### Abstract

In the field of quality assurance of _hybrid systems_ (that combine continuous
physical dynamics and discrete digital control), Platzer’s _differential
dynamic logic_ (dL) is widely recognized as a deductive verification method
with solid mathematical foundations and sophisticated tool support. Motivated
by benchmarks provided by our industry partner, we study a _relational
extension_ of dL, aiming to formally prove statements such as “an earlier
deployment of the emergency brake decreases the collision speed.” A main
technical challenge here is to relate two states of two dynamics _at different
time points_. Our main contribution is a theory of suitable _simulations_ (a
relational extension of _differential invariants_ that are central proof
methods in dL), and a derived technique of _time stretching_. The latter
features particularly high applicability, since the user does not have to
synthesize a simulation out of the air. We derive new inference rules for dL
from these notions, and demonstrate their use over a couple of automotive case
studies.

###### Index Terms:

hybrid system, cyber-physical system, formal verification, theorem proving,
dynamic logic, differential equation, relational reasoning

##  I Introduction

###  I-A Hybrid Systems

It has been more than a decade since the term _cyber-physical system_ (CPS)
was coined and became a target of ever-growing research efforts. In
particular, _quality assurance_ of CPS is attracting renewed attention in the
last few years, with the rise of _automated driving_. In the foreseeable
future, millions of cars will be driving on streets with the degree of
automation that is greater than ever by magnitudes. Ensuring safety and
reliability of those automated driving systems is therefore a pressing social
and economic challenge.

Quality assurance of CPS poses a unique academic challenge, too, namely the
combination of continuous physical dynamics and discrete digital control. This
important aspect of CPS has been referred to as _hybridity_. In the research
efforts on hybrid systems, two communities have naturally joined forces:
_control theory_ whose traditional application domain is continuous dynamics,
and _formal methods_ that have mainly focused on the analysis of software
systems. The collaboration has produced a number of novel scientific
observations and practical techniques. They include the use of formal methods
techniques in control (bisimilarity [9], temporal logic specification [8], and
so on), and conversely, transfer of control theory notions (such as Lyapunov
functions) to formal methods. See e.g. [23].

###  I-B Deductive Verification of Hybrid Systems

In the formal methods community, a traditional classification of techniques
consists of _model checking_ (that is usually automata-based and automatic),
and _deductive verification_ (that is based on logic and can be automated or
interactive).111The classification is not definite: there are some works that
eagerly aim at integration of (logic- or type system-based) theorem proving
and model checking, including [12]. The applicability of automated model
checking techniques is naturally limited for hybrid systems, since the latter
has continuous state spaces and thus the search spaces become uncountable.
This has led to the active study of _discrete abstraction_ of hybrid dynamics,
where a principal method is the use of _approximate bisimulations_ derived
from suitable Lyapunov functions. See e.g. [9].

The deductive approach, in contrast, is not necessarily prohibited for hybrid
systems. Logical formulas can stand for infinitely many states thanks to their
free variables; and formal deduction of those formulas is no less valid even
if the semantic domain is the set of reals, for example.

That said, it is still a hard task to design a deductive system that is
actually _useful_ in hybrid system verification. Such a system should come
with concise and intuitive syntax for expressing continuous-time dynamics
(i.e. differential equations), as well as powerful and versatile reasoning
principles for such dynamics.

Platzer’s _differential dynamic logic_ $\mathsf{dL}$ [18] adequately meets
these criteria. Its syntax is systematic and intuitive, extending the classic
formalism of _dynamic logic_ [10] with differential equations as programs. Its
proof rules encapsulate several essential proof principles about differential
equations, notable among which are _differential invariant_ (DI) for universal
properties and _side deduction_ for existential properties. The logic
$\mathsf{dL}$ has served as a general platform that accommodates a variety of
techniques, including those which come from real algebraic geometry. See e.g.
[19], where Grönwall’s inequality is used to derive the so-called Darboux
inequality rule. Furthermore, $\mathsf{dL}$ comes with sophisticated tool
support: the latest tool KeYmaera X [15] comes with graphical interface for
interactive proving and a number of automation heuristics.

###  I-C Relational Reasoning on Hybrid Systems

In this work, we aim at a new direction in the field of deductive verification
for hybrid systems. We are motivated by the following example; it came up in
our collaboration with automotive industry.

######  Example I.1 (leading example: collision speed).

Consider two cars $\mathrm{C}$ and $\mathrm{C}^{\sharp}$, whose positions and
velocities are denoted by $x,x^{\sharp}$ and $v,v^{\sharp}$, respectively.
Their dynamics are governed by the following differential equations.

$\dot{x}=v,\quad\dot{v}=1;\qquad\quad\dot{x^{\sharp}}=v^{\sharp},\quad\dot{v^{\sharp}}=2.$
(1)

We assume that they both start at the same position ($x=x^{\sharp}=0$), with
the initial velocity $v=v^{\sharp}=0$, and they both drive towards a wall at
the position $x=x^{\sharp}=1$. Our question is: _which car has a greater
collision speed?_

The two hatched areas designate the traveled distances ($x=x^{\sharp}=1$). We
can compute the collision speeds ($v=\sqrt{2}$ and $v^{\sharp}=2$) via the
closed-form solutions of the differential equations (1), concluding $v\leq
v^{\sharp}$ when $x=x^{\sharp}=1$.

Figure 1: An ad-hoc proof for Example I.1

A natural answer is the second car $\mathrm{C}^{\sharp}$ that accelerates
harder (see (1)). Therefore we aim to prove the following claim.

The two dynamics in (1), with the initial states
$x=x^{\sharp}=v=v^{\sharp}=0$, exhibit $v\leq v^{\sharp}$ when
$x=x^{\sharp}=1$. (2)

We further aim to prove the claim in a _formal_ and _modular_ manner, so that
the proof methods we use apply to other examples of the same nature.
Therefore, differential dynamic logic $\mathsf{dL}$ is naturally a platform of
our choice.

It turns out that this _relational reasoning_ that compares two different
dynamics is not easy in $\mathsf{dL}$. Giving an ad-hoc proof is not hard: see
Figure 1, where the proof relies on the closed-form solutions of the dynamics.
However, we prefer not to use closed-form solutions (that are not always
available).

Moreover, it is desirable that our proof is solely by _local reasoning_ ,
without inspecting the global properties of the dynamics. The logic
$\mathsf{dL}$ offers a powerful rule for that purpose, namely the
_differential invariant_ (DI) rule. The rule roughly says: if $g(x)$ is
initially nonnegative, and the time derivative of $g$ (along the
dynamics—which is given by the Lie derivative) is nonnegative, then $g(x)$
stays nonnegative _no matter how long_ the dynamics runs. Note that a global
safety property is reduced to a local property about a Lie derivative; the DI
rule is a continuous-time analogue of the celebrated proof method by _loop
invariants_.

The discussion so far already suggests a viable strategy: instead of
(differential) invariants for unary safety proofs, in relational reasoning we
can use “binary invariants,” that is, _(bi)simulations_. Our main contribution
of this paper is to develop a theory about simulations and related notions
between continuous-time dynamics, and to embody the theory in the form of
concise and useful proof rules in $\mathsf{dL}$.

Note that such simulations necessarily relate _different time points_ of the
two dynamics. For example, in Figure 1, comparing $v$ and $v^{\sharp}$ at the
same time point does not suffice: at $t=t^{\sharp}=1$, the car
$\mathrm{C}^{\sharp}$ hits the wall but $\mathrm{C}$ does not yet. Although it
is easy to see that $v<v^{\sharp}$ at time $1$, $\mathrm{C}$ continues
driving, in the course of which $\mathrm{C}$’s velocity $v$ keeps growing.

###  I-D Technical Contributions

In this paper we make the following technical contributions.

  1. 1.

(Formulation of relational reasoning in $\mathsf{dL}$) We formulate the
problem of relational reasoning in differential dynamic logic $\mathsf{dL}$.
We focus on comparing different continuous-time dynamics (therefore comparing
different discrete-time controls is currently out of our scope). We observe
that this problem is expressible in the syntax of $\mathsf{dL}$ (e.g. in [19,
17]); nevertheless we introduce a syntactic shorthand for readability
(§III-A).

  2. 2.

(Simulation and the (SIM) rule) We define _simulations_ between two dynamics,
and formulate their soundness result for relational reasoning (§III-B). The
latter result gives rise to a syntactic proof rule (SIM), in §III-C.

  3. 3.

(Time stretching and the (TS) rule) While foundational, our theory up to this
point does not answer the question of how to find a simulation. Restricting to
so-called _equational exit conditions_ , we devise a syntactic method for
synthesizing a simulation-like notion, called _time stretch function_. In §IV
we develop the theory, eventually leading to a succinct proof rule (TS).

We find the (TS) rule powerful: it _synchronizes_ two dynamics and reduces
relational reasoning to common proof obligations $\mathsf{dL}$. For the
latter, we can fully exploit the advanced proof rules already developed in
$\mathsf{dL}$.

  4. 4.

(Additional rules including the (DII) rule) Besides the two principal new
rules (SIM) and (TS), we introduce some $\mathsf{dL}$ rules that we needed for
our case studies (§V). Notable is what we call the different _inductive_
invariant (DII) rule; it is much like the differential invariant (DI) rule in
$\mathsf{dL}$ (see e.g. [19]) but it allows to additionally assume the target
inequality itself in an evolution domain constraint.

These rules seem to be new, although they might be derivable from the
comprehensive calculus in [17].

  5. 5.

(Case studies) In addition to Example I.1, we conduct three case studies that
are more complex (§VI). They are inspired by our industry collaboration.

###  I-E Relational Reasoning in Industry Practice

The current work stemmed out of our collaboration with an industry partner.
From this experience, we argue that relational reasoning on hybrid systems has
ample practical significance.

Firstly, _monotonicity_ properties as exemplified in Example I.1 abound even
in real-world examples. Monotonicity properties take the following form: we
are given a parametrized model $M(p)$; and we aim to show that

$p_{1}<p_{2}$ implies $M(p_{2})$ is less safe than $M(p_{1})$.  (3)

These properties occur often especially in the context of _product lines_ ,
such as Euro car segments A–F.

Secondly, proof goals in relational reasoning (such as monotonicity) tend to
be easier to establish, compared to (unary, non-relational) safety
specifications. The proof of the latter is generally hard, requiring
inspection of every small detail of the system. Therefore we expect that, in
relational reasoning, the general difficulty of scaling deductive methods to
real-world examples is less of a problem.

Thirdly, relational reasoning (especially on monotonicity) can serve as a
powerful technique in _test-case reduction_. As we discussed previously, it
can happen that a real-world example is too complex for its safety property to
be deductively verified. In this situation, one would turn to empirical
quality assurance methods (i.e.  _testing_). If a monotonicity property (such
as (3)) can be deductively established (it is often easier than safety), the
monotonicity property allows us to focus our testing efforts to the extreme
case $M(p_{\max})$. This spares all the test cases that we would have spent
for $M(p)$ with smaller $p$’s.

###  I-F Related Work

We already mentioned some related works, including those on $\mathsf{dL}$.
Some other related works are discussed here.

Simulink (from the Mathworks, Inc.) is the industry standard in modeling
hybrid systems; therefore, any quality assurance method is desired to be able
to take Simulink models as its input. This is not easy for formal verification
methods, notably because Simulink models do not have rigorous semantics. The
recent work [13] tackles this problem, identifying a fragment of Simulink, and
devising a translator from Simulink models to $\mathsf{dL}$ programs. Their
translation is ingenious, and their tool is capable of proving rather
complicated properties when used in combination with KeYmaera X [15].

This work is about relational extension of $\mathsf{dL}$. Relational extension
of the _Floyd–Hoare logic_ —as the discrete-time prototype of
$\mathsf{dL}$—has been energetically pursued, too, especially in the context
of _differential privacy_. See e.g. [4, 2, 6].

In deductive verification of hybrid systems, an approach alternative to
Platzer’s $\mathsf{dL}$ uses _nonstandard analysis_ [20] and regards
continuous dynamics as if it is discrete [21, 22]. The logic built on top is
literally the same as the classic Floyd–Hoare logic, whose soundness in the
extended hybrid setting is shown by a model-theoretic result called the
_transfer principle_. Its tool support has been pursued, too [11].

This is not the first time that relational reasoning—in a general sense, as
opposed to the specific sense of §I-E—is pursued in $\mathsf{dL}$.
Specifically, the work [14] introduces the _refinement_ primitive
$\beta\leq\alpha$; it asserts a refinement relation between two hybrid
dynamics, that is, that the set of successor states of $\beta$ is included in
that of $\alpha$. The work [14] is inspired by the software engineering
paradigm of incremental modeling (supported by languages and tools such as
Event-B [1, 5]); the outcome is a rigorous deductive framework for refining an
abstract model (with more nondeterminism) into a more concrete one (with less
nondeterminism). In contrast, as demonstrated in §I-E, we compare one concrete
model (not necessarily with nondeterminism) with another. Here we draw
inspirations from the relational extensions of the Floyd–Hoare logic [4, 2,
6], rather than Event-B. Combining these two orthogonal directions of
relational extension of $\mathsf{dL}$ is important future work.

###  I-G Organization and Notations

In §II we recall the differential dynamic logic $\mathsf{dL}$: its syntax,
semantics and some proof rules. Our target problem of relational reasoning is
formulated in §III, where we introduce a syntactic shorthand
$\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$.
The theory of simulations and the (SIM) proof rule are introduced there, too.
The theory (and its limitation in applicability) motivates our theory of time
stretching in §IV, where we restrict to equational exit conditions. The
resulting (TS) rule, combined with some additional rules that we introduce in
§V, are exploited in the three case studies in §VI. We conclude in §VII.

##  II Preliminaries: the Logic $\mathsf{dL}$

We base ourselves on _differential dynamic logic_ ($\mathsf{dL}$) [16, 17].
While some key concepts and proof rules are recalled here, the reader is
referred to [16, 17] for full details.

###  II-A Syntax

We assume a set of variables that are denoted by $x,y,\dotsc$, and a set of
function symbols $f,g,\dotsc$ that come with the arity information. We write
$\textstyle x$ for a vector of variables $x_{1},\dots,x_{n}$ (following [19]),
and write $f({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ for the application of an
$n$-ary function symbol $f$ to these variables. Finally, we write boldface
${\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ to designate a vector
${\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})=\left(\,f_{1}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}),\,\dotsc,\,f_{m}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\,\right)$ of function
applications.

We first introduce hybrid programs.

######  Definition II.1 (hybrid programs, differential dynamics).

_Hybrid programs_ are defined by the following BNF expression. Here
$\textstyle x$ is a vector of variables,
${\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ is a vector of function
applications where all the function symbols in $\textstyle f$ has the arity
$|{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}|$, and $P,Q$ are formulas of real arithmetic.

${\alpha}_{1},{\alpha}_{2}\;\ {::=}\
\;{?P}\;\mid\;\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\mathbin{\&}Q\;\mid\;{\alpha}_{1};{\alpha}_{2}\;\mid\;{\alpha}_{1}\cup{\alpha}_{2}$

Hybrid programs in the form $\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}Q$ are called
_differential dynamics_ , where
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$ is called its _differential
equation system_ and the formula $Q$ is called its _evolution domain
constraint_. We write simply $\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$ instead of
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}\textsc{true}$.

Hybrid programs here include standard constructs such as tests ($?P$),
sequential compositions and non-deterministic branchings. The _assignment_ and
_iteration_ operators (i.e. $x:=f(x)$ and $\alpha^{*}$) in $\mathsf{dL}$ are
dropped for simplicity, since we do not use them in this paper. Such
constructs can, however, be included if necessary. In this paper, we are
especially interested in analyzing differential dynamics
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}Q$. The intention
is that the dynamics develops according to the differential equation
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$, as long as the evolution
domain constraint $Q$ is satisfied.

######  Definition II.2 ($\mathsf{dL}$ formulas).

Formulas are defined by the following grammar, where ${f}_{1}$ (resp.
${f}_{2}$) is a function symbol with arity
$|{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1}|$ (resp. $|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{2}|$), $x$ is a variable,
$\alpha$ is a hybrid program and $\sim\ \in\\{<,\leq,>,\geq,=\\}$ is a
comparison operator.

$\small\begin{array}[]{l}\varphi,{\varphi}_{1},{\varphi}_{2}\ {::=}\
{f}_{1}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1})\sim{f}_{2}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{2})\mid\neg\varphi\mid{\varphi}_{1}\wedge{\varphi}_{2}\mid\forall
x.\,\varphi\mid\left[\alpha\right]\varphi\mid\langle\alpha\rangle\varphi\end{array}$

Although $\mathsf{dL}$ could allow arbitrary formulas in tests $?P$ and as
evolution domain constraints $Q$, we limit ourselves to first-order formulas
in those constructs. This is also done in [19].

###  II-B Semantics

In this section we briefly recall the interpretation of a $\mathsf{dL}$
formula $\varphi$ from Definition II.2, following [17, 19].

Let $\mathcal{V}=\\{x_{1},\dots,x_{n}\\}$ be the set of variables that occur
in the given formula. A _state_ $\omega\in{\mathbb{R}}^{\mathcal{V}}$ is then
an assignment of a real value to each variable in $\mathcal{V}$. An
_interpretation_ $I$ assigns, to each function symbol $f$ of arity $m$, a
continuous function $I(f):\Omega\rightarrow\mathbb{R}$, where the domain
$\Omega\subseteq{\mathbb{R}}^{m}$ is an open subset.

######  Remark II.3.

For the semantics of $\mathsf{dL}$, not much is required about the
interpretation $I(f)$. It is however common to require that the differential
equation $\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$ has a unique maximal
solution. While the local Lipschitz property is enough (by Picard–Lindelöf’s
theorem), we can also impose a stronger property, such as $C^{1}$, rationals,
polynomials, etc. For the purpose of this paper, any of these suffices,
although in the polynomial case we will need some trick to accommodate the
canonical time stretch function (that is rational per se, see §IV).

From now on, for simplicity, we assume that $I(f)$ is $C^{1}$.

Given a formula $\varphi$, we write
${I}\left\llbracket{\varphi}\right\rrbracket$ for the set of all states in
which $\varphi$ holds in the interpretation $I$. The semantics of comparison
operations and first order formulas are then defined as usual, e.g.
$\omega\in{I}\left\llbracket{{f}_{1}(y_{1},\ldots,y_{k}))\leq{f}_{2}(z_{1},\ldots,z_{l})}\right\rrbracket$
if $I(f_{1})(\omega(y_{1}),\ldots,\omega(y_{k}))\leq
I(f_{2})(\omega(z_{1}),\ldots,\omega(z_{l}))$, and
$\omega\in{I}\left\llbracket{\neg\varphi}\right\rrbracket$ if
$\omega\notin{I}\left\llbracket{\varphi}\right\rrbracket$.

The semantics of hybrid programs are given as transition relations on states,
i.e.
${I}\left\llbracket{\alpha}\right\rrbracket\subseteq{\mathbb{R}}^{n}\times{\mathbb{R}}^{n}$.

######  Definition II.4 (hybrid program semantics).

The semantics of hybrid programs are given inductively as follows.

  1. (1)

${I}\left\llbracket{?P}\right\rrbracket=\\{(\omega,\omega)\mid\omega\in{I}\left\llbracket{P}\right\rrbracket\\}$.

  2. (2)

${I}\left\llbracket{\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\mathbin{\&}Q}\right\rrbracket=\\{({\omega}_{1},{\omega}_{2})\mid{\exists}{t\in{\mathbb{R}}_{\geq
0}}.\>{\omega}_{1}=\psi({0})\wedge\\\
{\omega}_{2}=\psi({t})\wedge{\forall}{{t}^{\prime}\in[0,t]}.\>\psi({{t}^{\prime}})\in{I}\left\llbracket{Q}\right\rrbracket\\}$
where $\psi$ is a solution of the dynamics
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}=I({\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}})({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ on $[0,t]$.

  3. (3)

${I}\left\llbracket{{\alpha}_{1}\cup{\alpha}_{2}}\right\rrbracket={I}\left\llbracket{{\alpha}_{1}}\right\rrbracket\cup{I}\left\llbracket{{\alpha}_{2}}\right\rrbracket$,

  4. (4)

${I}\left\llbracket{{\alpha}_{1};{\alpha}_{2}}\right\rrbracket={I}\left\llbracket{{\alpha}_{1}}\right\rrbracket\circ{I}\left\llbracket{{\alpha}_{2}}\right\rrbracket$.

The semantics of the modal formula
${I}\left\llbracket{\left[\alpha\right]\varphi}\right\rrbracket$ are then
given as $\\{\omega\mid\text{for all
}\omega^{\prime},\,(\omega,{\omega}^{\prime})\in{I}\left\llbracket{\alpha}\right\rrbracket\text{
implies }{\omega}^{\prime}\in{I}\left\llbracket{\varphi}\right\rrbracket\\}$.
For the dual operator:
${I}\left\llbracket{\langle\alpha\rangle\varphi}\right\rrbracket={I}\left\llbracket{\neg\left[\alpha\right]\neg\varphi}\right\rrbracket$.
These are all as in [19].

To ease notation, we write simply $\left\llbracket{\varphi}\right\rrbracket$
or $\left\llbracket{\alpha}\right\rrbracket$ instead of
${I}\left\llbracket{\varphi}\right\rrbracket$ or
${I}\left\llbracket{\alpha}\right\rrbracket$ respectively, the interpretation
$I$ being implicit.

###  II-C Proof Rules

In this paper we use several $\mathsf{dL}$ proof rules taken from the
literature; see e.g. [19, 17]. In particular, we heavily use those rules which
deal with differential dynamics, such as the _differential invariant_ (DI) and
the _differential cut_ (DC) rules.

######  Definition II.5 (some $\mathsf{dL}$ proof rules).

One can use the following proof rules in $\mathsf{dL}$, where
$(\sim,\simeq)\in\\{\,(=,=),(>,\geq),(\geq,\geq)\,\\}$ and
${\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ denotes the Lie derivative of
the function symbol $g$ with arity $\textstyle x$ with respect to the dynamics
given by $\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ [19].

$\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\sim
0\lx@proof@logical@and\Gamma,Q\vdash
g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\sim 0\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\simeq 0$
$\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]\varphi\lx@proof@logical@and\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]C\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}(Q\wedge
C)\right]\varphi$
$\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}Q\right]\varphi
Q\vdash\varphi$

The differential invariant rule (DI) is the central rule for proving safety
properties [19, 17]: it reduces a global property of the dynamics to local
reasoning by the means of Lie derivatives. The differential cut rule (DC) on
the other hand allows the evolution domain constraint $Q$ to be strengthened
by a proposition $C$ that is proven to be invariant throughout the dynamics.
The differential weakening rule (DW) allows to prove the postcondition
directly from the evolution domain constraint, disregarding the differential
dynamics.

##  III Relational Reasoning in Differential Dynamic Logic, and Simulations

We formulate the kind of relational reasoning in $\mathsf{dL}$ that we are
interested in. It turns out that no extension of the syntax is needed,
although we introduce a syntactic shorthand for readability. After doing so in
§III-A, we present our theory of _simulations_ in §III-B, eventually leading
to a syntactic proof rule (SIM) in §III-C.

###  III-A Relational Differential Dynamics (RDD) Formulas

######  Definition III.1 (relational differential dynamics (RDD) formula).

A $\mathsf{dL}$ formula $A$ is called a _relational differential dynamics
formula_ (RDD formula) if it is of the following form:

$A\;\equiv\;\Bigl{(}\,\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}});\;\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}});\;?E\right]B\,\Bigr{)},$

where we require that the variables in $\textstyle x$ and those in
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}$ are disjoint. The expressions $E$ and $B$ are $\mathsf{dL}$
formulas containing variables from both $\textstyle x$ and
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}$.

To improve readability we introduce the following syntax denoting the above
$\mathsf{dL}$ formula:

$A\;\equiv\quad\left[\left\llangle\begin{array}[]{c}{\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})}\\\
\hline\cr{\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})}\end{array}\right\rrangle{E}\right]{B}.$ (4)

It is also written horizontally as:

$\displaystyle
A\;\equiv\quad\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B},\quad$
(5)
$\displaystyle\quad\text{where}\qquad\delta\equiv\left(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\right)\quad\text{and }$
$\displaystyle\quad\phantom{\text{where}}\qquad{\delta}^{\sharp}\equiv\left(\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})\right).$

The formula $E$ is called the _exit condition_ ; the formula $B$ is called the
_postcondition_.

Our interpretation of the RDD formula $A$ in Definition III.1 is that $\delta$
and ${\delta}^{\sharp}$ run in parallel and get synchronized at the end by
means of the exit condition $E$. It is important that the two dynamics can
take different amounts of time; see §I-C.

######  Notation III.2 (solutions $\psi,\psi^{\sharp}$).

In the setting of Definition III.1, by Picard-Lindelöf’s theorem, the
differential equation $\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$ in $\delta$ has a unique
maximal solution, for the initial state
${\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0}$, and its interval of definition is of the form
$[0,T_{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0}})$, with
$T_{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0}}\in\mathbb{R}_{\geq 0}\cup\\{\infty\\}$. This unique solution of
$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})$ from
${\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0}$ is denoted by

$\psi({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},-)\;\colon\quad[0,T_{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0}})\longrightarrow{\mathbb{R}}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}|}.$

Similarly, the unique solution of
$\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})$ in
${\delta}^{\sharp}$ from ${{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0}$ is denoted by
$\psi^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0},-)\colon[0,T^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0}})\rightarrow{\mathbb{R}}^{|{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}|}$. In case the
initial state is obvious, we write simply $\psi({t})$ and
${\psi}^{\sharp}({t})$.

######  Example III.3 (collision speed).

The problem in Example I.1 is expressed as the following RDD formula:
$A\;\equiv\;\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$,
where

$\displaystyle\delta\equiv\bigl{(}\dot{x}=v,\dot{v}=1\bigr{)},\quad{\delta}^{\sharp}\equiv\bigl{(}\dot{x^{\sharp}}=v^{\sharp},\dot{v^{\sharp}}=2\bigr{)},\quad$
$\displaystyle E\equiv\bigl{(}x=x^{\sharp}=1\bigr{)},\quad\text{and
}B\equiv\bigl{(}v\leq v^{\sharp}\bigr{)}.$

###  III-B Simulations for RDD Formulas

Our simulation notion for RDD formulas is based on the following transition
system ${T}_{\delta}$ induced by $\delta$.

######  Definition III.4 (transition system ${T}_{\delta}$).

Let $\delta\equiv\left(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\right)$ be a differential
dynamics. It gives rise to a transition system
${T}_{\delta}=(\mathbb{R}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}|},\xrightarrow{{T}_{\delta}})$,
where the state space is the set
$\mathbb{R}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}|}$ of vectors, and the
transition relation
${\xrightarrow{{T}_{\delta}}}\subseteq\mathbb{R}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}|}\times\mathbb{R}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}|}$ is defined as follows:

$\displaystyle{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1}\xrightarrow{{T}_{\delta}}{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{2}\quad\stackrel{{\scriptstyle\text{def.}}}{{\Longleftrightarrow}}\quad({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1},{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{2})\in\left\llbracket{\delta}\right\rrbracket.$

The definition can be described using the solution $\psi$ of
$\delta\equiv\left(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\right)$ as follows (cf.
Notation III.2): ${\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1}\xrightarrow{{T}_{\delta}}{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{2}$ if and only if there exists
$t\in[0,T_{x_{1}})$ such that 1) ${\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{2}=\psi({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{1},t)$, and 2)
$\psi({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{1},t^{\prime})\in\left\llbracket{Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})}\right\rrbracket$ for each
$t^{\prime}\in[0,t]$.

######  Definition III.5 (simulation).

Let
$A\equiv\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$
be the RDD formula in Definition III.1. A relation
$R\subseteq{\mathbb{R}}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}|}\times{\mathbb{R}}^{|{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}|}$ is a _simulation_
between $\delta$ and ${\delta}^{\sharp}$ if, for any pair
$({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{0})\in R$ and for
any ${{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}_{1}$ such that
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0}\xrightarrow{{T}_{\delta}}{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}_{1}$, there exists
${{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{1}$ such that ${{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{0}\xrightarrow{{T}_{{\delta}^{\sharp}}}{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1}$ and
$({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1})\in R$.

The following properties will be needed in our use of simulations. See
Proposition III.7 later.

######  Definition III.6.

We say a simulation $R$ _supports_ $B$ under $E$ if we have
$R\cap\left\llbracket{E}\right\rrbracket\subseteq\left\llbracket{B}\right\rrbracket$.

We say an exit condition $E$ is _essentially included_ in a simulation $R$ if
we have

$\small\begin{array}[]{l}\left\llbracket{E}\right\rrbracket\cap\left\\{({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{1})\;\Big{|}\;{\exists}{({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{0})\in
R}.\>{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0}\xrightarrow{{T}_{\delta}}{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{0}\xrightarrow{{T}_{{\delta}^{\sharp}}}{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1}\right\\}\subseteq
R.\end{array}$

Here are some intuitions. The support condition guarantees that, as long as we
stay in the simulation $R$, the postcondition $B$ holds when we exit. The
intention behind the essential inclusion condition is that
$\left\llbracket{E}\right\rrbracket$ should be included in $R$, so that $R$
speaks about every possible exit situation. However, the proper inclusion
$\left\llbracket{E}\right\rrbracket\subseteq R$ is too much to ask, especially
when we happen to choose a lax $E$. Therefore essential inclusion restricts
the inclusion requirement to the reachable part.

######  Proposition III.7 (relational reasoning by simulations).

Let
$A\equiv\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$
be the RDD formula in Definition III.1, and let $R$ be a simulation relation
between $\delta$ and ${\delta}^{\sharp}$.

Assume that $R$ supports the postcondition $B$ under the exit condition $E$,
and that $E$ is essentially included in $R$ (Definition III.6). Then we have

$R\subseteq\left\llbracket{A}\right\rrbracket\enspace.$

######  Proof.

Let $({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{0})\in R$ be
arbitrary and let ${{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}_{1}$ be such that
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0}\xrightarrow{{T}_{\delta}}{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}_{1}$. Let us now consider an
arbitrary ${{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1}$ such that
${{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{0}\xrightarrow{{T}_{{\delta}^{\sharp}}}{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1}$ and
$({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{1})\in\left\llbracket{E}\right\rrbracket$. We can assume
such ${{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1}$ to exist as
otherwise, ${({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{0})}\left\llbracket{\delta;{\delta}^{\sharp};?E}\right\rrbracket=\emptyset$.
Since $E$ is essentially included in $R$, we have also
$({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1})\in R$. Finally,
since $R$ supports $B$ under $E$,
$({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{1},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{1})\in
R\cap\left\llbracket{E}\right\rrbracket\subseteq\left\llbracket{B}\right\rrbracket$.
∎

######  Example III.8 (collision speed).

Let us illustrate how we can prove RDD formulas using simulations by solving
our leading example on collision speed (Example I.1). Recall the formal
representation
$A\equiv\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$
of the problem from Example III.3; our goal is to prove that the RDD formula
$A$ is true under the initial condition $\Gamma\equiv(x=x^{\sharp}=0\wedge
v=v^{\sharp}=0)$.

By Proposition III.7, it is enough to construct a simulation
$R\subseteq\mathbb{R}^{2}\times\mathbb{R}^{2}$ that supports the postcondition
$B\equiv(v\leq v^{\sharp})$, such that the exit condition
$E\equiv(x=x^{\sharp}=1)$ is essentially included in $R$. We moreover need
that $R$ contains the initial condition $\Gamma$, i.e.,
$\bigl{(}\,(0,0),\,(0,0)\,\bigr{)}\in R$.

We use the closed-form solutions of the dynamics at hand to construct $R$,
namely

$\displaystyle\psi:\,\mathbb{R}_{\geq
0}\to\mathbb{R}^{2},\qquad\psi(t)=\bigl{(}\,{t^{2}/\,2},\,{t}\,\bigr{)};\text{
and}$ $\displaystyle\psi^{\sharp}:\,\mathbb{R}_{\geq
0}\to\mathbb{R}^{2},\qquad\psi^{\sharp}(t^{\sharp})=\bigl{(}\,{(t^{\sharp})^{2}},\,{2t^{\sharp}}\,\bigr{)}.$

As explained earlier, we want to compare the speeds of those two dynamics at
the same _position_ , not at the same _time_. Thus we want to define $R$ by

$R=\bigl{\\{}\bigl{(}\psi(t),\psi^{\sharp}(t^{\sharp})\bigr{)}\mid\pi_{1}\bigl{(}\psi(t)\bigr{)}=\pi_{1}\bigl{(}\psi^{\sharp}(t^{\sharp})\bigr{)}\bigr{\\}},$

where $\pi_{1}$ is the first projection (extracting positions). Solving
$\frac{t^{2}}{2}=\pi_{1}(\psi(t))=\pi_{1}(\psi^{\sharp}(t^{\sharp}))=(t^{\sharp})^{2}$,
we obtain

$R=\bigl{\\{}\,\bigl{(}\,({t^{2}/\,2},\,{t}),\,({t^{2}/\,2},\,{\sqrt{2}t})\,\bigr{)}\;\big{\mid}\;t\in\mathbb{R}_{\geq
0}\,\bigr{\\}}$

It is then easy to check that $R$ is indeed a simulation that satisfies the
assumptions of Proposition III.7.

###  III-C Simulation Based Proof Rule

Using Proposition III.7, we formulate a syntactic $\mathsf{dL}$ proof rule
which allows proving an RDD formula using a simulation.

######  Definition III.9 (simulation proof rule (SIM)).

The _simulation rule_ is given as follows, using four premises.

$\Gamma\vdash\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}\begin{matrix}R\vdash\left[\delta\right]\langle{\delta}^{\sharp}\rangle
R\qquad R,E\vdash B\qquad
R\vdash\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{R}\\\
\Gamma\vdash\left[?Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})\right]R\end{matrix}$

Note that, to be precise, $R$ here is a $\mathsf{dL}$ formula whose
interpretation is indented to be a simulation.

The first premise expresses the simulation condition on $R$; the second is for
the support of $B$ under $E$; the third is the essential inclusion of $E$ in
$R$; and the last demands that $R$ holds in the initial states.

We observe that, in the (SIM) rule, the conditions required of $R$ in
Proposition III.7 are succinctly expressed in the $\mathsf{dL}$ syntax. In
particular, the deft expression
$R\vdash\left[\delta\right]\langle{\delta}^{\sharp}\rangle R$ of the
simulation condition by the combination of two modalities demonstrates the
versatility of $\mathsf{dL}$.

######  Theorem III.10.

The simulation proof rule (SIM) in Definition III.9 is sound. ∎

######  Remark III.11.

How useful the rule (SIM) is depends on the expressivity of the logic
$\mathsf{dL}$, that is, how many simulations $R$ we can express in the logic.
Given the close tie between the theory of (bi)simulations and that of fixed
points (such as the Knaster–Tarski theorem), we expect it be useful to be able
to express fixed points in $\mathsf{dL}$. A possible example is an extension
of the $\mathsf{dL}$ syntax that has the least and greatest fixed operators: a
user writes a function $\Phi$ and the expression $\mu x.\,\Phi(x)$ designates
its fixed point. Such extension of $\mathsf{dL}$ is future work.

##  IV Time Stretch Functions and Reasoning Thereby

Although theoretically simple and foundational, the simulation rule (SIM)
introduced in Definition III.9 is largely generic making it impractical for
many properties. In particular, the proof of the first premise, showing that
$R$ is in fact a simulation, is likely to require explicit solution of (some)
of the differential equations.

To avoid the need for explicit solutions, and following the intuitions that we
developed in §III, we introduce another construction which, although only
usable under constrained circumstances, provides a nice way to compare two
different dynamics. If simulations compare states, this new construction
features a function that relates the elapsed times of the two dynamics. It is
called a _time stretch function_. The main goal of this section is to describe
this semantical tool in order to design a proof rule in $\mathsf{dL}$ allowing
us to prove relational differential dynamics formulas. After some semantical
preparations, describing some fundamental properties of time stretching – much
as synchronizing two dynamics according some exit conditions – we prove the
soundness of our rule.

We will illustrate the usefulness of this rule in §VI, by solving examples
inspired by our collaboration with the industry.

###  IV-A Time Stretch Functions

A time stretch function is just a monotonic rescaling of time:

######  Definition IV.1 (time stretch function).

Let $T\in\mathbb{R}_{\geq 0}$. A function $k\colon[0,T]\to{\mathbb{R}}_{\geq
0}$ is called a _time stretch function_ if $k$ is $C^{1}$, $k(0)=0$ and
$\dot{k}(t)>0$ for each $t\in[0,T]$.

######  Remark IV.2.

In particular, $k$ is strictly increasing. Then $k$ is a bijection from
$[0,T]$ to $[0,k(T)]$. We denote the inverse from $[0,k(T)]$ to $[0,T]$ by
$k^{-1}$.

###  IV-B Stretched Dynamics

Our main interest of a time stretch function is to relate states of two
different dynamics, much as those of a relational differential dynamics
formula
$A\;\equiv\;\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$.
More precisely, a time stretch function will relate a time of one dynamics to
a time of the other. This will allow us to combine two dynamics (with two
different time scales) into one (with a unique time scale). In this section,
we look at how to rescale a dynamic by using a time stretch function and prove
the dynamics produced by this process visits the same states as the initial
dynamics, but at a different time.

######  Definition IV.3 (stretched dynamics ${{\delta}^{\sharp}}_{k}$).

Let $A$ be the RDD formula in Definition III.1, and let $k$ be a time stretch
function (Definition IV.1). From a dynamics
${\delta}^{\sharp}\equiv(\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}))$, we obtain a new
dynamics

${{\delta}^{\sharp}}_{k}\equiv\Bigl{(}\bigl{(}\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\cdot\dot{k}(t)\bigr{)}\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})\Bigr{)}.$ (6)

The dynamics ${{\delta}^{\sharp}}_{k}$ is called the dynamics _stretched by_
$k$.

Definition IV.3 of the stretched dynamics relies on the time $t$. This is not
a real problem, as we will not use this stretched dynamics inside
$\mathsf{dL}$, but only to help our proofs, the continuity of the derivative
of $k$ being enough to apply Picard-Lindelöf’s theorem. We can, however, use
it inside dL by assuming $t$ to be a part of the $\textstyle x$ vector and
requiring $k$ to be smooth enough, e.g., $C^{2}$. Provided the solution
${\psi}_{k}$ of the stretched system exists at the relevant interval, it
retains the results of the solutions of the original system:

######  Lemma IV.4.

Let $A$ be the RDD formula in Definition III.1, $k$ be a time stretch function
and ${{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}_{0}\in\mathbb{R}^{|{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}|}$. Let
$T\in{\mathbb{R}}_{\geq 0}$ be arbitrary such that ${\delta}^{\sharp}$ has a
solution ${\psi}^{\sharp}$ on $[0,k(T)]$. Then the function that maps $t$ to
${\psi}^{\sharp}(k(t))$ is a solution of the stretched dynamics
${\delta}_{k}$.

Reciprocally, if the stretched dynamics ${\delta}_{k}$ has a solution
${\psi}_{k}$ on $[0,T]$, then the function that maps ${t}^{\sharp}$ to
${\psi}_{k}({k}^{-1}({t}^{\sharp}))$ is a solution of ${\delta}^{\sharp}$ on
$[0,k(T)]$, with $k^{-1}$ being the inverse of $k$ (see Remark IV.2).

######  Proof.

Both directions boils down in deriving the candidate solutions:

  * •

For the first direction,
$\frac{d{\psi}^{\sharp}(k(t))}{dt}(s)=\dot{k}(s)\cdot\dot{{\psi}^{\sharp}}(k(s))=\dot{k}(s)\cdot{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({\psi}^{\sharp}(k(s)))$.

  * •

For the other direction,
$\frac{d{\psi}_{k}(k^{-1}(t))}{dt}(s)=\dot{k^{-1}}(s)\cdot\dot{{\psi}_{k}}(k^{-1}(s))=\frac{1}{\dot{k}(k^{-1}(s))}\cdot\dot{k}(k^{-1}(s))\cdot{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({\psi}_{k}(k^{-1}(s)))={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({\psi}_{k}(k^{-1}(s))$. ∎

###  IV-C Canonical Time Stretching, Semantically

For the moment, the time stretch function arbitrarily relates states of two
dynamics, keeping the same solutions. Now, we would like to construct
particular time stretch functions so that the two dynamics synchronize their
exit time. Given an RDD formula $A$ as in Definition III.1, we restrict the
exit condition to a single equality
$E\equiv(g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}))$ with $g$ and
${g}^{\sharp}$ strictly monotonic in some sense. We show it is possible to
obtain a time stretch function $k$ from $\delta,{\delta}^{\sharp},g$ and
${g}^{\sharp}$.

######  Definition IV.5 (monotonic exit condition).

Let $A$ be an RDD formula as in Definition III.1. Assume that the exit
condition $E\equiv(g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}))$ is an equality,
with $g$ and ${g}^{\sharp}$ smooth enough (e.g., $C^{2}$).

Given $({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$, let us define
the following two functions:

$\displaystyle g_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}\colon[0,T_{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0}})\longrightarrow\mathbb{R},$
$\displaystyle g_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}(t)=g(\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0},t}));$
$\displaystyle{g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}\colon[0,T_{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0}})\longrightarrow\mathbb{R},$
$\displaystyle{g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}(t^{\sharp})={g}^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},t^{\sharp}})).$

We say that the exit condition $E$ in $A$ is _monotonic at
$({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$_ if the
derivatives of $g_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}$ and
${g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}$ are both strictly
positive or both strictly negative.

######  Definition IV.6 (canonical time stretch function).

Let $({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}_{0},{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}_{0})$ be some initial
states, and $A$ be an RDD formula as in Definition III.1. Assume that the exit
condition $E\equiv(g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}))$ is monotonic at
$({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$ (Definition
IV.5) and that $g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0})={g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$. Assume given
$t,t^{\sharp}\in\mathbb{R}_{\geq 0}$ with
$g(\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},t}))={g}^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},t^{\sharp}}))$.
Then we define the function:

$k\colon[0,t]\longrightarrow[0,t^{\sharp}],\quad
k(s)=({g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}})^{-1}\circ
g_{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}(s)$

called the _canonical time stretch function_.

######  Proposition IV.7.

In the setting of Definition IV.6, $k$ is a time stretch function with
$k(t)=t^{\sharp}$.

######  Proof.

First, let us prove that $k$ is well-defined. Since
${g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}$ is strictly
monotonic on $[0,t^{\sharp}]$, it has an inverse
$h=({g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}})^{-1}$, defined from
${g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}([0,t^{\sharp}])$ to
$[0,t^{\sharp}]$. By assumption,
${g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}(0)=g_{f}(0)$ and
${g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}(t^{\sharp})=g_{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}(t)$, so that $h$ is defined from
$g_{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}([0,t])$ to $[0,t^{\sharp}]$. Then $k$ is defined from $[0,t]$ to
$[0,t^{\sharp}]$. Furthermore, since $g$ and ${g}^{\sharp}$ are continuously
differentiable and $\textstyle f$ and
${{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle
f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}$ are continuous, $k$ is $C^{1}$. Since
$g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0})={g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$, then $k(0)=0$.
Finally,

$\dot{k}(s)$ | $=$ | $\dot{g_{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}(s)\dot{h}(g_{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}(s))$ |  | derivation of $h\circ g_{f}$
---|---|---|---|---
| $=$ | $\frac{\dot{g_{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}(s)}{\dot{{g}^{\sharp}_{{{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}}(k(s))}$ |  | derivation of $h=(g_{f})^{-1}$

which is strictly positive by monotonicity of the exit condition. ∎

###  IV-D Towards a Syntactic Representation

From now on, we aim at a syntactic representation of the reasoning with time
stretch functions inside $\mathsf{dL}$. We answer the following question: Is
there any suitable sound rule that we can use to prove RDD formulas, using
time stretch functions?

The main idea is to combine the two dynamics $\delta$ and ${\delta}^{\sharp}$
using the canonical time stretch function $k$, in order to get a unique
dynamics, and do proofs in $\mathsf{dL}$ on this new dynamics instead. A
natural way to combine $\delta$ and ${\delta}^{\sharp}$ would be to study the
stretched dynamics by $k$ (Definition IV.3):

$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}),\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={f}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\cdot\dot{k}(t)\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})$

When we expand the definition of $k$ we obtain the following:

$\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}),\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}=\frac{\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}(\psi({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},t))}{\mathcal{L}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}(\psi^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0},k(t)))}\cdot{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})$

The problem is that this dynamics is not practical as it depends on the
initial conditions and the actual solutions of the dynamics. However, using
Lemma IV.4, we can replace the solution
$\psi^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(t))$ by
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}$ and, by construction, we can replace the solution
$\psi({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0},t)$ by $\textstyle x$, which
leads to:

######  Definition IV.8.

In the setting of Definition IV.6, we define:

$\delta_{A}\equiv\Bigl{(}\bigl{(}\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}),\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}=\frac{\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})}{\mathcal{L}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})}\cdot{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\bigr{)}\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})\Bigr{)}$

called the _synchronized dynamics_.

######  Remark IV.9.

Observe that, since $g$ and ${g}^{\sharp}$ are $C^{2}$, the function that maps
${\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}$ to
$\frac{\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})}{\mathcal{L}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})}\cdot{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})$ is $C^{1}$, as
required in Remark II.3.

The following will be the main argument of the proof of soundness of our
$\mathsf{dL}$ rule, stating that, much as the stretched dynamics, the combined
dynamics preserves the visited states.

######  Proposition IV.10.

Assume given ${\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0}\in\mathbb{R}^{|{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}|}$ and
${{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0}\in\mathbb{R}^{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}$ such that
$g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0})={g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$, and the exit
condition is monotonic.

Assume $t,t^{\sharp}\in\mathbb{R}_{\geq 0}$ with
$g(\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},t}))={g}^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},t^{\sharp}}))$.
Then the function which maps $s\in[0,t]$ to

$(\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},s}),{\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)}))$

is a solution of the synchronized dynamics on $[0,t]$, with the initial
condition $({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$.

Reciprocally, assume that $(\Phi,\Phi^{\sharp})$ is a solution of $\delta_{A}$
on $[0,T]$, with the initial condition
$({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})$, then $\Phi$,
$\Phi^{\sharp}$ allow the presentation:

$\Phi=\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},\\_})\quad\quad\Phi^{\sharp}={\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},\bar{k}(\\_)})$

where $\bar{k}$ is some time stretch function. Furthermore, for every
$s\in[0,T]$, $g(\Phi(s))={g}^{\sharp}(\Phi^{\sharp}(s))$.

######  Proof.

For the first direction, the only thing to prove is that
$\theta(s)={\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)})$ is
solution of $\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}=\frac{{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}\,({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})}{{\mathcal{L}}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}\,({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})}{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})$:

$\dot{\theta}(s)$ | $=$ | $\dot{k}(s)f^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)}))$
---|---|---
| $=$ | $\frac{\dot{g_{f}}(s)}{\dot{g^{\sharp}_{f^{\sharp}}}(k(s))}f^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)}))$
| $=$ | $\frac{{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}{g}\,(\psi({{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0},s}))}{{\mathcal{L}}_{{{\mathchoice{\text{\boldmath$\displaystyle f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle f$}}{\text{\boldmath$\scriptscriptstyle f$}}}}^{\sharp}}{{g}^{\sharp}}\,({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)}))}f^{\sharp}({\psi}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0},k(s)}))$

For the other direction, let us first observe that
$\Phi=\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0},\\_})$ is obvious by unicity
of the solution. Now, let us construct $\bar{k}$. It is defined as the unique
primitive of the function
$h(s)=\frac{\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}(\Phi(s))}{\mathcal{L}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}(\Phi^{\sharp}(s))}$ such that $\bar{k}(0)=0$.
To prove that $\bar{k}$ is a time stretch function, it only remains to prove
that its derivative $h$ is strictly positive.
$h(0)=\frac{\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0})}{\mathcal{L}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{{g}^{\sharp}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0}))}$, which is
strictly positive by monotonicity of the exit condition. Since
$\Phi=\psi({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}_{0},\\_})$, and again by
monotonicity of the exit solution, we know that $h$ never takes the value $0$.
Finally, since $h$ is continuous, it is always strictly positive. So then, we
can look at the stretched dynamics ${\delta}^{\sharp}_{\bar{k}}$. By
construction, $\Phi^{\sharp}$ is a solution of ${\delta}^{\sharp}_{\bar{k}}$
on $[0,t]$, so we can conclude using Lemma IV.4. Finally, the last requirement
is proved as follows. Define the following continuously derivable functions on
$[0,T]$:

$r(s)=g(\Phi(s)),\quad r^{\sharp}(s)={g}^{\sharp}(\Phi^{\sharp}(s)).$

Those functions are equal because:
$r(0)=g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0})={g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}_{0})=r^{\sharp}(0)$,
and $\dot{r}(s)=\mathcal{L}_{f}g(\Phi(s))=\dot{r^{\sharp}}(s)$. ∎

###  IV-E Time Stretch Function Based Proof Rule

Now, we have all the semantical ingredients to describe our $\mathsf{dL}$ rule
and prove its soundness. We call it the _time stretch rule_ (TS); it utilizes
the synchronized dynamics to combine the two differential dynamics. Once the
dynamics are synchronized, the time stretch rule may be easily followed by
other $\mathsf{dL}$ rules previously developed for non-relational reasoning.
The rule derives an equivalence, much as the (DI) rule as presented in [17].

######  Definition IV.11 (time stretch proof rule).

Let
$A\equiv\left[\left\llangle{\delta}\;{|}\;{{\delta}^{\sharp}}\right\rrangle{E}\right]{B}$
be the RDD formula in Definition III.1.

The time stretch proof rule for $A$ is defined as follows.

$\Gamma\vdash\left[\llangle\delta\mid{\delta}^{\sharp}\rrangle
E\right]B\Longleftrightarrow\left[{\delta}_{A}\right]B\lx@proof@logical@and\Gamma\vdash\left[?Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\right]E\Gamma\vdash\left[\delta;{\delta}^{\sharp}\right]\frac{{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})}{{\mathcal{L}}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})}>0$

Note that the time stretch rule (TS) uses the standard $\mathsf{dL}$ syntax
and is therefore readily integrable with the rest of the $\mathsf{dL}$ proof
rules and into the theorem prover KeYmaera X.

######  Theorem IV.12.

The time stretch proof rule (TS) as defined in Definition IV.11 is sound.

######  Proof.

Assume that the premises hold. Assume given
$({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}_{0},{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}_{0})\in\left\llbracket{\Gamma}\right\rrbracket$. Both
directions of the (TS) rule are consequences of Proposition IV.10, since the
premises imply its assumptions. ∎

##  V Differential Inductive Invariants and Other Auxiliary Proof Rules

Here we introduce some auxiliary proof rules that we find crucial in many
examples of relational reasoning in $\mathsf{dL}$.

###  V-A Differential Inductive Invariants

It turns out that the differential invariant rule (DI) as introduced in
Definition II.5, although powerful, falls short of being able to capture some
invariant properties. As we have encountered such properties in our case
studies, we propose an inductive version of the differential invariant, which,
although slightly less general, provides more power by including the
postcondition in the evolution domain constraint.

######  Definition V.1.

Fix $n\geq 1$. The $n$-th order differential inductive invariant
($\text{DII}_{n}$) proof rule is given as follows, assuming that $\textstyle
f$ is $C^{n-1}$ and $g$ are $C^{n}$ and $\delta$ is a shorthand for the
differential dynamics
$\delta\equiv\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\mathbin{\&}Q\wedge
g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\geq 0$:

$\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\geq
0\lx@proof@logical@and\Gamma,Q\vdash
g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\geq
0\Gamma\vdash\left[\delta\right]D_{n}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$

where

$D_{n}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\,\equiv\,\bigvee\limits_{p=0}^{n-1}\Bigl{(}\bigwedge\limits_{k=1}^{p}{\mathcal{L}^{(k)}_{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\geq
0\Bigr{)}\wedge{\mathcal{L}^{(p+1)}_{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})>0$

and ${\mathcal{L}^{(k)}_{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle f$}}}g}$ is the $k$-th Lie derivative
of $g$ with respect to $\textstyle f$.

In particular, ($\text{DII}_{1}$) will be of particular use:

$\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q\right]g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\geq
0\lx@proof@logical@and\Gamma,Q\vdash
g({\mathchoice{\text{\boldmath$\displaystyle x$}}{\text{\boldmath$\textstyle
x$}}{\text{\boldmath$\scriptstyle x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\geq
0\Gamma\vdash\left[\delta\right]\mathcal{L}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})>0$

######  Theorem V.2.

The differential inductive invariant rules ($\text{DII}_{n}$) in Definition
V.1 are sound.

###  V-B Auxiliary Relational Rules

The following rules, while many of them are rather straightforward, play
essential roles in many examples of relational reasoning. We may further
identify two main categories of the auxiliary rules, first, rules that allow
us to manipulate or introduce (monotonic) equality exit conditions; second,
rules that facilitate relational reasoning in the standard syntax of
$\mathsf{dL}$.

####  V-B1 Monotonic Condition Swap

First auxiliary rule we introduce is the _monotonic condition swap_ rule
($\mathrm{MCS}$). $\mathrm{MCS}$ swaps the exit condition with the
postcondition, given the postcondition is given as inequality and some
monotonicity criteria are satisfied. Swapping the exit condition and the
postcondition is useful for obtaining exit conditions with simpler derivatives
(as illustrated in §VI-A) or to align the exit condition with initial
condition (§VI-B).

The $\mathrm{MCS}$ rule comes in several variations based on the direction of
the monotonicity of the functions involved in the exit condition and
postcondition. The variation when all functions are increasing is given in
Figure 2.

$\inferrule*[Right=MCS]{\Gamma\vdash\left[\left\llangle\begin{array}[]{c}{\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})}\\\
\hline\cr{\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})}\end{array}\right\rrangle{h({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})=h^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})}\right]{g({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\geq{g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})}\\\
\Gamma\vdash\left[?Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\wedge{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\right]h({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\leq
h^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})\\\
\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\right]{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}{g}({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})>0\\\
\Gamma\vdash\left[\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\right]{\mathcal{L}}_{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}h({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\geq 0\qquad\\\
\Gamma\vdash\left[\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\right]{\mathcal{L}}_{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}{h^{\sharp}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})\geq
0}{\Gamma\vdash\left[\left\llangle\begin{array}[]{c}{\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})}\\\
\hline\cr{\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})}\end{array}\right\rrangle{g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})}\right]{h({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\leq
h^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})}}$ Figure 2: Proof
rule for monotonic condition swap for relations using monotonically increasing
functions.

######  Theorem V.3.

The _monotonic condition swap (MCS)_ rule as given in Figure 2 is sound.

####  V-B2 Generating Exit Conditions

The other proof rules designed to manipulate equality exit conditions are the
_relational differential cut_ ($\mathrm{RDC}$) and _exit condition
propagation_ ($\mathrm{ECP}$) rules. $\mathrm{RDC}$ introduces new equality
exit condition based on other tests in style of differential cut rule
($\mathrm{DC}$). $\mathrm{ECP}$ allows to copy the exit condition to an
earlier place in the dynamics under some monotonicity conditions.

######  Definition V.4 (relational differential cut rule).

The _relational differential cut_ rule is given as follows, where
$\delta\equiv(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}))$ and
${\delta}^{\sharp}\equiv(\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\mathbin{\&}{Q}^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}}))$ are differential
dynamics, $\alpha$ and $\beta$ are shorthands for the hybrid programs:

$\alpha\equiv\delta;{\delta}^{\sharp};?g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}});?P\qquad\beta\equiv\delta;{\delta}^{\sharp};?P$
$\Gamma\vdash\left[\delta;{\delta}^{\sharp};?P\right]\varphi\Gamma\vdash\left[\alpha\right]\varphi\qquad\Gamma\vdash\left[\beta\right]g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})$

######  Theorem V.5.

The relational differential cut (RDC) rule is sound.

######  Definition V.6 (exit condition propagation rule).

The _exit condition propagation_ rule is given as follows, where
$\delta\equiv(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}))$,
${{\delta}^{\sharp}}_{1}\equiv(\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}_{1}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\mathbin{\&}{{Q}^{\sharp}}_{1}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}))$ and
${{\delta}^{\sharp}}_{2}\equiv(\dot{{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}}={{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}_{2}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\mathbin{\&}{{Q}^{\sharp}}_{2}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}))$ are differential
dynamics, and $\alpha$ is a shorthand for the hybrid program:

$\alpha\equiv\delta;{{\delta}^{\sharp}}_{1};?g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}});?P({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp});\delta;{{\delta}^{\sharp}}_{2};?g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp}})$
$\Gamma\vdash\left[\delta;{{\delta}^{\sharp}}_{1};?P({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp});{{\delta}^{\sharp}}_{2};?g({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})=g^{\sharp}({{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp}})\right]\varphi\begin{matrix}\Gamma\vdash\left[\alpha\right]\varphi\\\
\Gamma\vdash\left[{{\delta}^{\sharp}}_{1}\right]{\mathcal{L}}_{{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}_{1}}{g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})\geq
0\quad\Gamma\vdash\left[{{\delta}^{\sharp}}_{1};{{\delta}^{\sharp}}_{2}\right]{\mathcal{L}}_{{{{\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}}^{\sharp}}_{2}}{g}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}}^{\sharp})\geq 0\end{matrix}$

######  Theorem V.7.

The exit condition propagation rule ($\mathrm{ECP}$) is sound.

###  V-C Commutation and Absorption

Finally, we introduce rather straightforward, but convenient rules which allow
us to comfortably manipulate relational differential dynamics formulas within
the classical syntax of $\mathsf{dL}$. The _sequential composition
commutativity_ rule ($\mathrm{SCC}$) allows us to swap hybrid programs acting
on different variables, as they are independent to each other. The _merge
identical dynamics_ rule ($\mathrm{MID}$) simply allows to merge two identical
differential dynamics which directly follow each other.

######  Definition V.8 (sequential composition commutativity rule).

The _sequential composition commutativity_ rule is given as follows in two
versions (one for each modality), where
$\alpha({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})$ denotes a hybrid program which
acts on variables in $\textstyle x$ only.

$\Gamma\vdash\left[\alpha({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}});{\alpha}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\right]\varphi\Gamma\vdash\left[{\alpha}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp});\alpha({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}})\right]\varphi\quad\Gamma\vdash\langle\alpha({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}});{\alpha}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp})\rangle\varphi\Gamma\vdash\langle{\alpha}^{\sharp}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}^{\sharp});\alpha({\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}})\rangle\varphi$

######  Theorem V.9.

The sequential composition commutativity rules ($\text{SCC}_{[-]}$ and
$\text{SCC}_{\langle-\rangle}$) are sound.

######  Definition V.10 (merge identical dynamics rule).

The _merge identical dynamics_ rule is given as follows in two versions (one
for each modality), where
$\delta\equiv\left(\dot{{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}}={\mathchoice{\text{\boldmath$\displaystyle
f$}}{\text{\boldmath$\textstyle f$}}{\text{\boldmath$\scriptstyle
f$}}{\text{\boldmath$\scriptscriptstyle
f$}}}({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle
x$}}}})\mathbin{\&}Q({{\mathchoice{\text{\boldmath$\displaystyle
x$}}{\text{\boldmath$\textstyle x$}}{\text{\boldmath$\scriptstyle
x$}}{\text{\boldmath$\scriptscriptstyle x$}}}})\right)$ is a differential
dynamics (Definition II.1).

$\Gamma\vdash\left[\delta;\delta\right]\varphi\Gamma\vdash\left[\delta\right]\varphi\quad\quad\quad\Gamma\vdash\langle\delta;\delta\rangle\varphi\Gamma\vdash\langle\delta\rangle\varphi$

######  Theorem V.11.