Information Technology Reference
In-Depth Information
Since all clauses of
S
are linear, our normalization semi-procedure could also be
applied directly. The algorithm performs the following steps:
(
cut
)(17)(11)
P
(
f
(
x
)
,g
(
y
))
⇐
A
(
x
)
∧
B
(
y
)
∧
Q
(
x
)
(20)
(
cap1
)(20)
P
(
f
(
x
)
,g
(
y
))
⇐{
A, Q
}
(
x
)
∧
B
(
y
)
(21)
(
cap2
)(12)(15)(21)
{
A, Q
}
(
a
)
⇐
(22)
(
sp
)(21)
P
(
x, g
(
y
))
⇐
P
(
,g
(
B
))
(
x
)
∧
B
(
y
)
(23)
P
(
,g
(
B
))
(
f
(
x
))
⇐{
A, Q
}
(
x
)
(24)
P
(
x, y
)
⇐
P
(
,g
(
B
))
(
x
)
∧
P
(
P
(
,g
(
B
))
,
)
(
y
)
(
sp
)(23)
(25)
P
(
P
(
,g
(
B
))
,
)
(
g
(
y
))
⇐
B
(
y
)
(26)
(
cut
)(17)(25)
P
(
f
(
x
)
,g
(
y
))
⇐
P
(
,g
(
B
))
(
x
)
∧
P
(
P
(
,g
(
B
))
,
)
(
y
)
∧
Q
(
x
)
(27)
(
cap1
)(27)
P
(
f
(
x
)
,g
(
y
))
⇐{
P
(
,g
(
B
))
,Q
}
(
x
)
,P
(
P
(
,g
(
B
))
,
)
(
y
)
(28)
Our normalization procedure terminates, because
.
In fact
it always terminates, if the predicate
Q
is defined by finitely many Horn clauses of the
form
Q
(
t
)
⇐
H
S∩N
(
{
P
(
,g
(
B
))
,Q
}
)=
∅
. This is one situation where instantiation can be applied.
Our example shows that our normalization procedure in some cases dispenses with the
need for an instantiation pre-processing step. In example 1, we have seen that there are
cases where instantiation does not work, but our techniques can be applied. On the other
hand, there also exist examples where instantiation can be applied such that the resulting
finite set of Horn clauses is a finite set of
H
1
Horn clauses, but our normalization semi-
procedure does not terminate. This means that our techniques neither is subsumed by
instantiation, nor does dispense with the need of instantiation in all cases. Instead, our
normalization semi-procedure can be enhanced with instantiation in the same way as
H
1
solving can be enhanced.
3
An Application: Backward Reachability Analysis for
Constrained Dynamic Pushdown Networks
Bouajjani et al. [3] introduced
constrained dynamic pushdown networks (CDPNs)
as a
model of recursive programs with dynamic thread creation. CDPNs extend the model-
ing power of
pushdown automata
[2,5,9],andevenofPADs[10].
Assume that we are given a regular set
C
of
bad
configurations.
Backward reacha-
bility analysis
tries to determine the set pre
∗
(
C
) of all configurations from which bad
configurations can be reached. The system then can be considered as safe if the inter-
section of pre
∗
(
C
) with the set of initial configurations is empty. In this section, we
demonstrate that backward reachability can be described by means of finite sets of lin-
ear Horn clauses which our normalization semi-procedure normalizes in exponential
time in the worst-case.
A
constrained dynamic pushdown network
(CDPN for short) is a tuple
M
=(
P
,Γ,
Δ
),where
P
is a finite set of
control states
,
Γ
is a finite set of stack symbols disjoint
Search WWH ::
Custom Search