Experimental results on QBF-based refinement checking

over modal transition systems and their disjunctive, Boolean and parametric extensions

The table below lists the experiments conducted on the PMTS refinement checker. Columns correspond to the size of the systems to checked, rows to the types of the systems. "Alphabet n" denotes the size of the alphabet is n. Similarly, "Degree n" denotes the branching degree of the systems is n. We always generate 10 pairs of systems. "Global" systems are those with edges added randomly to form a tree and then random edges making the branching degree constant over the nodes. "Local systems" are systems consiting of five clusters each of which has the same characteristics as global systems. Each cluster has moreover 3 "interface" nodes each of which connects to other interface nodes with branching degree n/3 where n is the systems branching degree. The average running times as well as standard deviations (in parentheses) are in milliseconds.

Alphabet 2















Degree: 2















Local


















25
50
75
100
125
150
175
200
MTS
0 (±0) 0.01 (±0) 0.01 (±0.01) 0.02 (±0.01) 0.03 (±0.01) 0.03 (±0.02) 0.05 (±0.03) 0.07 (±0.01)
DMTS
0 (±0) 0.01 (±0) 0.02 (±0) 0.03 (±0) 0.04 (±0) 0.03 (±0.03) 0.04 (±0.05) 0.08 (±0.07)
BMTS
0 (±0) 0.01 (±0.01) 0.01 (±0.01) 0.01 (±0.01) 0.03 (±0.01) 0.04 (±0.02) 0.06 (±0.01) 0.08 (±0.01)
PMTS (1) 0 (±0) 0.01 (±0) 0.01 (±0.01) 0.02 (±0.01) 0.03 (±0.02) 0.05 (±0.01) 0.09 (±0.02) 0.09 (±0.05)
PMTS (2) 0 (±0) 0.01 (±0) 0.02 (±0) 0.03 (±0) 0.04 (±0.02) 0.07 (±0.01) 0.07 (±0.04) 0.15 (±0.03)
PMTS (5) 0.01 (±0) 0 (±0) 0.02 (±0.01) 0.02 (±0.02) 0.04 (±0.02) 0.08 (±0.02) 0.08 (±0.05) 0.07 (±0.09)
PMTS (10) 0 (±0) 0.01 (±0) 0.01 (±0.01) 0.02 (±0.02) 0.04 (±0.02) 0.04 (±0.04) 0.09 (±0.05) 0.14 (±0.01)


















Global


















25
50
75
100
125
150
175
200
MTS
0.03 (±0.01) 0.15 (±0.01) 0.29 (±0.16) 0.86 (±0.38) 0.87 (±0.49) 0.96 (±0.88) 1.88 (±1.06) 2.48 (±1.43)
DMTS
0.04 (±0.02) 0.22 (±0.05) 0.39 (±0.21) 0.91 (±0.14) 1.13 (±0.64) 1.34 (±1.24) 2.61 (±1.49) 3.19 (±1.81)
BMTS
0.03 (±0.01) 0.15 (±0.02) 0.3 (±0.17) 0.62 (±0.13) 0.83 (±0.48) 0.87 (±0.8) 1.61 (±0.91) 2.17 (±1.25)
PMTS (1) 0.03 (±0.02) 0.2 (±0.02) 0.37 (±0.21) 0.84 (±0.12) 0.97 (±0.55) 1.23 (±1.13) 2.44 (±1.41) 3.15 (±1.83)
PMTS (2) 0.04 (±0.02) 0.26 (±0.16) 0.38 (±0.22) 0.89 (±0.08) 1.2 (±0.68) 1.44 (±1.32) 2.88 (±1.7) 3.86 (±2.37)
PMTS (5) 0.04 (±0.02) 0.22 (±0.04) 0.42 (±0.24) 0.91 (±0.16) 1.26 (±0.72) 1.59 (±1.45) 2.83 (±1.6) 3.66 (±2.1)
PMTS (10) 0.04 (±0.02) 0.23 (±0.06) 0.47 (±0.27) 0.98 (±0.16) 1.25 (±0.71) 1.5 (±1.37) 3.61 (±2.41) 4.09 (±2.31)


















Alphabet 2















Degree: 5















Local


















