## 2 Materials and Methods
### Timed Colored Petri Net (Timed CPN)
#### 2.1.1 Timed Colored Petri Net, Formal Definitions:  
Timed Multiset  
Considering a non-empty set \(S\) and a set of time values \(\mathbb{T}\). The function \(tm:S\times\mathbb{T}\rightarrow\mathbb{N}\) assigning a non-negative integer \(tm(s,t)\in\mathbb{N}\) to each element \((s,t)\in S\times\mathbb{T}\) is a timed multiset. This sum should be is finite for all \(s\in S\). The non-negative integer \(tm(s)\) is the number of appearances (or coefficient) of \(s\) in \(tm\)[18]. \[tm(s)=\sum_{t\in\mathbb{T}}tm(s,t) \tag{1}\]Next, we refer to EXPR as the set of expressions provided by the language employed in inscription (e.g., CPN ML in the case of CPN Tools), and to Type[e] as the type of an expression \(\mathrm{e}\in\mathrm{EXPR}\), i.e., the type of values obtained when \(\mathrm{e}\) is evaluated. The set of free variables of an expression \(\mathrm{e}\) is named Var[e], and the type of a variable \(\mathrm{v}\) is Type[v]. The variables of a transition \(\mathrm{t}\) are denoted Var(\(\mathrm{t}\)). A timed colored Petri net is defined as follows [19]:  
\[CPN=(P,T,A,S,V,C,G,E,I) \tag{2}\]  
where:  
* P: is a finite state of places;
* T: is a finite state of transitions, and \(\mathrm{P}\cap\mathrm{T}=\emptyset\);
* A \(\subseteq\mathrm{P}\times\mathrm{T}\cup\mathrm{T}\times\mathrm{P}\): is a set of directed arcs;
* \(S\): Non-empty color sets finite set;
* V: Typed variables finite set where \(\mathrm{Type}[\mathrm{v}]\in\mathrm{S}\) for \(\mathrm{v}\in\mathrm{V}\);
* C: \(\mathrm{P}\to\mathrm{S}\): Function of color set attributing for each place a color set;
* G: \(\mathrm{T}\to\mathrm{EXPR}_{\mathrm{v}}\): Guard function providing for each transition \(\mathrm{t}\) a Boolean guard;
* The set of free variables appearing in a guard is required to form a subset of V, it is required that \(\mathrm{G}(\mathrm{t})\in\mathrm{EXPR}_{\mathrm{v}}\);
* E : A \(\to\mathrm{EXPR}_{\mathrm{v}}\): Function of arc expression defining for each arc \(\mathrm{a}\), a corresponding arc expression \(\mathrm{E}(\mathrm{a})\), and \(\mathrm{E}(\mathrm{a})\in\mathrm{EXPR}_{\mathrm{v}}\) is required. For an arc (\(\mathrm{p}\),\(\mathrm{t}\)) \(\in\mathrm{A}\) connecting a place \(\mathrm{p}\in\mathrm{P}\) to a transition \(\mathrm{t}\in\mathrm{T}\), it is required that the type of arc expression is the multiset type over the color set \(\mathrm{C}(\mathrm{p})\) of the place \(\mathrm{p}\). \(\mathrm{Type}[\mathrm{E}(\mathrm{a})]=\mathrm{C}(\mathrm{p})_{\mathrm{MS}}\) if \(\mathrm{p}\) is untimed, and \(\mathrm{Type}[\mathrm{E}(\mathrm{a})]=\mathrm{C}(\mathrm{p})_{\mathrm{TMS}}\) if \(\mathrm{p}\) is timed. where \(\mathrm{p}\) is the place linked to the arc \(\mathrm{a}\). MS and TMS, multisets and timed multisets, respectively;
* \(\mathrm{I}:\mathrm{P}\to\mathrm{EXPR}_{\emptyset}\): initialization function, attributing an initialization expression \(\mathrm{I}(\mathrm{p})\) to each place \(\mathrm{p}\) which is required to evaluate to a multiset over the color set of the place \(\mathrm{p}\), where \(\mathrm{Type}[\mathrm{I}(\mathrm{p})]=\mathrm{C}(\mathrm{p})_{\mathrm{MS}}\) if \(\mathrm{p}\) is untimed and \(\mathrm{Type}[\mathrm{I}(\mathrm{p})]=\mathrm{C}(\mathrm{p})_{\mathrm{TMS}}\) if \(\mathrm{p}\) is timed. Enabling and Occurrence of Timed CPN Steps  
In this section, we will see how timed CPN steps are enabled and occur. The concepts of bindings, binding elements, steps, and marking will be defined. A marking is a function \(\mathrm{M}\) that maps each place \(\mathrm{p}\in\mathrm{P}\) into a multiset \(\mathrm{M}(\mathrm{p})\) of tokens such that the following is true:  
* \(\mathrm{M}(\mathrm{p})\in\mathrm{C}(\mathrm{p})_{\mathrm{MS}}\) if \(\mathrm{p}\) is untimed. * \(\mathrm{M}(\mathrm{p})\in\mathrm{C}(\mathrm{p})_{\mathrm{TMS}}\) if \(\mathrm{p}\) is timed. A timed marking is a pair \((M,t^{*})\) where \(\mathrm{M}\) is a marking and \(t^{*}\in\mathbb{T}\in\) is the value of the global clock.