Information Technology Reference
In-Depth Information
are of type real but their values depend on a given time
interval. The simplest duration term is the symbol
Duration terms
denoting the
length
of the
given interval. The name Duration Calculus stems from the fact that for each
state assertion
`
there is a duration term
R
S
S
measuring the
duration
of
S
, i.e. the
accumulated time
S
holds in the given interval. Formally:
` j
R
S j op
real
(
::=
)
where
a vector of duration terms.
Duration formulae
denote truth values depending on a given time interval.
They are built from the constants
op
real
is an real-valued operator and
applied to dura-
tion terms, and are closed under the
chop operator
(denoted by
;
), propositional
connectives
true
and
false
, relations
rel
op
Boole
, and quantication
Q 2f8;9g
over rigid variables
x
.Weuse
F
for a typical duration formula:
F
::=
rel
(
)
j F
1
;
F
2
j op
Boole
(
F
)
j Qx:F
where
is a vector of duration formulae. Besides this basic syntax various ab-
breviations are used for duration formulae:
F
de
=
point interval
:
de
`
=0
de
=
R
S
dSe
` ^ `>
everywhere
:
=
0
de
=
somewhere
:
3
F
true
;
F
;
true
de
=
always
:
F
:
:F
Semantics.
The semantics of Duration Calculus is based on an
interpretation
I
that assigns a xed meaning to each observable, rigid variable and operator
symbol of the language. To an observable
obs
the interpretation
I
assigns a
function
obs
I
:
Time
ā! D
obs
:
This induces inductively the semantics of terms and hence state assertions. For
a state assertions
S
it is a function
S
I
:
Time
ā! Bool
where
Bool
is identied with the set
f
0
;
1
g
.
The semantics of a duration term
is denoted by
I
(
) and yields a real value
depending on a given time interval [
b; e
]
Time
. In particular,
`
denotes the
]and
R
S
length of [
b; e
the duration of the state assertion
S
in [
b; e
]asgivenby
the integral. Formally:
I
(
`
)[
b; e
]=
eāb;
(
R
S
]=
R
e
I
)[
b; e
b
S
I
(
t
)
dt:
The semantics of a duration formula
F
denotes a truth value depending on
I
and a given time interval [
b; e
]. We write
I;
[
b; e
]
j
=
F
if that truth value is
true
Search WWH ::
Custom Search