## 4 Proposed Framework
### Modelling and Verification
\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 & 97.808 & 51.731 & 54.089 & 54.106 & 51.509 & 98.993 & 98.231 & 97.697 \\ Discover using Decomposition & 99.026 & 99.882 & 98.851 & 98.215 & 98.301 & 98.557 & 99.060 & 98.143 \\ Mine for Heuristic Net & 42.123 & 31.69 & 23 & 29.92 & 30.62 & 31.377 & 47.430 & 37.896 \\ Mine Transition System & 99.467 & 97.626 & 98.595 & 98.781 & 98.636 & 99.596 & 98.181 & 97.89 \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Property \(R_{\text{conf}}=?\)\([F\ (s=x)]\). \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** \\ **3** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **Algorithm** \\ **4** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **5** \\ \end{tabular} & \begin{tabular}{c} **Replay** \\ **6** \\ \end{tabular} & \
\begin{tabular}{c} **Replay** \\ **Algorithm** \\ **7** \\ \end{tabular} &
\begin{tabular}{c} **Replay** \\ **8** \\ \end{tabular} \\ \hline Alpha Miner & 0.6471 & 0.6521 & 0.5545 & 0.6408 & 0.6476 & 0.5541 & 0.6471 & 0.6472 \\ Discover using Decomposition & 0.6502 & 0.6476 & 0.6454 & 0.6447 & 0.6464 & 0.6487 & 0.6462 & 0.6490 \\ Mine for Heuristic Net & 0.6494 & 0.6462 & 0.6524 & 0.6480 & 0.6456 & 0.6470 & 0.6486 & 0.6515 \\ Mine Transition System & 0.6471 & 0.6299 & 0.6255 & 0.6478 & 0.5660 & 0.6055 & 0.6459 & 0.5516 \\ \hline \hline \end{tabular}
\end{table} 
Table 5: Property \(P=?\)\([X\left(s=x\right)]\). The results linked to the specific property expressed as \(P=?\left[\
eg\left(s=x\right)U\leq 5\right.\)\(\left(s=y\right)\)] can be found in Table 7. This property represents an investigative query about _the likelihood that condition \(x\) does not appear before condition \(y\) within a defined period of 5 time units_. The property refers to an examination of model transitions within specific temporal constraints. It captures a restricted duration on the _until_ operator, essentially quantifying the time-bound behaviour of these transitions. This property can be used to validate if a system behaves as expected. For instance, in a business process, it can be used to check if a certain undesirable state \(\left(s=x\right)\) is avoided until a desired state \(\left(s=y\right)\) is reached within a certain time frame. The comparison between Table 3 and Table 7 highlights the impact of confidence levels on the same property, with Table 3 yielding higher confidence results. Table 8 presents the results obtained from the verification of the property \(R_{\text{cost}}=?\left[F\left(s=x\right)\right]\). Essentially, this property explores the aggregate _reward_, characterised as a _cost_ in this scenario, in relation to the transition to a specified state \(\left(x\right)\). Understanding the expected cost until a certain state is reached is crucial for process optimisation. For instance, if \(s\) represents a specific state in a process, the property can provide insights into the total cost of reaching state \(s\) at a 95% confidence level. Table 9 provides an in-depth evaluation of the property \(P=?\left[X\left(s=x\right)\right]\), a construct designed to estimate _the probability of transitioning into specific state \(x\) immediately following the initial state_.