Information Technology Reference
In-Depth Information
g
call(g)
call(g)
return(g)
call(g)
call(f)
return(f)
return(g)
return(g)
g
g
f
Fig. 1.
Representation of a program trace as a tree
t
An
unranked tree
t
over
Σ
is a tree such that its nodes are labeled by a letter
of
Σ
and have an arbitrary number of children (the children are ordered from
left to right). We call
a
-node
anodewithlabel
a
Σ
. The set of all unranked
trees over
Σ
is denoted by
T
Σ
.A
hedge
h
over
Σ
is a finite sequence (empty or
not) of unranked trees over
Σ
. The empty hedge is denoted by
,andthesetof
all hedges over
Σ
is denoted by
H
Σ
.
Trees can be described by well-balanced words which correspond to a depth-
first traversal of the tree. An opening tag is used to notice the arrival on a node
and a closing tag to notice the departure from a node. For each
a
∈
Σ
,let
a
itself represent the opening tag and
a
the related closing tag. The
linearization
[
t
]of
t
∈
∈
T
Σ
is the
well-balanced
word over
Σ
∪
Σ
, with
Σ
=
{
a
|
a
∈
Σ
}
,
inductively defined by: [
t
]=
a
[
t
1
]
[
t
n
]
a
, with
a
is the label of the root and
t
1
,...,t
n
are its
n
subtrees (from left to right). The linearization is extended to
hedges as follows. Let
h
=
t
1
···
···
t
n
be the sequence of trees
t
i
,1
≤
i
≤
n
.Then
[
h
]=[
t
1
]
[
t
n
]. We denote by [
T
Σ
](resp.[
H
Σ
]) the set of linearizations of all
trees in
T
Σ
(resp. hedges in
H
Σ
). Consider for instance the tree
t
in Figure 1:
its linearization is the word [
t
]=
ggggffgg
.Let
Pref
(
T
Σ
)denotethesetofall
prefixes of [
T
Σ
]:
Pref
(
T
Σ
)=
···
{
u
∈
(
Σ
∪
Σ
)
∗
|∃
v
∈
(
Σ
∪
Σ
)
∗
,uv
∈
[
T
Σ
]
}
.
2.2 Visibly Pushdown Automata
Definition 1.
A
visibly pushdown automaton
A
over a finite alphabet
Σ
is a
tuple
=(
Q,Σ,Γ,Q
i
,Q
f
,Δ
)
where
Q
is a finite set of states containing initial
states
Q
i
⊆
A
Q
, a finite set
Γ
of stack symbols, and a
finite set
Δ
of rules. Each rule in
Δ
is of the form
q
a
:
γ
Q
and final states
Q
f
⊆
q
with
a
−−→
∈
Σ
∪
Σ
,
q,q
∈
Γ
.
The left-hand side of a rule
q
a
:
γ
Q
,and
γ
∈
−−→
p
∈
Δ
is (
q,a
)if
a
∈
Σ
,and(
q,a,γ
)if
a
Σ
.AVPAis
deterministic
if it has at most one initial state, and it does not
have two distinct rules with the same left-hand side. We provide an example of
deterministic VPA in Figure 2a.
A
configuration
of a VPA
∈
Γ
∗
a
A
is a pair (
q,σ
)where
q
∈
Q
is a state and
σ
∈
stack content. A configuration is
initial
(resp.
final
)if
q
∈
Q
i
(resp.
q
∈
Q
f
)and
(
q
,σ
) if there is a transition
q
a
:
γ
Σ
,wewrite(
q,σ
)
a
q
σ
=
.For
a
∈
Σ
∪
→
−−→
in
Δ
verifying
σ
=
γ
σ
if
a
·
σ
if
a
∈
Σ
,and
σ
=
γ
·
∈
Σ
.Weextendthis
a
n
,bywriting(
q
0
,σ
0
)
u
notation to words
u
=
a
1
···
→
(
q
n
,σ
n
) whenever there
exist configurations (
q
i
,σ
i
) such that (
q
i−
1
,σ
i−
1
)
a
i
−→
(
q
i
,σ
i
) for all 1
≤
i
≤
n
.