196
J. Kolˇ c´ ak et al.
Definition 2 (language). We fix a set V of variables, denoted by x, y, . . . . The
set of terms is defined by the following grammar:
e, f, g, . . . ::= x | n | −e | e + f | e · f | e/f
where x ∈ V and n ∈ N. First-order formulas are defined by
P, Q, . . . ::= e ≤ f | ¬P | P ∧ Q | ∀x. P
A state is a function mapping each variable to a real number, ω : V → R.
We denote the set of all states by R
V . Given a state, each term has a valuation in the reals, and each formula has a valuation in Booleans defined by the
usual induction. We denote these by
e
ω ∈ R and
P
ω ∈ {true, false},
respectively. The models of a first-order formula P are the states satisfying P ,
P
:= {ω ∈ R
V
|
P
ω = true}.
We use classical shorthands, including e = f := e ≤ f ∧ f ≤ e, P ∨
Q := ¬(¬P ∧ ¬Q), ∃x. P := ¬(∀x. ¬P ), and := 0 ≤ 0. We denote a vector
(e 1 , . . . , e n ) of terms (or variables) by e when the length n is irrelevant or clear
from the context.
We now introduce the syntax of hybrid programs.
Definition 3 (hybrid programs). The set HP(V) of hybrid programs over
variables V is given by the following grammar:
α 1 , α 2 , . . . ::= ?P | x := e | ˙
x 1 = e 1 , . . . , ˙
x n = e n & Q | α 1 ; α 2 | α 1 ∪ α 2 | α
∗
1
We may also abbreviate ˙
x 1 = e 1 , . . . , ˙
x n = e n by ˙
x = e. Hybrid programs
of the form ˙
x = e & Q are especially important in this work. We call such a
program differential dynamics, where ˙
x = e is its differential equation and the
first-order formula Q is its evolution domain constraint. The intuitive meaning
of such a program is that the values of the variables x evolve continuously in
time according to ˙
x = e, as long as Q is satisfied at the current value of x. If we
see differential dynamics as a continuous analog of loops, then Q plays the role
of guard and ˙
x = e plays the role of body.
5 We write ˙
x = e instead of ˙
x = e & .
Definition 4 (solutions). A mapping ψ : [0, T ) → R
V with T ∈ [0, ∞] is called
a solution of a differential equation ˙
x 1 = e 1 , . . . , ˙
x n = e n if ψ is differentiable
in [0, T ) and, whenever t ∈ [0, T ), ˙
ψ(t)(x i ) =
e i
ψ(t) for i ∈ {1, . . . , n} and
˙
ψ(t)(y) = 0 for any y ∈ V \ {x 1 , . . . , x n }.
According to the Picard–Lindel¨ of theorem [13], for each differential equation
˙
x = e and each state ω, there is a unique maximal solution ψ ω : [0, T ω ) → R
V
of the differential equation satisfying ψ ω (0) = ω.
Definition 5 (semantics of hybrid programs). The semantics of a hybrid
program α is a relation −
α
→ ⊆ R
V
× R
V on states, defined by:
5 This analogy is not perfect: a typical while loop can only exit when its guard is false,
whereas a hybrid program can exit the differential dynamics while Q is satisfied.
J. Kolˇ c´ ak et al.
Definition 2 (language). We fix a set V of variables, denoted by x, y, . . . . The
set of terms is defined by the following grammar:
e, f, g, . . . ::= x | n | −e | e + f | e · f | e/f
where x ∈ V and n ∈ N. First-order formulas are defined by
P, Q, . . . ::= e ≤ f | ¬P | P ∧ Q | ∀x. P
A state is a function mapping each variable to a real number, ω : V → R.
We denote the set of all states by R
V . Given a state, each term has a valuation in the reals, and each formula has a valuation in Booleans defined by the
usual induction. We denote these by
e
ω ∈ R and
P
ω ∈ {true, false},
respectively. The models of a first-order formula P are the states satisfying P ,
P
:= {ω ∈ R
V
|
P
ω = true}.
We use classical shorthands, including e = f := e ≤ f ∧ f ≤ e, P ∨
Q := ¬(¬P ∧ ¬Q), ∃x. P := ¬(∀x. ¬P ), and := 0 ≤ 0. We denote a vector
(e 1 , . . . , e n ) of terms (or variables) by e when the length n is irrelevant or clear
from the context.
We now introduce the syntax of hybrid programs.
Definition 3 (hybrid programs). The set HP(V) of hybrid programs over
variables V is given by the following grammar:
α 1 , α 2 , . . . ::= ?P | x := e | ˙
x 1 = e 1 , . . . , ˙
x n = e n & Q | α 1 ; α 2 | α 1 ∪ α 2 | α
∗
1
We may also abbreviate ˙
x 1 = e 1 , . . . , ˙
x n = e n by ˙
x = e. Hybrid programs
of the form ˙
x = e & Q are especially important in this work. We call such a
program differential dynamics, where ˙
x = e is its differential equation and the
first-order formula Q is its evolution domain constraint. The intuitive meaning
of such a program is that the values of the variables x evolve continuously in
time according to ˙
x = e, as long as Q is satisfied at the current value of x. If we
see differential dynamics as a continuous analog of loops, then Q plays the role
of guard and ˙
x = e plays the role of body.
5 We write ˙
x = e instead of ˙
x = e & .
Definition 4 (solutions). A mapping ψ : [0, T ) → R
V with T ∈ [0, ∞] is called
a solution of a differential equation ˙
x 1 = e 1 , . . . , ˙
x n = e n if ψ is differentiable
in [0, T ) and, whenever t ∈ [0, T ), ˙
ψ(t)(x i ) =
e i
ψ(t) for i ∈ {1, . . . , n} and
˙
ψ(t)(y) = 0 for any y ∈ V \ {x 1 , . . . , x n }.
According to the Picard–Lindel¨ of theorem [13], for each differential equation
˙
x = e and each state ω, there is a unique maximal solution ψ ω : [0, T ω ) → R
V
of the differential equation satisfying ψ ω (0) = ω.
Definition 5 (semantics of hybrid programs). The semantics of a hybrid
program α is a relation −
α
→ ⊆ R
V
× R
V on states, defined by:
5 This analogy is not perfect: a typical while loop can only exit when its guard is false,
whereas a hybrid program can exit the differential dynamics while Q is satisfied.