The μ-Calculus Model-Checking Algorithm for Generalized Possibilistic Decision Process

Abstract

Model checking is a formal automatic verification technology for complex concurrent systems. It is used widely in the verification and analysis of computer software and hardware systems, communication protocols, security protocols, etc. The generalized possibilistic μ-calculus model-checking algorithm for decision processes is studied to solve the formal verification problem of concurrent systems with nondeterministic information and incomplete information on the basis of possibility theory. Firstly, the generalized possibilistic decision process is introduced as the system model. Then, the classical proposition μ-calculus is improved and extended, and the concept of generalized possibilistic μ-calculus (GPo_μ) is given to describe the attribute characteristics of nondeterministic systems. Then, the GPo_μ model-checking algorithm is proposed, and the model-checking problem is simplified to fuzzy matrix operations. Finally, a specific example and a case study are analyzed and verified. Compared with the classical μ-calculus, the generalized possibilistic μ-calculus has a stronger expressive power and can better characterize the attributes of nondeterministic systems. The model-checking algorithm can give the possibility that the system satisfies the attributes. The research work provides a new idea and method for model checking nondeterministic systems.

1. Introduction

The continuous enhancement of computer functions makes systems increasingly complex; for the purpose of the correctness of the systems, it usually spends more time on verification than on construction [1]. Formal methods are important methods to ensure the correctness and security of computer systems. They can integrate verification early in the design process and ensure the credibility of the system through strict logical reasoning and mathematical calculations.

Model checking is a formal automatic verification technology that can provide a complete formal verification framework of system attributes [2]. The classical model-checking technology is mainly used for qualitative research on the system—that is, to verify if the system satisfies the system attributes described by temporal logic formulas, such as Computation Tree Logic (CTL), Linear Temporal Logic (LTL), and μ-calculus [3,4]. If it is satisfied, the model checker returns “True”; otherwise, it returns “False” with specific counterexamples. However, in the design of actual systems, nondeterministic systems containing uncertain or inconsistent information are often encountered, so the qualitative research on the systems cannot meet the actual needs. In recent years, some scholars have proposed quantitative extensions to classical model checking, such as models that embed features into probability [5,6], possibility [7,8,9], and multi-valued [10,11,12], etc.

Different model-checking approaches are applicable to different model types. Narasimha et al. [13] proposed a model-checking algorithm based on the probabilistic labeled transition systems and μ-calculus to check whether the states in the finite probabilistic labeled transition systems satisfiy the logical formulas; Chechik et al. [14] extended the classical CTL and Kripke structure and proposed a multi-valued model checking algorithm. Gurfinkel et al. [15] studied the multi-valued μ-calculus model checking problem based on multi-valued Kripke structures and reduced it into several classical model-checking problems. The advantage of the reduction method is that the verification can be done automatically using existing model-checking tools. Mallya et al. [16] defined a multi-valued μ-calculus and proposed a new model-checking logic framework to verify arbitrary properties of multi-valued μ-calculus, which is more widely used.

Recently, Pan et al. [17] combined fuzzy logic with CTL, proposed Fuzzy Computation Tree Logic (FCTL), which is a fuzzy extension of classical CTL, and discussed model-checking problems. Li et al. [18,19,20,21] extended the classical LTL and CTL model-checking technology; they defined a quantitative model-checking verification method on the basis of possibility measures. Compared to probabilistic model checking, the possibilistic model checking does not need to satisfy countable additivity, and it is mainly used for the model checking of non-additive systems. Probabilistic model checking already has mature model-checking tools, such as PRISM PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others [22], etc., while possibilistic model checking is still in the theoretical research. Possibilistic model checking uses the theory of possibility measure as the theoretical basis for system modeling, which is suitable for systems with uncertain information in possibility theory [7].

There is some research on quantitative model-checking verification methods on the basis of possibility measures. Li et al. proposed Generalized Possibilistic LTL (GPoLTL), which is an extension of LTL, and gave quantitative model checking methods of linear-time properties based on generalized possibility measures in [18]. They also extended CTL to Generalized Possibilistic CTL (GPoCTL) and proposed a model-checking algorithm under the generalized possibilistic decision process in [21]. Our paper is the first to extend classical μ-calculus in possibility measure theory, and it studies the possibilistic model checking. The μ-calculus is very expressive and it can capture many other temporal (such as CTL^∗) and program logics [12]. We extend classical μ-calculus by adding a possibility value, which is denoted as Generalized Possibilistic μ-calculus (GPo_μ); the semantics interpret the GPo_μ formulas as mappings from the set of states of Generalized Possibilistic Decision Process (GPDP) to the domain of (0,1). The conjunction, disjunction, and negation logical operators are interpreted as the meet, join, and complementation operators in (0,1), respectively, so we use the fuzzy logic and possibility measure theory for reasoning and calculus attribute values of the systems. The GPo_μ can express some properties that GPoCTL and GPoLTL cannot describe. Finally, we solve the model-checking problems by fuzzy matrices.

This paper is organized as follows. Section 2 gives basic knowledge of fuzzy theory and possibility measure theory. In Section 3, the notion of the generalized possibilistic decision process is introduced as the model of nondeterministic systems. Section 4 introduces the generalized possibilistic μ-calculus (GPo_μ) to characterize the attributes for uncertain systems and gives a model-checking algorithm to verify the possibilities that the system states satisfy the attributes. A specific example and case study are explained in Section 5. We give a conclusion at the end of the paper.

2. Fuzzy Theory and Possibility Measure Theory

2.1. Fuzzy Theory

The fuzzy set [23] on domain U is defined by a function $A:U\to \left[0,1\right]$; then, $A$ is called a fuzzy subset on U. If the element in the domain U is represented by $x$, and $A\left(x\right)\in \left[0,1\right]$, then $A\left(x\right)$ is the membership degree that $x$ belongs to $A$.

Let A and B be two fuzzy subsets on U. For any $x\in U$, the membership functions of union $A{{\displaystyle \cup }}^{}B$, intersection $A{{\displaystyle \cap }}^{}B$ complement $A^c$, and implication $A\to B$, are defined as follows:

$$\left(A{{\displaystyle \cup }}^{}B\right)\left(x\right)=A\left(x\right)\vee B\left(x\right)=max\left\{A\left(x\right),B\left(x\right)\right\}$$

