Fault Diagnosis of Discrete-Event Systems under
Non-Deterministic Observations with Output Fairness

Let $\Sigma$ be a finite set of events. A finite (infinite) string over $\Sigma$ is a finite (infinite) sequence of events in $\Sigma$ of form $s=\sigma_{1}\sigma_{2}\dots\sigma_{n}(\dots)$, where $\sigma_{i}\in\Sigma$, for $i=1,\cdots,n$. A finite (infinite) language is a set of finite (infinite) strings. We denote by $\Sigma^{*}$ and $\Sigma^{\omega}$, respectively, the set of all finite and the set of all infinite strings over $\Sigma$. Note that the empty string, denoted by $\varepsilon$, is included in $\Sigma^{*}$. Given a finite language $L\subseteq\Sigma^{*}$, the prefix-closure of $L$ is defined by $\textsf{Pre}(L)=\{w\in\Sigma^{*}:\exists t\in\Sigma^{*}\text{ s.t. }wt\in L\}$. Similarly, for an infinite language $L\subseteq\Sigma^{\omega}$, its prefix-closure is the set of all its finite prefixes, i.e., $\textsf{Pre}(L)=\{w\in\Sigma^{*}:\exists t\in\Sigma^{\omega}\text{ s.t. }wt\in L\}$. For any string $s\in\Sigma^{*}\cup\Sigma^{\omega}$, we write $\textsf{Pre}(\{s\})$ as $\textsf{Pre}(s)$ for the sake of simplicity. Given an infinite string $s\in\Sigma^{\omega}$, $\textsf{Inf}(s)$ denotes the set of events that appear infinitely number of times in the string.

In this paper, we consider DES modeled by a deterministic finite-state automaton (DFA) $G=(Q,\Sigma,f,q_{0})$, where $Q$ is the finite set of states; $\Sigma$ is the finite set of events; $f:Q\times\Sigma\to Q$ is the partial transition function; and $q_{0}\in Q$ is the initial state. The transition function $f$ can be extended to $f:Q\times\Sigma^{*}\to Q$ recursively in the usual manner; see, e.g., [7]. The finite language generated by $G$ is defined by $\mathcal{L}(G)=\{s\in\Sigma^{*}:f(q_{0},s)!\}$, where “!” means “is defined”, and the infinite language generated by $G$ is defined by $\mathcal{L}^{\omega}(G)=\{s\in\Sigma^{\omega}:f(q_{0},s)!\}$. We assume that system $G$ is live, i.e., $\forall q\in Q,\exists\sigma:f(q,\sigma)!$.

In the partial observation setting, it is assumed that the occurrence of each event cannot be observed directly or perfectly. A commonly adopted simple approach is to partition the event set $\Sigma$ into observable events $\Sigma_{o}$ and unobservable events $\Sigma_{uo}$. Then natural projection $P:\Sigma^{*}\to\Sigma_{o}^{*}$ can be used to capture the issue of partial observability.

In many real-world scenarios, however, the sensor readings may be non-deterministic due to observation noises, sensor failures or malicious attacks. Furthermore, the sensor reading of the event occurrence can be state-dependent. To this end, more complicated observation models have been proposed in the literature. Here, we adopt state-dependent non-deterministic observation model proposed by [17, 18], which captures both state-dependency and non-determinism of observations.

Formally, we assume that $\Delta$ is a new set of all possible observations or output symbols. Then a state-dependent non-deterministic output function is

$$\mathcal{O}:Q\times\Sigma\to 2^{\Delta_{\varepsilon}},$$

where $\Delta_{\varepsilon}=\Delta\cup\{\varepsilon\}$. Intuitively, this output function means that if event $\sigma\in\Sigma$ occurs at state $q\in Q$, then the system is possible to observe any symbol in $\mathcal{O}(q,\sigma)$ non-deterministically.