25
50
75
100
125
150
175
200
MTS
0.01 (±0) 0.03 (±0.01) 0.07 (±0.01) 0.13 (±0.02) 0.23 (±0.03) 0.35 (±0.04) 0.45 (±0.06) 0.6 (±0.05)
DMTS
0.02 (±0) 0.07 (±0.02) 0.2 (±0.01) 0.33 (±0.02) 0.56 (±0.13) 0.67 (±0.09) 1.03 (±0.17) 1.42 (±0.36)
BMTS
0.02 (±0) 0.05 (±0.01) 0.18 (±0.13) 0.21 (±0.03) 0.32 (±0.15) 0.55 (±0.11) 0.61 (±0.13) 0.82 (±0.21)
PMTS (1) 0.05 (±0.02) 0.14 (±0.06) 0.18 (±0.16) 0.3 (±0.1) 3.4 (±4.19) 0.73 (±0.37) 0.85 (±0.47) 0.96 (±0.67)
PMTS (2) 0.02 (±0.01) 0.13 (±0.07) 0.19 (±0.1) 0.19 (±0.06) 1.61 (±1.6) 4.63 (±7.68) 1.03 (±0.28) *2.3 (±1.04)
PMTS (5) 0.02 (±0.01) 0.04 (±0.01) 0.23 (±0.25) 0.7 (±0.87) 0.58 (±0.3) 0.39 (±0.16) 1.13 (±0.66) *2.35 (±1.15)
PMTS (10) 0.02 (±0.01) 0.1 (±0.07) 0.16 (±0.1) *0.16 (±0.09) *0.29 (±0.15) 1.55 (±2.64) 0.97 (±1.04) 1.13 (±0.62)


















Global


















25
50
75
100
125
150
175
200
MTS
0.163 (+/-5) 1.006 (+/-149) 2.358 (+/-414) 5.036 (+/-700)







DMTS
0.268 (+/-9) 1.374 (+/-37) 3.622 (+/-28) 7.067 (+/-372)







BMTS
0.275 (+/-10) 1.091 (+/-15) 2.789 (+/-62) 3.07 (+/-632)







PMTS
0.827 (+/-19) 3.371 (+/-192) 2.752 (+/-28) 10.416 (+/-483)







PMTS (1) 0.34 (±0.14) 2.04 (±0.7) 5.38 (±2.63) 8.81 (±4.62) 11.78 (±5.95) 17.41 (±11.93) 27.33 (±16.87) 58.06 (±1.86)
PMTS (2) 1.44 (±2.57) 7.07 (±10.03) *3.76 (±1.83) 9.52 (±3.91) 17.76 (±6.22) 22.8 (±12.75) 34.42 (±12.94) 83.38 (±26.08)
PMTS (5) 0.29 (±0.14) 1.83 (±1.32) *5.19 (±2.22) 12.79 (±2.41) 15.71 (±9.33) 26.6 (±10.19) *35.3 (±18.11) 89.25 (±15.17)
PMTS (10) *0.43 (±0.14) 1.36 (±0.62) 6.7 (±2.29) 13.66 (±5.15) *18.27 (±9.92) *21.1 (±6.03) 51.67 (±15.67) 232.83 (±44.13)




































Alphabet 5















Degree: 10















Local


















25
50
75
100
125
150




MTS
0.43 (±0.35) 1.25 (±0.25) 3.24 (±0.29) 5.5 (±0.72) 9.89 (±3.27) 14.39 (±3.28)



DMTS
0.65 (±0.47) 2.16 (±0.52) 5.86 (±4.03) 8.03 (±3.32) 11.61 (±5.23) 16.25 (±4.86)



BMTS
0.42 (±0.18) 1.56 (±0.28) 3.2 (±0.3) 5.88 (±1.24) 8.15 (±0.84) 12.92 (±2.47)



PMTS (1) 0.4 (±0.19) 2.7 (±2.61) 3.68 (±1.47) 10.49 (±7.45) 8.33 (±1.78) 11.3 (±1.71)



PMTS (2) 1.26 (±0.62) 1.34 (±0.26) 5.79 (±4.35) 5.96 (±1.14) 10.78 (±4.68) 12.66 (±1.87)



