Information Technology Reference
In-Depth Information
Tabl e 1.
Number for each type (universal, right-universal, null
rel
h
, timeout) among 90
instances, with a timeout of 300s, and various number of states and transition densities.
Average (preprocessing/online) time is given in parentheses (in s).
|Q|
universality
right-universality
null
rel
h
tr. density: 8 tr. density: 16 8 16 8 16 8 16 8 16
10 12 (0.59/0.01) 40 (1.19/0.01) 22 (16.62/9.36) 44 (11.00/1.10) 52 (0.67/0.01) 0 2 2 2 4
20 13 (9.35/0.01) 29 (0.86/0.01) 14 (20.44/30.85) 41 (5.18/1.07) 46 (9.62/0.01) 0 14 17 3 3
30 9 (20.22/0.01) 34 (13.39/0.01) 11 (21.23/5.85) 34 (27.31/3.43) 40 (1.23/0.01) 0 30 21 0 1
Tabl e 2.
Time and data structures size on random VPAs, with transition density of
16,
|Q|
= 20,
|Σ|
=
|Γ|∈{
2
,
3
,
4
}
, and timeout of 300s
VPA id
Response
Time (s.)
|H| |Reach
(
u
)
| |Safe
(
u
)
|
q20-a02-x02-o16-c16-f0.5-00 right-universal w.r.t.
a
1
0.03
3
4
33
q20-a02-x04-o16-c16-f0.5-02 right-universal w.r.t.
a
1
0.07
3
8
53
q20-a02-x04-o16-c16-f0.5-06 right-universal w.r.t.
a
0
0.06
3
5
54
q20-a03-x02-o16-c16-f0.5-06 right-universal w.r.t.
a
2
0.13
12
4
32
q20-a03-x03-o16-c16-f0.5-06 right-universal w.r.t.
a
0
0.37
23
4
59
q20-a03-x03-o16-c16-f0.5-09 right-universal w.r.t.
a
2
a
0
1.74
13
14
179
q20-a03-x04-o16-c16-f0.5-07 right-universal w.r.t.
a
2
1.02
44
5
116
q20-a04-x02-o16-c16-f0.5-03 right-universal w.r.t.
a
3
0.71
71
5
75
q20-a04-x02-o16-c16-f0.5-07 right-universal w.r.t.
a
0
1.07
81
5
74
q20-a04-x03-o16-c16-f0.5-03 right-universal w.r.t.
a
2
15.88
359
5
447
16) and fixed density 0
.
5 of final states
6
. The considered tree
t
0
is a complete
binary tree up to height 3 filled with randomly generated letters of
Σ
.Weonly
comment the experiment using a SAT solver since it outperforms the approach
with operator
. We observe several behaviors (see Table 1): many automata are
either universal, or right-universal w.r.t.
u
with
|
u
|
= 1 (except 7 cases where
= 2), or exhibits a hedge
h
with
rel
h
being the null relation
7
;thenumberof
timeout increases with
|
u
|
. Table 2 indicates, for some representative VPAs, the
execution time and the sizes of
|
Q
|
.
When it declares that a given VPA is right-universal w.r.t.
u
, our algorithm has
the nice property that it reproduces the
same execution
(thus with the same time)
foreachtree
t
0
suchthat
u
isprefixof[
t
0
].Thisisclearlynotthecaseforthe
member-
ship algorithm
that computes
Reach
([
t
0
]) and checksif it containsa final configura-
tion.Forinstance,onarandomVPAwithsize
H
,
Reach
(
u
)and
Safe
(
u
)
= 20andtransitiondensity8,our
algorithm consumes less than 5s to declare that the automaton is right-universal
w.r.t.
a
, whereas the membership algorithm takes more than 300s as soon as the
height of a binary tree
t
0
with an
a
-root is equal to 8.
|
Q
|
6
To deal with managable and not too small sets
H
.
7
This means that the automaton is never right-universal w.r.t.
u
, for any proper
prefix
u
of [
t
0
]. Therefore, in such cases, our algorithm is slower that the membership
algorithm.
