## 4 Proposed Framework
### Modelling and Verification
The key principle here is that the sample runs of a stochastic system are generated in accordance with the system's defined distribution. This allows for the estimation of the probability measure on the system's executions. A formal model of the discovered process, as shown in Figure 6, is presented along with its defined properties below. ```
dtmc moduleexamplemodel s:[1..5]init1; []s=1->0.5:(s'=2)+0.33333:(s'=3)+0.16667:(s'=5); []s=2->0.6:(s'=3)+0.4:(s'=4); []s=3->0.4:(s'=2)+0.6:(s'=4); []s=5->(s'=4); endmodule
```  
``` constintx; constinty; //Checkingdeadlockstate E[F\"deadlock\"] //Probabilityofreachingstarex? P=? [Fs=x] //YESorNOverification. P<0.7[(s=x)U(s=y)]

### Analysis

The analysis phase within SMC plays an integral role, addressing the results derived from the process and analysing them using a range of key determinants, i.e., _reliability parameters_. A deeper understanding of these reliability parameters provides the ability to closely examine the dependability of the SMC results. Typically, these parameters find associations with the statistical confidence and accuracy of the outcomes obtained from the model-checking procedure. Among the reliability parameters, the concept of _confidence interval_ finds prominence, with its elements being confidence level and width. A significant feature within this context is the _statistical test_. An instance of such a test is the sequential probability ratio test (SPRT) [34]. As illustrated in dotted block 3 in Figure 5, the first assessment criterion is the count of paths. This criterion is essential to evaluating the results. If the execution traces or paths are insufficient for making a conclusive decision, additional paths are generated from the established formal model. Conversely, when there are adequate paths executed, the next step involves reviewing the results and proceeding towards making a decision on whether to accept or reject these results. The basis for such decision making, whether to accept or reject the results, resides in the user requirements, serving as the determining factor for the application of statistical-model-checking techniques to process models. The implication of a user rejecting the acquired results denotes that alterations can be made to the modelling parameters of the process model's discovery and replay. Let us consider a formal model represented by \(\mathcal{M}\), and let \(\varphi\) represent a temporal logic property. In this scenario, the task of the SMC algorithm is to approximate the value of \(\mathbb{P}_{\mathcal{M}}[\varphi]\), where \(\mathbb{P}_{\mathcal{M}}[\varphi]\) denotes the probability that \(\mathcal{M}\) satisfies \(\varphi\). To achieve this, the algorithm generates multiple random paths or samples, denoted by \(s_{1},s_{2},\ldots,s_{n}\), in \(\mathcal{M}\). For every \(s_{i}\), the algorithm checks if \(\varphi\) holds. This results in a sequence of Bernoulli random variables \(X_{i}\) defined as \(X_{i}=1\) if \(\varphi\) holds for \(s_{i}\) and \(X_{i}=0\) otherwise. The SMC algorithm uses the generated samples to estimate \(\mathbb{P}_{\mathcal{M}}[\varphi]\). The estimate is then validated against the user-defined acceptance/rejection criteria that are defined using the reliability parameters. If the estimate falls within acceptable limits, it is accepted. Otherwise, the algorithm iterates, either generating more samples or modifying the model or the property, until a satisfactory estimate is obtained. ## 5 Case Study

### Event Log and Process-Mining Algorithms

The implementation of the proposed approach is based on a dataset of a loan application process performed in a financial institution [3]. The data contain all applications filed on an online system in 2016 and their subsequent events until February 2017. There are 31,509 applications filed in total, and for these applications, 42,995 offers were created in total. The events in this dataset represent real-life events captured by the institute's operational processes.