# Modeling a New AQM Model for Internet Chaotic Behavior Using Petri Nets
## 4 Formal Description of Our Dynamical Model Using Petri Nets  
In this section, we present a formal description of our dynamical model of AQM using PNs. The precise nature of the PN graphical representation facilitates the understanding of the behavior of our AQM scheme represented in Figure 1.  
To begin with, we introduce the fundamentals of PNs that are used for the formal specification of our AQM. Once the specification is introduced, PN theory and its analysis techniques based on algebraic methods are applied for verification and correctness. Due to space constraints in this article, the reader is directed to [28] for further explanation concerning the mathematical properties of PNs applied to the design and validation process. A PN is a directed graph described by places (represented by circles) and transitions (represented by bars), which are connected to each other with arcs. Connections between nodes of the same type (i.e., place to place and transition to transition) are not allowed. The places can contain zero or more tokens (represented by dots) that fire the transitions. The dynamic structure of a PN is defined by the movements of tokens from one place to another and is referred to as marking, i.e., it represents the PN status according to the fired transitions. Our dynamical model of AQM is a PN represented by (\(P\), \(T\), \(F\), \(W\), \(G\), \(M_{0}\)), where:  
\(P\) = {\(P_{1}\),..., \(P_{n}\)} is a finite set of \(n\) places. The places hold the token (or tokens) and show the PN marking during its evolution. \(T\) = {\(T_{1}\),..., \(T_{m}\)} is a finite set of \(m\) transitions. They are the active events of the PN, which are used to change the position of the token (or tokens) during the evolution of the PN. In addition, the transitions can have guards that can restrict their firing, and they must be evaluated as true for the transition to be fireable. In addition, \(T\) and \(P\) are disjoint sets: \(P\cap T=\varnothing\), \(P\cup T\
eq\varnothing\). \(F\subseteq(PxT)\cup(TxP)\). \(F\) is a set of arcs (flow relation), where (\(PxT\)) is a set \(I\) of input arcs, which connect places to transitions. A place \(p\) is called an input place of a transition \(t\) if there exists an input arc from \(p\) to \(t\). Then, (\(TxP\)) is a set \(O\) of output arcs, which connect transitions to places. A place \(p\) is called an output place of a transition \(t\) if there exists an output arc from \(t\) to \(p\). A transition (an event) has a certain number of input and output places representing the pre- and post-conditions of the event, respectively. \(W\): \(F\rightarrow\{\)1,2,3,...\(\}\) is a weight function. The arcs are labeled with their weights (positive integers). Labels for unity weight are usually omitted. Consequently, a PN is said to be ordinary if all of its arc weights are 1s. \(G=\{G_{1},...,G_{m}\}\) are the guards. They are Boolean expressions constructed by using the variables to enable and fire the associated transition under certain conditions. \(Mo=\{M_{1},...,M_{n}\}\) is the initial marking. \(M\) is a marking state that assigns to each place a non-negative integer. If a marking assigns to the place \(p\) a non-negative integer \(k\), we say that \(p\) is marked with \(k\) tokens. Graphically, we place \(k\) tokens in place \(p\). A marking is denoted by a vector \(M\) of \(n\) components, where \(n\) is the total number of places. The \(p\)-th component of \(M\), denoted by \(M(p)\), is the number of tokens in place \(p\). \(M_{o}\) represents where the tokens are positioned initially. Additionally, a PN follows some rules that our AQM model monitors as well. A transition \(t\) is said to be enabled if each input place \(p\) of \(t\) is marked with at least \(w(p,t)\) tokens, where \(w(p,t)\) is the weight of the arc from \(p\) to \(t\). A firing of an enabled transition \(t\) removes \(w(p,t)\) tokens from each input place \(p\) of \(t\) and adds \(w(t,p)\) tokens to each output place \(p\) of \(t\), where \(w(t,p)\) is the weight of the arc from \(t\) to \(p\).