Information Technology Reference
In-Depth Information
Proposition 1.
Let
ua
∈
Pref
(
T
Σ
)
.
⇐⇒ ∃C
∈
C
)
C ∈
LSafe
(
ua
)
Safe
(
u
)
,
C ∈
Pred
a
(
(3)
∃C
∈
C
)
C ∈
Safe
(
ua
)
⇐⇒ ∀
h
∈
H
Σ
,
LSafe
(
ua
)
,
C ∈
Pred
h
(
(4)
However, to get an algorithm, we face the problem that the number of hedges
to consider in Equivalence (4) is infinite. We use relations to overcome this.
Alsothesizeof
Safe
(
u
) may be huge and not all configurations of
Safe
(
u
)are
crucial for checking right-universality w.r.t.
u
. We use antichains to get a compact
representation of
Safe
(
u
). These two concepts are explained in the following
section.
4 An Antichain-Based Algorithm for Right-Universality
In this section, we give an antichain-based algorithm for incrementally checking
right-universality of a VPA, that uses the approach given in Sections 3.2-3.4.
Let us summarize this approach. Let [
t
0
] be the linearization of a given tree
t
0
. We initialize a stack
with set
Init
defined in (2) and we start by computing
Safe
(
u
) with
u
being the first letter of [
t
0
] (see (1)). Suppose that
Safe
(
u
)has
been computed from the current read prefix
u
of [
t
0
]. Then, if the next letter
read in [
t
0
]is
a
S
Σ
, we compute
Safe
(
ua
)from
Safe
(
u
) by Steps 1 and 2, and we
put
Safe
(
u
)onthestack
∈
S
. If the next letter read in [
t
0
]is
a
∈
Σ
,thenwepop
. The element that has been popped is the set
Safe
(
u
)=
Safe
(
ua
)
where
u
is the unique prefix of
u
such that
u
=
u
a
[
h
] (except if
ua
=
t
0
in
which case the popped set is equal to
Init
=
Safe
(
ua
)), see Section 3.3. At each
computation of
Safe
(
u
), we check whether
Reach
(
u
)
the stack
S
∈
Safe
(
u
)(seeTheorem1).
4.1 Finite Number of Hedges
We begin by showing that only a finite number of hedges has to be considered
in Equivalence (4). The reason is that a hedge
h
does not change the stack of
a configuration during a run of a VPA, that is (
q,σ
)
[
h
]
−−→
(
q
,σ
). So
h
can be
considered as a function mapping each state
q
to the set of states obtained when
traversing
h
from
q
. Formally, for every
h
∈
H
Σ
,
rel
h
is the function from
Q
rel
h
(
q
)iff(
q,σ
)
[
h
]
to 2
Q
such that
q
∈
(
q
,σ
)forsome
σ
Γ
∗
.Thenumber
−−→
∈
2
|Q|
. These functions naturally
define an equivalence relation of finite index over
H
Σ
:
h
of such functions is finite, and bounded by
|
Q
|·
h
⇐⇒
∼
rel
h
=
rel
h
.
Let us note
H
for a subset containing one hedge per
∼
-class. We have
|
H
|≤
2
|Q|
. The next lemma indicates that the computation of
h
-predecessors can
be limited to
h
|
Q
|·
H
.
Lemma 2.
For every
h
∈
C
iff there exists
h
∈
∈
H
Σ
,
C
is a
h
-predecessor of
H
h
, such that
is a
h
-predecessor of
C
.
with
h
∼
C
The set
H
can be computed by a saturation method based on the VPA rules.
