Information Technology Reference
In-Depth Information
from
P
,and
Δ
is a finite set of transition rules of the following forms: either (a)
Φ
:
pγ
Γ
∗
,
→
p
1
w
1
,or(b)
Φ
:
pγ
→
p
1
w
1
p
2
w
2
,where
p, p
1
,p
2
∈
P
,γ
∈
Γ, w
1
,w
2
∈
and
Φ
is a
constraint over
P
, i.e., a regular word language over
P
.
For the remainder of this section let
M
be a CDPN. In order to define the set of all
configurations
for
M
, we consider a stack symbol
γ
∈
Γ
as a unary function symbol
and a control state
p
∈
P
as a 2-ary function symbol. We denote the empty stack by the
constant
0
and use the binary function symbol
cons
and the constant
nil
to construct
lists. For a unary function symbol
γ
and a term
t
we also write
γt
instead of
γ
(
t
).In
contrast to Bouajjani et al. [3] we define the set Proc
M
of all configurations for
M
by:
Stack ::=
Γ
(Stack)
|
0
Children ::=
cons
(Proc
M
,
Children)
|
nil
Proc
M
::=
P
(Stack
,
Children)
We also denote the function symbol
cons
by the right associative infix functional sym-
bol :: and the constant
nil
by []. Furthermore, we abbreviate the list
t
1
::
...
::
t
n
::[]
as [
t
1
,...,t
n
]. We denote the control state
p
of a process
t
=
p
(
s,
[
t
1
,...,t
n
]) by
st
(
t
). A process
p
(
γ
1
...γ
k
0
,
[
t
1
,...,t
n
]) consists of the control state
p
, the stack
γ
1
...γ
k
0
(
γ
1
is the top-most stack-element), and a list of child processes [
t
1
,...,t
n
].
p
(
γδ
0
,
[
q
(
0
,
[])]), for instance, is a configuration that consists of one root process and
one child process.
The transition relation
→
M
for a CDPN
M
is the smallest relation between config-
urations that fulfills the following properties:
1. If
Φ
:
pγ
→
p
1
w
1
∈
Δ
and
st
(
t
1
)
···
st
(
t
n
)
∈
Φ
,then
C
[
p
(
γs,
[
t
1
,...,t
n
])]
→
M
C
[
p
1
(
w
1
s,
[
t
1
,...,t
n
])]
.
2. If
Φ
:
pγ
→
p
1
w
1
p
2
w
2
∈
Δ
and
st
(
t
1
)
···
st
(
t
n
)
∈
Φ
,then
C
[
p
(
γs,
[
t
1
,...,t
n
])]
→
M
C
[
p
1
(
w
1
s,
[
p
2
(
w
2
,
[])
,t
1
,...,t
n
])]
.
Here,
denotes a one-hole-context. We omit
M
, whenever it is clear from the context.
Given a set of configurations
C
, we define the set of backward reachable config-
urations pre
∗
M
(
C
) by pre
∗
M
(
C
):=
{
C
C
:
t
∗
. We want to compute
pre
∗
M
(
C
) for a given regular set of configurations
C
. Bouajjani et al. [3] showed that
the set of backward reachable configurations is regular, if we start from a regular set of
configurations and all constraints appearing in the CDPN are
stable
. A constraint
Φ
is
called stable iff
st
(
t
1
)
···
st
(
t
n
)
∈
t
|∃
t
0
∈
→
M
t
0
}
Φ
, whenever
t
1
,...,t
n
,t
1
,...,t
n
are configurations
such that
t
j
→
t
j
Φ
.
In order to do backward reachability analysis through linear Horn clauses, we first
define a mapping between the least model of a set of Horn clauses with a special 4-ary
predicate
P
and a regular set of configurations. In the Horn clause framework, a control
state
p
is a constant instead of a binary function symbol. For convenience, the states of the
finite tree automaton for the set
C
, are represented by (finitely many) natural numbers.
For a set
S
of Horn clauses that contains a 4-ary predicate
P
,and
i
holds for all
j
=1
,...,n
,and
st
(
t
1
)
···
st
(
t
n
)
∈
∈
N
,wedefine
L
i
(
S
) to be the set of configurations
t
such that the judgment
t
∈L
i
(
S
) can be derived
from derivations
D
for
P
(
i, p, s,
[
i
1
,...,i
n
])
∈H
S
by the rule:
Search WWH ::
Custom Search