206
J. Kolˇ c´ ak et al.
first car is expressed as a hybrid program α := ( δ 1 ; ?v = v cut ; δ 2 ) with two
modes: δ 1 := ( ˙
x = v, ˙
v = a & v ≤ v cut ) and δ 2 := ( ˙
x = v, ˙
v = a cut ). The second
car follows the simple dynamics δ := ( ˙
x = v, ˙
v = a). Our goal is to prove the
sequent Γ
α; δ
(x = x = l ⇒ v ≤ v), where the initial conditions are given
by
Γ := (x = x = 0, 0 < v = v = v 0 , 0 < v cut , 0 < a cut ≤ a)
Technically, the (Sync) rule merges one differential dynamics with another,
but the program the first car executes is a more complicated composition of
dynamics and testing. However, it is possible to synchronize piecewise, first synchronizing δ with δ 1 until the first car changes modes, then synchronizing δ
with δ 2 for the remainder of their runs. This slightly generalized synchronization
procedure means that we can instead show
Γ
δ 1 ⊗ (x,x) δ; ?v = v cut ; δ 2 ⊗ (x,x) δ
(x = x = l ⇒ v ≤ v)
There are also now two sets of synchronizability conditions to satisfy, but both
are again straightforward. Since δ 1 and δ are nearly identical (except for the
evolution domain constraint), their synchronization δ 1 ⊗ (x,x) δ basically identifies
the two dynamics. The synchronization of δ 2 and δ is exactly the synchronization
performed above in Section 6.1, and proceeds in the same way.
7 Conclusions and Future Work
In this paper, we present a relational extension of the differential dynamic logic
based on time stretching of dynamics. This reparametrization enables us to enforce that comparisons between two systems occur when certain conditions are
satisfied, for example when two cars are passing through the same position.
While such reparametrizations can be thought of as stretching or compressing
time for one of the dynamics, we also show they can be conducted by a transformation of the dynamics themselves, based on Lie derivatives. We call this
process synchronizing the dynamics (Definition 19), and it leads us to a new
dL proof rule, the (Sync) rule (Theorem 24). We implemented the new rule in
the KeYmaera X tool and use our extension to demonstrate several nontrivial
relational properties of dynamical systems.
In the future, we think it would be interesting to combine our relational
logic with orthogonal relational extensions of dL [14] which focus on refinement
relations with varying levels of nondeterminism. We also hinted in our last case
study that it is possible to synchronize wider classes of hybrid programs than just
two differential dynamics. We also think that the level of automated proof search
available in KeYmaera X may enable the automatic detection of monotonic
properties in product lines. This may be useful in industry both to provide sanity
checks on formalized models of products, as well as enabling strong guarantees
to be more easily obtained for those models.
J. Kolˇ c´ ak et al.
first car is expressed as a hybrid program α := ( δ 1 ; ?v = v cut ; δ 2 ) with two
modes: δ 1 := ( ˙
x = v, ˙
v = a & v ≤ v cut ) and δ 2 := ( ˙
x = v, ˙
v = a cut ). The second
car follows the simple dynamics δ := ( ˙
x = v, ˙
v = a). Our goal is to prove the
sequent Γ
α; δ
(x = x = l ⇒ v ≤ v), where the initial conditions are given
by
Γ := (x = x = 0, 0 < v = v = v 0 , 0 < v cut , 0 < a cut ≤ a)
Technically, the (Sync) rule merges one differential dynamics with another,
but the program the first car executes is a more complicated composition of
dynamics and testing. However, it is possible to synchronize piecewise, first synchronizing δ with δ 1 until the first car changes modes, then synchronizing δ
with δ 2 for the remainder of their runs. This slightly generalized synchronization
procedure means that we can instead show
Γ
δ 1 ⊗ (x,x) δ; ?v = v cut ; δ 2 ⊗ (x,x) δ
(x = x = l ⇒ v ≤ v)
There are also now two sets of synchronizability conditions to satisfy, but both
are again straightforward. Since δ 1 and δ are nearly identical (except for the
evolution domain constraint), their synchronization δ 1 ⊗ (x,x) δ basically identifies
the two dynamics. The synchronization of δ 2 and δ is exactly the synchronization
performed above in Section 6.1, and proceeds in the same way.
7 Conclusions and Future Work
In this paper, we present a relational extension of the differential dynamic logic
based on time stretching of dynamics. This reparametrization enables us to enforce that comparisons between two systems occur when certain conditions are
satisfied, for example when two cars are passing through the same position.
While such reparametrizations can be thought of as stretching or compressing
time for one of the dynamics, we also show they can be conducted by a transformation of the dynamics themselves, based on Lie derivatives. We call this
process synchronizing the dynamics (Definition 19), and it leads us to a new
dL proof rule, the (Sync) rule (Theorem 24). We implemented the new rule in
the KeYmaera X tool and use our extension to demonstrate several nontrivial
relational properties of dynamical systems.
In the future, we think it would be interesting to combine our relational
logic with orthogonal relational extensions of dL [14] which focus on refinement
relations with varying levels of nondeterminism. We also hinted in our last case
study that it is possible to synchronize wider classes of hybrid programs than just
two differential dynamics. We also think that the level of automated proof search
available in KeYmaera X may enable the automatic detection of monotonic
properties in product lines. This may be useful in industry both to provide sanity
checks on formalized models of products, as well as enabling strong guarantees
to be more easily obtained for those models.