RREF-Based, Sound Detection of Invariant-Coverage Violations in Petri Net-Based Concurrent Systems

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.