Based on the output function $\mathcal{O}:Q\times\Sigma\to 2^{\Delta_{\varepsilon}}$, we can define a non-deterministic observation mapping $M:\mathcal{L}(G)\to 2^{\Delta^{*}}$, where $\Delta^{*}$ is the set of finite strings over $\Delta$ and we have $\varepsilon\in\Delta^{*}$, recursively as:

• •

  $M(\varepsilon)=\{\varepsilon\}$;

• •

  for any $s\in\Sigma^{*}$ and $\sigma\in\Sigma$, we have

  $$M(s\sigma)=\{\alpha\beta\!\in\!\Delta^{*}:\alpha\!\in\!M(s)\wedge\beta\in\mathcal{O}(f(q_{0},s),\sigma)\}$$

Intuitively, $M(s)\in\Delta^{*}$ is the set of all possible observations (or output strings) upon the occurrence of internal string $s\in\Sigma^{*}$. The observation mapping is also extended to $M:2^{\Sigma^{*}}\to 2^{\Delta^{*}}$ by: for any language $L\subseteq\mathcal{L}(G)$, $M(L)=\cup_{s\in L}M(s)$.

Since the observation is non-deterministic, for any specific internal string $s\in\mathcal{L}(G)$, it may have different output realizations. To “embed” the actual observation occurred into the internal execution of the system, we define

$$\Sigma_{e}=Q\times\Sigma\times\Delta_{\varepsilon}$$

as the set of extended events. Then an extended string is a finite or infinite sequence of extended events. We say a finite extended string

$$s=(q_{0},\sigma_{0},\delta_{0})(q_{1},\sigma_{1},\delta_{1})\dots(q_{n},\sigma_{n},\delta_{n})\in\Sigma_{e}^{*}$$

is generated by $G$ if $f(q_{i},\sigma_{i})=q_{i+1},\forall i<n$ and $\delta_{i}\in\mathcal{O}(q_{i},\sigma_{i}),\forall i\leq n$. We denote by $\mathcal{L}_{e}(G)$ the set of all finite extended strings generated by $G$. The infinite extended strings are defined analogously and the set of all infinite extended strings generated by $G$ is denoted by $\mathcal{L}^{\omega}_{e}(G)$.

For any extended string $s=(q_{0},\sigma_{0},\delta_{0})(q_{1},\sigma_{1},\delta_{1})\cdots$, we define $\Theta_{Q}(s)=q_{0}q_{1}\cdots,\Theta_{\Sigma}(s)=\sigma_{0}\sigma_{1}\cdots$ and $\Theta_{\Delta}(s)=\delta_{0}\delta_{1}\cdots$ as its corresponding state sequence, (internal) event string and output string, respectively. Clearly, for any $s\in\mathcal{L}_{e}(G)$, we have $\Theta_{\Delta}(s)\in M(\Theta_{\Sigma}(s))$ because $\Theta_{\Delta}(s)$ is a specific observation realization of internal string $\Theta_{\Sigma}(s)$.

In this work, we assume that the system is subject to faults whose occurrences need to be diagnosed within a finite number of steps. Specifically, we assume that $\Sigma_{F}\subset\Sigma$ is the set of fault events. For the sake of simplicity, we do not distinguish among different fault types. We say a string $s\in\Sigma^{*}\cup\Sigma^{\omega}$ is faulty if some event in $\Sigma_{F}$ appears in $s$ and we write $\Sigma_{F}\in s$ with a slight abuse of notation; otherwise, it is normal. We define $\mathcal{L}_{F}(G)$ and $\mathcal{L}_{F}^{\omega}(G)$ as the sets of all finite and infinite faulty strings generated by $G$, respectively. Similarly, we define $\Sigma_{e,F}=Q\times\Sigma_{F}\times\Delta^{\varepsilon}$ as the set of extended fault events and denote by $\mathcal{L}_{e,F}(G)=\{s\in\mathcal{L}_{e}(G):\Sigma_{e,F}\in s\}$ the set of all finite extended faulty strings generated by $G$; the extended infinite faulty language $\mathcal{L}_{e,F}^{\omega}(G)$ is also defined analogously. Finally, we define $\Psi_{e}(G)$ as the set of all finite extended faulty strings in which fault events occur for the first time, i.e.,

