## 2 Background
### Statistical Model Checking  
Statistical model checking is a method that employs simulation techniques to evaluate specific properties defined within a stochastic temporal logic framework. This approach is especially beneficial for assessing systems that are interactive, distributed, and embedded and exhibit stochastic behaviour. Unlike other verification strategies, such as numerical analysis, SMC is distinguished by its capacity to analyse systems with large state space and to accommodate systems with unspecified implementation components. As a versatile and scalable solution, SMC offers a practical alternative for evaluating the properties of stochastic systems, as highlighted in [28; 29; 30] and in a comprehensive survey [31]. The conceptual roots of SMC are linked to pioneering work by [32], who initially proposed this technique to explore the properties of probabilistic systems. Their approach integrates Monte Carlo simulation [33] methods, a class of computational algorithms that rely on repeated random sampling to obtain numerical results, and statistical hypothesis testing. In practice, SMC leverages the power of statistical methods, particularly Monte Carlo simulations, to approximate the likelihood that a stochastic system satisfies a particular property. It achieves this by conducting multiple random simulations of the system in question and then applying statistical analysis to estimate the probability that a given property holds. Figure 4 illustrates the general workflow of SMC. As shown in Figure 4, the high-level model is the model of a complex and/or partially uncontrollable system on which we wish to perform SMC. The model generates sample paths, and the number of properties can be utilised to perform verification. As the verification results are statistical in nature, it is required to get an idea of reliable results by running an optimal number of steps, and the analysis stage is responsible for this process by checking the number of paths  
Figure 3: Process mining with discovery and conformance [24]. and drawing a conclusion. If the number of paths is sufficient to accept the results, then the process ends with drawing a conclusion; otherwise, additional paths are generated from the defined model. In the domain of SMC, statistical tests are instrumental in making informed decisions regarding the system, based on the outputs of the simulation runs. The selection of the test depends on the nature of the verification we intend to achieve--on whether we aim to affirm if the estimated probability surpasses a specific threshold or if it lies within a certain interval. Notably, a number of statistical tests are commonly employed in SMC, such as [PERSON]'s sequential probability ratio test (SPRT) [34]; the Chernoff-Hoeffding test [35], which is based on Chernoff-Hoeffding bounds [36]; and the Bayesian test [37]. Meanwhile, an estimator in SMC serves as a protocol for calculating an approximation of a particular quantity based on the data observed. More specifically, in SMC, an estimator's function is to approximate the probability of a path formula or a system property. This is achieved by executing a number of system runs or simulation traces and computes the fraction of runs that comply with the property. Statistical tests and estimators, when incorporated into SMC, enhance its capabilities, making it a practical and robust tool for validating stochastic systems. The power of SMC lies in its ability to effectively deal with complex as well as _black-box_-type systems (a black-box system refers to an operational system where our knowledge is limited to a predetermined set of historical traces acquired during its operational period). Furthermore, the technique provides a method of verification that is statistically valid and exhibits excellent scalability with respect to the dimension of the state space and the complexity of the properties under verification.