## 5 An Illustrative Example and Case Study
### Case Study  
We use the intelligent washing machine studied in [18] as an example to better explain the application of the GPo\({}_{\mu}\) model-checking method. As shown in Figure 3, it is the control system of the intelligent washing machine, where S\({}_{0}\) to S\({}_{10}\) 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\({}_{0}\), and the clothes are very dirty, there is a lot of detergent, and the system is off. From S\({}_{1}\) to S\({}_{2}\), it can be found that the dosage of the detergent is decreasing. At S\({}_{3}\), the detergent is 0, but the clothes are still dirty, and the detergent should be added, so S\({}_{3}\) may return to initial state S\({}_{0}\) or return to S\({}_{2}\). In addition, each state has a self-circulation, and the possibility is 1, which are omitted in the figure.  
For the intelligent washing machine system, we convert some properties into GPo\({}_{\mu}\) formulae:  
* The possibility that the washing machine can be turned off at the next time, which is denoted as \(\circ\
eg t\)_running_.
* The possibility that the clothes can be cleaned when the washing machine is in the next state, which is denoted as \(\Box\
eg dirty\).
* The possibility that the washing machine may have detergent before the clothes are clean, which is denoted as \(\mu X.\
eg dirty\vee(\mathit{deterget}\wedge\circ X)\).
* The possibility that detergent is always in the washing machine, which can be denoted as \(\
u X.\mathit{deterget}\wedge\circ X\).
* The possibility that only with detergent, the clothes can be cleaned in the washing machine, which is denoted as \(\
u X.(\mathit{deterget}\rightarrow\
eg dirty)\wedge\circ X\).  
The results of verifying the properties of the intelligent washing machine system you can see in the following Table 1.  
The table lists the possibility value that each state meets the properties. For example, for Property 1,\(\|\diamond\
eg ruunting\|(S_{0})=\|\diamond\
eg ruunting\|(S_{3})=\|\diamond\
eg ruunting\|(S_{7})=1\), the result indicates that only at states \(\mathsf{S}_{0}\), \(\mathsf{S}_{3}\),\(\mathsf{S}_{7}\) can the washing machine be turned off at the next time. For Property 3, we know \(\|\mu X.\
eg dirty\vee(\mathit{deterget}\wedge\circ X)\|(S_{7})=0\), which indicates the possibility that the washing machine may have detergent before the clothes only at \(\mathsf{S}_{7}\) are clean is 0, because the clothes are clean and there is no detergent, so \(\mathsf{S}_{7}\) does not need to satisfy Property 3. For Property 5, \(\|\
u X.\mathit{deterget}\wedge\circ X\|(S_{0})\) = \(\|\
u X.\mathit{deterget}\wedge\circ X\|(S_{1})=\|\
u X.\mathit{deterget} \wedge\circ X\|(S_{5})=\|\
u X.\mathit{deterget}\wedge\circ X\|(S_{9})\)= 1, which indicates that detergent is potentially always in the washing machine at states \(\mathsf{S}_{0}\), \(\mathsf{S}_{1}\), \(\mathsf{S}_{5}\), and \(\mathsf{S}_{9}\).  
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\({}_{\mu}\) formulas, and we can express different properties of the systems that the GPoLTL formulae can not express.