Information Technology Reference
In-Depth Information
a state assertion
P
, the integral
R
P
is called the
duration
, because it measures
the time
P
holds in the given interval, when the Boolean values are encoded
with 0 for
false
and 1 for
true
.
Duration formulas
are built from duration terms of Boolean type and closed
under propositional connectives, the chop connective, and quantication over
rigid variables and variables of duration terms. We use
D
for a typical duration
formula.
Semantics.
The semantics of Duration Calculus is based on an
interpretation
I
that assigns a xed meaning to each state name and operator symbol of the
language, and a time interval [
b
e
] the semantics denes
what domain values duration terms and what truth values duration formulas
;
e
]. For given
I
and [
b
;
denote. For example,
R
f
denotes the integral
R
e
b
f
(
t
)
dt
,
b.
f
denotes the limit
from the right in
b
(
f
(
b
+)), and
e.
f
denotes the limit from the left in
e
(
f
(
e
−
)).
A duration formula
D holds
in
I
and [
b
;
e
], abbreviated
I;
[
b
;
e
]
j
=
D
,ifit
denotes the truth value
true
for
e
].
The boolean connectives and quantiers have their usual meaning. The chop
operator is the only modality; given duration formulas
D
1
and
D
2
, the formula
(
D
1
;
D
2
) holds on the interval [
b
I
and [
b
;
e
] just when there is a chop point
m
such that
D
1
holds on the initial subinterval [
b
;
;
m
]and
D
2
holds on the nal subinterval
[
m
;
e
], see Fig. 2.
D
is
true
in
I
, abbreviated
Ij
=
D
,if
I;
[0
;
t
]
j
=
D
for every
t
2
Time
.A
model
of
D
is an interpretation
I
which makes
D
true, i.e. with
Ij
=
D
.The
formula
D
is
satisable
if there exists an interpretation
=
D
.
A
behaviour
is an interpretation restricted to the names of the elementary
states.
I
with
Ij
D
1
;
D
2
D
1
D
2
m
e
Time
b
Fig. 2.
Semantics of chop.
Abbreviations.
The length of an interval is often used; it is the duration of
the constant assertion
true
(
R
true
) which is abbreviated (
), pronounced `the
length'. The property that an assertion
P
holds (essentially everywhere) in an
`
interval is thus given by the atomic formula
R
P
=
. This holds trivially for a
point interval
of length zero, so we consider proper intervals of a positive length.
The two properties are combined in the abbreviation
`
def
=(
R
P
=
d
P
e
`
)
^
(
`>
0)
;
Search WWH ::
Custom Search