$\displaystyle\Psi_{e}(G)=\{s\in\mathcal{L}_{e,F}(G):\forall t\in\textsf{Pre}(s)\setminus\{s\},\Sigma_{e,F}\notin t\}.$

To capture whether or not the occurrences of fault events can be detected within a finite number of steps, the notion of diagnosability (under non-deterministic observations) has been proposed in the literature [17].

Intuitively, the above definition says that, for any faulty extended string in which fault events appear for the first time, there exists a finite detection bound such that, for any of its continuation longer than the detection bound, any other extended strings having the same observation must also contain fault events. Note that we consider extended strings rather than the internal strings in order to capture the issue of non-deterministic observations.

As we discussed in Remark 1, the non-deterministic output function can be used to capture the issue of intermittent loss of observations. Here, however, we argue that the original definition of diagnosability in Definition 1 may be too strong for the case of intermittent loss of observations.

To see this, we still consider system $G_{1}$ shown in Figure 1, where the reliable event set is $\{a\}$, the unreliable events set is $\{b,c\}$ and the unobservable event set is $\{\sigma_{\!f},u\}$. As we have discussed in Example 2, this system is not diagnosable because there are two infinite extended strings:

• •

  one is faulty $s_{F}=(1,\sigma_{\!f},\varepsilon)[(2,a,a)(3,b,b)(4,c,\varepsilon)]^{\omega}$;

• •

  the other is non-faulty $s_{N}=(1,u,\varepsilon)[(5,a,a)(6,b,b)]^{\omega}$

and they have the same observation, i.e., $\Theta_{\Delta}(s_{1})=\Theta_{\Delta}(s_{2})$ $=(ab)^{\omega}$. As a result, the occurrence of fault in string $s_{F}$ can never be detected within a finite number of steps.

Note that, the existence of above extended string $s_{F}$ is due to the following physical scenario: the infinite internal string $\sigma_{\!f}(abc)^{\omega}$ is executed, i.e., the system loops forever in the cycle formed by states $2,3$ and $4$, and each time when event $c$ is executed at state $4$, the sensor reads $\varepsilon$ due to observation loss. In other words, the sensor corresponds to transition $4\xrightarrow{c}$ has to fail permanently in order to draw the conclusion that the system is not diagnosable. However, this source of non-diagnosability seems violate the setting of intermittent loss of observations. In the context of intermittent loss of observations or non-deterministic observations, it makes more sense to assume that each possible observation is eventually possible. Therefore, if event $c$ at state $4$ corresponds to a sensor that may be unreliable but will not fail permanently, then along the infinite loop of $\sigma_{\!f}(abc)^{\omega}$, once one has a single chance to observe output $c$ for transition $4\xrightarrow{c}$, it will conclude immediately that fault events have occurred.

The above discussion suggests that the exiting definition of diagnosability under non-deterministic observations is a bit strong than its underlying physical setting because it includes the situation where some output symbols are disabled permanently. In order to bridge this discrepancy between the definition of diagnosability and the physical meaning of non-deterministic observations, in this work, we put an additional fairness assumption on those sensors that are subject to intermittent loss of observations, or non-deterministic observations in a broad sense. Specifically, we assume that $\Delta^{\prime}\subseteq\Delta$ is a set of “fair” output symbols in the sense that if they have infinite opportunities to occur, then they will indeed occur infinite number of times.

In order to formalize this fairness requirement, we use the linear temporal logic (LTL) formulas. Formally, an LTL formula $\varphi$ is constructed based on a set of atomic propositions $\mathcal{AP}$, Boolean operators and temporal operators as follows:

$$\varphi::=true\ |\ p\ |\ \varphi_{1}\wedge\varphi_{2}\ |\ \neg\varphi\ |\ \bigcirc\varphi\ |\ \varphi_{1}U\varphi_{2},$$

