5.6 Complete Experimental Results
5.6.2 Comparisons of Improved Constructions
We also compared the four constructions with one optimization heuristic for Ramsey in Section 5.5 and all optimization heuristics in Sections 5.2, 5.3, and 5.4 based on 7963, 4851, and 2951 effective samples respectively in A10, A15, and A20. Recall that the following heuristics were proposed in this paper: simplifying DPWs by simulation (+S) and merging equivalent states (+E) for SP; maximizing the B¨uchi acceptance set (+A) for Rank; deterministic decoration (+D), reducing transitions (+R), and merging adjacent nodes (+M) for Slice. The heuristic for Ramsey is the simplification of intermediate classic finite automata on finite words (+m). The comparisons are summarized in Table 5.8, which shows that SP+ASE still outperforms the other three in the average state size and in running time. Table 5.8 also shows the following changes made by our heuristics in the comparison: (1) SP+ASE outperforms Rank+A in the number of smallest complements after pruning dead states, and (2) Slice+ADRM creates fewer reachable states than Rank+A in average, and finishes more tasks than Rank+A and Ramsey+Am.
As the heuristic of preminimization applied to the input automata, denoted by +P, is considered to help the nondeterministic constructions more than the deter-ministic one, we also compare the four improved constructions with preminimization and summarize the results in Table 5.9. We only applied the preminimization imple-mented in the GOAL tool, namely the simplification by simulation in [86]. According
Effective
Constructions T M Samples S
R(Win) S
L(Win) S
L/S
RA
10Ramsey+Am 924 3 7,963 461.56 (9.50) 257.21 (1,323.75) 0.56
SP+ASE 0 0 26.96 (7,701.83) 7.42 (3,062.75) 0.28
Rank+A 2,285 0 438.66 (71.83) 23.28 (1,818.75) 0.05
Slice+ADRM 2 0 115.79 (179.83) 12.76 (1,757.75) 0.11
A
15Ramsey+Am 3,119 2 4,851 666.86 (0.0) 251.53 (895.75) 0.38
SP+ASE 13 7 23.88 (4,772.5) 5.77 (1,675.42) 0.24
Rank+A 3,927 0 384.35 (20.0) 11.38 (1,138.42) 0.03
Slice+ADRM 228 0 185.02 (58.5) 9.65 (1,141.42) 0.05
A
20Ramsey+Am 5,009 14 2,951 618.07 (0.00) 125.76 (618.75) 0.20
SP+ASE 83 133 18.81 (2,929.67) 3.81 (894.75) 0.20
Rank+A 4,955 0 427.75 (5.17) 8.41 (717.25) 0.02
Slice+ADRM 1,220 0 213.76 (16.17) 5.96 (720.25) 0.03
Table 5.8: A comparison of the four improved complementation constructions based on A10, A15, and A20
to our experimental results, the preminimization does improve Ramsey, Rank, and Slice more than SP in the complementation but does not close too much the gap between them in the comparison, though there are other preminimization techniques that we did not implement and apply in the experiment.
The comparisons of the four improved constructions based on the nonuniversal automata without and with preminimization are summarized respectively in Ta-ble 5.10 and in TaTa-ble 5.11. These comparisons based on the nonuniversal automata are quite consistent to those based all the automata.
5.7 Summary of this Chapter
We examined the performance of the four complementation approaches by experi-ments with three test sets of 11,000 automata. The experimental results showed that the determinization-based approach performs better than the other three in most cases in terms of time and size of states. This is surprising and goes against the conventional wisdom that the nondeterministic approaches are better. The
Ramsey-Effective
Constructions T M Samples S
R(Win) S
L(Win) S
L/S
RA
10Ramsey+PAm 813 6 8,565 355.43 (53.0) 220.28 (1,453.25) 0.62
SP+PASE 0 0 22.25 (6,032.0) 6.97 (2,794.25) 0.31
Rank+PA 1,765 0 306.92 (1,209.5) 20.54 (2,208.25) 0.07
Slice+PADRM 2 0 89.70 (1,270.5) 11.40 (2,109.25) 0.13
A
15Ramsey+PAm 2,825 6 5,618 479.99 (17.50) 225.08 (1,031.25) 0.47
SP+PASE 12 7 19.47 (3,820.67) 5.89 (1,698.75) 0.30
Rank+PA 3,383 0 232.63 (875.67) 10.68 (1,476.75) 0.05
Slice+PADRM 216 0 135.74 (904.17) 9.12 (1,411.25) 0.07
A
20Ramsey+PAm 4,647 15 3,741 390.30 (16.5) 159.04 (762.75) 0.41
SP+PASE 102 110 13.51 (2,335.0) 4.49 (1,059.42) 0.33
Rank+PA 4,422 0 208.18 (685.0) 7.76 (964.92) 0.04
Slice+PADRM 1,180 0 133.69 (704.5) 6.66 (953.92) 0.05
Table 5.9: A comparison of the four improved complementation constructions based on A10, A15, and A20 with preminimization
based approach is not competitive in complementation though it is competitive in universality and containment testing.
We also proposed various optimization heuristics for three of the approaches and performed an experiment with one of the test sets to show the improvement.
The experimental results also showed that our heuristics substantially improve SP and Slice in creating far fewer states. Rank and especially Slice can finish more complementation tasks with our heuristics.
Effective
Constructions Samples S
R(Win) S
L(Win) S
L/S
RA
10Ramsey+Am 2,672 944.62 (1) 764.56 (1) 0.809
SP+ASE 41.65 (2,428.17) 20.14 (1,740) 0.484
Rank+A 356.82 (67.67) 67.39 (496) 0.189
Slice+ADRM 116.78 (175.17) 36.05 (435) 0.309
A
15Ramsey+Am 1,270 1,310.06 (0.0) 957.96 (0.50) 0.731
SP+ASE 39.90 (1191.5) 19.21 (780.17) 0.482
Rank+A 314.22 (20.0) 40.64 (243.17) 0.129
Slice+ADRM 186.90 (58.5) 34.04 (246.17) 0.182
A
20Ramsey+Am 478 1,117.59 (0.00) 772.57 (0) 0.691
SP+ASE 35.62 (456.67) 18.35 (277) 0.515
Rank+A 350.93 (5.17) 46.74 (99) 0.133
Slice+ADRM 219.55 (16.17) 31.59 (102) 0.144
Table 5.10: A comparison of the four improved complementation constructions based on the nonuniversal automata in A10, A15, and A20
Effective
Constructions Samples S
R(Win) S
L(Win) S
L/S
RA
10Ramsey+PAm 2,752 845.03 (1.5) 682.96 (0.5) 0.808 SP+PASE 39.54 (2,096.5) 19.57 (1,341.5) 0.495
Rank+PA 305.25 (294.5) 61.78 (755.5) 0.202
Slice+PADRM 107.76 (361.5) 33.35 (656.5) 0.309
A
15Ramsey+PAm 1,495 1,125.22 (1.0) 843.07 (0.5) 0.749
SP+PASE 38.71 (1110.5) 19.39 (668.0) 0.501
Rank+PA 260.28 (177.0) 37.39 (446.0) 0.144
Slice+PADRM 163.29 (206.5) 31.47 (380.5) 0.193
A
20Ramsey+PAm 692 1,084.23 (0.00) 856.38 (0.00) 0.790 SP+PASE 33.57 (478.33) 19.86 (297.67) 0.592 Rank+PA 224.91 (97.33) 37.55 (202.67) 0.167 Slice+PADRM 165.83 (116.33) 31.61 (191.67) 0.191
Table 5.11: A comparison of the four improved complementation constructions based on the nonuniversal automata in A10, A15, and A20 with preminimization
Chapter 6
Containment Testing Algorithms
In this chapter, we propose an incremental containment testing approach based on the determinization-based complementation constructions, namely Safra’s construc-tion [77], Muller-Schupp construcconstruc-tion [70, 4], and Safra-Piterman construcconstruc-tion [74].
We will focus on how to apply Safra-Piterman construction in incremental contain-ment testing. The other two approaches can be applied in the same way. In the following, we first briefly describe Safra-Piterman construction, then present how to apply the construction in incremental universality testing (a special case of con-tainment testing), and finally describe the extension to incremental concon-tainment testing.
6.1 Safra-Piterman Construction
Safra-Piterman construction performs a subset construction with a tree structure, called compact Safra trees, to capture all runs of a B¨uchi automaton on a word.
Each node in a compact Safra tree is labeled by a set of states of the automaton. A compact Safra tree satisfies the following two properties:
• If node n is a child of node m, then n ⊂ m.
• If node n is a sibling of m, then n ∩ m = ∅.
Although the evolution of compact Safra trees are complicated and there are sev-eral annotations associated to compact Safra trees, we can abstract these evolution process and annotations into two functions, namely the transition function and the coloring function. Let A = (Σ, Q, q0, δ, F ) be a B¨uchi automaton where Σ is a finite alphabet, Q a finite set of states, q0 the initial state, δ : Q × Σ → 2Q a transi-tion functransi-tion, and F ⊂ Q a B¨uchi acceptance condition. Let TA denote the set of compact Safra trees over the states of A. The transition function is defined as δTA: T × Σ → TAwhile the coloring function is defined as ρA: TA× N. We may omit the superscript A if it is clear in the context. Based on Safra-Piterman construction in [74], we have the following lemma.
Lemma 6.1.1. Let A = (Σ, Q, q0, δ, F ) be a B¨uchi automaton and P = (Σ, S, s0, ∆, G) a deterministic parity automaton defined as the following:
• S = T .
• s0 is a tree with the only root node {q0}.
• ∆ = δT.
• G = ρ.
Then, L(P ) = L(A).
Although the conventional wisdom is that the determinization-based comple-mentation constructions have to be performed stage by stage with deterministic automata as the intermediate results, we point out that these constructions in fact can be performed incrementally. We first show how to perform the determiniza-tion construcdeterminiza-tions incrementally. Let f be a funcdeterminiza-tion, we define the update of f as
f [k ⇒ v]:
f [k ⇒ v](x) = v if x = k f(x) if x 6= k
The incremental Safra-Piterman determinization construction is shown in Algo-rithm 7.
5:
Remove an element s from U6:
for a ∈ Σ do L(A) = Σω, or in other words, L(A) = ∅. To perform the universality testing incre-mentally based on Safra-Piterman construction, we have to construct complement automata on the fly. The incremental Safra-Piterman determinization construction has been shown in the previous section. The rest is to show how to construct a complement deterministic parity automaton and convert it to an equivalent B¨uchi automaton incrementally.To construct a complement deterministic parity automaton incrementally, we simply follow the incremental Safra-Piterman construction but increment the color of every state by 1. This is achieved by defining another function ρ0 : T × N such that ρ0(t) = ρ(t) + 1.