## 4 GPo\({}_{\mu}\) Model-Checking Algorithm
### Model-Checking Algorithm  
Given a GPDP \(M\), a state \(s\), and a GPO\({}_{\mu}\) formula \(\Phi\), the purpose of GPO\({}_{\mu}\) model checking is to calculate the value of \(\|\Phi\|_{\varepsilon}(s)\). For GPO\({}_{\mu}\) formula \(\Phi\), the value of \(\|\Phi\|_{\varepsilon}(s)\) can be calculated recursively in \(|\Phi|\) steps; \(|\Phi|\) represents the length of the formula \(\Phi\)[25], which are given as follows:  
\[\left|p\right|=1|X|=1\]  
\[\left|j\right|=1|\
eg\Phi|=|\Phi|+1\]  
\[|\Phi\vee\Psi|=|\Phi\wedge\Psi|=|\Phi|+|\Psi|+1\]  
\[|\diamond\Phi|=|\Box\Phi|=|\Phi|+1\]  
\[\left|\mu X.\Phi\right|=|\
u X.\Phi|=|\Phi|+2.\]  
For formulas \(\Phi=p,\Phi=X\), \(\Phi=j\), \(\Phi=\
eg\Phi\), \(\Phi=\Phi\vee\Psi\), \(\Phi=\Phi\wedge\Psi\), the value of \(\|\Phi\|_{\varepsilon}(s)\) can be calculated recursively according to Equations (1)-(6). \(P_{\Phi}\) denotes the column vector that the possibility that formula \(\Phi\) holds on \(s\), i.e., we have,  
\[P_{\Phi}=\left(\|\Phi\|_{\varepsilon}(s)\right)_{s\in S}. \tag{13}\]  
To calculate the possibility about formula \(\Phi=\diamond\Phi\), for any state and any \(\alpha\in Act\), we convert the value of the formula into matrix operations,  
\[\|\diamond\Phi\|_{\varepsilon}(s)=\vee_{t\in S,\alpha\in Act}(R(s,\alpha,t) \wedge\|\Phi\|_{\varepsilon}(t))=R_{\alpha}\circ P_{\Phi}.\]  
Therefore, the maximum and minimum values of \(\|\diamond\Phi\|_{\varepsilon}(s)\) denoted by fuzzy matrices are shown below:  
\[\left(\|\diamond\Phi\|_{\varepsilon}(s)_{max}\right)_{s\in S}=R_{max}\circ P _{\Phi} \tag{14}\]  
\[\left(\|\diamond\Phi\|_{\varepsilon}(s)_{min}\right)_{s\in S}=R_{min}\circ P_{ \Phi}. \tag{15}\]For \(\Phi=\Box\Phi\), according to Theorem 1, i.e., \(\
eg\|\Box\Phi\|_{\varepsilon}(s)=\|\Diamond\
eg\Phi\|_{\varepsilon}(s)\), for any state and any \(\alpha\in Act\), we have  
\[\|\Box\Phi\|_{\varepsilon}(s)=\
eg\|\diamond\
eg\Phi\|_{\varepsilon}(s)=\
eg( R_{\alpha}\circ P_{\Phi}{}^{c})=(R_{\alpha}\circ P_{\Phi}{}^{c})^{c} \tag{16}\]  
Thus, we use the fuzzy matrix to calculate the maximum and minimum values of \(\|\Box\Phi\|_{\varepsilon}(s)\) as shown below:  
\[\left|j\right|=1|\
eg\Phi|=|\Phi|+1\]0  
\[\left|j\right|=1|\
eg\Phi|=|\Phi|+1\]1  
For \(\Phi=\mu X.\Phi(X)\) and \(\Phi=\
u X.\Phi(X)\), we use the fixpoint algorithm [21]; the corresponding algorithm is presented in Algorithm 1. ```
Input: A function \(f\) from the possibility distributions on the state set \(S\) into itself. Output: The fixpoint of \(f\). 1. Function Fixpoint(\(Q,f\))
2. \(Q^{\prime}=f(Q)\)
3. while\(Q\
eq Q^{\prime}\)do
4. \(Q=Q^{\prime}\)
5. \(Q^{\prime}=f(Q)\)
6. endwhile
7. return\(Q\)
8. End Function
```  
**Algorithm 1**Fixpoint algorithm  
Furthermore, we respectively set \(Q=0\) or \(Q=1\) to calculate the least fixpoint or the greatest fixpoint in the initial recursion, which is different with the classical fixpoint algorithm. Hence, according to the \(\text{GPo}_{\mu}\) semantic, we give the \(\text{GPo}_{\mu}\) model-checking algorithm, it is presented in Algorithm 2:  
```
Input: A GPDP Mand a GPo\(\upmu\) formula \(\Phi\). Output: For each state in \(M\), the possibility \(s\ |=\Phi\), i.e., \(\|\Phi\|_{\varepsilon}(s)\). 1. Function Check (\(\Phi\))
2. Case \(\Phi\)
3. \(p\) return\(L(s,p)\)
4. \(X\) return \(\varepsilon(X)\)
5. \(j\) return \(j\)
6. \(\
eg\Phi\) return\(1-\|\Phi\|_{\varepsilon}(s)\)
7. \(\Phi\vee\Psi\) return\(\|\Phi\|_{\varepsilon}(s)\vee\|\Psi\|_{\varepsilon}(s)\)
8. \(\Phi\wedge\Psi\) return\(\|\Phi\|_{\varepsilon}(s)\wedge\|\Psi\|_{\varepsilon}(s)\)
9. \(\diamond\Phi\) return\(R_{\alpha}\circ P_{\Phi}{}^{c}\)
10. \(\Box\Phi\) return\((R_{\alpha}\circ P_{\Phi}{}^{c})^{c}\)
11. \(\mu X.\Phi(X)\) return Fixpoint \((0,f_{\Phi})\)
12. \(\
u X.\Phi(X)\) return Fixpoint \((1,f_{\Phi})\)
13. End Case
14.