This paper introduces a novel algorithm for the efficient verification of a Petri net-based concurrent control system. The proposed method is based on the computation of transition invariant coverage to detect possible errors in the modelled system. Transition invariants play a crucial role in ensuring the correctness and reliability of such systems; however, existing methods often struggle with high computational demand, especially in the case of large and complex systems. The proposed approach addresses this challenge by performing a fast polynomial-time analysis to identify uncovered transitions, thereby streamlining the verification process. The effectiveness and efficiency of the proposed technique is verified experimentally with a set of 386 test modules (benchmarks) and compared against two well-known established methods: the classical method proposed by Martínez–Silva (as a reference algorithm) and PIPE (Platform Independent Petri Net Editor) tool. The results of the experiments confirm high performance of the presented algorithm, which was able to compute results for all the tested cases. In contrast, both the reference algorithm as well as the PIPE tool failed to deliver results for all examined models within one hour. The proposed algorithm is especially useful in early design stages, offering system designers timely insights into potential issues.

Verifying a Petri net-based concurrent system is essential, since errors such as unbounded resource accumulation or deadlocks are costly after deployment. Invariant coverage is a diagnostic, but computing a minimal invariant basis can have exponential worst-case cost. Coverage can also be decided by linear-feasibility methods without basis enumeration, although diagnosis may require feasibility checks for places or transitions and an external optimization solver. This paper introduces Fast Verification Plus (FV+): two algorithms that use the reduced row echelon form of a Petri net incidence matrix to detect uncovered places and transitions in polynomial time. FV+ is sound: every reported element is genuinely uncovered. Its incompleteness is characterized. Evaluation on 386 Hippo repository models, against the Martínez-Silva algorithm, PIPE2, and GreatSPN, showed zero false positives among 752 P- and T-invariant coverage analyses. Although incomplete in general, FV+ achieved 100% agreement with coverage decisions on those analyses. This corpus level agreement does not establish completeness. It also returned results on models where other methods timed out. FV+ is thus a fast, solver-free structural filter that complements invariant-basis and LP-based coverage analysis.