Information Technology Reference
In-Depth Information
2
Q×
B
4
×Γ
≤
2
,is
specified in two parts, one handling the evaluation of the finite control separately
and another part working on the stack. Let therefore be
δ
c
:
Q
For better readability, the transition function
δ
:
Q
×
Γ
×
Σ
→
2
Q×
B
4
the
×
Σ
→
control transition function.
Finite Control.
The finite control evaluates propositional formulae directly
according to the input symbol, also, next formulae just consume the input and
delegate their argument to the next step. The semantics of a formula X
a
ϕ
eval-
uates to
if the next position is a return and the current position is not a call.
However,
δ
c
will never be evaluated on X
a
when reading a call symbol, as can
be seen from the definition of the transition function
δ
below. Therefore we do
not make a distinction for that case here. Until and release formulae are simply
handled using their unfolding.
⊥
,a
)=
{
(
∅
,
)
}
if
p
∈
a
δ
c
(
{
p
}
∅
if
p
∈
a
,a
)=
∅
if
p
∈
a
δ
c
(
{¬
p
}
{
(
∅
,
)
}
if
p
∈
a
δ
c
(
{
ϕ
∧
ψ
}
,a
)=
δ
c
(
{
ϕ,ψ
}
,a
)
δ
c
(
{
ϕ
∨
ψ
}
,a
)=
δ
c
(
{
ϕ
}
,a
)
∪
δ
c
(
{
ψ
}
,a
)
p
)
δ
c
(
{
X
ϕ
}
,a
)=
{
{
ϕ
}
,
⊥
}
(
p
)
δ
c
(
{
X
ϕ
}
,a
)=
{
(
{
ϕ
}
,
}
X
a
ϕ
p
)
δ
c
(
{
}
,a
)=
{
(
{
ϕ,
¬
ret
}
,
⊥
}
p
)
δ
c
(
{
X
a
ϕ
}
,a
)=
{
(
{
ϕ,
¬
ret
}
,
}
δ
c
(
{
ϕ
U
ψ
}
,a
)=
δ
c
(
{
ψ
∨
(
ϕ
∧
X(
ϕ
U
ψ
))
}
,a
)
δ
c
(
{
ϕ
R
ψ
}
,a
)=
δ
c
(
{
ψ
∧
(
ϕ
∨
X(
ϕ
R
ψ
))
}
,a
)
ϕ
U
a
ψ
X
a
(
ϕ
U
a
ψ
))
δ
c
(
{
}
,a
)=
δ
c
(
{
ψ
∨
(
ϕ
∧
}
,a
)
ϕ
R
a
ψ
X
a
(
ϕ
R
a
ψ
))
δ
c
(
{
}
,a
)=
δ
c
(
{
ψ
∧
(
ϕ
∨
}
,a
)
Sets of formulae (clauses) are interpreted as conjunctions. We can therefore
remove alternation by directly evaluating the single formulae on the input symbol
and combining the respective results:
δ
c
(
{
ϕ
1
,...,ϕ
n
}
,a
)=
δ
c
(
{
ϕ
1
}
,a
)
·
...
·
δ
c
(
{
ϕ
n
}
,a
)
The result of a single evaluation
δ
c
(
ϕ,a
) are sets of tuples (
K,b
)ofclauses
and verdicts. In order to combine them the clauses need to be brought back
to the disjunctive clause form which is realized by an operation
·
:Let
K
i
=
(
K
i
,b
i
)
,H
j
=(
H
j
,c
j
)
∈ Q×
B
4
be tuples of states (i.e. conjunctive clauses) and
verdicts. Sets of such tuples are combined by means of a the meet-like operation
·
:2
Q×
B
4
2
Q×
B
4
2
Q×
B
4
as follows.
×
→
