# Workflow Trace Profiling and Execution Time Analysis in Quantitative Verification
## 5 Time Analysis
### Linear Systems of Moments  
In the following, we present an efficient quantitative verification method to compute \(E[Y^{j}]\) for \(1\leq i\leq k\). Although our main result (i.e., Theorem 1) can be proved directly (c.f., Lemma 4.1 in [20]), we relate it to a well-known property of convolution. We first present a basic property of mixture distributions. **Proposition 1**. : _If \(E[X_{s}^{j}]\) exists for all \(s\in S\backslash G\) then_  
\[E[Y^{j}]=\sum_{s\in S\backslash G}\alpha(s)E[X_{s}^{j}]\]  
_where \(Y\) is defined in Equation (4)._  
With the above proposition, it suffices to consider the moments of \(X_{s}\) for all \(s\in S\). We recall the following property about the probability distribution of \(X_{s}\). **Lemma 1** ([14]). : _It holds that_  
\[Pr(X_{s}\leq t)=\sum_{r\in\operatorname{Post}(s)}\mathbf{P}[s,r]\int_{0}^{t} \mathbf{F}^{\prime}[s,r](x)\cdot Pr(X_{r}\leq t-x)\mathrm{d}x\]or, equivalently,_  
\[f_{X_{s}}=\sum_{r\in\mathrm{Post}(s)}\mathbf{P}[s,r]\big{(}\mathbf{F}^{\prime}[s,r]*f_{X_{r}}\big{)}\]  
_where \(f_{X_{s}}\) and \(f_{X_{r}}\) are the PDFs of \(X_{s}\) and \(X_{r}\), respectively, and \(*\) denotes the convolution._  
In the following, we show that the moments of \(X_{s}\) for all \(s\in S\) can be alternatively characterised by a sequence of linear systems and thus can be computed efficiently in practice. We define an equation system as follows: (i) first,  
\[ \begin{cases}x_{s}^{(1)}=0&\text{if }s\in G\\ x_{s}^{(1)}=\sum_{r\in\mathrm{Post}(s)}p_{s,r}\Big{(}x_{r}^{(1)}+\mu_{s,r}^{(1 )}\Big{)}&\text{if }s\
ot\in G.\end{cases}  \tag{5}\]  
(ii) second, for \(j\geq 2\),  
\[ \begin{cases}x_{s}^{(j)}=0&\text{if }s\in G\\ x_{s}^{(j)}=\sum_{r\in\mathrm{Post}(s)}p_{s,r}\bigg{(}x_{r}^{(j)}+\sum_{i=1}^{j }\binom{j}{i}\cdot\mu_{s,r}^{(i)}\cdot x_{r}^{(j-i)}\bigg{)}&\text{if }s\
ot\in G.\end{cases}  \tag{6}\]  
Based on Lemma 1, the following theorem holds as a result of a well-known property of convolution [27]. Theorem 1: _Given (1) and (2), \(x_{s}^{(j)}=E[X_{s}^{j}]\) for all \(s\in S\) and \(1\leq j\leq k\) are the unique solutions to Equations (5) and (6)._  
In the first instance, Equations (5) and (6) form a linear system with \(k|S|\) variables (where \(S\) is the state space of SMC \(\mathcal{M}\)). However, because for each order \(j\leq k\), only unknowns up to the order \(j\) are included in the equations; the whole linear system can be reduced to \(k\) smaller linear systems, each of which has at most \(|S|\) unknowns. Solving the linear systems can involve inverting a matrix with size \(|S|\times|S|\). Recall that matrix inversion can be carried out in the time complexity \(O(|S|^{3})\). Therefore, based on the standard time complexity of solving linear systems, we have the following result. Proposition 2: _The time complexity of computing up to the k-order FPT moments in an SMC is \(O(k|S|^{3})\), where \(S\) is the state space of the SMC._  
We note that Equation (5) is just the standard characterisation of expected accumulated rewards for Markov Reward Models (MRMs) (c.f., ([28], Chapter 10)). If \(k=2\), we have the following equations to compute the second moments:  
\[ \begin{cases}x_{s}^{(2)}=0&\text{if }s\in G\\ x_{s}^{(2)}=\sum_{r\in\mathrm{Post}(s)}p_{s,r}\Big{(}x_{r}^{(2)}+2\mu_{s,r}^{(1 )}x_{r}^{(1)}+\mu_{s,r}^{(2)}\Big{)}&\text{if }s\
ot\in G.\end{cases}  \tag{7}\]  
Our approach can be improved slighly by separating the offline computation and the online computation. The linear systems that produce the FPT moments (Equations (5) and (6)) are entirely based on the SMC model, which is in turn determined by the workflow transition system, the execution summary and DFA. The fixed transition system and the given DFA determine the structures of the linear systems, while the execution summary provides the coefficients of the linear systems. In view of this, we can pre-compute a sequence of abstract linear systems, whose coefficients are instantiated online.