$$\left(A{{\displaystyle \cap }}^{}B\right)\left(x\right)=A\left(x\right)\wedge B\left(x\right)=min\left\{A\left(x\right),B\left(x\right)\right\}$$

$$A^c\left(x\right)=1-A\left(x\right)$$

$$(A\to B)=A\left(x\right)\to B\left(x\right)=A^c\left(x\right)\vee B\left(x\right)$$

Let $Q={(q_{ij})}_{m\times n}$ be a matrix; if $\left(q_{ij}\right)\in \left[0,1\right]$, then Q is a fuzzy matrix. For arbitrary fuzzy matrice Q, R, $Q={(q_{ij})}_{m\times n}$, $R={(r_{ij})}_{m\times n}$, the union of the fuzzy matrix $Q{{\displaystyle \cup }}^{}R$, intersection $Q{{\displaystyle \cap }}^{}R$, and the complement operation $Q^c$ are defined as follows:

$$Q{{\displaystyle \cup }}^{}R={(q_{ij}\vee r_{ij})}_{m\times n}$$

$$Q{{\displaystyle \cap }}^{}R={(q_{ij}\wedge r_{ij})}_{m\times n}$$

$$Q^c={(1-q_{ij})}_{m\times n}.$$

Given fuzzy matrices $Q={(q_{ik})}_{m\times p}$, $r={(r_{kj})}_{p\times n}$, their $\vee -\wedge$ composite operation, denoted by $Q\circ R$, which is defined by $Q\circ R=\stackrel{p}{\underset{k=1}{\vee }}\left(q_{ik}\wedge r_{kj}\right)$.

2.2. Possibility Measure Theory

Let I be the index set, the possibility measure on nonempty set U is a mapping POS:$2^U\to \left[0,1\right]$, satisfying the following formulae [21]:

$$POS(\varnothing )=0, \left(2\right) POS(U)=1, \left(3\right) \mathrm{If} E_i\subseteq U, \mathrm{and}i\in I, \mathrm{then}POS({\displaystyle {\cup }_{i\in I}{E}_i})={\vee }_{i\in I}POS(E_i).$$

If POS only satisfies the Formulae (1) and (3), then POS is called a generalized possibility measure. If POS is a generalized possibility measure on nonempty set U, for any E ⊆ U, satisfy $POS(E)=$ ${\vee }_{x\in E}POS(\left\{x\right\})$.

3. Generalized Possibilistic Decision Process

In the design of practical systems, there are systems that have both nondeterministic choices of actions and possibility distributions of states. We give the notion of the generalized possibilistic decision process as the models for uncertainty systems.

Definition 1.

A generalized possibilistic decision process (GPDP) [24] is a tuple $M=\left(S,I,Act,R,AP,L\right)$, where S is a finite, nonempty set of states; $I:S\to \left[0,1\right]$ is the possibilistic initial distribution function; Act is a set of actions; $R:S\times Act\times S\to \left[0,1\right]$ is the possibilistic transition distribution function, and for every state $s\in S$ and every action $\alpha \in Act$, there is a state $s^{\prime }$ such that $R\left(s,\alpha ,s^{\prime }\right)>0$; AP is a set of atomic propositions; $L:S\times AP\to \left[0,1\right]$ is a labeling function, $L\left(s,a\right)$ denotes the possibility that the atomic proposition $a$ holds on state s.

If S and AP are both finite, we call M a finite GPDP. $R\left(s,\alpha ,t\right)$ represents the possibility that the system evolves from state s into state t by action α. If $R\left(s,\alpha ,t\right)>0$, state t is called the successor of state s, and state s is the predecessor of state t. The set of direct α-successors of s is defined as: $Post\left(s,\alpha \right)=\left\{t\in S|R\left(s,\alpha ,t\right)>0\right\}$. The set of predecessors of t is defined by: $Pre\left(t\right)=\left\{s\in S|R\left(s,\alpha ,t\right)>0\right\}$. The set of actions that state s can trigger is defined as: $Act\left(s\right)$ = $\left\{\alpha \in Act|\exists s^{\prime }\in S,R\left(s,\alpha ,s^{\prime }\right)>0\right\}$.

The paths in the GPDP M is denoted as $\pi$, and $\pi =s_0{\alpha }_0{s}_1{\alpha }_1{s}_2\cdots$.$Paths(s)$ and $Path{s}_{fin}(s)$ denote the set of infinite paths and the set of finite paths starting from state s, respectively. $Paths(M)$ and $Path{s}_{fin}(M)$ represent the set of all infinite paths and the set of all finite paths in M, respectively.

In $M=\left(S,I,Act,R,AP,L\right)$, for any $\alpha \in Act$, we can use the fuzzy matrix to express the possibilistic transition distribution function $R:S\times \alpha \times S\to \left[0,1\right]$, which is denoted as $R_{\alpha }$,$R_{\alpha }={(R\left(s,\alpha ,s^{\prime }\right))}_{s,s^{\prime }\in S}$, in which $R_{\alpha }$ is the fuzzy transition matrix corresponding to action α in M. The maximum possibilistic transition matrix is expressed as $R_{max}={\vee }_{i=0}^n{R}_{\alpha i}$, which is also expressed by

$${(R_{max}\left(s,t\right))}_{s,t\in S}={(\underset{\alpha \in Act\left(s\right)}{\vee }R\left(s,\alpha ,t\right))}_{s,t\in S}.$$

The minimum possibilistic transition matrix is expressed as $R_{min}={\wedge }_{i=0}^n{R}_{\alpha i}$, that is,

$${(R_{min}\left(s,t\right))}_{s,t\in S}={(\underset{\alpha \in Act\left(s\right)}{\wedge }R\left(s,\alpha ,t\right))}_{s,t\in S}.$$

The transition matrix closure of a fuzzy matrix R is denoted as R⁺, $R^{+}=R\vee R^2\vee R^3\vee \cdots R^{\left|S\right|}$, where $R^{k+1}$ = $R^k\circ R$. The reflexive transition closure of the fuzzy matrix R is denoted as R^*, $R^{\ast }=R^0\vee R^{+}$, where R⁰ denotes the identity matrix.

