Diagnosability of Discrete-Event Systems with Uncertain Observations

1 Introduction

A DES is a conceptual model of a dynamical system, where the system behavior is described by transitions over a finite set of states and each transition is associated with an event out of a finite set of events [Cassandras and Lafortune, 2008]. Model-based diagnosis of DESs is a task that takes as input the DES model of a (natural or man-made) system along with a relevant observation and produces as output a diagnosis, i.e. some pieces of information explaining whether what has been observed is consistent either with a normal behavior or an abnormal one. There are several notions of diagnosis of DESs in the literature featuring different levels of abstraction. According to a common notion, the diagnosis of a DES is a set of candidates, each candidate being a set of faults, where a fault is an undesired state transition. The definition of a candidate requires that the faults included in a candidate are consistent with both the DES model and the given observation. However, distinct candidates may bring conflicting information. This is the case, for instance, when according to a candidate the system is free of faults while according to another it is affected by faults. A DES that is repeatedly diagnosed while it is being monitored (that is, a new set of candidates is produced every time a new observable event is processed) is diagnosable if such ambiguity can be removed once a finite sequence of observable events have taken place. Diagnosability is very desirable and system designers often want to enforce it.

DES diagnosability was introduced by the diagnoser approach [Sampath et al., 1995], where a necessary and sufficient condition is proposed to check diagnosability based on the construction of a so-called diagnoser. The problem of deciding diagnosability was then proved to be polynomial by using the twin plant method [Jiang et al., 2001]. Similar approaches to diagnosability checking can be found in [Yoo and Lafortune, 2002; Cimatti et al., 2003]. Recently, there has been an increasing interest in applying DES techniques to the diagnosability analysis of hybrid systems [Bayoudh and Travé-Massuyès, 2014]. Existing works are focused on how to verify the intrinsic diagnosability of a DES and assume that candidates are computed by an exact diagnostic algorithm that takes as input a completely certain observation. Exceptions include diagnosability under imperfect conditions for modular structures [Contant et al., 2006], decentralised analysis [Sengupta and Tripakis, 2004], and approximate diagnosers [Su and Grastien, 2014]. As remarked in this latest paper, the diagnosability property can be exhibited even when some incomplete or approximate diagnostic algorithms are used, i.e. algorithms that do not perform a complete search of the behavioral space of the DES. However, this work still relies on a completely certain observation while in the real world the observation may be uncertain, as remarked by some contributions on diagnosis of DESs [Lamperti and Zanella, 2002; Grastien et al., 2007]. In a broader perspective, one can see that the ability to remove ambiguities in candidates depends not only on the DES and the diagnostic algorithm at hand but also on the available observations.

This paper investigates whether the ability to disambiguate DES candidates, i.e. the diagnosability property, holds for a diagnosable system with uncertain observations. The uncertainty is measured by a parameter, which allows to study the level of noise that can affect the observation without impacting the performance of diagnosis. The remaining of this paper is organized as follows. The next section presents the relevant literature review on DES diagnosability. Section 3 introduces uncertain observations along with the notions of compound observable event and uncertainty measure. Section 4 extends the original definition of DES diagnosability to the case when an uncertain observation is considered. It also extends the twin plant method so as to check diagnosability of DESs with uncertain observations. Finally, Section 5 draws conclusions and hints at directions for future research.

2 Background

A DES diagnosis problem consists in a DES D and a (finite) observation O, the latter representing what has been observed while D was running during a time interval of interest.

2.1 Discrete Event Systems

A (partially observable) DES D is a 4-tuple (⌃↪ L↪ obs↪ flt), where ⌃ is the finite set of events that can take place in the system; L ✓ ⌃⇤ is the behavior space, which is a prefixclosed and live, i.e. deadlock-free, language that models all (and only) the possible sequences of events, or traces, that can take place in the system. Function obs associates each trace ⌧ with an observation obs(⌧ ) 2 ⌃⇤o and is defined as the projection of ⌧ on the subset ⌃o ✓ ⌃ of observable events, i.e. obs(⌧) is a copy of ⌧, where all non-observable events have been removed. The length of the sequence of events in obs(⌧) is denoted ♣obs(⌧)♣. obs(L) is the prefix-closed and live observable language relevant to L 1 . The set of unobservable faulty events, or faults, is denoted as ⌃f , where ⌃f ✓ ⌃ ∩ ⌃o. Function flt associates each trace ⌧ with the sequence flt(⌧) 2 ⌃⇤f of faulty events that appear in the trace itself.

