Information Technology Reference
In-Depth Information
M
(
t
)
X
(
t
)
the current mode
∈
M
and the current value
∈
R
, respectively.
Time
we define the
previous value
of
X
at
t
by
prev
(
X
,
t
) = lim
u
→
t
(
X
(
u
)). Satisfaction of a condition containing
prev
entails
that the respective limes does exist.
9
X
and 0
<
t
Further on, for
∈
Definition 10 (Runs of a Hybrid Automaton).
A
run
of a hybrid automa-
ton H= (
,Var,R
d
,R
c
,m
0
,
Θ
)isatupleoftrajectories
π
=
M
,
(
X
)
X
∈
Var
,
M
M
:
Time
X
:
Time
with
→
M
and
→
R
for X
∈
Var , iff
Time
N
:
τ
0
=0
∃
(
τ
i
)
i
∈
N
∈
∧∀
i
∈
N
:
τ
i
<τ
i
+1
,
a strictly increasing sequence of discrete switching times, satisfying the following
conditions:
1.
non-Zeno
:
∀
t
∈
Time
∃
i
∈
N
:
t
≤
τ
i
[
τ
i
,τ
i
+1
):
M
(
t
)=
M
(
τ
i
)
2.
mode switching times
:
∀
i
∈
N
∀
t
∈
3.
continuous evolution
:
=
X
•
=
R
c
(
M
(
τ
i
))(
X
)
t
∈
Var
loc
Var
out
:
σ
∀
i
∈
N
∀
[
τ
i
,τ
i
+1
)
∀
X
∈
∪
|
d X
(
t
)
dt
Y
(
t
)
|
Y
∈
Var
}
.
Thus in
σ
the variable X
•
gets the value of the derivative of the function X
at t
and all other variables Y
where
σ
is the valuation
σ
=
{
X
•
→
(
t
)
}∪{
Y
→
Var get the value of the function
ˆ
Yatt
.
∈
X
(
t
)
=
Θ
(
M
(
t
))
4.
invariants
:
∀
t
∈
Time
:
{
X
→
|
X
∈
Var
}|
5.
urgency
:
we have that
,
m
)
R
d
∀
i
∈
N
∀
t
∈
[
τ
i
,τ
i
+1
)
∀
(
m
,
↑
Φ,
A
∈
M
(
t
)=
m
X
(
t
)
⇒{
X
→
|
X
∈
Var
} |
=
Φ
6.
discrete transition firing
:
∀
i
∈
N
we have that
(
M
(
τ
i
+1
)=
M
(
τ
i
)
Var
out
:
X
(
τ
i
+1
)=
prev
(
X
,τ
i
+1
))
Var
loc
∧∀
X
∈
∪
(
R
d
:
M
(
τ
i
)=
m
M
(
τ
i
+1
)=
m
,
m
)
∃
(
m
,
↑
Φ,
A
∈
∧
∧
Var
loc
Var
out
:
∃
σ
∈
Var
→
R
:
∀
X
∈
∪
σ
(
X
)=
prev
(
X
,τ
i
+1
)
∧
σ
|
=
Φ
X
(
τ
i
+1
)=
σ
(
X
)
Var
in
:
∧∀
X
∈
X
(
τ
i
+1
)=
Var
loc
Var
out
:
∧∀
X
∈
∪
A
(
σ
)(
X
))
9
In fact, our definition of a run implies that these limits do exist for all local and
output variables in any run.
Search WWH ::
Custom Search