Information Technology Reference
In-Depth Information
⎛
⎝
i<|w|
⎞
⎛
⎞
j<i
⎠
⎝
⊥
⎠
4
(
w
(
i
)
)
4
(
w
(
j
)
)
p
4
(
w
(
i
)
)
ϕ
U
ψ
4
(
w
)=
ψ
ϕ
ϕ
i<|w|
⎛
⎝
i<|w|
⎞
⎛
⎞
4
(
w
(
i
)
)
4
(
w
(
j
)
)
⎠
⎝
p
4
(
w
(
i
)
)
⎠
ϕ
R
ψ
4
(
w
)=
ϕ
i
ψ
ψ
j
≤
i<|w|
The abstract next operator can be defined in a similar manner as their direct
counter parts using the abstract successor
succ
a
instead of the direct successor.
While the the two-valued semantics FLTL considers observations as termi-
nated, the four-valued semantics FLTL
4
reflects the intuition, that a finite ob-
servation might still be continued and therefore next operators X and X evaluate
to
p
, respectively, at the end of a word. For the end of an abstract se-
quence, i.e. when there is no abstract successor, both cases are possible. When
observing an (unmatched) return symbol as the direct successor, the current
“procedure” definitely returns and there is no continuation. The abstract next
operators shall then give a definite verdict, i.e.
p
and
⊥
⊥
. On the other hand, if
the abstract sequence ends because the whole observation ends before the next
abstract successor, there might be a continuation and hence the evaluation is
preliminary, i.e.
or
p
or
⊥
p
.
⎧
⎨
4
(
w
(
n
)
) f
succ
a
(
w
)=
n
ϕ
∈
N
X
a
ϕ
4
(
w
)=
if
succ
a
(
w
) is undef.
⊥
∧
w
1
∈
Σ
r
⎩
p
⊥
otherwise
⎧
⎨
4
(
w
(
n
)
) f
succ
a
(
w
)=
n
ϕ
∈
N
X
a
ϕ
4
(
w
)=
if
succ
a
(
w
) is undef.
∧
w
1
∈
Σ
r
⎩
p
otherwise
Note that the semantics of X
a
is slightly different from the one in [14] to fit
together with the U
a
operator.
Based on the same idea, the abstract until and release operators are defined
as follows.
⎧
⎨
4
(
w
(
j
)
)
4
(
w
(
i
)
)
ψ
ϕ
if
complete
(
w
)
j∈
succ
a
∗
(
w
)
j<i
i∈
succ
a
∗
(
w
)
4
(
w
(
j
)
)
ϕ
U
a
ψ
4
(
w
)=
4
(
w
(
i
)
)
ψ
ϕ
⎩
i∈
succ
a
∗
(
w
)
j∈
succ
a
∗
(
w
)
j<i
otherwise
4
(
w
(
i
)
)
p
⊥
ϕ
i∈
succ
a
∗
(
w
)
