## 4 Petri Nets and GPenSIM
### Modular Petri Nets  
A modular Petri net is a Petri net that consists of one or more Petri modules and zero or more inter-modular connectors (IMCs). A Petri module is like any other Petri net, but with some specific rules:  
Figure 3: Example of a multiprocessor system with four jobs using a multi-queue setup. Adapted from [3]. * Tokens can only enter a Petri module through its input ports, which are transitions. * Tokens can only exit a Petri module through its output ports, which are also transitions. * Local places and transitions of a Petri module cannot have any direct arcs with elements outside the Petri module. Modular Petri nets possess two important benefits over the non-modular Petri nets [23]: modular Petri nets allow independent development and testing of Petri modules. After thorough testing of individual Petri modules, they are connected by IMCs to form the overall model. Petri modules can run on different computers. Hence, they run faster (take less simulation time). Modular Petri Nets: Definition  
* **Modular Petri net (MPN) = Petri nodules + IMCs (inter-modular connectors)** An MPN consists of one more Petri module and zero or more IMCs. * **Formal definition of MPN**: An **MPN** is defined as a two-tuple: \[MPN=(\mathbb{M},\mathcal{C})\]
* \(\mathbb{M}=\sum_{i=0}^{m}\Phi_{i}\) (one or more Petri modules). * \(\mathcal{C}=\sum_{j=0}^{n}\Psi_{j}\) (zero or more IMCs). **Formal definition of Petri module**: A **Petri module** is defined as a six-tuple: \[\Phi=(P_{L\Phi},T_{IP\Phi},T_{L\Phi},T_{OP\Phi},A_{\Phi},M_{\Phi 0}),\] where, * \(T_{IP\Phi}\subseteq T\): \(T_{IP\Phi}\) (input ports). * \(T_{L\Phi}\subseteq T\): \(T_{L\Phi}\) (local transitions). * \(T_{OP\Phi}\subseteq T\): \(T_{OP\Phi}\) (output ports). * \(T_{IP\Phi}\), \(T_{L\Phi}\), and \(T_{OP\Phi}\), all are mutually exclusive: \(T_{IP\Phi}\cap T_{L\Phi}=T_{L\Phi}\cap T_{OP\Phi}=T_{OP\Phi}\cap T_{IP\Phi}=\emptyset\). * \(T_{\Phi}=T_{IP\Phi}\cup T_{L\Phi}\cup T_{OP\Phi}\) (the transitions of the module). * \(P_{L\Phi}\subseteq P\) the local places. Since a module has only local places, \(P_{\Phi}\equiv P_{L\Phi}\). * \(\forall p\in P_{L\Phi}\), * \(\bullet p\in(T_{\Phi}\cup\emptyset)\) (a local place can be input by transition inside the module or none). * \(p\bullet\in(T_{\Phi}\cup\emptyset)\) (an output of a local place can be transition inside the module or none). * \(\forall t\in T_{L\Phi}\), * \(\bullet t\in(P_{L\Phi}\cup\emptyset)\) (input place of a module transition is a local place or none). * \(t\bullet\in(P_{L\Phi}\cup\emptyset)\) (output place of a module transition is a local place or none). * \(\forall t\in T_{IP\Phi}\) * \(\bullet t\in(P_{L\Phi}\cup P_{IM}\cup\emptyset)\) (input places of input ports can be local places, places in IMCs, or none). * \(t\bullet\in(P_{L\Phi}\cup\emptyset)\) (output places of output ports can be local places, places in IMCs, or none). * \(\forall t\in T_{OP\Phi}\) * \(\bullet t\in(P_{L\Phi}\cup\emptyset)\) (input places of output ports can be local places or an empty set). * \(t\bullet\in(P_{L\Phi}\cup P_{IM}\cup\emptyset)\) (output places of output ports can be local places, IM-places, or none). * \(A_{\Phi}\subseteq(P_{L}\times T_{\Phi})\cup(T_{\Phi}\times P_{L})\): where \(a_{ij}\in A_{\Phi}\) (internal arcs). * \(M_{\Phi 0}=[M(P_{L})]\) (initial markings in local places). **Formal definition of inter-modular connector**: An **inter-modular connector (IMC)** is defined as a four-tuple:\[\Psi=(P_{\Psi},T_{\Psi},A_{\Psi},M_{\Psi 0})\]  
where,  
* \(P_{\Psi}\subseteq P\): \(P_{\Psi}\) is the set of places in the IMC (known as the IM-places). \(\forall p\in P_{\Psi}\),
* \(\bullet p\in(T_{OP}\cup T_{\Psi}\cup\emptyset)\) (input transitions of IM-places can be output ports of modules, IM-transitions of this specific IMC, or none). * \(p\bullet\in(T_{IP}\cup T_{\Psi}\cup\emptyset)\) (output transitions of IM-places can be input ports of modules, IM-transitions of this specific IMC, or none). (IM-places are not allowed to have direct connections with local transitions of modules.)