## 4 Proposed Framework
### Modelling and Verification  
In this step, the primary focus lies in constructing a model and ensuring its validity for the system under investigation. A model is built to accurately represent the behaviour of the real-world system. The construction of this model typically involves formalising the processes obtained in the first step (Section 4.1), translating them into a formal language that can be used for further analysis. Dotted block 2 in Figure 5 illustrates the modelling and verification step. In this step, one can build a complete model of a system or can generate paths to perform verification. The formal model is generated with the help of a set of alignments, \(\Gamma_{L,\mathcal{N}}\), which results from the replayed process model, as shown in Figure 5. Set of alignments \(\Gamma_{L,\mathcal{N}}\) is used to create a transition probability matrix and/or rate matrix depending on the type of model we consider (i.e., discrete-time or continuous-time Markov model). In a formal model of type discrete-time Markov chain (DTMC) \(\mathcal{D}=(\mathcal{S},\tilde{s},\mathcal{L},P)\) (where \(\mathcal{S}\) is a finite set of states, \(\tilde{s}\in\mathcal{S}\) is the initial state, \(\mathcal{L}\colon\mathcal{S}\to 2^{\mathcal{A}P}\) is the labelling function, \(P\colon\mathcal{S}\times\mathcal{S}\to[0,1]\) is the transition probability matrix), where \(\sum_{s^{\prime}\in S}P(s,s^{\prime})=1\) for all \(s\in\mathcal{S}\), each element \(P(s,s^{\prime})\) of the transition probability matrix gives the probability of making a transition from state \(s\) to \(s^{\prime}\)[56]. And in a formal model of the type continuous-time Markov chain (CTMC) \(\mathcal{C}=(S,\tilde{s},L,R)\), \(S\) is a finite set of states; \(\tilde{s}\in S\) is the initial state; \(L\colon S\to 2^{\mathcal{A}P}\) is the labelling function; and \(R\colon S\times S\to\mathbb{R}_{\geq 0}\) is the transition rate matrix [56]. The logic used to express the properties of the formal \(DTMC\) model is _probabilistic computation tree logic (PCTL)_, while for \(CTMC\), it is _continuous stochastic logic (CSL)_. The syntax and semantics defined below  
Figure 6: Discovered model of \(\log L\). are for CSL (excluding the \(S\) operator), and if we change the time domain from \(\mathbb{R}_{\geq 0}\) to \(\mathbb{N}\), we obtain PCTL [57]. Let \(\Phi\) represent a _state_ formula and \(\psi\) represent a _path_ formula; then,  
\[\Phi ::=true\mid ap\mid\
eg\Phi\mid\Phi_{1}\wedge\Phi_{2}\mid P_{\sim p}[\psi]\] \[\psi ::=X\Phi\mid X^{\leq k}\Phi\mid\Phi_{1}\;U\;\Phi_{2}\mid\Phi_{1} \;U^{\leq k}\Phi_{2}\]  
where \(ap\) is an atomic proposition, \(ap\in AP\) (set of atomic propositions), \(\sim\in\{<,\leq,>,\}\), \(p\in[0,1]\), and \(k\in\mathbb{R}_{\geq 0}\). The operators (\(\
eg\), \(\wedge\)) represent logical \(NOT\) and \(AND\), respectively, while \(X\) (\"next\"), \(X^{k}\) (\"bounded next\"), \(U\) (\"until\"), and \(U^{k}\) (\"bounded until\") are standard operators in temporal logic. Note that we use bounded and unbounded \(X\) and \(U\) operators. The notion that a state \(s\) (or a path \(\pi\)) satisfies a formula \(\Phi\) is denoted by \(s\models\Phi\) (or \(\pi\models\Phi\)) and is defined as follows [57]:  
\[s \models ap \text{iff }ap\in AP(s)\] \[s \models\
eg\Phi \text{iff }s\
ot\models\Phi\] \[s \models\Phi_{1}\wedge\Phi_{2} \text{iff }s\models\Phi_{1}\;\wedge\;s\models\Phi_{2}\] \[s \models P\sim_{p}(\psi) \text{iff }\text{Prob }\{\pi\in\text{Path(s)}\mid\pi\models\psi\}\sim p\] \[\pi \models X\Phi \text{iff }\tau(\pi,1)\;<\;\infty\;\wedge\;\pi[1]\models\Phi\] \[\pi \models X^{\leq k}\Phi \text{iff }\tau(\pi,1)\;\leq k\;\wedge\;\pi[1]\models\Phi\] Figure 6:0 Figure 6:1  
This step involves generating a finite number of system simulations and leveraging statistical methods to determine whether the collected samples provide statistical proof of the system either meeting or failing to meet the specified requirements.