## 4 Proposed Framework
### Modelling and Verification
The _sequential probability ratio test (SPRT)_, based on _acceptance-sampling_ techniques [32], was performed to determine how many samples were needed for the defined property to return a true result within a given bound on the \(P\) operator. Table 10 outlines the derived outcomes associated with the verification of the property \(P\geq 0.5\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)\(?\)



statistical outcomes are obtained from different models, each demonstrating varied results for multiple properties, as shown in Tables 2-10. In this context, Tables 2-5 illustrate the estimation results at a 99% confidence level; Tables 6-9 highlight the results at a 95% confidence level; and Table 10 presents the hypothesis-testing results for each process model. ### Discussion

In the research conducted, we utilised statistical-model-checking methods to verify properties associated with a complex system. The outcomes demonstrated significance, highlighting the value of such methods when delving into complex systems based on probability. Initially, our analysis involved the successful implementation of a formal model (_DTMC, in this case_) to represent the system under consideration. This model then underwent verification against various properties expressed using _PCTL_, spanning from simple _reachability_ to complex _bounded until_ properties. Subsequently, we embarked on an exhaustive statistical model evaluation of these properties. The checking process yielded a series of results, providing valuable insights into the system's behaviour. These insights paved the way for deducing probabilistic metrics significant for informed decisions about system management and control. During the analysis of properties described in Tables 2-10, which were utilised in the conducted case study, certain observations were made regarding the model's performance, specifically the model discovered through the application of the _Mine for Heuristic Net_ technique. The model exhibited better performance in its estimations, irrespective of whether the confidence level was set to 99% or 95%. It can be observed from Tables 2-9 that the _Mine for Heuristic Net_ discovery algorithm yielded better results in most of the replay algorithms compared with other process discovery algorithms. When considering probabilistic properties where a user desires higher probabilistic values, _Mine for Heuristic Net_ provided better results. Similarly, for cost-related properties where the objective is to minimise values, the specified discovery algorithm performed better. During the _hypothesis-testing_ phase, all four models under consideration demonstrated varied performance with different replay algorithms. As seen in Table 10, the first replay algorithm required fewer samples for _Mine for Heuristic Net_ to return a true result. In contrast, for the second replay algorithm, both _Alpha Miner_ and _Mine for Heuristic Net_ required a fewer (or the same) number of samples. Additionally, the results vary when moving from left to right in Table 10. Therefore, it is not possible to definitively select one discovery algorithm as superior. However, it is noteworthy to mention that these results are fundamentally statistical. Despite this statistical nature, the findings indicate that the _Mine for Heuristic Net_ model offers certain advantages. Particularly, it appears to be more beneficial in relation to reward- or cost-associated properties, as well as in the estimation of probabilistic properties. The statistical-model-checking techniques were found to be remarkably effective in handling the inherent randomness of the _DTMC_ model. Notably, these techniques offered a practical alternative to traditional, exhaustive model-checking approaches, which are often obstructed by the state-space explosion problem. Moreover, the statistical-model-checking techniques provided both upper and lower bounds to the property probabilities, thereby providing quantifiable uncertainty measures for each result.