204
J. Kolˇ c´ ak et al.
For the formalization of case studies in Section 6, we extended KeYmaera X
version 4.7 (available at [17]) with the (Sync) rule. This extension of KeYmaera
X, together with our proofs in case studies, are currently available at http://
group-mmm.org/rddl tacas 2020/.
The KeYmaera X implementation is structured in a flexible manner, from
which we benefited. To add a rule to KeYmaera X, one has to implement a
Scala program that take the conclusion of the rule and generate the premises of
the rule as subgoals. The fact that any Scala program is allowed here enabled
us to implement complex algorithms, such as inductive translation of formulas.
In implementing the (Sync) rule, the functions in KeYmaera X called
helpers helped us, such as in the Lie derivative computation and the functionality to simplify formulas into equivalent ones. The bulk of our effort regarded the
⊗ (g,g) operator. There we did a bit more general than we stated in the paper: not
only taking dynamics of form ˙
x = e & Q, we also allow sequences of dynamics
possibly interleaved by guards and nondeterministic choices. This feature was
utilized in the case study that will be described in Section 6.3.
6 Case Studies
We describe three case studies where we proved relational properties of hybrid
dynamics. We did so formally in our extension of KeYmaera X described in
Section 5. In all the examples, we apply the (Sync) rule as a main proof step,
in conjunction with the existing rules in dL. Below, we describe our example
systems and outline the important steps in the formal proofs.
6.1 Collision Speed with Constant Acceleration
In this section we apply the (Sync) rule to the running Example 1. For this example we consider two dynamics δ C :=
˙
x = v, ˙
v = a
and δ C := ( ˙
x = v, ˙
v = a).
Both dynamics represent a car with constant acceleration. Our claim is that if
acceleration is larger in the first system, then the first car is necessarily faster
than the second car after traveling the same distance l; formally,
Γ
δ C ; δ C
(x = l ∧ x = l ⇒ v ≤ v)
(7)
where
Γ := {0 = x = x, 0 < v = v 0 , v = v 0 , v 0 ≥ v 0 , 0 ≤ a ≤ a}
We apply the (Sync) rule, where g := x and g := x. The first two synchronizability conditions are Γ x = x and x = l, x = l x = x, which are trivial.
The last two synchronizability conditions are
Γ
δ C
L δ C g = v > 0
Γ
δ C
L δ C g = v > 0
which are proven using differential invariants (DI). The synchronized formula is
Γ
δ C , ˙
x = v · (v/v), ˙
v = a · (v/v) & v > 0 ∧ v > 0
(x = l ∧ x = l ⇒ v ≤ v)
J. Kolˇ c´ ak et al.
For the formalization of case studies in Section 6, we extended KeYmaera X
version 4.7 (available at [17]) with the (Sync) rule. This extension of KeYmaera
X, together with our proofs in case studies, are currently available at http://
group-mmm.org/rddl tacas 2020/.
The KeYmaera X implementation is structured in a flexible manner, from
which we benefited. To add a rule to KeYmaera X, one has to implement a
Scala program that take the conclusion of the rule and generate the premises of
the rule as subgoals. The fact that any Scala program is allowed here enabled
us to implement complex algorithms, such as inductive translation of formulas.
In implementing the (Sync) rule, the functions in KeYmaera X called
helpers helped us, such as in the Lie derivative computation and the functionality to simplify formulas into equivalent ones. The bulk of our effort regarded the
⊗ (g,g) operator. There we did a bit more general than we stated in the paper: not
only taking dynamics of form ˙
x = e & Q, we also allow sequences of dynamics
possibly interleaved by guards and nondeterministic choices. This feature was
utilized in the case study that will be described in Section 6.3.
6 Case Studies
We describe three case studies where we proved relational properties of hybrid
dynamics. We did so formally in our extension of KeYmaera X described in
Section 5. In all the examples, we apply the (Sync) rule as a main proof step,
in conjunction with the existing rules in dL. Below, we describe our example
systems and outline the important steps in the formal proofs.
6.1 Collision Speed with Constant Acceleration
In this section we apply the (Sync) rule to the running Example 1. For this example we consider two dynamics δ C :=
˙
x = v, ˙
v = a
and δ C := ( ˙
x = v, ˙
v = a).
Both dynamics represent a car with constant acceleration. Our claim is that if
acceleration is larger in the first system, then the first car is necessarily faster
than the second car after traveling the same distance l; formally,
Γ
δ C ; δ C
(x = l ∧ x = l ⇒ v ≤ v)
(7)
where
Γ := {0 = x = x, 0 < v = v 0 , v = v 0 , v 0 ≥ v 0 , 0 ≤ a ≤ a}
We apply the (Sync) rule, where g := x and g := x. The first two synchronizability conditions are Γ x = x and x = l, x = l x = x, which are trivial.
The last two synchronizability conditions are
Γ
δ C
L δ C g = v > 0
Γ
δ C
L δ C g = v > 0
which are proven using differential invariants (DI). The synchronized formula is
Γ
δ C , ˙
x = v · (v/v), ˙
v = a · (v/v) & v > 0 ∧ v > 0
(x = l ∧ x = l ⇒ v ≤ v)