## 5 An Illustrative Example and Case Study  
### An Illustrative Example  
In this section, let us give an example used in [24] to illustrate the \(\text{GPo}_{\mu}\) model-checking algorithm. Assume that a new type of disease occurs, and the doctors do not have enough knowledge to treat such diseases, they can only make treatment plans based on their own experience. Depending on the treatment options taken by the doctors, the patient's physical health is also uncertain. So, GPDP is used to model the patient's treatment process. Assume that the doctors divide the patient's status into three states, which are represented by \(s_{0}\), \(s_{1}\), and \(s_{2}\), respectively, that is, \(S=\{s_{0},s_{1},s_{2}\}\), and the initial state of the patient is \(s_{0}\). \(\text{AP}=\{\text{P},\text{G},\text{E}\}\) is the set of atomic propositions, where \(\text{P},\text{G},\text{E}\) respectively indicate that the patient's health status is \"poor\", \"general\", and \"excellent\" in a certain state. For these three health conditions of patients, different doctors understand differently. Therefore, we give them a fuzzy value to indicate the degree of physical health. For example, \(\text{L}(s_{0},\text{P})=0.7\) denotes that the degree that the patient's health is \"poor\" on state \(s_{0}\) is 0.7; let \(\text{Act}=\{\alpha,\beta,\gamma\}\), which means that the doctors treat the patient with \(\alpha,\beta,\gamma\): three different treatment schemes. \(\text{R}(s_{0},\beta,s_{2})=0.5\) denotes that the possibility that this patient's health status changes from the state \(s_{0}\) to \(s_{2}\) is 0.5 after the doctors adopt the treatment scheme \(\beta\). From Figure 2, we can get the corresponding truth matrices of \(P,G,E,P_{P}=\Big{(} \begin{array}{ccc}0.7&0.3&0.1\end{array} \Big{)}^{T}\), \(P_{G}=\Big{(} \begin{array}{ccc}0.15&0.24&0.65\end{array} \Big{)}^{T}\), and \(P_{E}=\Big{(} \begin{array}{ccc}0.2&0.51&0.8\end{array} \Big{)}^{T}\). \(R_{\alpha}\), \(R_{\beta}\), and \(R_{\gamma}\) respectively denote the fuzzy matrices of three treatment schemes. The maximum possibilistic transition matrix is \(R_{max}\), and the minimum possibilistic transition matrix is \(R_{min}\). \[R_{\alpha}=\left( \begin{array}{ccc}0.8&0.3&0.8\\ 0.1&0.2&0.1\\ 0.3&0.3&0.1\end{array} \right) R_{\beta}=\left( \begin{array}{ccc}0.5&0.5&0.5\\ 0.2&0.4&0.8\\ 0.5&0.7&0.8\end{array} \right) R_{\gamma}=\left( \begin{array}{ccc}0.2&0.7&0.2\\ 0.6&0.5&0.9\\ 0.8&0.5&0.9\end{array} \right)\]  
Figure 2: The GPDP of the patient treatment process. Some calculations are presented as follows in detail. \(\|\diamond E\|_{\varepsilon}(s)\) denotes the possibility that the patient's health eventually changes to \"excellent\" after a treatment. \(\|\diamond E\|_{\varepsilon}(s)_{max}\), \(\|\diamond E\|_{\varepsilon}(s)_{min}\) respectively represent the maximum and minimum possibilities of \(\|\diamond E\|_{\varepsilon}(s)\) in three states. \[\|\diamond E\|_{\varepsilon}(s)_{max}=R_{max}\circ P_{E}=\Big{(} \begin{array}[ ]{ccc}0.8&0.8&0.8\end{array} \Big{)}^{T},\]  
\[\|\diamond E\|_{\varepsilon}(s)_{min}=R_{min}\circ P_{E}=\Big{(} \begin{array}[ ]{ccc}0.3&0.2&0.3\end{array} \Big{)}^{T}.\]  
Hence,  
\[\|\diamond E\|_{\varepsilon}(s_{0})_{max}=0.8,\ \|\diamond E\|_{\varepsilon}(s_{1})_{max} =0.8,\ \|\diamond E\|_{\varepsilon}(s_{2})_{max}=0.8.\]  
\[\|\diamond E\|_{\varepsilon}(s_{0})_{min}=0.3,\ \|\diamond E\|_{\varepsilon}(s_{1})_{min} =0.2,\ \|\diamond E\|_{\varepsilon}(s_{2})_{min}=0.2.\]  
\(\|\Box E\|_{\varepsilon}(s)\) denotes the possibility that the patient's health always changes to \"excellent\" after a treatment. \(\|\Box E\|_{\varepsilon}(s)_{max}\) and \(\|\Box E\|_{\varepsilon}(s)_{min}\) respectively represent the maximum and minimum possibilities of \(\|\Box E\|_{\varepsilon}(s)\) in three states. \[\|\Box E\|_{\varepsilon}(s)_{max}=(R_{min}\circ P_{E}^{\ \ \ \ })^{c}=\Big{(} \begin{array}[ ]{ccc}0.7&0.8&0.7\end{array} \Big{)}^{T},\]  
\[\|\Box E\|_{\varepsilon}(s)_{min}=(R_{max}\circ P_{E}^{\ \ \ \ })^{c}=\Big{(}