Information Technology Reference
In-Depth Information
The distinguishing aspect between finitary and infinitary semantics is the need
for handling the end of a trace which is reflected by discriminating weak and strong
operators. A formula X
ϕ
describes what should happen at the next time step. If
the trace ends here, it needs to be specified if that is desired or not. The temporal
operatorsX, X
a
,UandU
a
are considered as strong operators having an existential
character. They require the next position to exist and evaluate to
p
if not. Con-
sequently, their duals X, X
a
,RandR
a
have a weak, i.e. universal character; they
impose restrictions only on actually existing positions. If there is no successive po-
sition, they evaluate to
⊥
p
. Note that the next operators and their (weak) duals
therefore do not coincide on finite traces as they do on infinite ones.
Abstract Successors.
For the semantics of the abstract temporal modalities, we
use the notion of abstract steps in terms of the abstract successor function
succ
a
as in the infinitary CaRet semantics. We define the partial function
succ
a
:
Σ
∞
N
0
mapping a word to the
abstract successor
of its first position. For
Σ
∞
,
succ
a
(
w
)=1if
any
w
Σ
r
is
not a return. If
w
starts with a call, then the abstract successor is its matching
return, if it exists:
succ
a
(
w
)=
i
if
w
0
∈
∈
|
w
|≥
2,
w
0
∈
Σ
c
is not a call and
w
1
∈
Σ
c
and
i
∈
N
0
is the smallest number
s.t.
w
i
∈
Σ
r
and in
w
1
...w
i
the number of positions
j
with
w
j
∈
Σ
r
is greater
than the number of positions
j
with
w
j
∈
Σ
c
.
succ
a
(
w
) is undefined in all other
cases. Further, we let
succ
a
∗
(
w
) denote the set of positions
{
i
1
,i
2
,...
}
on a word
Σ
∞
s.t.
i
1
=0and
i
j
+1
=
succ
a
(
w
(
i
j
)
). Additionally, we define a predicate
complete
(
w
)thatistrueif
succ
a
∗
(
w
) has a maximal element
i<
w
∈
|
w
|−
1and
w
i
+1
∈
Σ
r
is a return, otherwise
complete
(
w
) is false. That is,
complete
(
w
)is
true if a return in
w
is not matched and thus the abstract sequence formed by
the positions in
succ
a
∗
(
w
) terminates because of the first unmatched return.
We define the semantics in conformance with FLTL
4
as defined in [4]. The
semantics of a formula is given in terms of a function that maps words
w ∈ Σ
=
2
AP
to the
B
4
-lattice. For propositions and boolean connectives, the two-valued
semantics can be directly lifted to the
B
4
-lattice.
4
(
w
)=
4
(
w
)=
if
p
∈
w
0
if
p
∈
w
0
p
¬
p
⊥
if
p
∈
w
0
⊥
if
p
∈
w
0
ϕ
∧
ψ
4
(
w
)=
ϕ
4
(
w
)
ψ
4
(
w
)
ϕ
∨
ψ
4
(
w
)=
ϕ
4
(
w
)
ψ
4
(
w
)
For the (direct) strong and weak next operators the semantics is defined as
discussed above.
4
(
w
)=
4
(
w
)=
4
(
w
(1)
) f
4
(
w
(1)
) f
ϕ
|
w
|
>
1
ϕ
|
w
|
>
1
X
ϕ
X
ϕ
p
p
⊥
otherwise
otherwise
The standard semantics of the U and R operator is lifted to
B
4
. The right parts
of the definitions deal with the end of words.
