Information Technology Reference
In-Depth Information
dis
represents an interval between two discrete points. When considering the
Discrete Step Time Models, the chop point should satisfy
pt
.
The sublanguage
DSL
, which is the union of
SC
,
ID
,
CC
,
DP DC
and
RC
,
forms a relatively complete specification for the discrete time structure.
Let
disemb
(
ϕ
) be a formula that is obtained from
ϕ
by replacing each proper
subformula
ψ
of
ϕ
by
ψ
dis
. For example
disemb
(
φ
dis
)
(
dis
∧
¬
ψ
)=(
φ
∧
∧
¬
(
ψ
∧
dis
).
Theorem 2.
Let ϕ be a DC formula with no occurrence of temporal proposition
letters. Then,
DSL
dis
⇒
disemb
(
ϕ
)
exactly
|
=
SDC
ϕ.
Proof.
The proof works in exactly the same way as the proof of Theorem 1.
Any discrete step time model
I
,
[
a, b
] can be extended to a model that satisfies
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
]
|
=
SDC
ϕ
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 discrete step time model that
satisfies
.
For the “if” part, notice that if
DL
|
=
SDC
ϕ
then
dis
⇒
intemb
(
ϕ
) is a valid
DL
formulainDCwiththeassumption
. Consequently, from the relative com-
pleteness of DC,
disemb
(
ϕ
)isprovableinDCwiththeassumption
DL
.
Sampling Time Models.
A sampling time model consists of the time points where
we sample the data. Assume that the samplings are frequent enough and that
any state change should be at a sampling point. To specify this time model, we
can use
DSL
and an additional assumption
step
⇒
=1
/h
where
h
SL
h
be the language
for the sampling time model with the sampling time step 1
/h
.
∈
N
,
h>
0, i.e. 1
/h
is the sampling time step. Let
4
Specifying Sampling, Periodic Task Systems and
Projection to Discrete Time
4.1
Sampling
Sampling and specifying periodic task systems are immediate applications of the
results presented in the previous section.
We have built a language for sampling time models based on the continuous
time DC. Hence, we can use the proof system of DC to reason about validity of a
formula in that time and state model. How to relate the validity of a formula
D
in that time and state model with the validity of a formula
D
in the original DC?
In our early work [9], we have considered that relation, but had to formulate the
Search WWH ::
Custom Search