## 5 Conclusions and Discussion About Advantages and Limitations of the Proposed Method  
This section summarizes the paper by exposing the main advantages but also limitations of the proposed algorithm. Moreover, plans are presented and briefly discussed. In this work, a novel fast verification algorithm for Petri net-based concurrent systems is proposed. The technique is based on the analysis of the system by searching for transitions that are not covered by t-invariants. Such uncovered transitions usually refer to critical issues in the system, such as deadlocks, lack of liveness, or unboundedness. The existing methods may be inefficient due to exponential computational complexity. This means that the Petri net-based concurrent system can be examined for an exceptionally long time, or never even properly verified (the results are not obtained within the assumed time). The main advantage of the proposed technique definitely relates to the polynomial computational complexity. As is shown in Section 2.4, the run-time of the algorithm is cubic polynomial \(O(|P|^{2}|T|)\), where \(|P|\) denotes the number of places and \(|T|\) denotes the number of transitions in the system. Furthermore, the experimental setup confirmed the high efficiency and effectiveness of the proposed algorithm. The method is able to compute the results for all tested cases. In contrast, the reference Martinez-Silva algorithm, as well as the PIPE tool could not obtain the results for all benchmarks. Furthermore, the results of the experiments indicated that for only two benchmarks the proposed method did not find the proper solution (we will discuss this later in detail). This means that the proposed algorithm computed the correct results for 384 tested cases. What is important is that the method clearly points out the possible incorrect transitions in the system. This is extremely important for the designers since they can immediately check their systems without additional time-consuming analysis and verification. Finally, let us underline that the verification of uncovered transitions performed using the proposed method permits the detection of errors in a system which is bounded, safe, and even deadlock-free. The presented case study example indicates that there exist systems for which techniques or tools (e.g., PIPE) do not show any errors in the system, although particular transitions and places are not reachable. Such a situation may be crucial from the functional point of view, since required operations (such as turning off demand of high energy, or even more crucial operations, like turning on an alarm system) are never executed. Besides the above listed benefits, the presented technique also has certain limitations. The first relates to the improper results of the analysis. Since the technique is based on linear algebra, it analyses the pure structure of the system (e.g., without taking the initial state into account). Moreover, the method searches for uncovered transitions in the system by examination of the transformed incidence matrix (c.f. Section 2.3) and identifies rows containing only a leading one. A leading one in a row indicates that the corresponding transition (linked to the column) cannot be covered by any t-invariant, as \(t_{i}=0\). Once the algorithm finishes computation, it provides a list of transitions that are definitively uncovered. This means that in some cases not all uncovered transitions may be detected. Indeed, the results of the experiments show that there are two benchmarks (out of 386) where the proposed method could not find all the uncovered transitions. On the other hand, such tests (-0.5%) seem to be extremely few, since the vast majority of the benchmarks analysed identified all the uncovered transitions. It is also important to emphasize that our method is not intended to replace exact analysis but to serve as a tool for the initial verification of Petri net models. This approach is particularly beneficial during the early stages of system design, where quick feedback is essential for iterative refinement.