Information Technology Reference
In-Depth Information
prior computations as much as possible. In the sequel
t
0
always refers to this
particular tree.
We recall that the right-universality problem is ExpTime-complete for VPAs,
but in PTime for deterministic VPAs [GNT09]. A dual problem to right-uni-
versality w.r.t.
u
is to ask whether every word starting with
u
is
rejected
by a
given VPA. This problem is in PTime, even when the VPA is not deterministic.
Indeed, this amounts to check whether no configuration reached after reading
u
can reach a final configuration.
2.4 Towards an Algorithm
In this section we consider several approaches for addressing right-universality of
VPAs, and justify our choice of considering safe sets of configurations. Readers
not familiar with the related litterature can skip this section at first reading.
As explained in the introduction, we discard the naive approach consisting in
determinizing the VPA and then applying the algorithm in [GNT09], in order
to avoid state-space explosion.
The algorithm given in [GNT09] for deterministic VPAs is a progressive com-
putation of
safe states
, with the property that the VPA is right-universal w.r.t.
u
iff the state reached after reading
u
is safe. Note that safe states cannot be
determined statically: a state can be safe at some position of the word, but not
at another one. A first idea for the non-deterministic case is a subset construc-
tion, using sets of safe states instead of safe states, but this direct adaptation is
not correct. Hence,
safe sets of configurations
will be the basis of our algorithm,
instead of safe states. This point raises new questions, as the configuration space
is infinite, unlike the state space. In fact we will see that at each event, safe sets
of configurations have the same stack height as the depth of the word
u
leading
to this event, and are thus of finite (but potentially huge) cardinality at each
time point.
Recently, several authors have proposed ecient algorithms to check univer-
sality of VPAs [TO12, FKL13, BDG13]. The method that we give in [BDG13]
computes in an incremental way the set
R
of accessibility relations for all hedges
(i.e.
in the present paper, also called summaries in [AM04]).
It uses
antichains
to get smaller objects to manipulate (in particular to limit
R
{
rel
h
|
h
∈
H
Σ
}
to a strict smaller subset) and to avoid an explicit determinization step. It
can be easily adapted for checking right-universality of VPAs [BDG12, Section
3.4]. However we face the problem of computing the whole set
(instead of a
strict subset): experiments indicate that this step is too much time consuming
[BDG13]. For this reason we do not follow this approach, but use antichains over
safe sets of configurations rather than accessibility relations. This approach is
developed in the next section.
R
3 Safe Sets of Configurations
In this section, [
t
0
] is a fixed tree whose linearization is read letter by letter,
and
u
denotes the current read prefix. We introduce the new notion of safe set
