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 .
 
Search WWH ::




Custom Search