Let us take the generalized possibilistic decision process (GPDP) in Figure 1 as an example. The set of system states is denoted as $S=\left\{s_0,s_1,s_2,s_3\right\}$; $I=\left\{s_0\right\}$ represents the initial state of the system; $Act=\left\{\alpha ,\beta \right\}$ denotes the set of actions; $R\left(s_0,\beta ,s_1\right)$ = 0.72 denotes that the possibility of the system changing from state $s_0$ to $s_1$ by action β is 0.72; the set of atomic propositions is $AP=\left\{a,b,c\right\}$.$L\left(s_0,b\right)=0.4$ denotes that the possibility that atomic proposition b holds in the state $s_0$ is 0.4.

The corresponding fuzzy matrices of the generalized possibilistic decision process in Figure 1 is given in the order $s_0\to s_1\to s_2\to s_3$:

$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)$
$R_{max}=\left(\begin{array}{ccc}0.8& 0.7& 0.8\\ 0.6& 0.5& 0.9\\ 0.8& 0.7& 0.9\end{array}\right)$	$R_{min}=\left(\begin{array}{ccc}0.2& 0.3& 0.2\\ 0.1& 0.2& 0.1\\ 0.3& 0.3& 0.1\end{array}\right)$

Definition 2.

For a generalized possibilistic decision process M $=\left(S,I,Act,R,AP,L\right)$, a function GPo^M:Paths(M)$\to$[0,1] is defined as follows:

$$GP{o}^M(\pi )=I(s_0)\wedge {\wedge }_{i\ge 0}R(s_i,{\alpha }_i,s_{i+1}),$$

where $\pi$ = $s_0{\alpha }_0{s}_1{\alpha }_1{s}_2\cdots \in Paths(M)$. Furthermore, for any $E\subseteq paths(M)$, we define

$$GPo(E)=\vee \{GPo(\pi )|\pi \in E\}.$$

Hence, the function GPo: 2^Paths(M)$\to$[0,1] is a generalized possibility measure on $\Omega =2^{Paths(M)}$.

For a GPDP M $=\left(S,I,Act,R,AP,L\right)$, the function $r:S\to [0,1]$ is defines as:

$$r(s)=\vee \{{\wedge }_{i\ge 0}R(s_i,{\alpha }_i,s_{i+1})|s_1=s,s_i\in S,{\alpha }_i\in Act\},$$

then $r(s)$ denotes the maximum possibility measure of a path starting from state s.

Furthermore, any finite Generalized Possibilistic Kripke Structure (GPKS) [18] can be regarded as a finite GPDP with only one action available in any state.

In the generalized possibilistic decision process, once the possibility distribution is selected by actions indeterminately, the selection of the next state is also performed by possibility selection. The uncertainty process describes the alternation of concurrent processes in a distributed system with incomplete information. Therefore, the generalized possibilistic decision process is very suitable as a model for uncertain systems.

4. GPo_μ Model-Checking Algorithm

4.1. Generalized Possibilistic μ-Calculus

The classical μ-calculus [2] is used to represent the properties of the transition systems. It is mainly used for qualitative research on the Boolean systems, but it has certain limitations; it can not describe the properties of nondeterministic systems with possibility information. In this section, we extend the classical μ-calculus by adding the possibility value, and propose the concept of generalized possibilistic μ-calculus (GPo_μ); the semantics interpret the GPo_μ formulas as mappings from the set of states of GPDP to the domain of [0,1]. The conjunction, disjunction, and negation logical operators are interpreted by fuzzy theory and possibility measure theory, so as to analyze the safety and reliability of uncertain systems.

Definition 3. (Syntax of GPo_μ)

Let AP be the set of atomic propositions, $\Phi$, $\Psi$ be GPo_μ formulae, and $Var=\left\{X_1,X_2,X_3\cdots \right\}$ be a set of relational variables; the generalized possibilistic μ-calculus is defined recursively by the grammar:

$$\Phi :=p\left|X\right|j\left|\neg \Phi \right|\Phi \vee \Psi \left|\Phi \wedge \Psi \right|\diamond \Phi \left|\square \Phi \right|\mu X.\Phi \left(X\right)|\nu X.\Phi \left(X\right)$$

where $p\in AP$, $X\in Var$,$j\in \left[0,1\right]$.

Here, to ensure the fixpoint formulas is monotonic, the variable X should be under an even number of negations. The following are the formulas of negativity and duality under the generalized possibilistic μ-calculus:

$$\neg \neg \Phi \equiv \Phi$$

$$\neg \left(\Phi \wedge \Psi \right)\equiv \neg \Phi \vee \neg \Psi$$

$$\neg \mu X.\Phi \left(X\right)\equiv \nu X.\neg \Phi \left(\neg X\right)$$

$$\neg \nu X.\Phi \left(X\right)\equiv \mu X.\neg \Phi \left(\neg X\right).$$

Definition 4. (Semantics of GPo_μ)

Given a generalized possibilistic decision process (GPDP) and GPo_μ formulas, Var denotes a set of relational variables, $s\in S$ is a state. The environment is defined as $\epsilon :Var\to j^S$, in which $j^S$ denotes the mapping from state to possibility value. For GPo_μ formula, its semantic is a fuzzy set ${\Vert \Phi \Vert }_{\epsilon }:S\to \left[0,1\right]$, which is defined as follows:

$${\Vert p\Vert }_{\epsilon }\left(s\right)=L\left(s,p\right)$$

(1)

$${\Vert X\Vert }_{\epsilon }\left(s\right)=\epsilon \left(X\right)$$

(2)

$${\Vert j\Vert }_{\epsilon }\left(s\right)=j$$

(3)

$${\Vert \neg \Phi \Vert }_{\epsilon }\left(s\right)=1-{\Vert \Phi \Vert }_{\epsilon }\left(s\right)$$

(4)

$${\Vert \Phi \vee \Psi \Vert }_{\epsilon }\left(s\right)={\Vert \Phi \Vert }_{\epsilon }\left(s\right)\vee {\Vert \Psi \Vert }_{\epsilon }\left(s\right)$$

(5)

$${\Vert \Phi \wedge \Psi \Vert }_{\epsilon }\left(s\right)={\Vert \Phi \Vert }_{\epsilon }\left(s\right)\wedge {\Vert \Psi \Vert }_{\epsilon }\left(s\right)$$

(6)

