# Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification
## 4 Model Building
### SMC Model  
With the workflow profile and DFA, we can define an SMC model. Our presentation of an SMC follows the probabilistic model checking literature [19] but also specifies the absorbing states explicitly.  
**Defintion 4** (Semi-Markov chain).: _An SMC (with absorbing states) \(\mathcal{M}\) is the tuple \((S,\alpha,\mathbf{P},\mathbf{F},G)\) where_  
* \(S\) _is a state space of_ \(\mathcal{M}\)_;_
* \(\alpha\) _is an initial (probability) distribution on_ \(S\)_;_
* \(\mathbf{P}\) _is a transition (probability) matrix on_ \(S\)_;_
* \(\mathbf{F}\) _is an_ \(|S|\times|S|\) _matrix of continuous probability distribution functions (i.e., Cumulative Distribution Functions (CDFs)) whose supports belong to_ \(\mathbb{R}_{\geq 0}\)_;_
* \(G\subset S\) _is a set of absorbing states (i.e.,_ \(\mathbf{P}[s,s]=1\) _if_ \(s\in G\)_)._  
Let \(\mathrm{Post}(s)\) be the set of successor states of \(s\), namely, \(\mathrm{Post}(s)=\{r\in S\mid\mathbf{P}[s,r]>0\}\). A _path_ in \(\mathcal{M}\) is given by an infinite alternating sequence of states and time values, namely \(\pi=s_{0}t_{0}s_{1}t_{1}s_{2}t_{2}\ldots\) with \(s_{i}\in S\) and \(t_{i}\in\mathbb{R}_{\geq 0}\), such that \(r\in\mathrm{Post}(s)\) for all \(i\). For convenience, let \(ht(\pi,i)=t_{i}\), which is the holding time of the path before the \(i\)-th jump. We use _Path_ to denote the set of paths in \(\mathcal{M}\) and \(\mathit{Path}_{k}\) to denote the set of those paths in \(\mathit{Path}\) originating from state \(s\). Following the literature [19], we define a probability measure on an SMC as follows: Let \(C(s_{0},I_{0},\ldots,I_{i-1},s_{i})\), where \(I_{j}\) is a non-empty interval in \(\mathbb{R}_{\geq 0}\), and denote a _cylinder_ set consisting of all paths in \(\mathit{Path}\) such that \(ht(\pi,j)\in I_{j}\), for all \(0\leq j\leq i\). Then, a _probability measure_\(Pr\) is defined by induction on \(i\): If \(i=0\), \(Pr(C(s_{0}))=\alpha(s_{0})\); for all \(i\geq 1\)  
Figure 4: DFA examples.  
\[Pr(C(s_{0},I_{0},\ldots,s_{i},I_{i},s_{i+1}))=Pr(C(s_{0},I_{0},\ldots,s_{i})) \cdot\] \[\mathbf{P}[s_{i},s_{i+1}]\cdot(\mathbf{F}[s_{i},s_{i+1}](b)- \mathbf{F}[s_{i},s_{i+1}](a))\.\]  
where \([a,b]\) is the closure of \(I_{i}\). Based on the probability measure \(Pr\), we can formally analyse a variety of stochastic and timed properties of an SMC \(\mathcal{M}\).  
For convenience, let \(\mathbf{F}^{\prime}\) contain the corresponding Probability Density Functions (PDFs) for the CDFs in \(\mathbf{F}\). Let \(F=\mathbf{F}[s,r]\) and \(f=\mathbf{F}^{\prime}[s,r]\). The \(k\)-_th moment_ of a random variable \(X\) is the expected value of the \(k\)-th power of \(X\), usually denoted as \(E[X^{k}]\) (where \(E\) is the \"expectation\" operator). Formally, let \(F\) and \(f\) be the CDF and PDF of \(X\), respectively; the \(k\)-th moment of \(X\) is the following quantity (if it exists):  
\[E[X^{k}]=\int_{-\infty}^{\infty}x^{k}\mathrm{d}F(x)=\int_{-\infty}^{\infty}x^ {k}f(x)\mathrm{d}x\.\]  
The first moment of \(X\) is just its expected value \(E[X]\). The variance of \(X\) is derived from the first and second moments of \(X\), namely \(E[X^{2}]-E[X]^{2}\). We can also mention the moments of a CDF (or PDF) without referring to a random variable.