Information Technology Reference
In-Depth Information
(a) Size of
H
.
(b) Time to compute
H
.
Fig. 3.
Space and time consumption for computing
H
on 50 VPAs of various densi-
ties,
|Q|
= 10,
|Σ|
=
|Γ|
= 3, and timeout of 60s
6 Experiments
We have implemented Algorithm 2 in a prototype tool together with the data
structures and improvements proposed in Section 5 (following both approaches,
using operator
and a SAT solver). We mainly use Python, with C binding to
the Glucose SAT solver (first ranked in recent SAT competitions) [Glucose].
The experimental tests are performed on two different benchmarks, one com-
posed of randomly generated VPAs, and another one based on the translation of
XPath expressions to VPAs. The experiments were run on a PC equipped with
an Intel i7 2.8GHz processor, 6 GB of RAM and running Linux Ubuntu 3.2.
6.1 Randomly Generated VPAs
During the random generation of VPAs
A
=(
Q,Σ,Γ,Q
i
,Q
f
,Δ
),
|
Q
i
|
is fixed
to 1, and several parameters vary: the sizes
|
Q
|
,
|
Σ
|
and
|
Γ
|
, the density of final
states
|Q
f
|
|Q|
, and the transition density
5
. Our online algorithm for checking right-
universality needs to compute the set
of minimal hedges as a preprocessing.
This set can be huge and thus lead to a timeout. In Figure 3a (resp. Figure 3b), we
indicatethe averagesizeof
H
(resp. the averageexecution time to compute it) for
randomly generated VPAs with variable transition density (from 1 to 19) and vari-
able final state density. In this test, we distinguish universal automata from non-
universal ones since a universal VPA is right-universalw.r.t all
u
H
.
The two figures show that timeout happens for instances with transition density
around 12, and that the density of final states has few influence.
In the next experiment, we study the behavior of our algorithm on 90 ran-
dom instances of size 10 (resp. 20, 30), with fixed transition density 8 (resp.
∈
Pref
(
T
Σ
)
\{
}
5
Equal to the number of outgoing transitions per state and per symbol.
