Information Technology Reference
In-Depth Information
Transition Calculus [56], an extension of the Duration Calculus (DC) [57]. In DC,
real-time interval properties of system observables
obs
, which are interpreted as
functions
obs
I
:
Time
→
Data
, can be expressed and proven. For example,
(
M
=
NEG
⇒
acc
=0
)
expresses that in every interval (
) if the mode observable
M
has the value
NEG
(for
negotiating
) throughout this interval (
M
=
NEG
) then the observable
acc
(for
acceleration
) is zero throughout this interval (
).
The State Transition Calculus can additionally express properties of instan-
taneous transitions. For example,
acc
=0
Time
if then the
truth value of the assertion
M
=
NEG
switches from false to true. In DC, this
can be expressed as
↑
M
=
NEG
is true at
t
∈
whichistoholdinanin-
terval surrounding
t
. The chop operator ; is applied at time
t
and expresses the
concatenation of two intervals where
¬
(
M
=
NEG
)
;
M
=
NEG
¬
(
M
=
NEG
)
holds in the first one and
in the second one.
It can be defined that a hybrid automaton
H
is a
model
of a formula
F
,
abbreviated as
H
M
=
NEG
|
=
F
.
Correcting Modes. For each controller
C
i
we stipulate a set
COR
(
C
i
) of
correcting maneuvers
. Then we assume a relation
COR
(
C
2
)
of
matching modes
characterizing which pairs of maneuver are claimed to re-
solve hazardous states. For each pair (
m
1
,
m
2
)
MATCH
⊆
COR
(
C
1
)
×
MATCH there is an
activation
condition
characterized by a state assertion
Φ
(
m
1
,
m
2
). Activation conditions of
maneuvers must observe the following constraints:
∈
-
timely activation
: the activation of the maneuvers occurs early enough to
guide the trac agents to a safe state using the associated control laws.
-
completeness
: for each possible approach to a hazardous state there is at
least one matching pair of correcting modes whose activation condition is
enabled in time.
For ground-based trac agents like trains there is a special class of corrective
modes, enforcing a complete stop of the trac agent, thus reaching a
fail-safe
state
. We refer to such corrective modes as
recovery modes
and assume that there
is a single matching pair (
r
1
,
r
2
) of recovery modes.
Let
Φ
start
be the disjunction of all activation conditions of these modes:
Φ
start
∨
(
m
1
,
m
2
)
∈
MATCH
Φ
(
m
1
,
m
2
)
.
Intuitively, if any of these conditions becomes true, a hazardous state has been
reached, which can compensated by the associated matching pair of correcting
modes. By completeness of the set of activation conditions,
Φ
start
⇔
Φ
(
r
1
,
r
2
)
thus charac-
terizes all hazardous states.
The flexibility of having multiple matching correcting modes entails the need
for a
negotiation phase
, in which agents agree on which pair of maneuvers is to
be activated. The design of this phase has to address the following critical issues:
Search WWH ::
Custom Search