Information Technology Reference
In-Depth Information
Return.
Having all the information from the stack when reading a return symbol
a
r
∈
P
can simulate the transition relation
δ
on all current states. This,
however is not done directly on
R
but on the current states at call-time
R
by consecutively applying
a
c
,
S
and then
a
r
to obtain the new set of current
states
R
and the new effect relation
S
. We obtain the output from all possible
transitions via
a
r
,after
a
c
and
S
have been applied.
We let
δ
((
S,R
)
,a
r
,
(
S
,R
,a
c
)) = (
S
,R
,,
) such that
Σ
r
,
(
q,q
,
)
q
1
,q
2
,γ
,γ
,
:(
q
1
,γ
γ
,
)
δ
(
q,a
c
,γ
)
,
U
=
{
|∃
∈
S,
(
q
,,
)
δ
(
q
2
,a
r
,γ
)
(
q
1
,q
2
)
∈
∈
}
S
=
(
q,q
)
q
3
,
:(
q,q
3
)
S
,
(
q
3
,q
,
)
{
|∃
∈
∈
U
}
R
=
q
|∃
R,
:(
q,q
,
)
{
q
∈
∈
U
}
=
|∃
R,q
:(
q,q
,
)
{
q
∈
∈
U
}
Note that the stack might have been necessary for computing the effect
S
but
once it is known, the effect can be applied to a set of states without using the
stack.
Finally, we need to specially treat the case of a return action
a
r
∈
Σ
r
when
reading the bottom symbol. Let
δ
((
S,R
)
,a
r
,
#) = (
S
,R
,
#
,
) such that
S
=
(
q,q
)
q
,
:(
q,q
)
S,
(
q
,
#
,
)
δ
(
q
,a
r
,
#)
{
|∃
∈
∈
}
R
=
q
|∃
R,
:(
q
,
#
,
)
{
q
∈
∈
δ
(
q,a
r
,
#)
}
=
|∃
R,q
:(
q
,
#
,
)
{
q
∈
∈
δ
(
q,a
r
,
#)
}
3.4 Constructing a VPMM for CaRet
+
The idea of the construction is that the Mealy machine maintains the formulae
that need to be proved. When reading an input symbol it verifies the proposi-
tional part and postpones the resulting future obligations. Standard LTL formu-
lae are encoded into the finite control and evaluated on the next input. Abstract
until and release operators are reduced to checking their unfolding.
When observing a call action, the abstract next modalities push their argu-
ment on the stack as future obligation. On return, this obligation is removed
from the stack and evaluated together with the current obligation stored in the
finite control.
The transition function maintains a disjunctive clause form of stored obliga-
tions and thereby removes alternation on the fly. The output in every step is the
truth value from the evaluation of the current finite control state combined with
the current evaluation of the stack. The stack evaluation describes the truth
values of the suspended abstract operators from higher levels.
Given a CaRet
+
formula
Φ
we construct a Vpmm
M
B
4
)
where the control states
Q
=2
sub
(
Φ
)
store a set of formulae to be evaluated upon
the next input symbol and the stack alphabet
Γ
=2
sub
(
Φ
)
=(
Q,Σ,Γ,δ,Q
0
,
×
B
4
×
B
4
stores the
future obligations, the current and the previous stack evaluation.
