## 4 Proposed Framework
### Modelling and Verification
This property involves the use of the _NEXT_ operator, denoted by \(X\), which indicates the subsequent reachable state in the model's sequence. The specific state, denoted by \(x\), represents a chosen state in the model. This property can be used to verify the \begin{table}
\begin{tabular}{l c c c c c c c c} \hline \hline
**Process Discovery Algorithm** & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **1** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **2** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **3** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **4** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **5** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **6** \\ \end{tabular} & \
\begin{tabular}{c} **Replay** \\ **Algorithm** \\ **7** \\ \end{tabular} &
\begin{tabular}{c} **Replay** \\ **Algorithm** \\ **8** \\ \end{tabular} \\ \hline Alpha Miner & 0.105 & 0.086 & 0.05 & 0.21 & 0.086 & 0.092 & 0.105 & 0.093 \\ Discover using Decomposition & 0.111 & 0.118 & 0.104 & 0.099 & 0.109 & 0.106 & 0.114 & 0.094 \\ Mine for Heuristic Net & 0.157 & 0.264 & 0.153 & 0.271 & 0.135 & 0.148 & 0.158 & 0.132 \\ Mine Transition System & 0.275 & 0.104 & 0.097 & 0.111 & 0.104 & 0.093 & 0.109 & 0.106 \\ \hline \hline \end{tabular}
\end{table} 
Table 6: Property \(P=?\left[F\leq 10\left(s=x\right)\right]\). \begin{table}
\begin{tabular}{l c c c c c c c c} \hline \hline
**Process Discovery Algorithm** & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **1** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **2** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **3** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **4** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **5** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **6** \\ \end{tabular} & \
\begin{tabular}{c} **Replay** \\ **Algorithm** \\ **7** \\ \end{tabular} &
\begin{tabular}{c} **Replay** \\ **Algorithm** \\ **8** \\ \end{tabular} \\ \hline Alpha Miner & 0.013 & 0.063 & 0.031 & 0.039 & 0.052 & 0.010 & 0.017 & 0.014 \\ Discover using Decomposition & 0.015 & 0.015 & 0.016 & 0.015 & 0.021 & 0.013 & 0.016 & 0.018 \\ Mine for Heuristic Net & 0.130 & 0.158 & 0.031 & 0.120 & 0.134 & 0.136 & 0.201 & 0.104 \\ Mine Transition System & 0.022 & 0.016 & 0.014 & 0.014 & 0.015 & 0.017 & 0.016 & 0.015 \\ \hline \hline \end{tabular}
\end{table} 
Table 7: Property \(P=?\left[\
eg\left(s=x\right)\right]U\leq 5\left(s=y\right)\right]\). likelihood of transitioning from one state to another in the very next step. This is particularly useful in processes where immediate transitions are critical, as it aids in understanding the short-term behaviours and immediate consequences of the current state. #### 5.2.3 Hypothesis Testing

Hypothesis testing, an essential tool in statistical analysis, can be performed on a set of collected samples. This process involves two distinct methodologies: fixed-size sampling and sequential testing. In the context of fixed-size sampling, the total number of samples required is determined in advance. This process is systematic, calculating the sample quantity according to risk functions corresponding to error probabilities denoted by \(\alpha\) and \(\beta\)[60]. It is a predetermined approach where the sample size is set before the commencement of the experiment. Sequential testing, on the other hand, contrasts with the fixed-size sampling method. In this approach, samples are successively assembled, and statistical analyses are performed concurrently [34]. The process continues iteratively until sufficient information to make a decision with the necessary confidence level is acquired. This method provides flexibility, since the total number of required observations is not set in advance.