## 1 Introduction
Firstly, efficiently eliminating all non-minimal invariants is crucial. Secondly, the necessity to consider all possible linear combinations results in a rapid increase in the number of rows in the intermediate data structure, potentially reaching millions before being reduced to a manageable number. Heuristics, such as selecting columns that yield fewer new rows, are employed to mitigate this effect, although they are not universally effective. This algorithm can be straightforwardly adapted for t-invariants either by directly applying it or by transposing the incidence matrix, as p-invariants of the transposed net correspond to t-invariants of the original net. To summarize the above, let us underline crucial problems related to the verification of Petri net-based concurrent systems. The main drawback of such an examination is that it relies on the computational complexity of existing methods. Although such techniques are usually effective (that is, they return proper results), they can be highly inefficient (in terms of computation time), especially in the case of complex systems. This means that the verification process may not be completed within the assumed time. Therefore, in practical applications, this may impact the design process. During the development of control systems, it is often necessary to analyse and refine the specification multiple times before arriving at the final specification. When existing methods require excessive computation time, the iterative design process becomes inefficient or infeasible, which can delay or compromise the system's development. To address these problems, a novel fast verification algorithm is proposed in this paper. The main benefit of the presented method is its polynomial computational complexity, which means that the results can be obtained even for complex concurrent systems. The main contributions of this work are as follows:  
* Proposition of a novel preliminary verification algorithm of Petri net-based concurrent systems. The main advantage of the method is its polynomial computational complexity. * Experimental verification of the efficiency (run-time) and effectiveness (proper results) of the proposed algorithm with a set of 386 Petri net-based concurrent systems (including real-life concurrent systems, cyber-physical systems, and manufacturing systems). * A case study verification example of a real-life Petri net-based concurrent system. In particular, a home area network (HAN) modelled by a Petri net is verified and used to demonstrate the efficiency of the proposed method. * Detailed discussion about the verification techniques of Petri net-based concurrent systems, including detailed analysis of the advantages and limitations of the proposed method. The paper is structured as follows: the introduction provides an overview of the challenges in verifying Petri net-based concurrent control systems and the motivation for the proposed algorithm. The next section presents the application of t-invariants to the verification of Petri net-based concurrent systems and details the proposed algorithm's approach to computing transition invariant coverage and identifying uncovered transitions. The experimental setup section presents the evaluation of the proposition using 386 test benchmarks and compares its performance against the reference method and the PIPE tool. Finally, the conclusion summarizes the findings, highlighting the algorithm's efficiency and practicality in early design stages, and discusses future research directions.