# Modeling a New AQM Model for Internet Chaotic Behavior Using Petri Nets
## 5 Validation
### Invariance Analysis  
Next, we introduce the invariance analysis of our model. Invariants look for properties that remain constant with respect to certain patterns of executing the PN. Furthermore, invariants are used later to prove the properties of our AQM, such as reversibility and boundedness. We use the two most widely studied classes of invariants for the PN [28]. First, a natural solution of the equation \(\mathrm{C}\cdot x=0\) is called a transition invariant (T-invariant). It indicates a sequence of transitions (firing vector \(x\) with one entry for each transition), which leads back to the initial marking \(M_{0}\). Table 2 shows the T-invariants for our AQM. They are the different firing vectors that return to the initial state for the next incoming packet at the router. Figure 3 shows each T-invariant, with the transition flow colored in purple. Second, a natural solution of the equation \(y\cdot C=0\) is called a place invariant (P-invariant). A P-invariant is a vector with one entry for each place. It indicates that the number of tokens in all reachable places satisfies some linear invariant. Once a P-invariant called \(y\) is calculated, the following holds for every reachable state \(M:y\cdot M_{0}=y\cdot M\). P-invariants are more difficult to detect than T-invariants. This is because the former are involved with the entire space state and all possible executions directions of the system (AQM in our case). Table 3 shows the P-invariants of our AQM for any reachable place \(M\) represented at the reachability tree of Figure 2. \begin{table}
\begin{tabular}{c c c} \hline \hline
**T-Invariant** & **Content** & **Description** \\ \hline
1T-inv & (1,1,1,0,0,1,0,0,0,0,0,1) & Accept packet, AQL below min. threshold \\
2T-inv & (1,1,0,0,1,0,1,0,0,0,0,0) & Drop packet, AQL over max. threshold \\
3T-inv & (1,1,0,1,0,0,0,1,0,1,0,1) & Accept packet, AQM probability function \\
4T-inv & (1,1,0,1,0,0,0,0,1,0,1,0) & Reject packet, AQM probability function \\ \hline \hline \end{tabular}
\end{table} 
Table 2: T-invariants in our AQM. Figure 2: Reachability tree of our AQM. For any reachable place \(M\), the vector \(y\) (1,1,0,0,0,0,0,0,0) of the 1P-inv is a natural solution of the equation \(y\cdot C=0\) and it holds the linear invariant \(y_{\text{p1}}\cdot M_{0}+y_{\text{p2}}\cdot M_{0}=y_{\text{p1}}\cdot M+y_{\text{p2 }}\cdot M=1\), where \(y_{\text{pj}}\) =(0,...,0,1,0,....0) and 1 is located in the \(j\) position. That is, the token can be only in one of the places \(y_{\text{p1}}\) or \(y_{\text{p2}}\). This P-invariant (1P-inv) indicates a similarity with the mutual exclusion behavior in our AQM. Initially, P1 holds a token, and, once transition T1 is fired, the token moves to place P2. Next, transition T2 is fired, and P1 holds the token at the same time that our AQM continues processing the packet through place P3. Figure 4 shows how the token can be in places P1 or P2 but never in both in any reachable marking place, i.e., the router is ready for a new packet once the current one has passed to AQM. \begin{table}
\begin{tabular}{c c c} \hline \hline
**P-Invariant** & **Content** & **Description** \\ \hline
1P-inv & (1,1,0,0,0,0,0,0,0,0) & Router ready, received packet \\
2P-inv & (0,1,1,1,1,1,1,1,1,1) & AQM in process, received packet \\ \hline \hline \end{tabular}
\end{table} 
Table 3: P-invariants in our AQM. Figure 3: T-invariants of our AQM. Additionally, we studied the P-invariant 2P-inv. For any reachable place M, the vector \(y\) (0,1,1,1,1,1,1,1,1,1) of the 2P-inv is a natural solution of the equation \(y\cdot\mathrm{C}=0\) and it holds the linear invariant \(y_{p2}\): \(M_{0}+y_{p3}\cdot M_{0}+y_{p4}\cdot M_{0}+y_{p5}\cdot M_{0}+y_{p6}\cdot M_{0}+y_ {p7}\cdot M_{0}+y_{p8}\cdot M_{0}+y_{p9}\cdot M_{0}+y_{p10}M_{0}=y_{p2}\cdot M+y_ {p3}\cdot M+y_{p4}\cdot M+y_{p5}\cdot M+y_{p6}\cdot M+y_{p7}\cdot M+y_{p8}\cdot M +y_{p9}\cdot M+y_{p10}\cdot M=1\).