PMTS (5) 0.77 (±0.21) 2.06 (±1.02) 4.65 (±3.44) 5.37 (±0.49) 9.37 (±1.84) 11.65 (±1.67)





















Global


















25
50
75
100
125
150




MTS
0.24 (±0.01) 1.17 (±0.06) 3.12 (±0.4) 5.44 (±0.41) 8.11 (±0.83) 11.67 (±1.01)



DMTS
0.53 (±0.21) 3.21 (±0.63) 4.73 (±1.21) 10.75 (±4.6) 18.39 (±10.34) 33.45 (±16.24)



BMTS
0.27 (±0.03) 1.48 (±0.06) 3.89 (±0.49) 6.06 (±1.21) 8.88 (±1.81) 13.75 (±2.96)



PMTS (1) 0.25 (±0.02) 1.49 (±0.08) 3.29 (±0.78) 6.88 (±0.68) 10.07 (±1.23) 15.64 (±1.33)



PMTS (2) 0.26 (±0.05) 1.5 (±0.26) 3.72 (±0.55) 6.84 (±0.74) 8.1 (±0.56) 15.19 (±3.19)



PMTS (5) 0.27 (±0.03) 1.51 (±0.22) 3.58 (±0.67) 6.76 (±0.76) 10.46 (±1.75) 14.88 (±2.28)

























































Alphabet: 10















Degree: 10















Local


















25
50
75
100
125
150
175
200
MTS
0.19 (±0.01) 0.78 (±0.04) 2.03 (±0.12) 3.98 (±0.34) 5.13 (±0.78) 6.75 (±0.61) 10.53 (±3.05) 13.38 (±2.19)
DMTS
0.39 (±0.04) 1.74 (±0.16) 4.24 (±0.35) 7.27 (±0.38) 8.27 (±0.69) 11.63 (±0.82) 13.9 (±0.8) 77.5 (±8.57)
BMTS
0.21 (±0.02) 1 (±0.06) 2.58 (±0.28) 4.38 (±0.58) 6.22 (±0.72) 8.47 (±0.79) 12.33 (±3.02) 16.43 (±2.49)
PMTS (1) 0.21 (±0.02) 1.01 (±0.13) 2.65 (±0.29) 4.85 (±0.46) 6.15 (±0.75) 8.98 (±1.3) 11.39 (±1.16) 16.08 (±5.07)
PMTS (2) 0.23 (±0.04) 1.03 (±0.24) 2.6 (±0.28) 4.95 (±0.72) 6.38 (±1.43) 8.72 (±0.49) 11.04 (±2.98) 36.5 (±17.57)
PMTS (5) 0.27 (±0.04) 1.13 (±0.14) 2.88 (±0.3) 4.84 (±0.41) 6.4 (±1.12) 9.30 (±0.93) 10.9 (±0.73) 49.88 (±3.95)


















Global


















25
50
75
100
125
150
175
200
MTS
0.18 (±0.01) 0.84 (±0.07) 2.12 (±0.09) 3.88 (±0.48) 5.63 (±0.72) 7.64 (±0.76) 10.3 (±3.58) 14.18 (±3.26)
DMTS
0.44 (±0.06) 2.23 (±0.14) 5.31 (±0.39) 8.59 (±0.49) 10.13 (±0.78) 14.14 (±1.08) 13.96 (±2.62) 66.92 (±7.96)
BMTS
0.21 (±0.02) 1.08 (±0.08) 2.65 (±0.29) 4.58 (±0.4) 6.7 (±1.23) 9.63 (±1.86) 12.44 (±3.6) 17.06 (±4.93)
PMTS (1) 0.26 (±0.05) 1.12 (±0.12) 2.74 (±0.18) 4.57 (±0.54) 7.58 (±0.66) 10.31 (±1.5) 11.26 (±1.91) 16.41 (±2.64)
PMTS (2) 0.28 (±0.02) 1.12 (±0.08) 2.92 (±0.3) 5.6 (±0.5) 7.87 (±0.48) 10.14 (±1.83) 11.45 (±1.83) 22.81 (±16.9)
PMTS (5) 0.25 (±0.06) 1.17 (±0.15) 2.94 (±0.41) 6.36 (±1.35) 7.8 (±1.03) 10.01 (±1.63) 11.9 (±1.65) 36.51 (±19.99)