Language L of DES D = (⌃↪ L↪ obs↪ flt) can be represented by a finite automaton (FA) G = (X↪ ⌃↪ δ↪ x0), called the behavioral model, where X is the set of states and δ ✓ X ⇥⌃⇥X is the set of state transitions. Each x 2 X represents a state that D can be in and each triple (x↪ σ↪ x0 ) 2 δ represents a possible state change. State x0 2 X is the initial one, i.e. the state of the system at the moment when we have started to observe its evolution. A path in automaton G is a sequence of transitions starting from the initial state, concisely represented as x0 σ1 -! x1 σ2 -! · · · σn --! xn, where n ≥ 1. A trace is a projection of a path on ⌃, e.g. σ1▷ · · · ▷ σn. Figure 1 displays the behavioral model G of a DES D that will be used as a running example throughout this paper. Such a model encompasses one faulty event f, another unobservable event u, and seven observable events (a-e, g, and h). A possible path is 0 h-! 8 g-! 9 e-! 3 f-! 4 c-! 4, corresponding to the trace h▷ g▷ e▷ f▷ c, where ▷ is the concatenation operator.

Given a diagnosis problem (D↪O), a diagnosis candidate is a pair (x↪ ') 2 X ⇥ 2⌃f , where x represents the state that system D has reached by a path generating O and ' represents the set of faults of this path. The diagnosis is the set of all the candidates relevant to the diagnosis problem (D↪O). The diagnosis relevant to our sample system D in Figure 1 and observation O = h▷ g▷ e▷ c is ¶(4↪ ¶f♦)♦. Such a diagnosis consists of just one candidate, meaning that, once observation O has been perceived, the state of D is certainly 4 and fault f has necessarily occurred.

1 Note that the fact that L is assumed to be live does not imply that obs(L) is live. However, following the diagnoser approach [Sampath et al., 1995], we also assume that obs(L) is live.

2.2 Diagnosability

Following [Sampath et al., 1995], a DES D exhibits the diagnosability property as far as a fault f 2 ⌃f is concerned if the occurrence of such a fault can always be detected and isolated without any ambiguity once a finite sequence of observable events has been recorded. Given an observation, an exact diagnostic algorithm is able to draw all the sets of faults relevant to all the traces consistent with such an observation. If, for whichever path that has preceded the occurrence of the fault, and for whichever sequence of transitions (generating k observable events) that has followed it, all the traces that are consistent with such an observation include the fault, then such a fault is certain (and it is said to be diagnosable) as it belongs to the intersection of all the candidate sets of faults. The system is said to be diagnosable if all its faults are diagnosable. We denote Lf = (⌃⇤ f⌃⇤ ) \ L the set of traces that include fault f and ¯ Lf = (⌃⇤ f)\L the set of traces that end with fault f.

Definition 1 (Diagnosability [Sampath et al., 1995]). Given a DES D = (⌃↪ L↪ obs↪ flt) whose set of faults is ⌃f ✓ ⌃, a fault f 2 ⌃f is diagnosable if

SystemD is diagnosable if all its faults are diagnosable.

DES D of our example in Figure 1 is diagnosable with k = 1 since the occurrence of fault f is precisely detected once the occurrence of observable event c has been perceived immediately after having perceived either b or h▷ g▷ e. One can appreciate that such a notion of diagnosability relies on the function obs, which provides the sequence of observable events that have occurred in the system during its evolution, where such a sequence reflects the chronological order of the occurrence of events within a trace. The above definition of diagnosability implicitly assumes that, if a DES follows a trace u, the observation O processed by the diagnostic engine equals obs(u). An observation like this is certain.

3 Temporal and Logical Uncertainty of Observations

In the literature, diagnosability has so far been confined to certain observations. However, observation are uncertain in many applications. We present two types of uncertainties, i.e. temporal and logical, and for each of them, a measure of how uncertain the observation is. These measures are by no means the only ones possible.

3.1 Temporally Uncertain Observations

In observation O = h▷ g▷ e▷ c used above, the occurrence order of the observable events is known. This observation is depicted in the top graph of Figure 2, where the order is represented by the arrows between observed events. Implicit arrows, e.g. from h to e, are not displayed. We say that the observation is temporally certain. However, the temporal order of the observable events that have occurred within the DES is not always known, in particular when they occur in a short time span. The bottom graph of Figure 2 shows a temporally uncertain observation O0 , where the order between observable events g and e is unknown. Since we do not know which sequence, i.e. either h▷ g▷ e▷ c or h▷ e▷ g▷ c, actually occurred, an exact diagnostic algorithm has to consider both of them. The pair of observable events e and g can altogether be considered as a temporally compound event e◁◁g, which cumulatively represents both sequences e▷ g and g▷ e. We can describe the uncertain observation as a sequence O0 = h▷ e◁◁g▷ c.

Definition 2 (Temporally compound observable event). A temporally compound observable event of level ` (with ` ≥ 1) is a multiset of ` reciprocally temporally unrelated instances of observable events. When ` > 1, not all the ` instances are identical. A temporally compound event of level 1 is a single observable event.

We use ✓✓⌃o k ◆◆ and ✓✓ ⌃o k◆◆ to denote the collection of multisets of ⌃o of cardinality k and of cardinality k or less, respectively. Notice that ✓✓ ⌃o k◆◆ = Sik ✓✓⌃o i ◆◆. Although a temporally compound event is univocally identified by writing the values of all the instances that it includes, independently of their order, using ◁◁ as a separator, we put such values in alphabetical order in this paper.

Definition 3 (Temporal uncertainty level). A temporally uncertain observation is a sequence of temporally compound observable events. The temporal uncertainty level of a temporally uncertain observation O is the maximum level of the compound observable events that O includes.

The lowest temporal uncertainty level of an observation is 1 corresponding to a certain observation. The temporal uncertainty level of the observation in the bottom graph of Figure 2 instead is 2, since events e and g are reciprocally temporally unrelated. Notice that the temporally uncertain observations defined above do not encompass all the temporally uncertain observations as defined in [Lamperti and Zanella, 2002]. However, the class of temporally uncertain observation we are addressing is meaningful. If an exact diagnostic algorithm is adopted to diagnose a DES in a monitoring context, the diagnosis output is monotonic [Lamperti and Zanella, 2011] for whichever temporally uncertain observation that is a sequence of temporally compound events, provided that a new set of candidates is output only after all the observable events in a temporally compound event have been processed.

3.2 Logically Uncertain Observations

A temporally uncertain observation is a certain observation, where some temporal constraints have been relaxed. Similarly, a logically uncertain observation is a logical relaxation of a certain one. The so-called logical content [Lamperti and Zanella, 2002] of an observed event is its (discrete) value. If such a value is not known with certainty, the relevant observation is logically uncertain.

Figure 3 shows a logically uncertain observation, where the logical uncertainty comes from the fact that i) the first observed event is not known with certainty, i.e. it could be either e or h, and ii) whether the third observed event (e) actually occurred is not certain, which is represented by ". Since we do not know which sequence (either h▷ g▷ e▷ c or h▷ g▷ c or e▷ g▷ e▷ c or e▷ g▷ c) actually occurred, an exact diagnostic algorithm has to consider all of them.

Because logically uncertain observations may include ", we use the notation ⌃o+ = ⌃o [ ¶"♦. We define a logically compound observable event as a set of events belonging to ⌃o+. The degree of this compound event, tantamount to the level of a temporally compound observable event, is here defined as the maximal distance according to a specified distance matrix (increased by 1 for normalization) between any pair of events included in the compound event.

Definition 4 (Distance matrix and logically compound observable event). The distance matrix M is a map that associates any pair in ⌃o ⇥ ⌃o+ with a (possibly infinite) non-negative integer while respecting these constraints, i.e. 8(e1↪ e2) 2 ⌃o ⇥ ⌃o+, M(e1↪ e2) = 0 if e1 = e2, M(e1↪ e2) > 0, if e1 6= e2, M(e2↪ e1) = M(e1↪ e2), if e2 6= ". A logically compound observable event o of degree d (with d ≥ 1) is a non-empty subset of elements from ⌃o+, that is not the singleton ¶"♦, such that d = max¶M(e1↪ e2) ♣ ¶e1↪ e2♦ ✓ o)♦

+ 1. A logically compound event of degree 1 is a single observable event.

Given the system D in Figure 1, we assume that observable events b and d are hard to distinguish. We also assume that a, e, and h are less difficult to distinguish, and sometimes it is difficult to find out whether what has been perceived is either pure noise (that is, no observable event has occurred in the DES) or observable event e. This can be modeled by M(b↪ d) = 1; M(a↪ e) = M(a↪ h) = M(e↪ h) = 2; M(e↪ ") = 3; and M(·) = 1 for any other pair of distinct elements.

We use 2⌃o+↪d and 2⌃o+↪d to denote the collection of subsets of ⌃o+, where each subset represents a logically compound observable event of degree d, and d or less, respectively. Notice that 2⌃o+↪d = Sid 2⌃o+↪i . We use the symbol # as a separator to represent the logically compound observable event, e.g. e#h. Although a logically compound event is univocally identified by writing all the values that are included, independently of their order, we put such values in an order in this paper so that " precedes any other event and all the other events are in alphabetical order.

Definition 5 (Logical uncertainty degree). A logically uncertain observation is a sequence of logically compound observable events. The logical uncertainty degree of a logically uncertain observation is the maximum degree of the logically compound events that are included.

The logical uncertainty degree of observation e#h▷ g▷ "#e▷ c depicted in Figure 3 is 4 because the distance between " and e is 3.

3.3 Unifying Uncertainty Representations

The examples presented in this paper use either pure temporal uncertainty or pure logical uncertainty. However, a combination of both uncertainties could be adopted. To make the next definitions independent of the specific type of the considered uncertainty and of its measure (since several measures can be envisaged for the same uncertainty type), we introduce the extension of an observation. Such a notion encapsulates both the specific kind of uncertainty and its value according to a specific measure.

Definition 6 (Extension). Given a type of uncertainty k, the value m of a specific measure of this uncertainty, and a certain observation O, the extension ♣♣O♣♣km of the observation is the set of certain and uncertain observations that O could produce according to the given uncertainty type and up to the given uncertainty measure, where O 2 ♣♣O♣♣km.

We now talk about km as the uncertainty that can affect the observation produced by the system. For instance, we denote the extension up to temporal uncertainty of level ` as ♣♣O♣♣◁◁` and denote the extension up to logical uncertainty of degree d as ♣♣O♣♣#d . In our example, given the trace ⌧ whose certain observation is obs(⌧) = h▷ g▷ e▷ c, the extension of such an observation to the second temporal uncertainty level is ♣♣obs(⌧)♣♣◁◁2 = ¶h▷ g▷ e▷ c↪ h▷ g▷ c◁◁e↪ h▷ e◁◁g▷ c↪ g◁◁h▷ e▷ c↪ g◁◁h▷ c◁◁e♦, while its extension to the third logical uncertainty degree based on the distance matrix provided in Section 3.2 is

♣♣obs(⌧)♣♣#3 = ¶x▷ g▷ y▷ c♦, which is a set including sixteen sequences, where x 2 ¶h↪ a#h↪ e#h↪ a#e#h♦ and y 2 ¶e↪ a#e↪ e#h↪ a#e#h♦. Notice that ♣♣obs(⌧)♣♣◁◁1 = ♣♣obs(⌧)♣♣#1 = ¶h▷ g▷ e▷ c♦, i.e. these extensions give a certain observation. This is a general property, i.e. for any trace ⌧, ♣♣obs(⌧)♣♣◁◁1 = ♣♣obs(⌧)♣♣#1 = ¶obs(⌧)♦ since both ♣♣◁◁1 and ♣♣#1 comprise no uncertainty. Given an uncertain observation Ou, the fact Ou 2 ♣♣O1♣♣km \ ♣♣O2♣♣km for certain observations O1 and O2 means that observable behavior O1 can be mistaken for observable behavior O2 if the observation is affected by uncertainty km.

4 Diagnosability with Uncertain Observations

This section proposes a definition of diagnosability with an observation affected by a (generic) uncertainty km. According to this generalized definition, a faulty behavior should always eventually produce an observation that cannot be mistaken for an observation produced by a nominal behavior.

Definition 7 (Diagnosability under uncertainty). Given a DES D = (⌃↪ L↪ obs↪ flt) with a set of faults ⌃f ✓ ⌃ and an uncertainty km, a fault f 2 ⌃f is km-diagnosable if

System D is km-diagnosable if every fault f 2 ⌃f is kmdiagnosable.

Comparing Definition 1 with Definition 7, it is easy to see that the latter one is a generalization of the former since ♣♣O♣♣km is a singleton when km comprises no uncertainty. System D in Figure 1 is ♣♣◁◁2 -diagnosable. Indeed, fault f is identified by observing either b▷ c⇤ or e▷ c⇤ ; changing the order of two consecutive observed events does not eliminate the fact that b will be observed; a temporally uncertain observation with level `  2 will not modify the order between h and e. However, the system is not ♣♣◁◁3 -diagnosable since observation e◁◁g◁◁h▷ c⇤ cannot be precisely diagnosed as it is relevant both to a normal and a faulty trace.

