Safe Diagnosis of Stochastic Discrete Event Systems by Constructing Safe Verifier

Abstract

Safe diagnosis was viewed as the first necessary step of fault-tolerant supervision of discrete event systems (DESs), and a method of safe diagnosis for stochastic DESs was proposed by constructing safe diagnosers in the literature. However, the complexity of constructing such safe diagnosers is exponential. In this paper, we present an algorithm to perform safe diagnosis of stochastic DESs by constructing a nondeterministic automaton called the safe verifier. The necessary and sufficient condition for safe diagnosability of stochastic DESs is proposed. It is worth noting that the complexity of constructing the safe verifier is polynomial in the number of states and events of the system.

1 Introduction

Due to the practical and theoretical importance, failure diagnosis, which aims to timely identify and exactly characterize the occurrence of incipient faults, has received considerable attention in recent years (for example, [1,2,3,4] and the references, therein). In particular, Sampath et al. [3] proposed an approach for failure diagnosis of discrete event system (DES), in which a diagnoser was constructed to perform the on-line detection and off-line verification of the diagnosability properties of the system. Thorsley et al. [4] extended the framework of [3] to stochastic DESs. For the decentralized systems, Qiu and Kumar [2] and Liu et al. [5] investigated the failure diagnosis issue of the decentralized classical and stochastic DESs by constructing the local diagnosers.

Motivated by the fact that the complexity of constructing such diagnosers in above references is exponential in the cardinality of the states of the system, Yoo and Lafortune [6] presented a polynomial-time verification for the diagnosability of partially observed DESs. In [7, 8], two polynomial test methods for stochastic diagnosability of DESs were developed by constructing different diagnosis models. Moreira et al. [9] proposed a polynomial-time failure diagnosis approach for decentralized DESs. In our prior work [10], the diagnosability and safe diagnosability of fuzzy DESs were studied, respectively, in both of which the complexity of constructing the models for failure diagnosis are polynomial-time.

This paper aims to present a new approach to deal with the safe diagnosis problem for stochastic DESs by constructing the safe verifier, which was investigated in our previous work by constructing the safe diagnosers [11]. More specifically, after formalizing the notion of safe diagnosability of stochastic DESs, we construct a non-fault automaton to represent the specification language. Then, a recognizer of the illegal language is introduced to distinguish the forbidden strings from the system behaviors, and a safe verifier is constructed to realize the safe diagnosis of the system. In particular, a necessary and sufficient condition for the verification of safe diagnosability of stochastic DESs is proposed. It is worth noting that the construction of the safe verifier is polynomial-time in the number of states and events of the system.

2 Notations and Preliminaries

A stochastic DES is modeled by a stochastic automaton $G = (X,\Sigma ,\eta_{G} ,x_{0} ),$ where $X$ is a set of states with the initial state $x_{0}$, $\Sigma$ is the set of events, $\eta_{G} :X \times\Sigma \times X \to [0,\,1]$ is a partial state transition probability function.

Define a partial transition function $\delta_{G} :X \times\Sigma \to X$ as: $\delta_{G} (x,\sigma ) = x^{\prime}$ if and only if $\eta_{G} (x,\sigma ,x^{{\prime }} ) > 0$, where $x,x^{{\prime }} \in X$ and $\sigma \, \in \,\Sigma$. The event set $\Sigma$ is partitioned into the observable event set $\Sigma _{o}$ and the unobservable event set $\Sigma_{uo}$, $\Sigma _{f} \, \subseteq \,\Sigma _{uo}$ is the failure event set. Generally, $\Sigma _{f}$ is partitioned into a set of failure types $\Sigma _{f} =\Sigma _{f1} \cup\Sigma _{f2} \, \ldots \, \cup\Sigma _{fm}$.

For convenience, we introduce the notations from [1, 3, 4, 11]: Let $s \in L$, denote $pre\,(s)$ and $suf\,(s)$ as the prefixes and suffixes of $s$, respectively. $L_{\sigma } (G,x) = \{ u\sigma :\Pr (u\sigma |x) > 0,\,u \in\Sigma _{uo}^{*} ,\,\sigma \in\Sigma _{o} \}$, and $L/s = \{ t \in\Sigma ^{*} :st \in L\}$ represents the post-language. $\Psi (\Sigma_{fi} ) = \{ s \in L:s_{l} \in\Sigma _{fi} \}$, where $s_{l}$ is the final event of $s$. $P:\Sigma ^{*} \to\Sigma _{o}^{*}$ is the projection defined in the usual manner.