where $p\in\mathcal{AP}$ is an atomic proposition; $\bigcirc$ and $U$ denote “next” and “until”, respectively. Other Boolean connectives can be induced by $\wedge$ and $\neg$, e.g., $\varphi_{1}\vee\varphi_{2}=\neg(\neg\varphi_{1}\wedge\neg\varphi_{2})$ and $\varphi_{1}\rightarrow\varphi_{2}=\neg\varphi_{1}\vee\varphi_{2}$. Temporal operators $\Box$ “always” and $\lozenge$ “eventually” can be induced by until operator, i.e., $\lozenge\varphi=trueU\varphi$ and $\Box\varphi=\neg\lozenge\neg\varphi$. LTL formulas are evaluated over infinite sequences of atomic proposition sets (called words). For any infinite word $s\in(2^{\mathcal{AP}})^{\omega}$, we denote by $s\models\varphi$ if it satisfies LTL formula $\varphi$. The reader is referred to [1] for more details on the semantics of LTL.

In our context of non-deterministic observations, we choose extended events as atomic propositions, i.e., $\mathcal{AP}=\Sigma_{e}$. For the sake of simplicity, each extended event $(q,\sigma,\delta)$ will also be written as $\sigma_{q}^{\delta}$ meaning that event $\sigma$ occurs at state $q$ and generates observation $\delta$. For simplicity, we define

$$\sigma_{q}:=\bigvee_{\delta\in\mathcal{O}(\sigma,q)}\sigma_{q}^{\delta}$$

as the proposition formula meaning that transition $q\xrightarrow{\sigma}$ occurs no matter what output it generates. Then we introduce the notion of $\Delta^{\prime}$-fairness as follows.

The above subset of outputs $\Delta^{\prime}\subseteq\Delta_{\varepsilon}$ is referred to as the fair outputs meaning that these outputs will always have the opportunity to be measured. Specifically, this requirement is captured by formula $\varphi_{fair}$ saying that, for any transition $q\xrightarrow{\sigma}$, if it is fired infinite number of times, then any of its fair outputs, i.e., $\sigma\in\Delta^{\prime}\cap\mathcal{O}(q,\sigma)$, can actually be observed infinite number of times. This excludes the case where some fair outputs are disabled permanently. We define

$$\mathcal{L}_{e}^{\varphi}(G)=\{s\in\mathcal{L}^{\omega}_{e}(G):s\models\varphi_{fair}\}$$

as the set of infinite extended strings generated by $G$ satisfying $\varphi_{fair}$. We also define $\mathcal{L}^{\varphi}_{e,F}(G)=\mathcal{L}^{\varphi}_{e}(G)\cap\mathcal{L}_{e,F}^{\omega}(G)$ as the set of infinite faulty extended strings satisfying $\varphi_{fair}$.

Based on the above notion of $\Delta^{\prime}$-fairness on extended strings, now we modify the existing definition of diagnosability as shown in Definition 1 to the output-fair diagnosability (OF-diagnosability) defined as follows.

Intuitively, OF-diagnosability revises the standard diagnosability by restricting our attention only to those infinite extended strings satisfying the fairness assumption and investigates whether or not faults in those “output-fair” strings can be detected.

We show that the proposed notion of a OF-diagnosability provides the necessary and sufficient condition for the existence of diagnoser that works “correctly” under the $\Delta^{\prime}$-fairness assumption. Formally, a diagnoser is a function

$$D:M(\mathcal{L}(G))\to\{0,1\}$$

that decides whether a fault has happened (by issuing “$1$”) or not (by issuing “$0$”) based on the output string. We say that a diagnoser works correctly under the $\Delta^{\prime}$-fairness assumption if it satisfies the following conditions:

1. C1)

   By assuming that each fair-output will actually be observed infinitely if they have infinite chances to be observed, the diagnoser will issue a fault alarm for any occurrence of fault events, i.e.,

   $$(\forall s\in\mathcal{L}^{\varphi}_{e,F}(G))(\exists s^{\prime}\in\textsf{Pre}(s)))[D(\Theta_{\Delta}(s^{\prime}))=1].$$

