## 3 Related Work
In [46], the authors presented a new probabilistic approach to conformance checking by incorporating stochastic process models, considering routing probabilities and frequencies. The work in [47] proposed a runtime verification technique called predictive runtime verification. The unique aspect of this work is that instead of assuming the availability of a system model, the authors describe a runtime verification workflow where the model is learned and incrementally refined using process-mining techniques. The authors in [48] presented an approach for the automatic analysis of business process models discovered through the application of process-mining techniques. Formal verification techniques such as model checking, however, often encounter a common problem known as the state explosion problem, where the number of states in a model may grow exponentially with the size of the model. Hence, alternative approaches that can handle large models are needed. A unique algorithm that employs Monte Carlo simulation [33] and hypothesis testing for non-explosive, stochastic discrete-event systems was proposed in [32] and further elaborated in [49]. Monte Carlo simulation--a statistical method--permits the modelling of random variables and their potential outcomes. This approach has significantly improved probabilistic model checking capabilities and highlighted the potential of using simulations to strengthen model-checking methodologies. The authors in [32] presented a model-independent method for verifying properties of discrete-event systems, which often have complex dynamics that are difficult to analyse. The uniqueness of this approach lies in its model independence, making it versatile for any discrete-event system. The sole model-dependent aspect is the establishment of sample execution paths and the probability measure on these path sets. In [50], the algorithm of [32] was extended to statistically verify black-box systems. The paper [50] presents a novel statistical methodology for analysing stochastic systems against specifications specified in a sub-logic of continuous stochastic logic. The system under study behaves as a black-box that is already deployed, from which sample traces can be passively observed but cannot be manipulated. More applications of SMC in stochastic systems can be found in [28; 29; 30]. A comprehensive overview of the SMC methodology, its real-world implementations, and its applications in various domains can be found in the literature reviews conducted in [31; 51]. These surveys explain how SMC emerges as a formidable strategy for approximating the probability that a system adheres to a certain temporal property. The methodology of SMC involves the examination of a finite collection of system executions, followed by the application of statistical techniques to generalise the findings. The outcomes of this process adhere to a confidence level that can be predefined by the user, thereby allowing for control over the precision of the results. The work emphasises SMC's capacity to alleviate the state-space explosion problem, along with its ability to manage requirements that surpass the expressiveness of traditional temporal logics. The work in [52] introduces a research direction that merges statistical model checking and process mining. The research aims to augment SMC by explaining the reasons behind specific estimates, which can assist in model validation or recommend improvements (enhancement). The integration of SMC and PM results in an approach to white-box behavioural model validation and enhancement. With this methodology, PM can detect discrepancies in the model by examining the simulations generated through SMC. Importantly, since SMC can determine the necessary number of simulations for a given analysis, it produces statistically reliable event logs suitable for PM applications. The work performed so far in the verification of process models suggests that process models must be validated for accuracy and precision to ensure their effectiveness.