Information Technology Reference
In-Depth Information
Definition 8 (Transition Separation).
The discrete transitions in a hybrid
automaton H are
separated
, if for any two transitions
(
m
1
,
A
1
,
m
1
)
and
↑
Φ
1
,
A
2
,
m
2
)
in R
d
of H with m
1
=
m
2
the following condition holds:
(
m
2
,
↑
Φ
2
,
∀
σ
:
Var
→
R
:(
σ
|
=
Φ
1
⇒A
1
(
σ
)
|
=
Φ
2
)
.
Separation implies that at any given point in time during a run, at most one
discrete transition fires. Thus our models have dense time but not
superdense
time, where a sequence of discrete transitions is permitted to fire at one instant
in time.
Discrete variables may be included into hybrid automata according to our
definition via an embedding of their value domain into the reals, and associating
a derivative of constantly zero to them (locals and outputs). Timeouts are easily
coded via explicit local timer variables with a derivative taken from
.
Note that this general model subsumes both controller and plant models,
by choosing the set of variables appropriately and enforcing certain modeling
restrictions. For our plant models, we require the absence of discrete transitions.
This entails that plant variables only evolve continuously and cannot be changed
by discrete jumps. This is convenient for the formulation of our approach but
not essential.
{−
1
,
0
,
1
}
Definition 9 (Restriction).
For a hybrid automaton H and a mode m
∈
M
let the
restriction
H
m be defined as H, but with the mode fixed to m. Formally,
this is the following hybrid automaton:
,
Var
,
R
d
m
,
R
c
H
m
=(
{
m
}
m
,
m
,Θ
m
)
where R
d
,
m
)
R
d
m
=
m
}
and R
c
m
=
{
(
m
,
↑
Φ,
A
∈
|
mand
Θ
marethe
restrictions of the mappings R
c
and
Θ
to the singleton set
{
m
}
.
A.1 Behaviour
We will in the definition of
runs
of a hybrid automaton interpret all transitions
as urgent, i.e., a mode will be left as soon as the triggering event occurs. This
can either be the expiration of a time-out or a condition (e.g., on the plant
sensors) becoming true. Valid runs also avoid Zeno behavior and time-blocks,
i.e., each run provides a valuation for each positive point in time. We did not
take provisions to ensure the existence of such a run, nor the property that each
initial behavior segment can be extended to a full run. Such might be added via
adequate modeling guidelines (e.g., by including the negation of an invariant as
trigger condition on some transition leaving the mode). As these properties are
not essential to the purpose of this paper we left them out.
We now give the formal definition of runs of a hybrid automaton
H
capturing
the evolution of modes and the real-valued variables over time. To this end, we
consider the continuous time domain
Time
=
R
≥
0
of non-negative reals, for the
M
:
Time
mode observable
M
a function
→
M
, and for every variable
X
∈
Var
a
X
:
Time
corresponding function
→
R
describing for each time point
t
∈
Time
Search WWH ::
Custom Search