Information Technology Reference
In-Depth Information
Definition 11 (Composable Hybrid Automata).
Let two hybrid automata
H
i
,
i
=1
,
2
, with discrete transition relations R
i
,
i
=1
,
2
, be given. For a
pair of transitions s
i
=(
m
i
,
R
i
,
i
=1
,
2
, the transition s
1
is
unaffected
by s
2
, if each variable for which there is an assignment in
A
i
,
m
i
)
↑
Φ
i
,
∈
A
2
appears
neither in
Φ
1
nor in
A
1
(on any of the right-hand sides).
The two transition relations are
composable
, if for each pair of transitions
s
i
∈
R
i
,
i
=1
,
2
,eithers
1
is unaffected by s
2
or vice versa.
Composability establishes essentially a direction on instantaneous communica-
tions - communications may have an immediate effect on the output and thus
the partner automaton, but they must not immediately influence the originator
of the information. Assuming composability, the rest of the construction of the
parallel composition automaton is rather standard.
For a mo de (
m
1
,
m
2
), the associated invariant condition is the conjunction
of the invariance conditions associated with
m
1
and
m
2
. Similarly, the set of
differential equations governing the continuous evolution while in mode (
m
1
,
m
2
)
is obtained by simply conjoining the set of differential equations attached to
m
1
and
m
2
, respectively - note that the disjointness conditions on variables assure,
that this yields a consistent set of differential equations. Finally, the discrete
transition relation consists of the following transitions:
A
2
)
,
(
m
1
,
m
2
))
for each pair of transitions
s
i
=(
m
i
,
1. ((
m
1
,
m
2
)
,Φ
1
∧A
1
(
Φ
2
)
,
A
1
∪A
1
(
A
i
,
m
i
)
R
i
,
i
=1
,
2 where
s
1
is
↑
Φ
i
,
∈
unaffected by
s
2
,
2. ((
m
1
,
m
2
)
,Φ
1
{¬A
1
(
Φ
2
)
Φ
2
trigger in
R
2
}
A
1
,
(
m
1
,
m
2
))
|
,
R
1
,and
3. transitions of the forms (1) and (2) with the role of
H
1
and
H
2
interchanged,
A
1
,
m
1
)
for each (
m
1
,
↑
Φ
1
,
∈
A
(
Φ
) denotes the substitution into
Φ
of
e
for
v
for each assignment
X
:=
where
∈A
A
1
(
A
2
) denotes the substitution of the assignments of
A
1
into the
e
,and
right-hand terms of
A
2
.
Composability ensures that the simultaneous transitions of Clause (1) indeed
capture the combined effect of both transitions. The separation of transitions in
the resulting automaton is inherited from separation in the component automata
by the way single-automata transitions (Clause (2)) are embedded.
Search WWH ::
Custom Search