Information Technology Reference
In-Depth Information
Appendix
A Communicating Hybrid Automata
For the sake of completeness, we include from [13] the description of communi-
cating hybrid automata which we use as a model for cooperating trac agents
in this paper. We assume that the signature of the real numbers is given with
function and predicate symbols like 0
,
1
,
+
,
R
in the usual way. (Real-valued) expressions, Boolean expressions, and first-order
formulas over this signature are defined as usual. By
Th
(
·
,<,
= interpreted on the domain
) we denote the theory
of the real numbers, i.e., the set of all first-order formulas that hold in
R
R
.
Definition 7 (Hybrid Automaton).
A
hybrid automaton
is a tuple H
=
(
,
Var
,
R
d
,
R
c
,
m
0
,Θ
)
where
M
1.
M
is a finite set of
modes
, with typical element m
∈
M
and with a distin-
,
2. Var is a set of
variables
ranging over the set
guished
mode observable
M ranging over
M
of real numbers. Typical
elements of Var are X
,
Y . Var is partitioned into disjoint sets of
input, local
and
output
variables: Var
=
Var
in
R
Var
out
, where local variables
cannot be accessed by other hybrid automata in a parallel composition (see
Subsection 8),
3. m
0
∈
M
Var
loc
∪
∪
is the
initial mode
,
4.
Θ
is a mapping that associates with each mode m
a
local invariant
Θ
(
m
)
, which is a quantifier-free first-order formula over Var,
5. R
d
∈
M
,
m
)
called
is the
discrete transition relation
with elements
(
m
,
↑
Φ,
A
transitions
, which are graphically represented as m
↑Φ/A
m
,where
−−−→
-
m
,
m
∈
M
,
-
the
trigger
Φ
guarding the transition describes the event that a quantifier-
free formula
Φ
over Var becomes true,
↑
-
A
is a (possibly empty) set of (disjoint)
assignments
of the form X
:=
e
with X
Var
out
and e an expression over Var.
6. R
c
is the
continuous transition relation
, i.e., a mapping that associates with
each mode m
Var
loc
∈
∪
Var
out
an expression
R
c
(
m
)(
X
)
over Var, which is taken as the right-hand side of the differential
equation X
•
=
R
c
(
m
)(
X
)
describing the evolution of X over time while H
is in mode m.
Var
loc
∈
M
and each variable X
∈
∪
Valuations
or
states
of the variables in
Var
are given by functions
σ
:
Var
→
R
.
A valuation
σ
assigning to each variable
X
the value
v
X
∈
R
is denoted by
σ
=
{
X
→
v
X
|
X
∈
Var
}
. For a valuation
σ
and a set of assignments
A
let
A
(
σ
):
Var
→
R
denote the
update
of
σ
according to
A
defined by
A
(
σ
)=
{
X
→
σ
(
e
)
|∃
e
:
X
:=
e
∈A}∪{
X
→
σ
(
X
)
|¬∃
e
:
X
:=
e
∈A}
.
For a valuation
σ
and a formula
Φ
let
σ
=
Φ
denote that
σ
satisfies
Φ
.
We require of the discrete transition relation that the execution of one tran-
sition does not immediately enable a further transition.
|
Search WWH ::
Custom Search