200
J. Kolˇ c´ ak et al.
and (Dbx) rules, as they accept only one dynamics followed by a comparison. In
order to make use of these rules in our relational reasoning, we introduce another
proof method. It “synchronizes” two dynamics.
After some theoretical preparations we define the new rule and prove its
soundness. We will illustrate the usefulness of this rule in Section 6, through
some case studies that are inspired by our collaboration with the industry.
4.1 Time Stretching
A key theoretical tool towards the soundness of our synchronization rule is called
time stretching. Its idea is very similar to the technique of time-reparametrization
for ODEs [7].
Definition 15 (time stretch function). Let T ∈ R ≥0 . A function K : [0, T ] →
R ≥0 is a time stretch function if K(0) = 0, K is continuously differentiable and
˙
K(t) > 0 for each t ∈ [0, T ].
Remark 16. The condition ˙
K(t) > 0 ensures that K is strictly increasing and is
a bijection from [0, T ] to [0, K(T )]. The inverse of K is K
−1 : [0, K(T )] → [0, T ],
and it is straightforward to check K
−1 is another time stretch function.
The next results tell us how to turn an ODE into another, given a time
stretching function K, so that a time-stretch ψ◦K of a solution ψ of one becomes
a solution of the other.
Lemma 17. Suppose f : R
V
→ R
V is a vector field and K : [0, T ] → [0, K(T )]
is a time stretch function. If ψ : [0, K(T )) → R
V satisfies ˙
ψ(s) = f (ψ(s))
for all s ∈ [0, K(T )), then the function ρ = ψ ◦ K : [0, T ) → R
V satisfies
˙
ρ(t) = ˙
K(t) · f (ρ(t)) for all t ∈ [0, T ).
Proof. We have ˙
ρ(t) = ˙
K(t)· ˙
ψ(K(t)) = ˙
K(t)·f (ψ(K(t))) = ˙
K(t)·f (ρ(t)), where
the first equality is by the definitions and the chain rule, the second equality is
by the assumption on ˙
ψ, and the last equality is by the definition of ρ.
Since the inverse of a time stretch function is another time stretch function,
we obtain the following corollary of Lemma 17.
Corollary 18. Let K : [0, T ] → [0, K(T )] be a time stretch function. Let ρ :
[0, T ) → R
V satisfy ˙
ρ(t) = ˙
K(t) · f (ρ(t)) whenever 0 ≤ t < T . Then the function
ψ : [0, K(T )) → R
V , defined by ψ(s) := ρ(K
−1 (s)), satisfies ˙
ψ(s) = f (ψ(s))
whenever 0 ≤ s < K(T ).
4.2 Towards a Syntactic Representation
So far our time-stretch function K has been a semantical object. Here we introduce a syntactic way of reasoning via time-stretch functions. Since a desired
time-stretch function is not necessarily expressible in dL, our syntactic reasoning
J. Kolˇ c´ ak et al.
and (Dbx) rules, as they accept only one dynamics followed by a comparison. In
order to make use of these rules in our relational reasoning, we introduce another
proof method. It “synchronizes” two dynamics.
After some theoretical preparations we define the new rule and prove its
soundness. We will illustrate the usefulness of this rule in Section 6, through
some case studies that are inspired by our collaboration with the industry.
4.1 Time Stretching
A key theoretical tool towards the soundness of our synchronization rule is called
time stretching. Its idea is very similar to the technique of time-reparametrization
for ODEs [7].
Definition 15 (time stretch function). Let T ∈ R ≥0 . A function K : [0, T ] →
R ≥0 is a time stretch function if K(0) = 0, K is continuously differentiable and
˙
K(t) > 0 for each t ∈ [0, T ].
Remark 16. The condition ˙
K(t) > 0 ensures that K is strictly increasing and is
a bijection from [0, T ] to [0, K(T )]. The inverse of K is K
−1 : [0, K(T )] → [0, T ],
and it is straightforward to check K
−1 is another time stretch function.
The next results tell us how to turn an ODE into another, given a time
stretching function K, so that a time-stretch ψ◦K of a solution ψ of one becomes
a solution of the other.
Lemma 17. Suppose f : R
V
→ R
V is a vector field and K : [0, T ] → [0, K(T )]
is a time stretch function. If ψ : [0, K(T )) → R
V satisfies ˙
ψ(s) = f (ψ(s))
for all s ∈ [0, K(T )), then the function ρ = ψ ◦ K : [0, T ) → R
V satisfies
˙
ρ(t) = ˙
K(t) · f (ρ(t)) for all t ∈ [0, T ).
Proof. We have ˙
ρ(t) = ˙
K(t)· ˙
ψ(K(t)) = ˙
K(t)·f (ψ(K(t))) = ˙
K(t)·f (ρ(t)), where
the first equality is by the definitions and the chain rule, the second equality is
by the assumption on ˙
ψ, and the last equality is by the definition of ρ.
Since the inverse of a time stretch function is another time stretch function,
we obtain the following corollary of Lemma 17.
Corollary 18. Let K : [0, T ] → [0, K(T )] be a time stretch function. Let ρ :
[0, T ) → R
V satisfy ˙
ρ(t) = ˙
K(t) · f (ρ(t)) whenever 0 ≤ t < T . Then the function
ψ : [0, K(T )) → R
V , defined by ψ(s) := ρ(K
−1 (s)), satisfies ˙
ψ(s) = f (ψ(s))
whenever 0 ≤ s < K(T ).
4.2 Towards a Syntactic Representation
So far our time-stretch function K has been a semantical object. Here we introduce a syntactic way of reasoning via time-stretch functions. Since a desired
time-stretch function is not necessarily expressible in dL, our syntactic reasoning