As mentioned in [11], the purpose of safe diagnosis is to prevent local faults developing into failures that can lead to serious hazards. So we should prevent the system executing a forbidden string from $\Gamma _{i}$ after a failure of type $f_{i}$, where $\{\Gamma _{i} \, \subseteq \,\Sigma ^{*} :i = 1,\,2,\, \ldots \,m\}$ is a class of forbidden string sets. The set of such illegal strings is called illegal language, denoted by $\Re_{f}^{i}$, which is defined as $\Re_{f}^{i} = \{ \omega \in L/s:s \in\Psi (\Sigma _{fi} ),\Gamma _{i} \in \omega \}$, where $\Gamma _{i} \in \omega$ represents that there is $t \in\Gamma _{i}$ such that $t$ is a substring of $\omega$.

Definition 1

[11]: A language $L$ generated by a stochastic automaton $G = (X,\,\Sigma ,\,\eta_{G} ,\,x_{0} )$ is said to be safe diagnosable if for any $\varepsilon \, > \,0$,

$$(\exists n_{0} \in N)\,(\forall s \in\Psi (\Sigma _{fi} ))\,(\forall t \in L/s \wedge ||t|| \ge n_{0} )\,(\exists v \in pre(t))\,(pre(v) \cap \Re_{f}^{i} = \varnothing )$$

and, at least one of the following conditions holds:

1. $\omega \in P^{{{ - }1}} [P(sv)] \Rightarrow\Sigma _{fi} \in \omega$, i.e., $D(sv) = 1$,

2. $\Pr (t:D(sv) = 0|v \in pre(t)) < \varepsilon$.

where the diagnosability function $D:\Sigma ^{*} \to \{ 0,1\}$ is defined as follows:

