Information Technology Reference
In-Depth Information
Let
denote this class of formulas.
Now consider two kinds of Duration Calculus semantics which are different
from the original one defined earlier for continuous time, and called discrete
semantics and discrete step time semantics.
Discrete Duration Calculus semantics are defined in the same way as for con-
tinuous time semantics except that all intervals are integer intervals. So,
a
,
b
,
m
and
m
i
in the definition should be integers instead of reals, and an interpretation
I
SC
should assign to each state variable
P
a function from
N
to
{
0
,
1
}
,andthen
+
expanded to a function from
)whichis
right continuous, and could be discontinuous only at integer time points. Let us
use
R
to
{
0
,
1
}
by letting
I
P
(
t
)=
I
P
(
t
=
DDC
to denote the modelling relation in these semantics.
Similarly, discrete step time Duration Calculus semantics are defined by re-
stricting the set of intervals to that of intervals between state change time points.
So,
a
,
b
,
m
and
m
i
in the definition should be time points where states change,
and an interpretation
|
I
should assign to each state variable
P
a function from
+
S
to
{
0
,
1
}
,where
S
is a countable subset of
R
intended to be the set of
time points for state changes that includes the set
N
.
I
P
is then expanded to
+
+
a function from
R
to
{
0
,
1
}
by letting
I
P
(
t
)=
I
P
(
t
s
), where
t
∈R
and
t
t
t
s
=max
{
∈S|
≤
t
}
.Then
I
P
(
t
) is also right continuous, and could be
discontinuous only at a point in
S
. Let us use
|
=
SDC
to denote the modelling
relation in this semantics.
To express that states are interpreted as right continuous functions, we can
use formula called
RC
P
⇒
P
for any state variable
P
In [14], Paritosh also proposed a semantics using only the intervals of the
form [0
,t
]. We can also specify this interval model with a temporal propositional
letter
Pre
.
Pre
is interpreted as true only for the interval of the form [0
,t
].
Pre
is specified by the set of formulas
Pref
defined as
Pre
true
⇒
Pre
(
>
0
Pre
)
Pre
¬
=0)
D
∧
D
⇒
(
Pre
∧
(
D
1
D
2)
D
1)
D
2
Pre
∧
⇒
(
Pre
∧
Proposition 3.
Let
I
be an interpretation that validates the set of formulas
Pref and
I
,
[0
,
0]
|
=
Pre.Then,
I
,
V
,
[
a, b
]
|
=
Pre iff a
=0
.
Proof.
Straightforward
Then, a formula
D
is valid in the prefix time interval model if and only if
Pre
⇒
D
is a valid formula in the original model of time interval.
So far, we have introduced special temporal propositional letters
int
,
step
and
Pre
together with DC formulas specifying their special features. We are going to
show that with these propositional letters we can provide a complete description
of many useful time models.
Search WWH ::
Custom Search