Given the distance matrix provided in Section 3.2, let us now consider the degree of logical uncertainty as 2. Hence, only events whose distance value between them is up to 1 need to be considered, i.e. the only uncertainty lies in event b, which may be confused with d. If the logically uncertain observation b#d▷ c⇤ is perceived, the diagnosis task cannot find out whether fault f has occurred or not, which proves that D is not ♣♣#2 -diagnosable.

Notice how the definition of diagnosability is well-behaved w.r.t. increasing uncertainty. If uncertainty ♣♣00 is stronger than ♣♣0 , i.e. ♣♣O♣♣00 ◆ ♣♣O♣♣0 for any certain observation O, then ♣♣00 -diagnosability implies ♣♣0 -diagnosability. Given a sequence ♣♣1 ↪ ♣♣2 ↪ ▷ ▷ ▷ of increasingly stronger uncertainties, the maximum index i such that the system is ♣♣i -diagnosable (or 0, if the DES is not diagnosable even for certain observations, or +1, if there does not exist any upper bound for i) defines the robustness of the system w.r.t. uncertainty. Since temporal uncertainty is increasingly stronger for increasing values of the uncertainty level and logical uncertainty is increasingly stronger for increasing values of the uncertainty degree (for any given distance matrix), we can conclude that the sample DES D is not ♣♣◁◁` -diagnosable for any ` > 2 and it is not ♣♣#d -diagnosable for any d > 1.

