Relational Differential Dynamic Logic
201
uses an indirect method that exploits a pair of functions called a synchronizer.
We will be eventually led to a syntactic reasoning rule (Sync) (Thm. 24).
Given a term g ∈ T (X) and a mapping ψ : [0, T ) → R
X , we define g ψ :
[0, T ) → R by
g ψ (t) :=
g
ψ(t) .
(5)
Intuitively, g ψ (t) is the value of g at time t when we follow the dynamics whose
solution is ψ.
Definition 19 (synchronizers). Let (δ, δ) be a pair of dynamics, (ω, ω) ∈
R
V
× R
V be a pair of states, and ψ : [0, T ) → R
V and ψ : [0, T ) → R
V be the
unique solutions of δ and δ from ω and ω, respectively. We say a pair of dL terms
(g, g) ∈ T ( V ) × T ( V ) synchronizes (δ, δ) from (ω, ω) if the following hold.
– g ψ (0) = g ψ (0)
– The derivatives of g ψ and g ψ are both strictly positive.
The following lemma ensures that, for any synchronizer, a corresponding time
stretch function exists.
Lemma 20. In the setting of Definition 19, let t ∈ [0, T ) and t ∈ [0, T ) be such
that g ψ (t) = g ψ (t). Then the function K, defined by K(s) := g ψ
−1 (g ψ (s)), is a
time stretch function from [0, t] to [0, t]. Moreover we have ˙
K(s) =
˙
g ψ (s)
˙
g ψ (K(s)) .
Proof. Since g ψ is strictly monotonic on [0, t], it has an inverse g ψ
−1 defined
from g ψ ([0, t]) to [0, t]. By assumption we have g ψ (0) = g ψ (0), and thus K(0) =
g ψ
−1 (g ψ (0)) = g ψ
−1 (g ψ (0)) = 0. Also since g ψ (t) = g ψ (t), we see that g ψ
−1 is
defined from g ψ ([0, t]) to [0, t]. Thus K = g ψ
−1
◦ g ψ is defined from [0, t] to [0, t].
˙
K(s) = ˙
g ψ (s) ·
˙
g ψ
−1
(g ψ (s))
derivative of K = g ψ
−1
◦ g ψ
=
˙
g ψ (s)
˙
g ψ (g ψ
−1 (g ψ (s)))
derivative of g ψ
−1
=
˙
g ψ (s)
˙
g ψ (K(s))
whose value is positive by assumptions on the derivatives of g ψ and g ψ .
We remark that time stretch functions we obtain in Lemma 20 are not necessarily expressible as a dL term, as exemplified by the following example.
Example 21. Consider two dynamics δ F := ( ˙
x = v, ˙
v = −v
2 ) and δ := ( ˙
x =
1). Their solutions ψ, ψ : R ≥0 → R
2 from initial value x = 0, v = 1 are
ψ(s) =
log(1 + s), (1 + s)
−1
ψ(s) = (s, 0)
Now let g = x and g = x. Then g ψ (s) = log(1 + s), g ψ = g ψ
−1 = id and thus
K(s) = g ψ
−1 (g ψ (s)) = log(1 + s). This is not rational and not expressible in dL.
201
uses an indirect method that exploits a pair of functions called a synchronizer.
We will be eventually led to a syntactic reasoning rule (Sync) (Thm. 24).
Given a term g ∈ T (X) and a mapping ψ : [0, T ) → R
X , we define g ψ :
[0, T ) → R by
g ψ (t) :=
g
ψ(t) .
(5)
Intuitively, g ψ (t) is the value of g at time t when we follow the dynamics whose
solution is ψ.
Definition 19 (synchronizers). Let (δ, δ) be a pair of dynamics, (ω, ω) ∈
R
V
× R
V be a pair of states, and ψ : [0, T ) → R
V and ψ : [0, T ) → R
V be the
unique solutions of δ and δ from ω and ω, respectively. We say a pair of dL terms
(g, g) ∈ T ( V ) × T ( V ) synchronizes (δ, δ) from (ω, ω) if the following hold.
– g ψ (0) = g ψ (0)
– The derivatives of g ψ and g ψ are both strictly positive.
The following lemma ensures that, for any synchronizer, a corresponding time
stretch function exists.
Lemma 20. In the setting of Definition 19, let t ∈ [0, T ) and t ∈ [0, T ) be such
that g ψ (t) = g ψ (t). Then the function K, defined by K(s) := g ψ
−1 (g ψ (s)), is a
time stretch function from [0, t] to [0, t]. Moreover we have ˙
K(s) =
˙
g ψ (s)
˙
g ψ (K(s)) .
Proof. Since g ψ is strictly monotonic on [0, t], it has an inverse g ψ
−1 defined
from g ψ ([0, t]) to [0, t]. By assumption we have g ψ (0) = g ψ (0), and thus K(0) =
g ψ
−1 (g ψ (0)) = g ψ
−1 (g ψ (0)) = 0. Also since g ψ (t) = g ψ (t), we see that g ψ
−1 is
defined from g ψ ([0, t]) to [0, t]. Thus K = g ψ
−1
◦ g ψ is defined from [0, t] to [0, t].
˙
K(s) = ˙
g ψ (s) ·
˙
g ψ
−1
(g ψ (s))
derivative of K = g ψ
−1
◦ g ψ
=
˙
g ψ (s)
˙
g ψ (g ψ
−1 (g ψ (s)))
derivative of g ψ
−1
=
˙
g ψ (s)
˙
g ψ (K(s))
whose value is positive by assumptions on the derivatives of g ψ and g ψ .
We remark that time stretch functions we obtain in Lemma 20 are not necessarily expressible as a dL term, as exemplified by the following example.
Example 21. Consider two dynamics δ F := ( ˙
x = v, ˙
v = −v
2 ) and δ := ( ˙
x =
1). Their solutions ψ, ψ : R ≥0 → R
2 from initial value x = 0, v = 1 are
ψ(s) =
log(1 + s), (1 + s)
−1
ψ(s) = (s, 0)
Now let g = x and g = x. Then g ψ (s) = log(1 + s), g ψ = g ψ
−1 = id and thus
K(s) = g ψ
−1 (g ψ (s)) = log(1 + s). This is not rational and not expressible in dL.