Relational Differential Dynamic Logic
193
1
√
2
√
2
2
˙
v = 2
˙
v = 1
t
v
The two hatched areas designate the traveled distances (x = x = 1). We can compute
the collision speeds (v =
√
2 and v = 2)
via the closed-form solutions of the differential equations (1), concluding v ≤ v when
x = x = 1.
Fig. 1. An ad-hoc proof for Example 1
respectively. Their dynamics are governed by the following differential equations:
˙
x = v, ˙
v = 1;
˙
x = v, ˙
v = 2.
(1)
Both cars start at the same position at rest (x = x = 0 ∧ v = v = 0), and
both drive towards a wall at position 1. We consider this question: which car is
traveling faster when it hits the wall?
The second car, C, has strictly greater acceleration all the time, so we can
imagine that C hits the wall harder. This hypothesis turns out to be correct, but
we are more interested in how this claim could be proven.
A simple proof would be to solve the differential equation exactly and notice
C has greater velocity at the end of its run. However, it is known that closed-form
solutions are scarce for ODEs—we want a proof method that is more general.
Another possible argument is based on the relationship between the accelerations. Since the second car’s acceleration is greater at every point in time,
we might be tempted to conclude that the second car’s velocity must always
be greater than the first car’s, based on the monotonicity of integration: a(t) ≤
a(t) ⇒ v(t) =
T
0
a(t) dt ≤
T
0
a(t) dt = v(t). However, this reasoning has a flaw.
C reaches the wall at an earlier point in time than C, and therefore C has more
time to accelerate. In the end, we have to compare
T
0
a(t) dt and
T
0
a(t) dt
where a(t) ≤ a(t) for all t ∈ [0, T ] but T > T, as depicted in figure 1.
Our solution, roughly stated, is to compare the two cars at the same points
in space by reparametrizing time for one of the two cars. This parametrization
is specially chosen to ensure the two cars pass through the same points in space
at the same points in time.
Our current work is about a logical infrastructure needed to support this
kind of relational reasoning comparing two different dynamics, based on dL. Our
semantical theory, as well as the resulting syntactic extension of dL by what
193
1
√
2
√
2
2
˙
v = 2
˙
v = 1
t
v
The two hatched areas designate the traveled distances (x = x = 1). We can compute
the collision speeds (v =
√
2 and v = 2)
via the closed-form solutions of the differential equations (1), concluding v ≤ v when
x = x = 1.
Fig. 1. An ad-hoc proof for Example 1
respectively. Their dynamics are governed by the following differential equations:
˙
x = v, ˙
v = 1;
˙
x = v, ˙
v = 2.
(1)
Both cars start at the same position at rest (x = x = 0 ∧ v = v = 0), and
both drive towards a wall at position 1. We consider this question: which car is
traveling faster when it hits the wall?
The second car, C, has strictly greater acceleration all the time, so we can
imagine that C hits the wall harder. This hypothesis turns out to be correct, but
we are more interested in how this claim could be proven.
A simple proof would be to solve the differential equation exactly and notice
C has greater velocity at the end of its run. However, it is known that closed-form
solutions are scarce for ODEs—we want a proof method that is more general.
Another possible argument is based on the relationship between the accelerations. Since the second car’s acceleration is greater at every point in time,
we might be tempted to conclude that the second car’s velocity must always
be greater than the first car’s, based on the monotonicity of integration: a(t) ≤
a(t) ⇒ v(t) =
T
0
a(t) dt ≤
T
0
a(t) dt = v(t). However, this reasoning has a flaw.
C reaches the wall at an earlier point in time than C, and therefore C has more
time to accelerate. In the end, we have to compare
T
0
a(t) dt and
T
0
a(t) dt
where a(t) ≤ a(t) for all t ∈ [0, T ] but T > T, as depicted in figure 1.
Our solution, roughly stated, is to compare the two cars at the same points
in space by reparametrizing time for one of the two cars. This parametrization
is specially chosen to ensure the two cars pass through the same points in space
at the same points in time.
Our current work is about a logical infrastructure needed to support this
kind of relational reasoning comparing two different dynamics, based on dL. Our
semantical theory, as well as the resulting syntactic extension of dL by what