4.1 Diagnosability and Temporal Uncertainty

The most popular approach to diagnosability analysis is the twin plant method [Jiang et al., 2001], which synchronizes two completely observable FAs, called verifiers, to search for non-diagnosable faulty behaviors. We now present the ♣♣◁◁` - verifier, which is the verifier that incorporates temporal uncertainty.

Definition 8 (♣♣◁◁` -Verifier). Let D = (⌃↪ L↪ obs↪ flt) be a DES, where ⌃o ✓ ⌃ and ⌃f ✓ ⌃ are the sets of observable and faulty events, respectively. Let G = (X↪ ⌃↪ δ↪ x0) be the FA generating L. The ♣♣◁◁` -verifier relevant to a fault f 2 ⌃f is the FA G◁◁` = (X◁◁` ↪ ⌃◁◁` ↪ δ◁◁` ↪ x◁◁` 0 ) defined as follows:

• ÷ X◁◁` = X ⇥ ¶N↪ F♦ and x◁◁` 0 = (x0↪N);
• ÷ ⌃◁◁` = ✓✓⌃o `◆◆; and
• ÷ δ◁◁` = ¶((x↪ φ)↪w↪ (x0 ↪ φ0 )) 2 X◁◁` ⇥ ⌃◁◁` o ⇥ X◁◁` ♣ 9x σ1 -! ▷ ▷ ▷ σn --! x0 ▷ w 2 ♣♣obs(σ1▷ · · · ▷ σn)♣♣◁◁` ^ (φ0 = N , φ = N ^ f 62 ¶σ1↪ ▷ ▷ ▷ ↪ σn♦)♦.

The size of the ♣♣◁◁` -verifier relevant to a fault and the computational complexity of its construction is O(♣X♣2 ♣⌃◁◁` ♣) = O(♣X♣2 ♣⌃o♣` ).

