198
J. Kolˇ c´ ak et al.
Proposition 8. −
α
→ ⊗ −
α
→ = −
α; α
→
→
Scenarios with two parallel differential dynamics are the main focus of this
work. We formalize an assertion relating two dynamics using the following format. It is a syntactic counterpart of Proposition 8.
Definition 9 (relational differential dynamics). We call hybrid programs
of the following form relational differential dynamics (RDD)
˙
x = e & Q ; ˙
x = e & Q
(3)
Now that we have ways to express separate systems evolving in parallel, we
turn to the construction of proofs which reason about their relationships.
Example 10. Using RDD, the problem in Example 1 is expressed as Γ C
δ C ; δ C
φ C where δ C :=
˙
x = v, ˙
v = 1
, δ C := ( ˙
x = v, ˙
v = 2), Γ C := {x =
x = 0, v = v = 0} is the precondition, and φ C := (x = x = 1 ⇒ v ≤ v) is the
postcondition.
Let us prove, in KeYmaera X, the RDD sequent Γ C
δ C ; δ C
φ C . In
KeYmaera X, the only applicable rule to this sequent turns it into Γ C
δ C
δ C
φ C . We then explicitly “solve” the second dynamics, yielding the following goal:
Γ C
δ C
∀t ≥ 0.
x = x + v · t + t
2 = 1 ⇒ v ≤ v + t
(4)
where x and v in φ C are replaced by their explicit solutions with respect to the
freshly introduced time variable t. Again differential invariant rules do not apply
to (4), so one must solve the first dynamics, too, yielding
Γ C ∀t ≥ 0. ∀t ≥ 0.
x + v · t + t
2 /2 = x + v · t + t
2 = 1 ⇒ v + t ≤ v + t
Since this goal is first order, the quantifier elimination, a central proof technique
in KeYmaera X [18], proves the goal.
The above example worked out since it admits explicit solutions expressible
in dL. This is not always the case as the following example demonstrates.
Example 11. We consider two objects moving through fluids subjected to different kinds of drag. One object moves through a viscous fluid and is therefore
subject to linear drag; its dynamics are δ F := ( ˙
x = v, ˙
v = −v).
The other object moves through a less viscous fluid and is subject to turbulent
drag; its dynamics are δ F := ( ˙
x = v, ˙
v = −v
2 ). Our goal is to show that
the latter has higher speed when both objects reach a certain point in space
(x = x = l).
The following functions v
∗
, x
∗
, v
∗ and x
∗ are solutions of the dynamics.
v
∗ (t) = v 0 · e
−t
x
∗ (t) = x 0 + v 0 · (1 − e
−t )
v
∗ (t) =
v 0
1 + v 0 · t
x
∗ (t) = x 0 + log(1 + v 0 · t)
J. Kolˇ c´ ak et al.
Proposition 8. −
α
→ ⊗ −
α
→ = −
α; α
→
→
Scenarios with two parallel differential dynamics are the main focus of this
work. We formalize an assertion relating two dynamics using the following format. It is a syntactic counterpart of Proposition 8.
Definition 9 (relational differential dynamics). We call hybrid programs
of the following form relational differential dynamics (RDD)
˙
x = e & Q ; ˙
x = e & Q
(3)
Now that we have ways to express separate systems evolving in parallel, we
turn to the construction of proofs which reason about their relationships.
Example 10. Using RDD, the problem in Example 1 is expressed as Γ C
δ C ; δ C
φ C where δ C :=
˙
x = v, ˙
v = 1
, δ C := ( ˙
x = v, ˙
v = 2), Γ C := {x =
x = 0, v = v = 0} is the precondition, and φ C := (x = x = 1 ⇒ v ≤ v) is the
postcondition.
Let us prove, in KeYmaera X, the RDD sequent Γ C
δ C ; δ C
φ C . In
KeYmaera X, the only applicable rule to this sequent turns it into Γ C
δ C
δ C
φ C . We then explicitly “solve” the second dynamics, yielding the following goal:
Γ C
δ C
∀t ≥ 0.
x = x + v · t + t
2 = 1 ⇒ v ≤ v + t
(4)
where x and v in φ C are replaced by their explicit solutions with respect to the
freshly introduced time variable t. Again differential invariant rules do not apply
to (4), so one must solve the first dynamics, too, yielding
Γ C ∀t ≥ 0. ∀t ≥ 0.
x + v · t + t
2 /2 = x + v · t + t
2 = 1 ⇒ v + t ≤ v + t
Since this goal is first order, the quantifier elimination, a central proof technique
in KeYmaera X [18], proves the goal.
The above example worked out since it admits explicit solutions expressible
in dL. This is not always the case as the following example demonstrates.
Example 11. We consider two objects moving through fluids subjected to different kinds of drag. One object moves through a viscous fluid and is therefore
subject to linear drag; its dynamics are δ F := ( ˙
x = v, ˙
v = −v).
The other object moves through a less viscous fluid and is subject to turbulent
drag; its dynamics are δ F := ( ˙
x = v, ˙
v = −v
2 ). Our goal is to show that
the latter has higher speed when both objects reach a certain point in space
(x = x = l).
The following functions v
∗
, x
∗
, v
∗ and x
∗ are solutions of the dynamics.
v
∗ (t) = v 0 · e
−t
x
∗ (t) = x 0 + v 0 · (1 − e
−t )
v
∗ (t) =
v 0
1 + v 0 · t
x
∗ (t) = x 0 + log(1 + v 0 · t)