$$D(sv) = \left\{ {\begin{array}{*{20}l} {1,} \hfill & {{\text{if}}\;\omega \in P^{{{ - }1}} [P(sv)] \Rightarrow \Sigma_{fi} \in \omega ,} \hfill \\ {0,} \hfill & {{\text{otherwise}}.} \hfill \\ \end{array} } \right.$$

(1)

3 Construction of Safe Verifier of Stochastic DESs

Let $G = (X,\,\Sigma ,\,\eta_{G} ,\,x_{0} )$ be a stochastic DES, $\Re_{f}^{i}$ be the illegal language and $\Gamma _{i}$ be the set of forbidden strings. In order to construct the recognizer $G_{r}$, we first define a label set of forbidden strings from $\varGamma_{i}$ as $LB = \{ N,F,B\} ,$ where the label $N$ represents that the failure does not occur in the behavior of system, $F$ represents that the system executes the failure but does not execute any forbidden string from $\Gamma _{i}$ after the occurrence of that failure, and $B$ means that the behavior of system containing a forbidden string from $\Gamma _{i}$ after the occurrence of a failure.

Algorithm 1: Construction of safe verifier of stochastic DESs

Step 1: Construct a non-fault automaton $H = (X^{{\prime }} ,\Sigma _{N} ,\eta_{H} ,\delta_{H} ,x_{0}^{{\prime }} )$ to generate the sublanguage of L without fault events, where $\Sigma _{N} =\Sigma -\Sigma _{f}$, $X^{{\prime }}$ is a set of finite states with the initial state $x_{0}^{{\prime }} = x_{0}$, for any $x^{{\prime }} \in X$, if there exists $\omega \in\Sigma ^{*}$ satisfying $\Sigma _{f} \notin \omega$ and $\eta_{G} (x_{0} ,\omega ,x^{{\prime }} ) > 0$, then $x^{{\prime }} \in X^{{\prime }}$, the state transition probability function $\eta_{H} :X^{{\prime }} \times\Sigma \times X^{{\prime }} \to [0,1]$ is defined as $\eta_{H} (x,\sigma ,x^{{\prime }} ) = \eta_{G} (x,\sigma ,x^{{\prime }} )$, for $\forall x,x^{{\prime }} \in X^{{\prime }}$, $\sigma \in\Sigma _{N}$ satisfying $\eta_{G} (x,\sigma ,x^{{\prime }} ) > 0$, the state transition function, $\delta_{H} :X^{{\prime }} \times\Sigma \to X^{{\prime }}$ is defined as $\delta_{H} (x,\sigma ) = x^{{\prime }}$ if and only if $\eta_{H} (x,\sigma ,x^{{\prime }} ) > 0$.

Step 2: Construct the recognizer of the illegal language $\Re_{f}^{i}$ as a stochastic automaton $G_{r} = (Q_{r} ,\,\Sigma ,\,\eta_{r} ,\,\delta_{r} ,\,p_{0} )$, where $Q_{r} \, \subseteq \,X\, \times \,LB$ is a set of finite states with the initial state $p_{0} = (x_{0} ,\,N)$, $\eta_{r}$ and $\delta_{r}$ are defined in the following Definitions 2 and 3, respectively.

Step 3: Construct the safe verifier $G_{v}$ based on the recognizer $G_{r}$, the $G_{v} = (Q_{v} ,\Sigma _{o} ,\delta_{v} ,\eta_{v} ,q_{0} )$ is a finite state automaton, where $Q_{v}$ is a set of finite states with the initial state $q_{0} = (x_{0} ,\,N,\,y_{0} )$, $Q_{v} \subseteq X\, \times \,LB\, \times \,Y$, where $Y = X^{{\prime }} \cup \{ E\}$, $E$ represents empty, $\eta_{v}$ and $\delta_{v}$ are defined in the following Definitions 4 and 5, respectively.

Definition 2

The partial state transition probability function of recognizer $G_{r}$ is defined as $\eta_{r} :Q_{r} \times\Sigma \times Q_{r} \to [0,1]$: for $p_{i} = (x_{i} ,lb_{i} )$, $p_{j} = (x_{j} ,lb_{j} ) \in Q_{r}$ and $\;\sigma \in \Sigma$, $\eta_{r} (p_{i} ,\sigma ,p_{j} ) = \eta_{G} (x_{i} ,\sigma ,x_{j} )$.

Definition 3

The partial state transition function of recognizer $G_{r}$, is defined as $\delta_{r} :Q_{r} \times \Sigma \to Q_{r}$: for $p_{i} = (x_{i} ,lb_{i} ) \in Q_{r}$, $lb_{i} \in LB$ and $\sigma \in \Sigma$,

$$\delta_{r} (p_{i} ,\sigma ) = \left\{ {\begin{array}{*{20}l} {(\delta_{G} (x_{i} ,\sigma ),N),} \hfill & {{\text{if}}\;\;\sigma \notin \Sigma_{f} ,lb_{i} = N,} \hfill \\ {(\delta_{G} (x_{i} ,\sigma ),F),} \hfill & {{\text{if}}\;\;(\sigma \in \Sigma_{f} ,lb_{i} = N) \vee lb_{i} = F,} \hfill \\ {(\delta_{G} (x_{i} ,\sigma ),B),} \hfill & {{\text{if}}\;\;(suf(s_{2} ) \cap\Gamma _{i} \ne \varnothing ,{\text{where}}} \hfill \\ {} \hfill & {s\sigma = s_{1} \sigma_{f} s_{2} ,\sigma_{f} \in \Sigma_{f} ) \vee lb_{i} = B.} \hfill \\ \end{array} } \right.$$

(2)

Definition 4

The state transition probability function $\eta_{v} :Q_{v} \times\Sigma _{o} \times Q_{v} \to [0,1]^{2}$ of safe verifier $G_{v}$ is defined as: for any $q_{1} = (x_{1} ,lb_{1} ,y_{1} )$, $q_{2} = (x_{2} ,lb_{2} ,y_{2} ) \in Q_{v}$, $\sigma \in \Sigma_{o}$, $\eta_{v} (q_{1} ,\sigma ,q_{2} ) = (\theta ,\theta^{{\prime }} ) > 0$ holds, where

$$\theta^{{\prime }} = \sum\limits_{{s \in L_{\sigma } (H,y_{1} )}} {\eta_{H} (y_{1} ,s,y_{2} )} ,\quad \theta = \sum\limits_{{s \in L_{\sigma } (G,x_{1} )}} {\eta_{G} (x_{1} ,s,x_{2} )} .$$

Definition 5

The state transition function of $\delta_{v} :Q_{v} \times \Sigma_{o} \to Q_{v}$ is defined as:

$$\delta_{v} (q_{1} ,\sigma ) = \left\{ {\begin{array}{*{20}l} {(\delta_{r} (p_{1} ,s),E) ,} \hfill & {{\text{if}}\;\;\delta_{H} (y_{1} ,\sigma )\,{\text{is}}\,{\text{undefined}}\,{\text{or}}\,y_{1} = E,} \hfill \\ {(\delta_{r} (p_{1} ,s),\delta_{H} (y_{1} ,\sigma )),} \hfill & {{\text{otherwise}},} \hfill \\ \end{array} } \right.$$

(3)

where for any $q_{1} = (x_{1} ,lb_{1} ,y_{1} ) \in Q_{v}$, $\sigma \in\Sigma _{o}$, $s \in L_{\sigma } (G,x_{1} )$, $p_{1} = (x_{1} ,lb_{1} ) \in Q_{r}$, state $E$ means that there is no transition originate from state $y_{1}$ with the event of $\sigma$.

Remark

It is worth noting that the construction of the safe verifier is polynomial-time in the number of states and events of the system.

4 Necessary and Sufficient Condition of Safe Diagnosability

Before proposing the necessary and sufficient condition, we introduce some concepts about the safe verifier.

Definition 6

For state $q_{i} = (x_{i} ,\,lb_{i} ,\,y_{i} ) \in Q_{v}$, if $lb_{i} = N$, then $q_{i}$ is called a normal state. The set of all normal states is denoted as $Q_{v}^{N}$, if $lb_{i} = B$, then $q_{i}$ is called a $B$ state, and the set of all $B$ states is denoted as $Q_{v}^{B}$, if $lb_{i} = F \wedge y_{i} \ne E$, then $q_{i}$ is called a fault state, and the set of all fault states is denoted as $Q_{v}^{F}$, where $Q_{v}^{N} ,Q_{v}^{B} ,Q_{v}^{F} \, \subseteq \,Q_{v}$.

Definition 7

If there exists the sequence of states $q_{k} ,q_{k + 1} ,q_{k + 2} ,\, \ldots \,q_{l} \in Q_{v}$ and events $\sigma_{k} ,\sigma_{k + 1} ,\sigma_{k + 2} ,\, \ldots \,\sigma_{l} \in \Sigma_{o}$, $0 \le k \le l$ such that

$$q_{k} \xrightarrow{{\sigma _{k} ,(\theta _{k} ,\theta ^{\prime}_{k} )}}q_{{k + 1}} \xrightarrow{{\sigma _{{k + 1}} ,(\theta _{{k + 1}} ,\theta ^{\prime}_{{k + 1}} )}}q_{{k + 2}} \,...\,q_{l} \xrightarrow{{\sigma _{l} ,(\theta _{l} ,\theta ^{\prime}_{l} )}}q_{k} ,$$

(4)

then the sequence of states $q_{k} ,q_{k + 1} ,q_{k + 2} ,\, \ldots \,q_{l} \in Q_{v}$ forms a state cycle, denoted as $cl = (q_{k} ,q_{k + 1} ,\, \ldots \,q_{l} )$, and the set of the states in the cycle $cl$ is denoted as $cl^{{\prime }}$.

Definition 8

Assume that $cl = (q_{k} ,q_{k + 1} ,q_{k + 2} ,\, \ldots \,q_{l} )$ is a state cycle of safe verifier $G_{v}$, and its probability of transition is $(\vartheta ,\vartheta^{{\prime }} ) = (\theta_{k} \theta_{k + 1} \, \ldots \,\theta_{l} ,\theta_{k}^{{\prime }} \theta_{k + 1}^{{\prime }} \, \ldots \,\theta_{l}^{{\prime }} )$, if $q_{i} \in Q_{v}^{B}$, $(k\, \le \,i\, \le \,l)$ and $\vartheta = 1$, then the state cycle $cl$ is called a recurrent $B$ state cycle, denoted as $cl_{recurrent}^{B}$.

Theorem 1

Let $L$ be the generated language of stochastic DES $G = (X,\Sigma ,\eta_{G} ,x_{0} )$ and $G_{v} = (Q_{v} ,\Sigma _{o} ,\delta_{v} ,\eta_{v} ,q_{0} )$ be the safe verifier. $L$ is safe diagnosable, if and only if, $G_{v}$ satisfies the following condition: There does not exist the states $q_{1} \in Q_{v}^{F} \vee Q_{v}^{N}$ , $q_{2} \in Q_{v}^{B}$ , $q_{3} \in cl_{recurrent}^{{{\rm B}{\prime }}}$ such that $\delta_{v} (q_{1} ,\sigma ) = q_{2}$ and $\delta_{v} (q_{2} ,\alpha ) = q_{3}$ , where $\sigma \in \Sigma_{o}$ , $\alpha \in \Sigma^{*}$ .

Due to the limitation of space, the proof is omitted. Next, some examples are provided to illustrate Algorithm 1 and Theorem 1.

Example 1

For comparison with the method proposed in [11], we consider the same stochastic system $G_{1} = (X,\Sigma ,\eta_{G} ,x_{0} )$ as that in [11] (Example 3 in [11]), which is shown in Fig. 1, where $\Sigma _{0} = \{ a,b\}$, $\Sigma _{f}^{i} = \{ \sigma_{f} \}$ and $\Gamma _{i} = \{ b\}$. In [11], it has been proved that $G_{1}$ is not safe diagnosable by constructing the safe diagnoser.

Fig. 1

Stochastic system $G_{1}$

In the following, we verify this result by constructing the safe verifier proposed in this paper (i.e., by using Algorithm 1 and Theorem 1).

According to Algorithm 1, we construct the non-fault automaton $H_{1}$ shown in Fig. 2 by Step 1 and the recognizer $G_{r1}$ shown in Fig. 3 by Step 2.

Fig. 2

Non-fault automaton $H_{1}$

Fig. 3

Recognizer $G_{r1}$

Then we construct the safe verifier $G_{v1}$ shown in Fig. 4 by Step 3.

Fig. 4

Safe verifier $G_{v1}$

Note that in Fig. 4, $\delta_{v} ((0,N,0),\,b) = (3,\,B,\,E)$,$\delta_{v} ((3,B,E),b) = (3,B,E)$ and $\delta_{v} ((2,F,1),b) = (3,B,E)$, $\delta_{v} ((3,B,E),b) = (3,B,E)$ where $(3,B,E) \in cl_{recurrent}^{{B\;\;\;\;\;\;\;\;\;\;{^{\prime}}}}$. By Theorem 1, $G_{1}$ is not safe diagnosable, which coincides with the result in [11].

Example 2

Consider the stochastic system $G_{2} = (X,\,\Sigma ,\,\eta_{G} ,\,x_{0} )$ shown in Fig. 5, which is the same example as that in [11] (Example 4 in [11]), where $\Sigma _{0} = \{ a,b,c\}$, $\Sigma _{f}^{i} = \{ \sigma_{f} \}$ and $\Gamma _{i} = \{ c\}$. In [11], it is proved that $G_{ 2}$ is safe diagnosable. Next, we verify the result by using the methods proposed in this paper.

Fig. 5

System $G_{2}$

Similar to Example 1, the safe verifier $G_{v 2}$ is constructed as that shown in Fig. 6. Note that $G_{v2}$ satisfies the conditions of Theorem 1. Therefore, we conclude $G_{2}$ being safe diagnosable, which coincides with the result obtained in [11].

Fig. 6

Safe verifier $G_{v2}$

5 Conclusion

Motivated by the fact that the complexity of constructing safe diagnosers to deal with safe diagnosability of stochastic DESs in [11] is exponential, a new algorithm is proposed by constructing the safe verifier to realize safe diagnosis of stochastic DESs, which is polynomial-time in the number of states and events of the system.