Relational Differential Dynamic Logic
205
One might try to show the inequality v − v ≥ 0 by the differential invariant
(DI) rule, but the Lie derivative of the term v − v is a − a · (v/v), which is not
obviously nonnegative. Instead, a trickier expression a·(v
2
−v
2
0 )−a·(v
2
−v
2
0 ) = 0
turns out to be an invariant. Its Lie derivative is a · (2v) · a · (v/v) − a · (2v) · a,
which is clearly 0, since we also know v > 0.
We do not have an intuitive explanation for this invariant, but it was found
by a template-based search, like many other invariants in dL. By positing the
existence of a polynomial invariant of a certain degree, we can find conditions on
the coefficients by requiring its Lie derivative and initial value are zero. Solving
these conditions for a second-degree invariant on the velocities in the system
yielded the invariant above.
After finding our invariant, we additionally have to show the invariant entails
our desired result, v ≤ v. This can be shown with a standard monotonicity
property of modal logics: from φ ψ and Γ [α]φ, we can conclude Γ [α]ψ,
where φ states the expression above is an invariant and the velocities are always
greater than their initial value, and ψ is our goal: v ≤ v.
6.2 Collision Speed with Different Kinds of Friction
Here we continue Example 11, where we consider two dynamics δ F ≡ ( ˙
x = v, ˙
v =
−v
2 ) and δ F ≡ ( ˙
x = v, ˙
v = −v). Our goal is Γ F [ δ F ; δ F ](x = x = l ⇒ v ≤ v),
with Γ F := {x = x = 0, 0 < v ≤ v ≤ 1}.
First, we establish the fact that the objects in this example always have
positive velocity. We show this by the (Dbx) rule (Definition 13), where L δ F v =
−v
2 and L δ F v = −v. This allows us to infer v > 0 and v > 0 hold at all times.
We apply the (Sync) rule along x = x, yielding the synchronized dynamics
˙
x = v, ˙
v = −v
2
, ˙
x = v · (v/v), ˙
v = −v · (v/v) & v > 0 ∧ v > 0
Note that the new evolution domain condition v > 0 allows us to rewrite v · (v/v)
to v. The synchronizability conditions follow immediately from the fact that
v > 0 and v > 0. For the synchronized formula, we apply the (DI) rule, so the
desired inequality v ≥ v is reduced to v
2
≤ v, that is, v ≤ 1. To this end, v > 0
tells us that the derivative of v, that is, −v
2 , is always negative, therefore v ≤ 1.
6.3 Model Refinement
In this example, we consider two abstract models of cars. The first car is able
to provide a high amount of constant acceleration a at low velocities, but at a
certain velocity v cut the engine switches to a different mode and then provides a
lesser, but still constant acceleration a cut . The second car is an abstracted version
of the first, which ignores this mode change and provides the same constant
amount of acceleration a at all velocities. Our aim in this example is to establish
a safety envelope around the first car’s behavior using the more simply stated
second car’s dynamics. Hence we show that the second car’s velocity is greater
than the first’s at any position x = x = l. More formally, the behavior of the
205
One might try to show the inequality v − v ≥ 0 by the differential invariant
(DI) rule, but the Lie derivative of the term v − v is a − a · (v/v), which is not
obviously nonnegative. Instead, a trickier expression a·(v
2
−v
2
0 )−a·(v
2
−v
2
0 ) = 0
turns out to be an invariant. Its Lie derivative is a · (2v) · a · (v/v) − a · (2v) · a,
which is clearly 0, since we also know v > 0.
We do not have an intuitive explanation for this invariant, but it was found
by a template-based search, like many other invariants in dL. By positing the
existence of a polynomial invariant of a certain degree, we can find conditions on
the coefficients by requiring its Lie derivative and initial value are zero. Solving
these conditions for a second-degree invariant on the velocities in the system
yielded the invariant above.
After finding our invariant, we additionally have to show the invariant entails
our desired result, v ≤ v. This can be shown with a standard monotonicity
property of modal logics: from φ ψ and Γ [α]φ, we can conclude Γ [α]ψ,
where φ states the expression above is an invariant and the velocities are always
greater than their initial value, and ψ is our goal: v ≤ v.
6.2 Collision Speed with Different Kinds of Friction
Here we continue Example 11, where we consider two dynamics δ F ≡ ( ˙
x = v, ˙
v =
−v
2 ) and δ F ≡ ( ˙
x = v, ˙
v = −v). Our goal is Γ F [ δ F ; δ F ](x = x = l ⇒ v ≤ v),
with Γ F := {x = x = 0, 0 < v ≤ v ≤ 1}.
First, we establish the fact that the objects in this example always have
positive velocity. We show this by the (Dbx) rule (Definition 13), where L δ F v =
−v
2 and L δ F v = −v. This allows us to infer v > 0 and v > 0 hold at all times.
We apply the (Sync) rule along x = x, yielding the synchronized dynamics
˙
x = v, ˙
v = −v
2
, ˙
x = v · (v/v), ˙
v = −v · (v/v) & v > 0 ∧ v > 0
Note that the new evolution domain condition v > 0 allows us to rewrite v · (v/v)
to v. The synchronizability conditions follow immediately from the fact that
v > 0 and v > 0. For the synchronized formula, we apply the (DI) rule, so the
desired inequality v ≥ v is reduced to v
2
≤ v, that is, v ≤ 1. To this end, v > 0
tells us that the derivative of v, that is, −v
2 , is always negative, therefore v ≤ 1.
6.3 Model Refinement
In this example, we consider two abstract models of cars. The first car is able
to provide a high amount of constant acceleration a at low velocities, but at a
certain velocity v cut the engine switches to a different mode and then provides a
lesser, but still constant acceleration a cut . The second car is an abstracted version
of the first, which ignores this mode change and provides the same constant
amount of acceleration a at all velocities. Our aim in this example is to establish
a safety envelope around the first car’s behavior using the more simply stated
second car’s dynamics. Hence we show that the second car’s velocity is greater
than the first’s at any position x = x = l. More formally, the behavior of the