Once G◁◁` has been built, it has to be synchronized with itself, which results in the twin plant. A state of the twin plant is ambiguous if it matches the pattern ((x↪N)↪ (x0 ↪ F)) or ((x↪ F)↪ (x0 ↪ N)). Diagnosability holds if no loop includes ambiguous states, as stated in Theorem 1. Notice that if a state in a loop is ambiguous, then all the states in the same loop are ambiguous.

Theorem 1. Given a DES D whose behavior is represented by FA G = (X↪⌃↪ δ↪ x0) and the ♣♣◁◁` -verifier G◁◁` , fault f in D is ♣♣◁◁` -diagnosable iff G◁◁` ⌦G◁◁` contains no loop of ambiguous states.

Proof outline: The proof is similar to the corresponding one in the classical twin plant approach [Jiang et al., 2001]. A loop of ambiguous states proves that there is an infinite ambiguous path in the twin plant. By construction, an infinite ambiguous path in the twin plant betrays the existence of two infinite behaviors of the DES, a nominal one and a faulty one, that can indefinitely generate the same uncertain observation, which shows that the finite delay k in Definition 7 after which the fault can be diagnosed does not exist. ⇤

The complexity of the whole method to check the ♣♣◁◁` - diagnosability of a fault is O(♣X♣4 ♣⌃o♣` ).

