## 2 Application of T-Invariants to the Verification of Petri Net-Based Concurrent Systems
### The Proposed Algorithm for Computation of Uncovered Transitions in a Petri Net-Based System  
Let us introduce a novel algorithm for computation of uncovered transitions in a Petri net-based concurrent system. The main advantage of the method is its computational complexity, while the results are computed in cubic polynomial time, which we prove later (in Section 2.4).  
Algorithm 1 shows the idea of the proposed method. It is assumed that, as the input, an incidence matrix of a Petri net-based concurrent system is provided, and the algorithm results in a set of detected uncovered transitions.  
From the general point of view, the algorithm consists of two main stages. The first one (lines 6-15) involves transformation of the incidence matrix into the reduced row echelon form (RREF). This operation is performed by basic algebraic transformations, such as multiplication, division, and subtraction. After obtaining the reduced matrix, the algorithm identifies uncovered transitions in the Petri net (lines 16-25). This process is executed in a completely different manner from existing solutions. Instead of searching for the coverage of t-invariants, the algorithm searches for the transitions that cannot form a proper t-invariant. According to Definition 7, an invariant corresponds to a vector that fulfils the equation \(A\overrightarrow{y}=\overrightarrow{0}\). The proposed technique searches for transitions that violate this condition. In particular, the method examines rows (places) holding nonnegative values in order to detect columns (transitions) that contains only nonnegative entries. If there exists such a transition (or transitions), it cannot form a proper t-invariant, since there is no entry that annuls its positive value. Hence, equation \(A^{\overrightarrow{i}}\overrightarrow{y}=\overrightarrow{0}\) cannot be fulfilled for this particular transition. In order to improve the functionality and run-time, additional properties of the RREF are also taken into account (e.g., _leading one_, etc.).  
```
1:Input: incidence matrix of concurrent system specified by a Petri net \(N=(P,T,F,M_{0})\)
2:Output: the set of uncovered transitions in a Petri net-based concurrent system //initialization:
3:read incidence matrix \(\boldsymbol{A}_{|T|\times|P|}\) of \(N\);
4:set uncoveredTransitions = \(\mathcal{O}_{7}\)//transposition of the incidence matrix:
5:transpose \(\boldsymbol{A}_{|T|\times|P|}\) into \(\boldsymbol{A}_{|P|\times|T|}\); //transformation of the matrix \(\boldsymbol{A}_{|P|\times|T|}\) into RREF \(\boldsymbol{A}_{|R|\times|T|}\):
6:foreachrow \(i\) in \(P\):
7:findrow \(j\) in \(P\) such that it contains the leftmost non-zero entry \(e\);
8:swap rows \(i\) and \(j\);
9:divide row \(i\) by \(e\);
10:foreachrow \(k\) in \(P-\{i\}\):
11:foreachcolumn \(l\) in \(T\):
12:set \(j=j-k*A[i][l]\);
13:endfor
14:endfor
15:endfor //computation of uncovered transitions within the matrix \(\boldsymbol{A}_{|R|\times|T|}\):
16:foreachrow \(i\) in \(R\) [such that \(i\) contains only nonnegative entries];
17:set \(e=[\)the first non-zero entry of for each row \(i\)];
18:foreachcolumn \(k\) in \(T\) [such that \(k\) is equal to or greater than \(e\)]:
19:set \(u=true\);
20:foreachrow \(j\) in \(R\):
21:if\(A[j][k]<0\)then\(u=false\);
22:endfor
23:if\(u=true\)then uncoveredTransitions = uncoveredTransitions \(\cup\{k\}\);
24:endfor
25:endfor //print and return results:
26:if uncoveredTransitions \(\
eq\emptyset\)then
27:print \"Uncovered transitions found in the system.\";
28:return uncoveredTransitions
29:else
30:print \"No uncovered transitions found in the system.\";
31:return\(\varnothing\) [empty set]
32:endif
```  
**Algorithm 1**Computation of uncovered transitions in a Petri net-based concurrent system.