Information Technology Reference
In-Depth Information
Integer Time Model
To specify that a state can only change at an integer time
point, we can use the formula
IS
:
step
⇒
int
forms a relative complete
specification for the discrete time structure. Let
ϕ
be a formula which does not
have any occurrence of temporal variables
int
ans
step
.Let
intemb
(
ϕ
)bea
formula that obtained from
ϕ
by replacing each proper subformula
ψ
of
ϕ
by
ψ
Let
DL
be the union of
SC
,
IS
,
ID
,
RC
.
DL
int
. For example
intemb
(
φ
int
)
(
int
∧
¬
ψ
)=(
φ
∧
∧¬
(
ψ
∧
int
).
Theorem 1.
Let ϕ be a DC formula with no occurrence of temporal proposition
letters. Then,
DL
int
⇒
intemb
(
ϕ
)
exactly when
|
=
DDC
ϕ.
Proof.
Any discrete time model
I
,
[
a, b
] can be extended to a model that satisfies
the formulas in
in the obvious way, namely with the interpretation for
int
and
step
with the intended meanings for them. By induction on the structure
of the formula
ϕ
, it is easy to prove that
DL
I
,
[
a, b
]
|
=
DDC
ϕ
if and only
I
,
[
a, b
]
|
=
intemb
(
ϕ
).
Then, the “only if” part follows directly from the soundness of the proof of
the DC system that
intemb
(
ϕ
) is satisfied by any integer model that satisfies
DL
.
The “if” part is proved as follows. From the above observation, if
|
=
DDC
ϕ
then
int
.
Consequently, from the relative completeness of DC,
intemb
(
ϕ
)isprovablein
DC with the assumption
⇒
intemb
(
ϕ
) is a valid formula in DC with the assumption
DL
DL
.
Discrete Step Time Model.
As it was said earlier, a discrete step time model
consists of all time points at which there is a the state change. Since we have
assumed that the special state variable
C
for the clock ticks is present in our
system that changes its value at every integer point, this model of time should
also include the set of natural numbers. This is the reason that we include
N
as
a subset of
. This time model was defined and used by Pandya et al in [14].
To represent a time point in this model, we introduce a temporal propositional
letter
pt
,
pt
holds for an interval [
t, t
]iff
t
=
t
S
and
t
is a time point at which
thereisastatechange.
pt
should satisfy:
pt
⇒
=0
pt
true
pt
step
⇒
pt
true
pt
int
⇒
pt
step
∗
int
⇒
Let
denote this set of formulas. The last formula in this set expresses our
assumption that no Zeno computation is allowed, i.e. in any time interval, there
are only a finite number of state changes. Let us define a DC formula
dis
as
DP
=(
pt
true
pt
)
dis
Search WWH ::
Custom Search