Information Technology Reference
In-Depth Information
of configurations related to
u
. We show how safe sets of configurations can be
defined from such sets associated to smaller prefixes
u
of [
t
0
]. This property will
be useful to derive an incremental algorithm for checking right-universality of
aVPA.
3.1 A Notion of Safety for Right-Universality
Γ
∗
be a non empty set of config-
Definition 3.
Let
A
be a VPA and
C ⊆
Q
×
urations. Let
u
∈
Pref
(
T
Σ
)
\{
}
be a non empty prefix of
t
0
.
-
C
is safe for
u
if for every
v
such that
uv
∈
[
T
Σ
]
,thereexist
(
q,σ
)
∈ C
and
Q
f
such that
(
q,σ
)
v
p
∈
→
(
p,
)
in
A
.
-
C
is leaf-safe for
u
if for every
v
=
av
with
a
∈
Σ
such that
uv
∈
[
T
Σ
]
,there
Q
f
such that
(
q,σ
)
v
.
4
exist
(
q,σ
)
∈ C
and
p
∈
→
(
p,
)
in
A
Let Safe
(
u
)=
{C | C
is safe for
u
}
and LSafe
(
u
)=
{C | C
is leaf-safe for
u
}
.
Intuitively, as stated in Theorem 1 below, if
C
is the set of configurations
reached in
A
after reading
u
,then
A
is right-universal w.r.t.
u
iff
C
is safe for
u
.
Indeed, for every possible
v
, one can find in
at least one configuration leading
to an accepting configuration after reading
v
. Before stating this theorem, let
us give the next definition. Let
Reach
(
u
) denote the set of configurations (
q,σ
)
such that (
q
0
,σ
0
)
u
C
→
(
q,σ
) for some initial configuration (
q
0
,σ
0
)of
A
.
Theorem 1.
A
is right-universal w.r.t.
u
iff Reach
(
u
)
∈
Safe
(
u
)
.
Let us illustrate this on the VPA
A
depicted in Figure 2a. Recall that this
VPA checks that the tree has a
g
-node with an
f
-child. After opening a
g
-root,
the set of safe configurations is
Safe
(
g
)=
{{
(
q
2
,γ
1
)
},{
(
q
2
,γ
0
)
}}
, which does
not contain the set of reached configurations, as
Reach
(
g
)=
{
(
q
1
,γ
0
)
}
. Indeed,
A
is not right-universal w.r.t.
g
,asno
f
-node has been encountered yet un-
der a
g
-node. For the word
gf
, as expected, the situation differs:
Safe
(
gf
)=
{{
(
q
2
,γ
1
γ
0
)
}
,
{
(
q
2
,γ
0
γ
0
)
}}
,and
Reach
(
gf
)=
{
(
q
2
,γ
0
γ
0
)
}
is a safe set of config-
urations. By Theorem 1,
is right-universal w.r.t.
gf
.
Hence, an algorithm computing both
Reach
(
u
)and
Safe
(
u
) can decide right-
universality w.r.t.
u
.Theset
Reach
(
u
) is easy to compute, just by firing tran-
sitions of the VPA. In Sections 3.2-3.4, we detail how the set
Safe
(
u
)canbe
defined from the set
Safe
(
u
) with
u
a proper prefix of
u
.Inthisway,while
reading the linearization [
t
0
]ofagiventree
t
0
,theset
Safe
(
u
) with
u
A
=
prefix
of [
t
0
], can be incrementally defined. In Section 4, we turn this approach into an
algorithm.
4
The name “leaf-safe” comes from the fact that we only consider suxes starting
with a
Σ
symbol, and thus continuations of the tree that do not add children to the
current node.
