Information Technology Reference
In-Depth Information
precisely via a DC formula with state variable
C
(without
int
). Perhaps
int
=
0 is the only formula that cannot be expressed by a formula via state variable
C
without
int
.
∧
can also be used as a means to define the variable
C
via
int
and vice-versa. If we use
CC
CC
to define
int
,theaxiomsfor
C
simply are:
C
∨¬
C
⇒
≤
1
(4)
¬
¬
((
C
C
C
)
∨
(
¬
C
C
C
))
⇒
≥
1
(5)
The relationship between these axioms and the axioms for
int
presented earlier
is formulated as:
Proposition 2.
Let interpretation
I
be such that the formulas in
CC
and axioms
(1) and (2) are satisfied by all intervals.
1. If the axioms (4) and (5) are satisfied by all intervals, the axiom (3) is
satisfied by all intervals.
2. If the axiom (3) is satisfied by all intervals then the axioms (4) and (5) are
satisfied by all intervals, too.
Proof.
ProofofItem1
. The axioms (4) and (5) implies that the formula
(
=1)
(
¬
P
P
¬
P
))
⇒
(
¬
P
P
∧
¬
P
))
is satisfied for any interval when
P
is either
C
or
¬
C
. For any interval [
b, e
],
if
e
−
b
≥
2 then there are
b
=
τ
0
< ... < τ
n
=
e
such that [
τ
i
,τ
i
+1
]satisfies
,and
τ
i
,0
<i<n
are the points the state
C
changes its value.
Therefore, from (3), (4) and
C
∨¬
C
CC
the formula
int
∧
= 1 is satisfied by [
τ
i
,τ
i
+1
]
when 0
<i<n
−
1, and
τ
1
−
τ
0
<
1and
τ
n
−
τ
n−
1
<
1. Furthermore, from
int
∧
=1
⇒
(
C
∨¬
C
)itfollowsthat[
τ
i
,τ
i
+1
], 0
<i<n
−
1aretheonly
intervals satisfying
int
= 1. Hence, (3) is satisfied by [
b, e
].
ProofofItem2
.Let
h>
0 be the first time point that state
C
changes its
value. From the axioms (1), (2) and (3) it follows that
h
∧
=1
is satisfied by and only by the intervals of the form [
n
+
h, n
+1+
h
],
n
≤
1and
int
∧
∈
N
.
Hence, if
is satisfied by all intervals, the axioms (4) and (5) are also satisfied
by all intervals.
CC
So, with the assumption that 0 is an integer point, the axioms (4) and (5) are
equivalent to the axiom (3).
Let
step
be a temporal propositional letter that represents two consecutive
state changes of the system under consideration. When there are several state
changes at a time point
t
,
step
evaluates to 1 over interval [
t, t
]. When two
consecutive state changes are at
t
and
t
=
t
,
step
is true for the
such that
t
interval [
t, t
], and for any state variable
P
,either
P
or
¬
P
holds for the
interval [
t, t
]. This is represented by:
step
∧
>
0
⇒
(
P
∨¬
P
) for any state variable
P
>
0)
(
step
step
∧
>
0
⇒¬
((
step
∧
∧
>
0))
Search WWH ::
Custom Search