## 3 Experimental Verification
In particular, the Martinez-Silva algorithm was not able to obtain results for 7 benchmarks (1.81% of all tested cases), while the PIPE tool failed to compute results for 47 Petri net-based systems (12.17% of all tested cases). This is an effect of the exponential complexity of those techniques. Moving on to the effectiveness analysis, the proposed method returned all uncovered transitions for 384 benchmarks (99.84% of all tested concurrent systems). This means that for only for two benchmarks (\(\sim\)0.5%) the algorithm could not find errors in the analysed system. This is an extremely high (and even surprising) value, since the aim of the method was preliminary verification, and it was expected that the proposed method would not be so accurate. Let us now analyse the selected representative benchmarks in more detail. It can be seen that for relatively small Petri nets (such as _bause1_) which consists of eleven places and eleven transitions, the run-time of the proposed analysis algorithm is even more than eight times longer than Martinez-Silva method. Nevertheless, let us underline that here we are \begin{table}
\begin{tabular}{c c c c c c c c} \hline \hline
**Benchmark** & **Places** & **Transitions** & \begin{tabular}{c} **Reference Method** \\ **Result** \\ \end{tabular} & \
\begin{tabular}{c} **PIPE Tool** \\ **Result** \\ \end{tabular} &
\begin{tabular}{c} **Proposed Method** \\ **Time [ms]** \\ \end{tabular} \\ \hline SHA\_decoder & 200 & 170 & true & 10.06 & true & 65,385 & true & 150.35 \\ cn\_crr25 & 200 & 51 & true & 1.42 & true & 34.00 & true & 16.00 \\ photovoltaics\_single\_module & 139 & 162 & n/a & timeout & n/a & timeout & true & 69.06 \\ manufacturing\_AM\_deadlock & 75 & 73 & false & 854.1 & false & 29,131 & false & 11.97 \\ decision\_making\_system\_v2 & 75 & 73 & false & 899.8 & false & 9697 & false & 12.21 \\ lnet\_p8n1 & 51 & 40 & false & 0.53 & n/a & timeout & false & 5.59 \\ RSA\_v1 & 49 & 58 & n/a & timeout & n/a & timeout & true & 5.79 \\ RSA\_v2 & 49 & 58 & true & 22.05 & n/a & timeout & true & 6.34 \\ effectiveness\_AM\_v2\_unsafe & 48 & 52 & n/a & timeout & n/a & timeout & false & 5.64 \\ state\_space48 & 48 & 48 & true & 0.67 & true & 3282 & true & 3.20 \\ zuberek5 & 41 & 31 & true & 0.80 & true & 2.00 & true & 2.12 \\ five\_food\_preparation\_lines & 37 & 33 & true & 0.38 & true & 1153 & true & 2.48 \\ crossroadSM\_FPGA & 32 & 12 & true & 0.12 & n/a & timeout & true & 0.50 \\ airplane\_flight\_procedure & 28 & 17 & n/a & timeout & n/a & timeout & true & 0.80 \\ HAN & 24 & 40 & true & 255,822 & n/a & timeout & true & 1.26 \\ two\_lanes\_long & 21 & 40 & n/a & timeout & n/a & timeout & true & 1.93 \\
66\_greenhouse\_automation & 17 & 22 & true & 8.36 & true & 859.00 & true & 0.70 \\ automation3 & 17 & 16 & false & 0.206 & false & 277.000 & true & 0.831 \\ bause1 & 11 & 11 & false & 0.10 & false & 134.00 & false & 0.87 \\ esparza1 & 11 & 10 & false & 0.064 & false & 261.000 & true & 0.397 \\ credit\_procedure & 10 & 8 & false & 0.16 & false & 93.00 & false & 0.90 \\ bridge & 8 & 6 & true & 0.03 & true & 309.00 & true & 0.23 \\
47\_two\_vehicles & 7 & 6 & true & 0.03 & true & 406.00 & true & 0.24 \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Sample of experimental research. dealing with fractions of milliseconds. A comparable situation can be found in the case of benchmarks with a dozen or so places and transitions, e.g., _bridge_, _credit_procedure_, and _47_two_vehicles_. For those benchmarks, the reference algorithm is slightly faster compared to the reference method and PIPE tool. Remarkably interesting results can be seen for systems that contain two hundred places (_SHA_decoder_, _cn_crr25_). Although those systems are relatively huge, both the Martinez-Silva algorithm and PIPE tool are faster than the proposed method. This can be explained due to the low level of complexity of such systems, and thus the small number of transition invariants. However, the efficiency of the analysed algorithms changes in the case of more complex systems.