## 1 Introduction
By applying model-checking techniques to the models discovered in process mining, we can verify whether certain properties hold, detect discrepancies between the intended and actual process, and even predict future process behaviour [12; 13; 14]. Historically, the verification of software and hardware systems was largely deterministic. Yet, as systems have become more complex and have begun to account for randomness and uncertainty, deterministic methods have been found lacking in comprehensiveness. The traditional binary output (YES or NO) of model checking may not be enough for real-world processes ranging from financial [15] to automotive [16] and healthcare [17] sectors having stochastic behaviour. Probabilistic model checking has risen to prominence in this context, providing a means to verify systems that incorporate probabilistic behaviours, with probabilistic models being intended to quantitatively assess system performance and precision [18]. In recent times, probabilistic model checking has established itself as a powerful method for verifying both hardware and software. This technique is recognised for its broad applications, notably in the assessment of reliability, dependability, and performance [19; 20]. A noteworthy collaboration was achieved by combining probabilistic model checking and process mining. This was implemented using discrete- and continuous-time Markov chain models, as detailed in [21; 22]. The authors proposed a framework to verify whether a discovered model satisfies certain desired properties or constraints and provided answers to questions of how likely, how long, and what factors influence possible paths in a process. Figure 1 illustrates the probabilistic model-checking method for process-mining models. While probabilistic model checking has made significant advancements in the field of software model checking, showcasing its effectiveness and robustness in approach, the persistent challenge of the state explosion problem continues to require innovative strategies to be overcome. One such solution is the application of statistical model checking (SMC), utilising simulation methods, particularly _discrete-event simulation (DES)_, as a mitigation strategy. SMC represents a methodology rooted in simulation for validating properties relevant to stochastic systems. It serves as an alternative to conventional model-checking techniques, notably the probabilistic ones, which often struggle with systems that exhibit large or infinite state space--a scenario that usually presents challenges for standard methods [23]. Within the scope of SMC, a system is conceptualised as a stochastic process, and the properties are expressed using temporal logic. The fundamental concept supporting SMC is the estimation of the likelihood that a system complies with a specific property. This research article aims to explore the application of statistical-model-checking techniques in process mining. The methodology presented in this article aims to extend the current process-mining techniques by introducing statistical model checking. In this study, we propose a novel methodology that integrates SMC and PM by formally modelling discovered and replayed process models and applying statistical methods to estimate the results. Our approach offers an efficient, automated evaluation to determine the alignment of a process model with user specifications, aiding users in choosing the most suitable process model. The proposed approach enables the validation of qualitative and quantitative properties of complex systems and/or systems with large state space, where it is difficult to perform probabilistic model checking. The aforementioned process is accomplished by executing several discrete simulations of the system under study, where each simulation trace is individually examined for the property of interest. The final result can be understood as a statistical representation of the given probability, supplemented by a confidence interval.