$${\Vert \diamond \Phi \Vert }_{\epsilon }\left(s\right)={\vee }_{t\in S,\alpha \in Act}\left(R\left(s,\alpha ,t\right)\wedge {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)$$

(7)

$${\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)={\wedge }_{t\in S,\alpha \in Act}\left(R\left(s,\alpha ,t\right)\to {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)$$

(8)

$${\Vert \mu X.\Phi \left(X\right)\Vert }_{\epsilon }\left(s\right)=\wedge \{Z\in j^S|{\Vert \Phi \Vert }_{\epsilon \left[X\leftarrow Z\right]}\le Z\}\left(s\right)$$

(9)

$${\Vert \nu X.\Phi \left(X\right)\Vert }_{\epsilon }\left(s\right)=\vee \{Z\in j^S|Z\le {\Vert \Phi \Vert }_{\epsilon \left[X\leftarrow Z\right]}\}\left(s\right)$$

(10)

Furthermore,$\epsilon \left[X\leftarrow Z\right]$ indicates a new environment, except that for $\epsilon \left[X\leftarrow Z\right]\left(X\right)=Z$, this environment is exactly the same as that of $\epsilon$.

Theorem 1.

Let $\mathsf{\Phi }$ be a GPo_μ formula; for any $s\in S$, it satisfies the following equations.

$$\neg {\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)={\Vert \diamond \neg \Phi \Vert }_{\epsilon }\left(s\right)$$

$$\neg {\Vert \diamond \Phi \Vert }_{\epsilon }\left(s\right)={\Vert \square \neg \Phi \Vert }_{\epsilon }\left(s\right)$$

Proof. 

$$\neg {\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)$$

$$=\neg \left({\wedge }_{t\in S,\alpha \in Act}\left(R\left(s,\alpha ,t\right)\to {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)\right)$$

$$=\vee \neg \left(R\left(s,\alpha ,t\right)\to {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)$$

$$=\vee \left(\neg \neg R\left(s,\alpha ,t\right)\wedge \neg {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)$$

$$=\vee \left(R\left(s,\alpha ,t\right)\wedge {\Vert \neg \Phi \Vert }_{\epsilon }\left(t\right)\right)$$

$$={\Vert \diamond \neg \Phi \Vert }_{\epsilon }\left(s\right)$$

 □

Similarly, Equation (2) can be proved.

Theorem 2.

Given GPo_μ formula $\Phi$, ${\Phi }_1$, and ${\Phi }_2$, functions $f_1$, $f_2$:$j^S$→$j^S$ are defined as follows:

$$f_1\left(X\right)\left(s\right)=\Vert {\Phi }_2\Vert {}_{\epsilon }\left(s\right)\vee \left(\Vert {\Phi }_1\Vert {}_{\epsilon }\left(s\right)\wedge \underset{s^{\prime }\in S,\alpha \in Act}{\vee }\left(R\left(s,\alpha ,s^{\prime }\right)\wedge X\left(s^{\prime }\right)\right)\right),$$

$$f_2\left(X\right)\left(s\right)={\Vert \Phi \Vert }_{\epsilon }\left(s\right)\wedge \underset{s^{\prime }\in S,\alpha \in Act}{\vee }\left(R\left(s,\alpha ,s^{\prime }\right)\wedge X\left(s^{\prime }\right)\right).$$

where $X\in j^S$, $s\in S$. If $X,Y\in j^S$ and $X\subseteq Y$, then $f_1\left(X\right)\subseteq f_1\left(Y\right)$,$f_2\left(X\right)\subseteq f_2\left(Y\right)$.

Proof. 

For a linear lattice [0,1], the $\wedge$,$\vee$ operations are monotonic. If $X\subseteq Y$, then for all $s\in S$, satisfy:

$$f_1\left(X\right)\left(s\right)=\Vert {\Phi }_2\Vert {}_{\epsilon }\left(s\right)\vee \left(\Vert {\Phi }_1\Vert {}_{\epsilon }\left(s\right)\wedge \underset{s^{\prime }\in S,\alpha \in Act}{\vee }\left(R\left(s,\alpha ,s^{\prime }\right)\wedge X\left(s^{\prime }\right)\right)\right),$$

$$\le \Vert {\Phi }_2\Vert {}_{\epsilon }\left(s\right)\vee \left(\Vert {\Phi }_1\Vert {}_{\epsilon }\left(s\right)\wedge \underset{s^{\prime }\in S,\alpha \in Act}{\vee }\left(R\left(s,\alpha ,s^{\prime }\right)\wedge Y\left(s^{\prime }\right)\right)\right)=f_1\left(Y\right)\left(s\right).$$

Hence, $f_1$ is monotonic, and $f_2$ is also monotonic, since $f_1$, $f_2$ is monotonic, and the possibility value (0,1) is a finite complete lattice. According to Knaster-Tarski’s theorem [11], $f_1$, $f_2$ have a least fixpoint and greatest fixpoint, respectively. Similiar to the classical μ-calculus, the CTL formulae for the generalized possibilistic decision process can also be expressed by the GPo_μ formulae. □

Therefore, we obtain Theorem 3.

Theorem 3.

The fixpoint semantics of CTL formulae for the generalized possibilistic decision process are expressed by GPo_μ formulae, as shown in the following:

$$\Vert \mathrm{E}({\Phi }_1\cup {\Phi }_2)\Vert =\mu X.(\Vert {\Phi }_2\Vert \vee (\Vert {\Phi }_1\Vert \wedge \Vert \diamond X\Vert ))$$

(11)

$$\Vert EG\Phi \Vert =\Vert \nu X.\Phi \wedge \diamond X\Vert .$$

(12)

Take Equation (12) as an example, we prove the correctness of Theorem 3.

Proof. 

According to Theorem 2, the fixpoint semantics of CTL formulae for generalized possibilistic decision process are expressed by GPo_μ formulae, as shown in the following:

$$\Vert \mathrm{E}({\Phi }_1\cup {\Phi }_2)\Vert =\mu X.(\Vert {\Phi }_2\Vert \vee (\Vert {\Phi }_1\Vert \wedge \Vert \diamond X\Vert ))$$

$$\Vert EG\Phi \Vert =\Vert \nu X.\Phi \wedge \diamond X\Vert$$

 □

Take Equation (12) as an example; we prove the correctness of Theorem 3.

Proof. 

According to Theorem 2,$f_2\left(X\right)\left(s\right)={\Phi }_{\epsilon }\left(s\right)\wedge \underset{s^{\prime }\in S,\alpha \in Act}{\vee }\left(R\left(s,\alpha ,s^{\prime }\right)\wedge X\left(s^{\prime }\right)\right)$ = $\nu X.(\Vert \Phi \Vert \wedge \Vert \diamond X\Vert )$ is monotonic. Let $A=\Vert EG \Phi \Vert$,$\left(A\right)(s)$ = $\underset{\pi \in \Pi (s)}{\vee }\underset{i\in N}{\wedge }(\Vert \Phi \Vert (\pi (i)\wedge R(\pi (i),\pi (i+1)))$ [24],

$$f_2\left(A\right)(s)=\Vert \Phi \Vert (s)\wedge {\vee }_{t\in S}(R(s,\alpha ,s_1)\wedge A(s_1))$$

$$=\Vert \Phi \Vert (s)\wedge {\vee }_{s_1\in S}(R(s,\alpha ,s_1)\wedge \underset{\pi \in \Pi (s_1)}{\vee }\underset{i\in N}{\wedge }(\Vert \Phi \Vert (\pi (i)\wedge R(\pi (i),\alpha ,\pi (i+1)))$$

$$=(\Vert \Phi \Vert (s){\vee }_{s_1\in S}(R(s,\alpha ,s_1))\underset{\pi \in \Pi (s_1)}{\vee }\underset{i\in N}{\wedge }(\Vert \Phi \Vert (\pi (i)\wedge R(\pi (i),\alpha ,\pi (i+1)))$$

$$=\underset{\pi \in \Pi (s)}{\vee }\underset{i\in N}{\wedge }(\Vert \Phi \Vert (\pi (i)\wedge R(\pi (i),\pi (i+1)))$$

$$=\left(A\right)(s)$$

$f_2\left(A\right)(s)$ = $\left(A\right)(s)$, so the A is a fixpoint of $f_2$.

Next, we prove that A is the greatest fixpoint of $f_2$. Assume that Z is the fixpoint of

$$f_2, Z=\Vert \Phi \Vert \wedge \Vert \diamond Z\Vert =\Vert \Phi \Vert \wedge R\circ P_Z.$$

$$\begin{gathered} Z(s)=\Vert \Phi \Vert (s)\wedge \underset{s_1\in S}{\vee }R(s,\alpha ,s_1)\wedge Z(s_1) \\ \le \Vert \Phi \Vert (s)\wedge \underset{s_1,s_2\in S}{\vee }R(s,\alpha ,s_1)\wedge \Vert \Phi \Vert (s_1)\wedge Z(s_1)\wedge R(s_1,\alpha ,s_2)\wedge Z(s_2)\wedge \cdots \end{gathered}$$

$$\le \underset{\pi \in \Pi (s)}{\vee }\underset{i\in N}{\wedge }(\Vert \Phi \Vert (\pi (i)\wedge R(\pi (i),\pi (i+1)))$$

$$\le \left(A\right)(s)$$

Hence,

$$A=\Vert EG \Phi \Vert \mathrm{is} \mathrm{the} \mathrm{greatest} \mathrm{fixpoint} \mathrm{of} \mathrm{the} \mathrm{function}{f}_2(X)=\Vert \Phi \Vert \wedge \Vert \diamond X\Vert .$$

 □

4.2. Model-Checking Algorithm

Given a GPDP M, a state s, and a GPo_μ formula $\mathsf{\Phi }$, the purpose of GPo_μ model checking is to calculate the value of ${\Vert \Phi \Vert }_{\epsilon }\left(s\right)$. For GPo_μ formula $\mathsf{\Phi }$, the value of ${\Vert \Phi \Vert }_{\epsilon }\left(s\right)$ can be calculated recursively in $\left|\Phi \right|$ steps; $\left|\Phi \right|$ represents the length of the formula $\mathsf{\Phi }$ [25], which are given as follows:

$$\left|p\right|=1\left|X\right|=1$$

$$\left|j\right|=1\left|\neg \Phi \right|=\left|\Phi \right|+1$$

$$\left|\Phi \vee \Psi \right|=\left|\Phi \wedge \Psi \right|=\left|\Phi \right|+\left|\Psi \right|+1$$

$$\left|\diamond \Phi \right|=\left|\square \Phi \right|=\left|\Phi \right|+1$$

$$\left|\mu X.\Phi \right|=\left|\nu X.\Phi \right|=\left|\Phi \right|+2.$$

For formulas $\Phi =p$, $\Phi =X$, $\Phi =j$, $\Phi =\neg \Phi$, $\Phi =\Phi \vee \Psi$, $\Phi =\Phi \wedge \Psi$, the value of ${\Vert \Phi \Vert }_{\epsilon }\left(s\right)$ can be calculated recursively according to Equations (1)–(6).

$P_{\Phi }$ denotes the column vector that the possibility that formula Φ holds on s, i.e., we have,

$$P_{\Phi }={({\Vert \Phi \Vert }_{\epsilon }\left(s\right))}_{s\in S}.$$

(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,

$${\Vert \diamond \Phi \Vert }_{\epsilon }\left(s\right)={\vee }_{t\in S,\alpha \in Act}\left(R\left(s,\alpha ,t\right)\wedge {\Vert \Phi \Vert }_{\epsilon }\left(t\right)\right)=R_{\alpha }\circ P_{\Phi }.$$

Therefore, the maximum and minimum values of ${\Vert \diamond \Phi \Vert }_{\epsilon }\left(s\right)$ denoted by fuzzy matrices are shown below:

$${\left({\Vert \diamond \Phi \Vert }_{\epsilon }{(s)}_{max}\right)}_{s\in S}=R_{max}\circ P_{\Phi }$$

(14)

$${\left({\Vert \diamond \Phi \Vert }_{\epsilon }{(s)}_{\min }\right)}_{s\in S}=R_{\min }\circ P_{\Phi }.$$

(15)

For $\Phi$ = $\square \Phi$, according to Theorem 1, i.e., $\neg {\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)$ =${\Vert \diamond \neg \Phi \Vert }_{\epsilon }\left(s\right)$, for any state and any $\alpha \in Act$, we have

$${\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)=\neg {\Vert \diamond \neg \Phi \Vert }_{\epsilon }\left(s\right)=\neg \left(R_{\alpha }\circ P_{\Phi }{}^c\right)={(R_{\alpha }\circ P_{\Phi }{}^c)}^c$$

(16)

Thus, we use the fuzzy matrix to calculate the maximum and minimum values of ${\Vert \square \Phi \Vert }_{\epsilon }\left(s\right)$ as shown below:

$${\left({\Vert \square \Phi \Vert }_{\epsilon }{(s)}_{max}\right)}_{s\in S}={\left(R_{min}\circ P_{\Phi }{}^c\right)}^c$$

(17)

$${\left({\Vert \square \Phi \Vert }_{\epsilon }{(s)}_{min}\right)}_{s\in S}={\left(R_{max}\circ P_{\Phi }{}^c\right)}^c.$$

(18)

For $\Phi$ = $\mu X.\Phi \left(X\right)$ and $\Phi$ = $\nu X.\Phi \left(X\right)$, we use the fixpoint algorithm [21]; the corresponding algorithm is presented in Algorithm 1.

Algorithm 1: Fixpoint algorithm

Input: A function f from the possibility distributions on the state set S into itself. Output: The fixpoint of f.   Function $\mathrm{Fixpoint}\left(Q,f\right)$    $Q^{\prime }=f\left(Q\right)$    $\mathbf{while} Q\ne Q^{\prime }$ do     $Q=Q^{\prime }$      $Q^{\prime }=f\left(Q\right)$    end while    return Q   End Function

Furthermore, we respectively set Q = 0 or Q = 1 to calculate the least fixpoint or the greast fixpoint in the initial recursion, which is different with the classical fixpoint algorithm.

Hence, according to the GPo_μ semantic, we give the GPo_μ model-checking algorithm, it is presented in Algorithm 2:

Algorithm 2: GPoμ model checking algorithm

Input:$\mathrm{A} \mathrm{GPDP} M\mathrm{and} \mathrm{a} \mathrm{GPo}{\mathsf{\mu }}_{ }\mathrm{formula} \Phi$. Output:$\mathrm{For} \mathrm{each} \mathrm{state} \mathrm{in} M , \mathrm{the} \mathrm{possibility} s$$|=\Phi$$, \mathrm{i}.\mathrm{e}.,{\Vert \Phi \Vert }_{\epsilon }\left(s\right)$.  Function Check (Φ)  Case Φ  $p$ $\mathbf{return} L\left(s,p\right)$  $X$ $\mathbf{return} \epsilon \left(X\right)$  $j$ $\mathbf{return} j$  $\neg \Phi$ $\mathbf{return} 1-{\Vert \Phi \Vert }_{\epsilon }\left(s\right)$  $\Phi \vee \Psi$ $\mathbf{return} {\Vert \Phi \Vert }_{\epsilon }\left(s\right)\vee {\Vert \Psi \Vert }_{\epsilon }\left(s\right)$  $\Phi \wedge \Psi$ $\mathbf{return} {\Vert \Phi \Vert }_{\epsilon }\left(s\right)\wedge {\Vert \Psi \Vert }_{\epsilon }\left(s\right)$  $\diamond \Phi$ $\mathbf{return} R_{\alpha }\circ P_{\Phi }$  $\square \Phi$ $\mathbf{return} {\left(R_{\alpha }\circ P_{\Phi }{}^c\right)}^c$  $\mu X.\Phi \left(X\right)$ return$\mathrm{Fixpoint} \left(0,f_{\Phi }\right)$  $\nu X.\Phi \left(X\right)$ return $\mathrm{Fixpoint} \left(1,f_{\Phi }\right)$  End Case End Function

In the GPo_μ model-checking algorithm, for the formulas $\Phi =p$, $\Phi =X$, $\Phi =j$, $\Phi =\neg \Phi$, $\Phi =\Phi \vee \Psi$, $\Phi =\Phi \wedge \Psi$, the time complexity of the formulae is related to the length of $\Phi$ and the size of the system model M. For the formulae $\Phi =\diamond \Phi$, $\Phi =\square \Phi$, the time complexity of each formula is related to fuzzy matrix synthesis operation, i.e., $O\left({\left|S\right|}^2\right)$. For fixpoint formulas $\mu X.\Phi \left(X\right)$ and $\nu X.\Phi \left(X\right)$, each fixpoint needs O(n) iterations, n =$\left|S\right|$, the time for each iteration through the fuzzy matrix synthesis operation is $O\left({\left|S\right|}^2\right)$, so the time complexity of the fixpoint formulae is $O\left({\left|S\right|}^3\right)$.

5. An Illustrative Example and Case Study

5.1. An Illustrative Example

In this section, let us give an example used in [24] to illustrate the GPo_μ 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, $\mathrm{S}=\left\{{\mathrm{s}}_0,{\mathrm{s}}_1,{\mathrm{s}}_2\right\}$, and the initial state of the patient is ${\mathrm{s}}_0$. $\mathrm{AP}=\left\{\mathrm{P},\mathrm{G},\mathrm{E}\right\}$ is the set of atomic propositions, where $\mathrm{P},\mathrm{G},\mathrm{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, $\mathrm{L}\left({\mathrm{s}}_0,\mathrm{P}\right)=0.7$ denotes that the degree that the patient’s health is “poor” on state ${\mathrm{s}}_0$ is 0.7; let $\mathrm{Act}=\left\{\mathsf{\alpha },\mathsf{\beta },\mathsf{\gamma }\right\}$, which means that the doctors treat the patient with $\mathsf{\alpha },\mathsf{\beta },\mathsf{\gamma }$: three different treatment schemes.$\mathrm{R}\left({\mathrm{s}}_0,\mathsf{\beta },{\mathrm{s}}_2\right)=0.5$ denotes that the possibility that this patient’s health status changes from the state ${\mathrm{s}}_0$ to ${\mathrm{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={\left(\begin{array}{ccc}0.7& 0.3& 0.1\end{array}\right)}^T$, $P_G={\left(\begin{array}{ccc}0.15& 0.24& 0.65\end{array}\right)}^T$, and $P_E={\left(\begin{array}{ccc}0.2& 0.51& 0.8\end{array}\right)}^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)$
$R_{max}=\left(\begin{array}{ccc}0.8& 0.7& 0.8\\ 0.6& 0.5& 0.9\\ 0.8& 0.7& 0.9\end{array}\right)$	$R_{min}=\left(\begin{array}{ccc}0.2& 0.3& 0.2\\ 0.1& 0.2& 0.1\\ 0.3& 0.3& 0.1\end{array}\right)$

Some calculations are presented as follows in detail.

${\Vert \diamond E\Vert }_{\epsilon }\left(s\right)$ denotes the possibility that the patient’s health eventually changes to “excellent” after a treatment.

${\Vert \diamond E\Vert }_{\epsilon }{(s)}_{max}$, ${\Vert \diamond E\Vert }_{\epsilon }{(s)}_{min}$ respectively represent the maximum and minimum possibilities of ${\Vert \diamond E\Vert }_{\epsilon }\left(s\right)$ in three states.

$${\Vert \diamond E\Vert }_{\epsilon }{(s)}_{max}=R_{max}\circ P_E={\left(\begin{array}{ccc}0.8& 0.8& 0.8\end{array}\right)}^T,$$

$${\Vert \diamond E\Vert }_{\epsilon }{(s)}_{min}=R_{min}\circ P_E={\left(\begin{array}{ccc}0.3& 0.2& 0.3\end{array}\right)}^T.$$

Hence,

$${\Vert \diamond E\Vert }_{\epsilon }{(s_0)}_{max}=0.8, {\Vert \diamond E\Vert }_{\epsilon }{(s_1)}_{max}=0.8, {\Vert \diamond E\Vert }_{\epsilon }{(s_2)}_{max}=0.8.$$

$${\Vert \diamond E\Vert }_{\epsilon }{(s_0)}_{min}=0.3, {\Vert \diamond E\Vert }_{\epsilon }{(s_1)}_{min}=0.2, {\Vert \diamond E\Vert }_{\epsilon }{(s_2)}_{min}=0.2.$$

${\Vert \square E\Vert }_{\epsilon }\left(s\right)$ denotes the possibility that the patient’s health always changes to “excellent” after a treatment.

${\Vert \square E\Vert }_{\epsilon }{(s)}_{max}$ and ${\Vert \square E\Vert }_{\epsilon }{(s)}_{min}$ respectively represent the maximum and minimum possibilities of ${\Vert \square E\Vert }_{\epsilon }\left(s\right)$ in three states.

$${\Vert \square E\Vert }_{\epsilon }{(s)}_{max}={\left(R_{min}\circ P_E{}^c\right)}^c={\left(\begin{array}{ccc}0.7& 0.8& 0.7\end{array}\right)}^T,$$

$${\Vert \square E\Vert }_{\epsilon }{(s)}_{min}={\left(R_{max}\circ P_E{}^c\right)}^c={\left(\begin{array}{ccc}0.2& 0.4& 0.2\end{array}\right)}^T.$$

Hence,

$${\Vert \square E\Vert }_{\epsilon }{(s_0)}_{max}=0.7, {\Vert \square E\Vert }_{\epsilon }{(s_1)}_{max}=0.8, {\Vert \square E\Vert }_{\epsilon }{(s_2)}_{max}=0.7.$$

$${\Vert \square E\Vert }_{\epsilon }{(s_0)}_{min}=0.2, {\Vert \square E\Vert }_{\epsilon }{(s_1)}_{min}=0.4, {\Vert \square E\Vert }_{\epsilon }{(s_2)}_{min}=0.2.$$

According to Formula (11), $\Vert E\left({\Phi }_1{{\displaystyle \cup }}^{}{\Phi }_2\right)\Vert \left(s\right)$ is the least fixpoint of $\tau \left(X\right)={\Phi }_2\vee \left({\Phi }_1\wedge \diamond X\right)$. Let $P_X={\left(\begin{array}{ccc}0& 0& 0\end{array}\right)}^T$, $\Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert \left(s\right)$ means the possibility that the patient’s health eventually changes from “poor” to “excellent”.

The process of calculating the maximum and minimum possibilities with fuzzy matrices is as follows:

$$\tau \left(X_1\right)=P_E\vee (P_p\wedge \left(R_{max}\circ P_X\right)={\left(\begin{array}{ccc}0.2& 0.51& 0.8\end{array}\right)}^T,$$

$$\tau \left(X_2\right)=P_E\vee (P_p\wedge \left(R_{max}\circ P_{X_1}\right)={\left(\begin{array}{ccc}0.7& 0.51& 0.8\end{array}\right)}^T,$$

$$\tau \left(X_3\right)=P_E\vee (P_p\wedge \left(R_{max}\circ P_{X_2}\right)={\left(\begin{array}{ccc}0.7& 0.51& 0.8\end{array}\right)}^T,$$

$$\tau \left(X_2\right)=\tau \left(X_3\right), \Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s)}_{max}={\left(\begin{array}{ccc}0.7& 0.51& 0.8\end{array}\right)}^T.$$

Similarly,

$$\Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s)}_{min}={\left(\begin{array}{ccc}0.3& 0.51& 0.8\end{array}\right)}^T.$$

Hence,

$$\Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_0)}_{max}=0.7, \Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_1)}_{max}=0.51, \Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_2)}_{max}=0.8.$$

$$\Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_0)}_{min}=0.3, \Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_1)}_{min}=0.51, \Vert E\left(P{{\displaystyle \cup }}^{}E\right)\Vert {(s_2)}_{min}=0.8.$$

According to Formula (12), $\Vert \mathrm{EG} \mathsf{\Phi }\Vert \left(s\right)$ is the greast fixpoint of $\tau \left(X\right)=\Phi \wedge \diamond X$. Let $P_X={\left(\begin{array}{ccc}1& 1& 1\end{array}\right)}^T$, $\Vert \mathrm{EG} E\Vert \left(s\right)$ means the possibility that the patient’s health is potentially always “excellent”.

The process of calculating the maximum and minimum possibilities by fuzzy matrices is as follows:

$$\tau \left(X_1\right)=P_E\wedge \left(R_{max}\circ P_X\right)={\left(\begin{array}{ccc}0.2& 0.51& 0.8\end{array}\right)}^T,$$

$$\tau \left(X_2\right)=P_E\wedge \left(R_{max}\circ P_{X_1}\right)={\left(\begin{array}{ccc}0.2& 0.51& 0.8\end{array}\right)}^T,$$

$$\tau \left(X_1\right)=\tau \left(X_2\right), \Vert \mathrm{EG} E\Vert {(s)}_{max}={\left(\begin{array}{ccc}0.2& 0.51& 0.8\end{array}\right)}^T.$$

Similarly,

$$\Vert \mathrm{EG} E\Vert {(s)}_{min}={\left(\begin{array}{ccc}0.2& 0.2& 0.2\end{array}\right)}^T.$$

Hence,

$$\Vert \mathrm{EG} E\Vert {(s_0)}_{max}=0.2, \Vert \mathrm{EG} E\Vert {(s_1)}_{max}=0.51, \Vert \mathrm{EG} E\Vert {(s_2)}_{max}=0.8,$$

$$\Vert \mathrm{EG} E\Vert {(s_0)}_{min}=0.2, \Vert \mathrm{EG} E\Vert {(s_1)}_{min}=0.2, \Vert \mathrm{EG} E\Vert {(s_2)}_{min}=0.2.$$

As a result, the possibility values that each state satisfies the attributes are obtained. Through these data, doctors can compare the results of different treatment options and then make the practical treatment scheme. Our algorithm provides data support for doctors’ decision analysis.

5.2. Case Study

We use the intelligent washing machine studied in [18] as an example to better explain the application of the GPo_μ model-checking method. As shown in Figure 3, it is the control system of the intelligent washing machine, where S₀ to S₁₀ are the states of the system, there is only one action in the system, and the possibility values are marked between states. The atomic propositions are dirty (di), detergent (de), and running (r), which denote the condition of the cloths, the state of the detergent, and the state of the system. The value of every atomic proposition is labeled at each state. For example, di = 1 means that the clothes are very dirty, di = 0.5 means that the clothes are moderately dirty, and di = 0 means that the clothes are clean. de = 1 means there is a lot of detergent, de = 0.5 means there is moderate detergent, and de = 0 means that there is no detergent. r =1 denotes that the machine is running, and r = 0 means that the washing machine is off. The initial state is S₀, and the clothes are very dirty, there is a lot of detergent, and the system is off. From S₁ to S₂, it can be found that the dosage of the detergent is decreasing. At S₃, the detergent is 0, but the clothes are still dirty, and the detergent should be added, so S₃ may return to initial state S₀ or return to S₂. In addition, each state has a self-circulation, and the possibility is 1, which are omitted in the figure.

For the intellgent washing machine system, we convert some properties into GPo_μ formulae:

Property1 

The possibility that the washing machine can be turned off at the next time, which is denoted as $\diamond \neg running$.

Property2 

The possibility that the clothes can be cleaned when the washing machine is in the next state, which is denoted as $\square \neg dirty$.

Property3 

The possibility that the washing machine may have detergent before the clothes are clean, which is denoted as $\mu X.\neg dirty\vee (deterget\wedge \diamond X)$.

Property4 

The possibility that detergent is always in the washing machine, which can be denoted as $\nu X.deterget\wedge \diamond X$.

Property5 

The possibility that only with detergent, the clothes can be cleaned in the washing machine, which is denoted as $\nu X.(deterget\to \neg dirty)\wedge \diamond X$.

The results of verifying the properties of the intelligent washing machine system you can see in the following

Table 1. Results of verifying the properties of the intelligent washing machine system.

Properties	GPoμ Fomulas	Verifying Results
Property1	$\diamond \neg running$	(1,0,0,1,0,0,0,1,0,0)T
Property2	$\square \neg dirty$	(0,0,0,0,0.5,0.5,0.5,0,1,1)T
Property3	$\Vert \mu X.\neg dirty\vee (deterget\wedge \diamond X)\Vert$	(0.5,0.5,0.5,0,0.5,0.9,0.5,1,1,1)T
Property4	$\nu X.deterget\wedge \diamond X$	(1,1,0.5,0,0.5,1,0,0,0.5,1)T
Property5	$\nu X.(deterget\to \neg dirty)\wedge \diamond X$	(0,0,0.5,1,0.5,0.5,1,1,1,1)T

.

The table lists the possibility value that each state meets the properties. For example, for Property 1,$\Vert \diamond \neg running\Vert (S_0)=\Vert \diamond \neg running\Vert (S_3)=\Vert \diamond \neg running\Vert (S_7)=1$, the result indicates that only at states S₀, S₃,S₇ can the washing machine be turned off at the next time. For Property 3, we know $\Vert \mu X.\neg dirty\vee (deterget\wedge \diamond X)\Vert (S_7)=0$, which indicates the possibility that the washing machine may have detergent before the clothes only at S₇ are clean is 0, because the clothes are clean and there is no detergent, so S₇ does not need to sytisfy Property 3. For Property 5, $\Vert \nu X.deterget\wedge \diamond X\Vert (S_0)$ = $\Vert \nu X.deterget\wedge \diamond X\Vert (S_1)$ = $\Vert \nu X.deterget\wedge \diamond X\Vert (S_5)$ = $\Vert \nu X.deterget\wedge \diamond X\Vert (S_9)$= 1, which indicates that detergent is potentially always in the washing machine at states S₀, S₁, S₅, and S₉.

In [18], they use the GPoLTL formulae to represent the properties of the systems and verified the fuzzy linear-time properties of systems. Diferent from them, we denoted the properties of the systems by GPo_μ formulas, and we can express diferent properties of the systems that the GPoLTL formulae can not express.

6. Conclusions

This paper introduced the μ-calculus model-checking algorithm for the generalized possibilistic decision process, which is an extension of the L_μ model checking in [26]. We first give the generalized possibilistic decision process, and then extend the classical μ-calculus to describe the complex logical relationships and attribute the characteristics of nondeterministic systems. We simplify the model-checking problem into fuzzy matrix operations. It implements attribute verification for nondeterministic systems, and we have explained some examples to prove the effectiveness and practicability of the algorithm.

The classical μ-calculus model-checking algorithm simply searches the finite state space of Boolean transition systems to find the satisfaction set of system properties. The GPo_μ model-checking algorithm is more powerful in terms of expressiveness for expressing possible information, because it can characterize uncertain information for dealing with the incompleteness of the information in the systems and specifications, and it can give the degree to which the systems satisfy the specifications. The satisfaction relation becomes the possibility values that expected properties hold, which is more in line with the characteristics of the actual systems.

In the actual system design, for a system containing possibility information, the system is uncertain (lack of basic information) or inconsistent (conflicts often occur when collecting information from multiple sources Information), and classical logic is unable to infer and calculate the relevant characteristics of uncertain systems. Our methods can verify the properties of nondeterministic systems, such as expert systems and intelligent control uncertain systems, etc. However, the research on the expression ability of extended μ-calculus is not enough, such as multilayer nesting between multiple fixpoint formulas, and research on the optimization of nesting algorithms is not enough. In the future, we will continue to study the expression ability of the algorithm and develop a practical model checker to implement automatic verification.