## 4 Proposed Framework
### Modelling and Verification
If the results remain significant at both the 95% and 99% confidence levels, it indicates a higher degree of certainty in our conclusions. On the other hand, discrepancies between these levels may suggest areas where further investigation is needed or where conclusions are more tentative. The second part of our verification procedure comprises _hypothesis testing_ applied to selected properties. By incorporating these two complementary approaches, we seek to provide a comprehensive evaluation of the properties under investigation. _Estimation_ at different confidence levels allows us to assess the reliability of the results across a range of statistical significance levels. _Hypothesis testing_, on the other hand, facilitates the rigorous validation of the underlying assumptions and predictions regarding the properties in question. The proposed framework, therefore, offers a multifaceted and robust evaluation of the model. \begin{table}
\begin{tabular}{l l l} \hline
**PM Algorithm** & **Num. of States** & **Num. of Transitions** \\ \hline Alpha Miner & 26 & \([178,254]\) \\ \hline Discover using Decomposition & 26 & 178 \\ \hline Mine for Heuristic Net & 27 & \([172,219]\) \\ \hline Mine Transition System & 26 & \([178,201]\) \\ \hline \end{tabular}
\end{table} 
Table 1: Model size of generated DTMC models. For some process discovery algorithms, the transition numbers differ among different replay algorithms. #### 5.2.1 Estimation with Confidence Level of 99%

In Tables 2-5, the derived results demonstrate the probabilistic estimates for the examined properties at a confidence level of 99%. In order to obtain reliable results, we conducted a sequence of 100 simulations for each property. Table 2 presents a comprehensive overview of the estimated results specific to each process discovery algorithm, inclusive of the corresponding replay algorithm. The focal property investigated here is expressed as \(P~{}=~{}7\) [\(F\leq 10~{}(s=x)\)]. In simpler terms, this property seeks to explore the _likelihood of arriving at state \(x\) (where \(x\) denotes a target state) within a time frame of 10 units_. The property is particularly useful in scenarios where timely completion or response is critical. It allows stakeholders to assess risks and make informed decisions with high-level confidence based on the likelihood of events within relevant time frames. For example, it can verify requirements such as a task's completion within a specified time frame or the prevention of system failures within a certain period. The findings pertaining to the particular property expressed as \(P=?\) [\(\
eg~{}(s=x)\)] \(U\leq 5\)\((s=y)\)] are presented in Table 3. This property represents an exploratory question inquiring about whether the _probability that state \(x\) does not occur before state \(y\) is encountered within a temporal window of 5 time units_. Essentially, we are investigating the constraint-based temporal behaviour of the model's transitions, imposing a bounded time limit on the _until_ (\(U\)) operator. The importance of this property lies in its ability to model circumstances where the occurrence of state \(y\) takes precedence and should be reached before state \(x\). This form of probabilistic property allows for the study of the ordered temporal relationships between different states within a fixed time constraint, offering valuable insights into the temporal dynamics of the system. Table 4 outlines the derived outcomes associated with the verification of the property \(R_{\textit{cost}}=?\) [\(F~{}(s=x)\)]. In essence, this property investigates the _accumulated reward_, represented in this context as a _cost_ required to transition to a designated state \(x\). It is important to note that state \(x\) could represent various scenarios, such as the _target state_, a _deadlock state_ that halts progression, or any other significant state within the system model.