The ♣♣◁◁2 -verifier for our sample DES D in Figure 1 is depicted in Figure 4. Instead of displaying all the transitions having the same source and target nodes, just one is shown, which is labeled by all the events triggering these transitions, where + is a separator.

4.2 Diagnosability and Logical Uncertainty

Logical uncertainty requires a more involved verifier. The main issue stems from the fact that an unbounded number of observation fragments such as "#e could be generated without any transition actually taking place in the system; we shall call them interrupting fragments. However, the condition specified in the definition of diagnosability only applies to system paths of non-trivial length, i.e. the k parameter in the definition. Therefore, sequences of interrupting fragments, regardless how long, need to be ignored as they do not represent arbitrary long paths in the system.

The purpose of the twin plant is to exhibit an infinite faulty path on the system, every prefix of which generates an observation similar to that of a non-faulty path. The idea of the verifier is to create copies hx↪ b↪ x0 i of transition hx↪ a↪ x0 i whenever M(a↪ b) + 1  d. As usual, the states are actually augmented with a label N or F that records whether a fault has occurred. In order to account for interrupting fragments, we also define interruption transitions δ3 in Definition 9, which are loops labeled by ". The semantics of such transitions is that nothing happened on the system but the sensors wrongly detected an observable event.

However, diagnosability cannot be checked with such verifier because the twin plant may now include cycles of interruption transitions. In order to prevent the inclusion of those cycles, we record the state flag F if an observable event has just occurred; otherwise, we record F 0 . We then search for cycles that contain at least one F state (cf. Theorem 2).