2. C2)

   The diagnoser will not issue a false alarm if the execution is still normal, i.e.,

   $$(\forall s\in\mathcal{L}_{e}(G):\Sigma_{e,F}\notin s)[D(\Theta_{\Delta}(s))=0].$$

The following theorem says that there exists a diagnoser working “correctly” under the $\Delta^{\prime}$-fairness assumption if and only if the system is OF-diagnosable.

We use the following examples to illustrate the concept of output fairness as well as the notion of OF-diagnosability.

To verify OF-diagnosability, our first step is to augment both the state-space and the event-space of $G$ such that

• •

  the information of whether or not a fault event has occurred is encoded in the augmented state-space; and

• •

  the information of where the event occurs and which specific output is observed are encoded in the augmented event-space.

Formally, given system $G=(Q,q_{0},\Sigma,f)$, fault events $\Sigma_{F}$ and output function $\mathcal{O}$, we define the augmented system as a new DFA

$$\tilde{G}=(\tilde{Q},\tilde{q}_{0},\Sigma_{e},\tilde{f}),$$

(5)

where

• •

  $\tilde{Q}\subseteq Q\times\{F,N\}$ is the set of augmented states;

• •

  $\tilde{q}_{0}=(q_{0},N)$ is the initial augmented state;

• •

  $\Sigma_{e}$ is the set of augmented events, which are just extended events;

