## 4 Proposed Framework
### Modelling and Verification
The event log contains 26 types of activities, which are divided into 3 types: _Application events, Offer events_, and _Workflow events_. To showcase the application of the suggested method, we employed a range of process discovery algorithms, including _Alpha Miner, Discover using Decomposition, Mine for Heuristic Net, and Mine Transition System_. And, for each discovered process model, we implemented various replay algorithms, _Heuristic cost-based fitness with Integer Linear Programming (ILP)_, \(A^{\star}\)_cost-based fitness with ILP, Best first search simple string distance (SSD) calculation, Dijkstra-based replayer, ILP-based replayer, LP-based replayer, Prefix-based \(A^{\star}\)_cost-based fitness, and Splitting replayer_[58]. ### Verification

For each of the four process discovery algorithms and each of the eight replay algorithms, we built a DTMC model in the PRISM model checker [59]. Table 1 presents a description of the generated DTMC models grouped by process-mining algorithm. The table is divided into three columns, in which the first column shows process discovery algorithms, the second column is about the number of states for each discovered and replayedalgorithm, and the third column presents the lowest and highest values of transitions for each algorithm. In the second column, we can observe variations in the number of states among discovery algorithms. The discovery algorithm _Mine for Heuristic Net_ has 27 states, while the others have 26. The reason is that the _Mine for Heuristic Net_ algorithm generates a discovery model that includes all (observable and unobservable) activities. A _(tau)_\(\tau\) transition, also known as a silent or invisible transition, represents unobservable activities. It does not correspond to any observable operation or event in the modelled process. It is used to represent internal actions or events that are unobservable or irrelevant to the analysis at hand. For example, in a workflow process, you might have actions like \"approve document\" or \"send email\" that are represented by observable transitions. However, there might be internal system checks or data processing steps that are not directly observable from the outside. These are modelled using \(\tau\) transitions, indicating that something happens, but it is not necessary to specify what that something is for the purposes of the model. These transitions can change the state of the Petri net without producing any visible outcome. As mentioned in Section 5.1, there are eight different replay algorithms, which were utilised to generate a formal model. Therefore, the number of transitions varies in each discovery algorithm, depending on the nature of the respective replay algorithm, except for _Discover using Decomposition_. The reason behind this is that the _Discover using Decomposition_ algorithm has consistent performance in each replay algorithm. In other words, the _Discover using Decomposition_ algorithm maintains consistent behaviour across different scenarios. The verification procedure is divided into two main steps. Firstly, we undertake _estimation_ exercises at _confidence levels of 99% and 95%_. This part of the study fundamentally focuses on the statistical evaluation of the properties under investigation within these confidence intervals. The choices of these specific confidence levels allows us to assess the robustness and reliability of our findings under different degrees of statistical certainty. The 95% confidence level is commonly used in research, as it offers a standard balance between statistical power and confidence. It implies that if the study were repeated multiple times, 95 out of 100 similar studies would produce results within this interval, suggesting a high level of reliability. However, to further strengthen our conclusions and to account for potential variations in the data, we also consider the 99% confidence level. By comparing results at these two levels, we aim to demonstrate the consistency of our findings.