Definition 9 (♣♣#d -Verifier). Let D = (⌃↪ L↪ obs↪ flt) be a DES, where ⌃o ✓ ⌃ and ⌃f ✓ ⌃ are the sets of observable and faulty events, respectively. Let G = (X↪⌃↪ δ↪ x0) be the FA generating L. Let M be the distance matrix. The ♣♣#d -verifier relevant to a fault f 2 ⌃f is the FA G#d = (X#d ↪ ⌃#d ↪ δ#d ↪ x#d 0 ) defined as follows:

• ÷ X#d = X ⇥ ¶N↪ F↪ F 0 ♦ and x#d 0 = (x0↪N);
• ÷ δ#d = δ1 [ δ2 [ δ3, where
• ÷ ⌃#d = ⌃o [ ¶"♦; and
• δ1 = ¶((x↪ φ)↪ e↪ (x0 ↪ φ0 )) 2 X#d ⇥⌃#d ⇥X#d ♣ 9e0 2 ⌃o▷ (x↪ e0 ↪ x0 ) 2 δ ^ M(e↪ e0 ) + 1  d ^ (φ0 2 ¶N↪ F♦) ^ (φ0 = N ,φ = N)♦ ;
• δ3 = ¶((x↪ φ)↪ "↪ (x↪ φ0 )) 2 X#d ⇥ ⌃#d ⇥ X#d ♣ (φ0 2 ¶N↪ F 0 ♦) ^ (φ0 = N ,φ = N)♦.
• δ2 = ¶((x↪ φ)↪ "↪ (x0 ↪ φ0 )) 2 X#d ⇥⌃#d ⇥X#d ♣ 9e0 2 ⌃ ∩ ⌃o▷ (x↪ e0 ↪ x0 ) 2 δ ^ (φ0 2 ¶N↪ F 0 ♦) ^ (φ0 = N , φ = N ^ e 6= f)♦ ;

The set of transitions of the verifier is partitioned into δ1, the transitions corresponding to an observable event; δ2, the transitions corresponding to a non-observable event; and δ3, the interruption transitions.

The size of the ♣♣#d -verifier relevant to a fault is O(♣X♣2 ♣⌃o♣).

Theorem 2. Given a DES D whose behavior is represented by FA G = (X↪ ⌃↪ δ↪ x0), a distance matrix M, and the ♣♣#d - verifier G#d , fault f in D is ♣♣#d -diagnosable iff G#d ⌦G#d contains no loop with an ambiguous state, i.e. a state ((x↪ N)↪ (x0 ↪ F )) or ((x↪ F )↪ (x0 ↪ N)).

Proof outline: The proof is similar to that of Theorem 1. The only difference is that it suffices for a loop to include an ambiguous state (instead of including ambiguous states only) and conclude that an infinite behavior after the fault is possible along which the diagnosis task cannot discriminate whether the fault has occurred. ⇤

The complexity of the whole method to check the ♣♣#d - diagnosability of a fault is O(♣X♣4 ♣⌃o♣).

Although checking diagnosability when the observation is both temporally and logically uncertain is beyond the scope of this paper, we briefly mention it here. If we want to find out whether a fault is (♣♣#d and ♣♣◁◁` )-diagnosable, we first transform G into G# = (X↪ ⌃↪ δ#↪ x0), where δ# is initially set to δ, i.e. 8e1 2 ⌃o↪ 8e2 2 ⌃o+ such that M(e1↪ e2)  d - 1, 8(x↪ e1↪ x0 ) 2 δ, we add (x↪ e2↪ x0 ) to δ#. Then, we apply the method described in Section 4.1 to G#. If the relevant twin plant does not include any loop of ambiguous states, we can conclude that the fault is diagnosable for whichever observation that mixes ♣♣#d uncertainty and ♣♣◁◁` uncertainty.

5 Conclusions

This paper investigates how uncertainty in observations can affect the diagnosability of a DES, i.e. the ability of detecting a fault without any ambiguity within a finite number of observable events after the fault has occurred. The analysis is carried out in a scenario, where the considered DES is diagnosable according to the original definition of DES diagnosability in the literature (that is, it is diagnosable given a certain observation) and the diagnostic algorithm is exact. In particular, the paper deals with the above topic in the context of event-based approaches to fault modeling [Jéron et al., 2006] and a relaxation of either the temporal constraints or the logical constraints between observed events is considered.

In the former case, the observation becomes a sequence of compound temporal events. If the maximum cardinality of the considered temporally compound events is i (which is called the temporal uncertainty level of the observation), this means that, after i (single) observable events have been recorded, we may be unable to find out in which temporal order they were produced by the DES. This is the case, for instance, when the observable events are conveyed to the observer through distinct channels, having distinct clocks or delays, and the synchronization error of these clocks (or thepossibly varying-length of these delays) is such that at most i events can be received without the observer being able to disclose their reciprocal temporal order.

In the latter case, the observation becomes a sequence of compound logical events. If the degree of logical uncertainty is i, each observable event occurred in the DES may be confused with some other observable event(s) or even with pure noise, provided that its distance from them is less than i. This is the case, for instance, when the observable events are conveyed to the observer through channels affected by noise. Hence, both temporal and logical relaxations are quite meaningful and representative of real world situations.

This paper provides a definition of DES diagnosability that extends the original definition [Sampath et al., 1995] in the literature, as well as a method to check whether the newly defined property holds for a given DES, that extends the original twin plant method [Jiang et al., 2001] considering temporal and logical uncertainty. If a DES is diagnosable even if the observation has a temporal uncertainty level of value i > 1 or a logical uncertainty degree i > 1, the diagnosis task can be performed without any loss in the ability to disambiguate candidates although the available measuring equipment cannot get a certain observation. The higher the uncertainty level/degree that still guarantees diagnosability, the less expensive the needed measuring equipment and its design.

Future research can follow two orthogonal directions, one focused on the distribution and the other on the extension of the proposed conceptual framework. Such a framework is currently based on a global model of the DES at hand and on its monolithic processing. Instead, the model can be compositional and a distributed processing method can be adopted. As to the second research direction, the new definition of DES diagnosability and the proposed method to check it could be adapted to state-based approaches of fault modeling. In addition, all kinds of temporal uncertainty should be addressed including the relaxations of temporal constraints that are not sequences of temporally compound events but bring to uncertain observations. A further challenge is to define diagnosability in the frame of temporal uncertainty, logical uncertainty, and approximate diagnostic algorithms altogether.

Acknowledgements

NICTA is funded by the Australian Government through the Department of Communications and by the Australian Research Council through the ICT Centre of Excellence Program.

The authors thank the reviewers for their comments.