• •

  $\tilde{f}:\tilde{Q}\times\Sigma_{e}\rightarrow\tilde{Q}$ is the transition function defined by: for any $\tilde{q}=(q,l)\in\tilde{Q}$ and $\tilde{\sigma}=(q,\sigma,\delta)\in\Sigma_{e}$, we have $\tilde{f}(\tilde{q},\tilde{\sigma})!$ if $f(q,\sigma)!$ and $\delta\in\mathcal{O}(q,\sigma)$. Furthermore, when $\tilde{f}(\tilde{q},\tilde{\sigma})!$, we have

  $$\tilde{f}(\tilde{q},\tilde{\sigma})=\left\{\begin{array}[]{l l}(f(q,\sigma),N)&\text{ if }l=N\wedge\tilde{\sigma}\!\notin\!\Sigma_{e,F}\\ (f(q,\sigma),F)&\text{ otherwise }\end{array}\right..$$

The above constructed augmented system $\tilde{G}$ has the following properties:

• •

  First, the augmented system $\tilde{G}$ generates extended strings. Essentially, it still tracks the original dynamic of the system by putting both the output realization and the current state information together with the internal event. Therefore, we have

  $$\mathcal{L}(\tilde{G})=\mathcal{L}_{e}(G)\text{ and }\mathcal{L}^{\omega}(\tilde{G})=\mathcal{L}_{e}^{\omega}(G).$$

• •

  Second, each augmented state $(q,l)\in Q\times\{F,N\}=\tilde{Q}$ has two components. The first component $q$ is the actual state in the original system $G$ and the second component $l\in\{N,F\}$ is a label denoting whether fault events have occurred. By the construction, the label will change from $N$ to $F$ only when an extended fault event occurs and once the label becomes $F$, it will be $F$ forever. We denote by $\tilde{Q}_{N}=\{(q,l)\in\tilde{Q}:l=N\}$ the set of normal augmented states and the set of faulty states $\tilde{Q}_{F}$ is defined analogously.

Let $r\in 2^{\tilde{Q}}$ be a set of states representing the current state estimation of the augmented system. By observing a new output symbol $\delta\in\Delta$, the estimate is updated by the following observable reach

$$\textsf{Next}(r,\delta)=\left\{\tilde{q}^{\prime}\in\tilde{Q}:\!\!\!\begin{array}[]{cc}\exists\tilde{q}\in r,\tilde{\sigma}\in\Sigma_{e}\text{ s.t }\\ \Theta_{\Delta}(\tilde{\sigma})\!=\!\delta\wedge\tilde{q}^{\prime}\!=\!\tilde{f}(\tilde{q},\tilde{\sigma})\end{array}\right\}.$$

Also, the system can execute silently without generating an output symbol. This is captured by the unobservable reach defined by:

$$\textsf{UR}(r)=\left\{\tilde{q}^{\prime}\in\tilde{Q}:\!\!\!\begin{array}[]{cc}\exists\tilde{q}\in r,s\in\Sigma_{e}^{*}\text{ s.t }\\ \Theta_{\Delta}(s)\!=\!\varepsilon\wedge\tilde{q}^{\prime}\!=\!\tilde{f}(\tilde{q},s)\end{array}\right\}.$$

Now, based on the augmented system $\tilde{G}=(\tilde{Q},\tilde{q}_{0},\tilde{\Sigma},\tilde{f})$, we construct the verification structure as follows:

$$V=(Q_{V},q_{V}^{0},\Sigma_{V},f_{V})$$

(6)

where

• •

  $Q_{V}\subseteq\tilde{Q}\times 2^{\tilde{Q}}$ is the set of states;

• •

  $q_{V}^{0}=(\tilde{q}_{0},\textsf{UR}(\{\tilde{q}_{0}\}))$ is the initial state;

• •

  $\Sigma_{V}=\Sigma_{e}$ is the event set, which is just the set of extended events;

• •

  $f_{V}:Q_{V}\times\Sigma_{V}\rightarrow Q_{V}$ is the transition function defined by: for any $(\tilde{q},r)\in\tilde{Q}\times 2^{\tilde{Q}}$ and $\tilde{\sigma}\in\Sigma_{V}$, we have

  $$f_{V}((\tilde{q},r),\tilde{\sigma})=\left\{\!\!\begin{array}[]{l l}(\tilde{q}^{\prime},r)&\text{if }\Theta_{\Delta}(\tilde{\sigma})=\varepsilon\\ (\tilde{q}^{\prime},r^{\prime})&\text{if }\Theta_{\Delta}(\tilde{\sigma})\in\Delta\end{array}\right.$$

  where $\tilde{q}^{\prime}=\tilde{f}(\tilde{q},\tilde{\sigma})$ and $r^{\prime}=\textsf{UR}(\textsf{Next}(r,\Theta_{\Delta}(\tilde{\sigma})))$.

Intuitively, each state $(\tilde{q},r)$ in the verification structure $V$ has two components. The first component $\tilde{q}\in\tilde{Q}$ tracks the current (augmented) state in $\tilde{G}$. Therefore, the transition of the first part is consistent with $\tilde{f}$. As a result, we also have

$$\mathcal{L}(V)=\mathcal{L}(\tilde{G})=\mathcal{L}_{e}(G)$$

and the same for the generated infinite language. On the other hand, the second component $r\in 2^{\tilde{Q}}$ captures the current state estimation of system $\tilde{G}$. Therefore, this component is updated only when a new output symbol is generated, i.e., $\Theta_{\Delta}(\tilde{\sigma})\in\Delta$. Furthermore, if it is updated, then it first updates the estimate by the observable reach to compute the set of state that can be reached immediately following the output. Also, we need to include all states that can be reached silently by using the unobservable reach. Essentially, we can image $V$ as the synchronization of the augmented system $\tilde{G}$ and its current-state estimate under the non-deterministic observation setting.

For any state $(\tilde{q},r)\in Q_{V}$ in $V$, we say the state is

• •

  certain if $\tilde{q}\in\tilde{Q}_{F}$ and $r\subseteq\tilde{Q}_{F}$;

• •

  uncertain if $\tilde{q}\in\tilde{Q}_{F}$ and $r\cap\tilde{Q}_{N}\neq\emptyset$.

We denote by $Q_{V}^{cer}$ and $Q_{V}^{unc}$ the set of certain states and uncertain states in $V$, respectively. Then for any string $s\in\mathcal{L}(V)$, based on the definition of uncertain and certain states, we have following properties:

• •

  For any faulty extended string $s\in\mathcal{L}(V)=\mathcal{L}_{e}(G)$, there exists a normal extended string $s^{\prime}\in\mathcal{L}_{e}(G)$ such that $\Theta_{\Delta}(s)=\Theta_{\Delta}(s^{\prime})$ if and only if $f_{V}(q_{V}^{0},s)\in Q_{V}^{unc}$.

• •

  For any faulty extended string $s\in\mathcal{L}(V)=\mathcal{L}_{e}(G)$, if $f_{V}(q_{V}^{0},s)\in Q_{V}^{cer}$, then for any of its continuation $st\in\mathcal{L}(V)$, we have $f_{V}(q_{V}^{0},st)\in Q_{V}^{cer}$.

Now we investigate the verification of OF-diagnosability. According to Definition 2, a system is not OF-diagnosable if and only if there exists an infinite extended faulty string satisfying the $\Delta^{\prime}$-fairness assumption but all states in $V$ reached along the string are uncertain. Then, since the systems is finite, only loops can generate infinite strings. This leads to the definition of fairly uncertain loop (FU-loop).

Formally, given the verification structure $V$, we define a run in $V$ as a finite sequence

$$\pi=q_{V}^{1}\xrightarrow{\sigma_{V}^{1}}q_{V}^{2}\xrightarrow{\sigma_{V}^{2}}\cdots\xrightarrow{\sigma_{V}^{n-1}}q_{V}^{n}$$

where $q_{V}^{1},\cdots,q_{V}^{n}\in Q_{V},\sigma_{V}^{1},\cdots,\sigma_{V}^{n}\in\Sigma_{V}$ and $q_{V}^{i+1}=f_{V}(q_{V}^{i},\sigma_{V}^{i}),i=1,\dots,n-1$. A run of the above form is called a loop if $q_{V}^{1}=q_{V}^{n}$.

Then given a loop $\pi=q_{V}^{1}\xrightarrow{\sigma_{V}^{1}}q_{V}^{2}\cdots\xrightarrow{\sigma_{V}^{n-1}}q_{V}^{n}$ in the verification structure, where $\sigma_{V}^{i}=(q^{i},\sigma^{i},\delta^{i})$, we say $\pi$ is

• •

  fair if for each transition that occurs in the loop, any of its fair output symbols must occur in the loop associating with the same transition, i.e.,

  	$\displaystyle(\forall i\in\{1,\cdots,n\})(\forall\delta\in\mathcal{O}(q^{i},\sigma^{i})\cap\Delta^{\prime})$
  	$\displaystyle(\exists j\in\{1,\cdots,n\})[(q^{j},\sigma^{j})\!=\!(q^{i},\sigma^{i})\wedge\delta^{j}\!=\!\delta]$

• •

  uncertainty if all states in the loop are uncertain, i.e.,

  $$\forall i\in\{1,\cdots,n\}:q_{V}^{i}\in Q_{V}^{unc}$$

• •

  reachable if there exists a finite string $s\in\mathcal{L}(V)$ such that $f_{V}(q_{V}^{0},s)=q_{V}^{1}$.

Clearly, by properties of the verification structure, we know that an uncertain loop will only be reached by faulty strings. Furthermore, if some state in a loop is uncertain, then all states in it are uncertain.

In the following two lemmas, we formally establish the relationship between strings satisfying the $\Delta^{\prime}$-fairness assumption and fair loops, according to the structure characteristics of $\Delta^{\prime}$-fairness assumption. Due to space constraint, their proofs are omitted here and are available in [sup-material].

First, we show that, for any reachable fair loop, it can generate an infinite extended string string satisfying the $\Delta^{\prime}$-fairness assumption.

On the other hand, given an infinite extended string satisfying $\varphi_{fair}$, it will also induce a fair loop.

Based on Lemmas 1 and 2, we obtain the following main result, which shows that, to check OF-diagnosability, it suffices to check the existence of a reachable fair and uncertain loop (FU-loop) in the verification structure $V$.