## 4 Proposed Framework
### Modelling and Verification
One critical aspect observed is this study is the trade-off between the accuracy of results and computational cost. While increasing the number of samples in the statistical-model-checking process could enhance the precision of results, it simultaneously led to an increase in the computational load. Therefore, determining an optimal balance between accuracy and computational efficiency is a significant challenge. In conclusion, the work in this article demonstrates the practicality and efficiency of using statistical-model-checking techniques for verifying the properties of complex models. The results obtained provide a solid foundation for the further use of these methods in more complex and larger probabilistic systems. Our findings also highlight the need for additional research to optimise the balance between result accuracy and computational effort in the model-checking process. ## 6 Conclusions

In this work, we integrate statistical model checking into the domain of process mining. The presented work demonstrates the feasibility and effectiveness of employing SMC to analyse process models extracted from event logs. By applying statistical techniques, we are able to assess complex process behaviours without yielding to the state-space explosion problem, a prevalent issue in traditional model checking. The methodology enables the verification of various properties in a more scalable and efficient manner. Through the combination of SMC and PM, robust tools are provided for businesses to analyse, optimise, and control their processes. The proposed methodology helps in the continuous monitoring and verification of business processes, ensuring that they meet the desired quality standards. As the methodology sets a new standard for process analysis, it encourages the adoption of forward-thinking approaches to process management. By staying ahead of the curve with such innovative methodologies, businesses can future-proof their processes against evolving operational challenges. The case study presented in this work further solidified the applicability and effectiveness of the proposed approach across different scenarios. However, this work is not without its limitations and challenges. The tuning of parameters in SMC, such as the confidence level and error margin (\(\alpha,\beta\)), requires careful consideration and a deep understanding of the underlying processes and statistical principles. Further research may focus on developing more user-friendly methods for non-experts to utilise the power of SMC in process mining. Moreover, while our approach has proven successful in handling various properties and models, certain highly complex or specialised scenarios may require further refinement and extension of our techniques. Conceptualization, G.S. and F.A.M. ; methodology, F.A.M. and G.S. ; software, F.A.M. ; validation, F.A.M. and G.S. ; formal analysis, F.A.M. and G.S. ; investigation, F.A.M. ; data curation, F.A.M. ; writing--original draft preparation, F.A.M. ; writing--review and editing, G.S., M.Z. and F.A.M. ; visualization, F.A.M. and G.S. ; supervision, G.S. and M.Z. All authors have read and agreed to the published version of the manuscript. This research received no external funding. Data available at a publicly accessible repository. The data presented in this study are openly available at [3]. The authors declare no conflict of interest. ## References

* (1)[PERSON] [PERSON]; [PERSON] _Discovery, Conformance and Enhancement of Business Processes_; Springer: Berlin/Heidelberg, Germany, 2011; Volume 136. * (2) [PERSON] [PERSON] Process mining: Overview and opportunities. _ACM Trans. Manag. Inf. Syst. (TMIS)_**2012**, 3, 1-17. [CrossRef]
* (3)[PERSON] BPI Challenge 2017. 2017. Available online: [[https://data.ttu.nl/articles/_/12696884/1](https://data.ttu.nl/articles/_/12696884/1)]([https://data.ttu.nl/articles/_/12696884/1](https://data.ttu.nl/articles/_/12696884/1)) (accessed on 10 July 2023).