Information Technology Reference
In-Depth Information
·
D
P
(
i, p, s,
[
i
1
,...,i
n
])
t
1
∈L
i
1
(
S
)
···
t
n
∈L
i
n
(
S
)
p
(
s,
[
t
1
,...,t
n
])
∈L
i
(
S
)
Example 3.
For the set
S
=
{
P
(1
,p,
0
,
[2])
⇐
,
P
(2
,q,
0
,L
)
⇐
C
(
L
)
,
C
([])
⇐
,
C
([1])
⇐
}
,
we have
L
1
(
S
)=
{
p
(0
,
[
q
(0
,
[])])
,p
(0
,
[
q
(0
,
[
p
(0
,
[
q
(0
,
[])])])])
, ...
}
.
Finally we are able to describe an arbitrary regular set of configurations
C
by a set of
Horn clauses this way:
Lemma 3.
Let
C
⊆
Proc
be a regular set of configurations (given as a tree automa-
ton). A set
S
C
of normal Horn clauses that contains a 4-ary predicate
P
and a natural
number
N
∈
N
can be constructed in linear time that fulfills the following properties:
1. It holds
∪L
N
(
S
)=
C
.
2. If
(
i, p
1
,s
1
,l
1
)
∈H
S
C
(
P
)
and
(
i, p
2
,s
2
,l
2
)
∈H
S
C
(
P
)
,then
p
1
=
p
2
.
3. If
(
i, p
1
,s
1
,
[
i
1
,...,i
n
])
∈H
S
C
(
P
)
,then
L
1
(
S
)
∪
...
L
i
j
=
∅
for all
j
=1
,...,n
.
Example 4.
For
C
=
{
#(
0
,
[])
,
#(
0
,
[#(
0
,
[])])
,
#(
0
,
[#(
0
,
[])
,
#(
0
,
[])])
,...
}
,
the set
S
C
=
{
P
(
x
N
,x
P
,x
S
,x
L
)
⇐
H
1
(
x
N
)
∧
H
#
(
x
P
)
∧
H
0
(
x
S
)
∧
P
list
(
x
L
)
,
P
(
x
N
,x
P
,x
S
,x
L
)
⇐
H
2
(
x
N
)
∧
H
#
(
x
P
)
∧
H
0
(
x
S
)
∧
H
[]
(
x
L
)
,
P
list
([])
⇐
,
P
list
(
x
N
::
x
L
)
⇐
H
2
(
x
N
)
∧
P
list
(
x
L
)
,H
0
(
0
)
⇐
,
H
1
(1)
⇐
, H
2
(2)
⇐
, H
#
(#)
⇐
, H
[]
([])
⇐
}
is a set of normal Horn clauses that fulfills the properties mentioned in lemma 3.
The finite set of Horn clauses constructed according to lemma 3 for
P
represents
the regular set
C
. We now add Horn clauses that describe backward reachability. Let
S
CDPN
(
M
) be the smallest set of Horn clauses that fulfills the following properties:
Δ
, then the following clauses are in
S
CDPN
(
M
):
1. If
Φ
:
pγ
→
p
1
w
1
∈
P
(
x
N
,p,γx
S
,x
L
)
⇐
P
(
x
N
,p
1
,w
1
x
S
,x
L
)
∧
Q
Φ
(
x
L
)
Δ
, then the following clauses are in
S
CDPN
(
M
).
2. If
Φ
:
pγ
→
p
1
w
1
p
2
w
2
∈
P
(
x
N
,p
1
,w
1
x
S
,x
N
::
x
L
)
∧
P
(
x
N
,p
2
,w
2
0
,
[])
∧
P
(
x
N
,p,γx
S
,x
L
)
⇐
Q
Φ
(
x
L
)
The predicate
Q
Φ
is a predicate that holds for a list
[
i
1
,...,i
n
]
iff there exists
t
j
∈
L
i
j
(
S
) for all
j
=1
,...,n
such that
st
(
t
1
)
...
st
(
t
n
)
∈
Φ
. Consider for instance the
constraint
Φ
, which is defined by the regular expression (
pq
)
∗
,where
p
and
q
are control
states. The corresponding predicate
Q
Φ
can be defined by the following Horn clauses:
Q
Φ
([])
⇐
Q
Φ
(
x
N
::
x
L
)
⇐
P
(
x
N
,p,x
1
,x
2
)
∧
Q
Φ
(
x
L
)
Q
Φ
(
x
N
::
x
L
)
⇐
P
(
x
N
,q,x
1
,x
2
)
∧
Q
Φ
(
x
L
)
Search WWH ::
Custom Search