Diagnosability is a procedure whose goal is to determine whether any failure - or a class of failures - can be determined in finite time after its occurrence. Earlier works on diagnosability of discrete event systems (DES) establish some intermediary models from the analyzed model and then call some procedures to check diagnosablity based on these models, while recent works try to give a diagnosability formulation as a modelchecking problem. However, there still lacks a single framework able to handle both of the diagnosability issues: how to model the problem? and how to decide it? In this paper, we build on some existing works which have formally established necessary and sufficient conditions for diagnosability of DES and we propose a generic operative formulation of diagnosability using the -calculus logic, which allows resolving the diagnosability issue within a single formalism.
Fault detection and isolation (FDI) is a crucial task,
both for safety and productivity reasons. Moreover,
systems become more and more complex, thus
making monitoring/diagnosis a challenging task
especially in automated systems. A typical issue to
deal with when performing the diagnosis process is
that of partial observability. Actually, it is often difficult
and costly to detect all the changes that may occur
within a complex system. Indeed, for technical and/or
economic reasons, setting enough devices/sensors
to catch all the information needed for control and
supervision is generally unfeasible when dealing with
large complex systems. Consequently, it becomes
essential to develop efficient techniques to carry
out FDI tasks. At a high level, dis
Diagnosability of DES has been defined first in
the se
In this paper, an operative definition of diagnosability
is developed, while using a slight variant of
calculus1, as it was initially propose
Using a single logical framework to give a formulation of diagnosability does not necessarily mean that the problem has been simplified. Indeed, we will see that some of the steps of our formulation are quite close to the cited works, especially those using a twin plant/verifier. Nevertheless, the benefits of using a single framework is twofold: from a theoretical point of view, this shows the existence of such a logical operative framework able to express the problem as a whole. Then from the practical point of view, this provides a way to quickly implement and experiment diagnosability only by looking at the semantics, and hopefully will it be useful to extend the diagnosability facilities, as will be shown in the sequel.
The paper is organized as follows: In section 2, we introduce diagnosability of DES as well as some related notations. Section 3 is devoted to give an overview on the related works. In section 4, we discuss our -calculus formulation for diagnosability of DES. Section 5 gives a brief discussion about complexity and finally section 6 concludes the paper while driving some perspectives for this work.
To properly give the definition of diagnosability that we consider, we need to introduce some concepts and notations relative to language theory.
An alphabet is a set of characters or symbols, usually denoted . A word is a sequence –or string– of characters. The set of all finite length words, composed of characters in is denoted . A language over is a subset of . A word is empty if it contains no letter, and is denoted . If w is a word then jwj denotes its length, i.e. the length of the character sequence constituting w (j j = 0). Two words a and b can be concatenated to form a new word denoted a:b (or ab for short). The 1Please note the absence of ”modal” concatenation operation complies with the property jabj = jaj + jbj. Using concatenation, it can be helpful to confuse the 1-length words (jwj = 1) with characters, and to consider the empty word as a “hidden” word/character. For w = ab, a and b are called prefix and suffix of w, respectively. A language L is called prefix-closed iff each prefix of each word in L is in L, i.e. (8w 2 L)(fa j 9b; w = abg L). For w 2 L, wi denotes the ith character of w. For i 2 N n f0g 8 i > jwj, wi = and w1 is the first character. By abuse of notation, if 2 and w 2 , then 2 w iff (9i)(wi = ).
Now, we will define diagnosability as given in the
se
We consider the following assumption: once a fault has occurred, the system remains irreparably faulty, that is to say faults are permanent. More precisely, given a sequence of alternating states and transitions, once a fault has occurred, every subsequent state eventually reached is considered faulty. From the monitoring point of view, this means we do not consider any maintenance operation that may be performed on the system.
Each subset i is denoted fi, that is f = Ui fi. s 2 ( fi))
with a fault in fi: (8s 2 L)(8fi 2 fi)(sjsj = fi , Definition 3 L=s = ft 2 js:t 2 Lg is the set of all suffixes of s in L.
Definition 4 (8i)((si 2 o ) P (s)i = si) ^ (si 2 u ) P (s)i = )), defines the projection P (s) of sequence s on the set of observable events o: if si is observable, then P (s)i = si, but if si is unobservable then P (s)i = .
Definition 5 PL 1(y) = fs 2 LjP (s) = yg gives all the sequences s in L for which the projection on o gives y.
(8i 2 f )(9ni 2 N)(8s 2 ( fi))(8t 2 L=s) (jtj ni ^ w 2 PL 1(P (s:t)) ) 9(f 2 fi)(f 2 w)) Informally speaking, this definition states that a given language is diagnosable iff for any sequence w with the same observable projection than a faulty sequence s:t with sjsj 2 fi, and t is sufficiently long, then w necessarily contains a fault from fi. Reasoning directly on languages is not always possible, because they are often infinite. An alternative is to use labeled transition systems (LTS).
tuple (Q; q0; ; !), in which:
q0 is the initial state is a set of events !: Q
We say that an LTS recognizes a word w = x1 : : : xn iff q0 x!1 : : : x!n, or in other words if the sequence of events given by w can occur from q0. The set of recognizable words forms the language recognized by the LTS. By extension, we say that an LTS is diagnosable (resp. not diagnosable), iff the language it recognizes is diagnosable (resp. non-diagnosable).
For the LTS in Figure 1, the set of observable events is fa; bg, while f is a fault (thus unobservable). The LTS is not diagnosable and the explanation is quite simple: any word of the language (ab) , coming from an observable projection, can originate either from a recognized sequence containing a fault (any word in f(ab) satisfies this), or from a non-faulty sequence (any word in (ab) also verifies this). Thus, there is no length n, such that after this length, one can always distinguish faulty sequences from normal ones, based on observed events.
On the other hand, the language recognized by the automaton of Figure 2 is diagnosable.
f 0 2
b b a a 1 3 f 0 2 a b a b 4 3 The difference between automata A and B is the appearance order of the observable events after the fault f. In B, a fault may appear either from the initial state, followed by an occurrence of b, or between two consecutive occurences of b. Therefore, when a fault f occurs, the projection on the set of observable events results in a sequence starting with b or it will include at least two consecutive b’s. Both cases cannot be obtained without the occurrence of f.
Several reference works in diagnosis of DES can
be found in the literature, these works can be
distinguished mainly according to the notations
used, to the framework considered (centralized
vs. distributed, untimed vs. timed), to the type
of faults (permanent vs. transient) or also to the
procedures adopted to investigate diagnosability.
Sa
Although diagnosability is not defined using an
“operative” logical framework, the originality of this
work comes from its efficient decision procedure,
which has been widely reused in several subsequent
work
The decision procedure is composed of three steps. From the original LTS G = (X; q0; ; !), one proceeds as follows:
Construction of Go “observable” version of G: = (Xo; q0; o; !o), the a) Xo = f(x; f ) j x 2 Q1 [ fq0g ^ f F g, where Q1 = fx 2 Q j (9x0 2 Q)(9e 2 o)(x0 !e x)g, i.e. Xo is the set of states which are the destination of an observable transition (Q1), plus the initial state q0. Each state is labeled with a set of faults f , indicating which ones may have occurred before reaching this state. b) !o: Xo o Xo is such that (x; f ) e2 !oo (x0; f 0) iff (9 2 u; x00 2 X) x ! x00 !e x0 ^ f 0 = ffi j j 2 fi g [ f . This is the observable reachability: if a state x0 is reachable from a state x by an unobservable sequence, or the empty sequence, directly followed by an observable event e, then (x; e; x0) is in !o.
Construction of Gd = (GojjGo) = (Xo Xo; (qo; qo); o; =)), where jj is the usual parallel composition, for which only the following rule applies, because the two composed LTS are the same (clones): q a2 !oo q0 r a2 !oo r0
qjjr =)a q0jjr0
And finally, a cycle-checking pass is needed within Gd: for every cycle q1 =) qn =)a q1, where 2 o and a 2 o, if (8i; j 2 [1; n])(qi = (s; f 1) ^ qj = (s0; f 2) ) f 1 = f 2) then G is diagnosable.
Several approaches use logical formulas to partially state diagnosability. All these works have in common the fact that they first build an intermediary LTS, in such a way to make the diagnosability decision a bit easier.
To the best of our knowledge, the
Diagnosability can be extended using a more general fault specification: instead of pointing only faulty states or events, one may also express that a given behavior is faulty (resp. normal) if it satisfies (resp. does not satisfy) a certain formula specifying the faulty (resp. safe) behavior.
In Jiang (2004), the authors use an LTL formula f to specify the boundary of the normal (safe) behavior: each state outside this boundary is considered as to be faulty. In particular, usual faults are specified using safety properties: if e is a faulty event, then :e gives the normal behavior. However, what is particularly interesting in this approach lies in the fact that faults may be much more subtle, as for instance: a deadlock (a blocking preventing any further action of the system); a livelock (the blocking of certain functionalities in the system: technically speaking, the system executes some tasks, but does not meet its functional requirements); the repeated occurrence of a given event: taken individually, each occurrence is not a fault; but the recurrence of the event denotes a faulty behavior; etc. For example, a nominal behavior could be the following: after a request, the system must answer by a response (i.e the system is reactive). To specify this requirement one can use the following formula: (request ! response). Any run which does not satisfy this property is considered as to be faulty.
In J e´ron (2006), Jeron et al. reuse, while generalizing
them, the ideas discussed previously. The main idea
is to use the LTS model to specify both the behavior
to be diagnosed (i.e the “faulty” behavior), and the
model of the system to be monitored. The idea is
likely to be inspired from the well-known technique
called as ”verification with observers”: when it is not
possible to express a given property using a logic (or
when using a logical formula leads to unsatisfying
performances), it remains possible to instrument the
behavioral model in order to facilitate the expression
of the property. This is exactly what is suggested
here: instead of giving a different logical formula
for each type of faults to be diagnosed, the system
model is composed with the fault model, then a
method, which is besides generic, is applied to check
diagnosabili
Concretely, given Gf the fault model and GM the model to be diagnosed, G = Gf GM is first computed, then a determinization is operated on this LTS. Thereafter, on this determinized LTS, the unobservable events are abstracted thus obtaining iGtsoebslf.: FGidniaaglly=thGisobsobtaGinobesd. TLhTeS diescicsoiomnpporsoecdeswsitihs thereby reduced to checking whether there is not a sequence indefinitely “undetermined”, i.e for which one component in Gdiag is faulty whereas the other is not. The system is then diagnosable iff such a sequence does not exist.
The goal of our formulation is twofold: to establish a homogeneous formal logical framework to specify the diagnosability problem, and to give a “decision algorithm”, directly deduced from the -calculus semantics.
The logic that we use here is typically a predicate
calculation extended with two fix-point operators
which have been propose
There are two entry points for this grammar: E and R. Each of these entry points defines a particular type of formula: E denotes boolean formulas, while R defines relations. A relation is defined by the set of elements respecting a given boolean formula, therefore, E-expressions are necessary to define a relation. Note, however, that in the sequel E will not be used as an entry point in our formulation.
Throughout the rest of the paper, we write [y=x] to say that every occurrence of x in is substituted by y. The semantics of -calculus expressions is defined on the complete lattice hO; i, as follows: J>K = true J?K = false J: K = not J K J = K =
equals J ^ K = J K and J K J _ K = J K or J K J(9x)( )K =ORi2OJ [i=x]K JR(y1; : : : ; yn)K = (y1; : : : ; yn) 2 R J n(x1; : : : ; xn): K = O j J [y1=x1;:::;yn=xn]K = trueg f(y1; : : : ; yn) 2 = Si1=0 Si, with S0 = ; and Si+1 = J x: K J [Si=x]K J [Si=x]K
J x: K = Ti1=0 Si, with S0 = O and Si+1 = The terms true and false are the basis B of the boolean algebra whose operators are the usual boolean operators and, or and not; equals: O O ! B allows the comparison of two elements in O; OR is the disjunction on a set of boolean terms and finally 2 is the usual membership operator.
In J x: K and J x: K, must be monotone, i.e. each occurence of x must be “covered” by an even number of negations.
The fix-point operator is an infinite union. However
and according to the Kn
Let hQ; q0; ; !i, with !: Q Q, the LTS modeling the system for which we want to check diagnosability. We do not want to handle any item other than states and events, thus O = Q [ . We also assume the existence of sets f of faulty events and o of observable events.
Firstly, we will introduce diagnosability in the sa
Informally speaking, a triplet (a; b; f ) is element of the UOReach relation, means that there exists an unobservable path between a and b. This path is labeled with a boolean f which is true when at least s !e t ^ s = q0 ^ : o(e) ^ f = f (e) _ s !e t ^ r e!0 s ^ o(e0) ^ : o(e) ^ f =
X(s; s0; f 0) ^ s0 !e t f = (f 0 _ f (e)) ^ : o(e) ^ X: (s; t; f ):(9s0)(9f 0)(9e)(9r)(9e0) 1
C f (e) _ CC
C A one of the events of this path is a fault; conversely f is false if there exists an unobservable normal (without fault) path between a and b. In order to reduce the size of this relation, only the states destination of an observable event, or the initial state, are considered as an origin of the unobservable paths. A graphical representation of this relation applied to the model of Figure 4 is given in Figure 5.
In Figures 5, 7, 10, 11, 12, 13, 15, 16, 17 and 19, T tag stands for TRUE (faulty path) and F for FALSE (no fault).
0 u 1
0 F 1 a a f
a F
F 2
a u u T
F 2
F F 3 4 u F 3 4 In the U OReach formula, the X fix-point operator indicates that the definition is recursive and that X denotes the set of elements in the relation at the previous step of the recursion. Since the samllest fix-point operator ( ) is used here, X is initially an empty set (;). The next operator, (s; t; f ), expresses that the relation UOReach is a ternary relation. The relation is defined by giving the valuation space that the three parameters, here (s; t; f ) can have. UOReach is defined by three cases:
Initially, s corresponds to the states issued from an observable transition from which an unobservable transition is possible, f indicates whether the event labelling the unobservable transition is faulty or not. Formally, this case can be written as: (9r)(9e0)(9e)(r e!0 s ^ o(e0) ^ s !e t ^ : o(e) ^ f = f (e))
By default, the initial state is considered as to be issued from an observable transition: (s !e t ^ s = q0 ^ : o(e) ^ f = f (e))
The third case is the recursion operation: there exists a path between s and t if there is a triplet (s; s0; f 0) in UOReach such that an unobservable transition links s0 to t. The parameter f of the new triplet (s; t; f ) is true if f 0 is true (a fault has already occurred between s and s0), or when the transition s0 !e t is faulty (i.e. f (e)): therefore we propagate the information that a fault is possible between s and s0 to the new triplet. Formally, this case is expressed as follows: (9s0)(9f 0)(9e)(U OReach(s; s0; f 0) ^ s0 !e t ^ : o(e) ^ f = f 0 _ f (e))
o(e) ^ s = q0 ^ s !e t ^ :f Nextobs = 0
X: (s; e; t; f ):(9s")(9e0)(9f 0)(9s0) 1
C _ CC
A The second step consists in determining the observable reachability of the LTS for which we examine dianosability. The observable reachability is an LTS which keeps only the observable events, and in which a transition links a state s to a state t iff it is possible to reach t from s through an unobservable sequence (may be ) followed by an observable event. Here, the origin state s has to be either the initial state q0, or a state destination of an observable event.
To each triplet (s; e; t) involved in an element of the observable reachability relation, we assign a boolean f denoting the existence of a faulty path (a path containing a fault) when f is true, and a normal path (without any fault) when f is false. The graphical representation of Nextobs relation is given in Figure 7. As for UOReach, Nextobs relation is defined according to two cases:
Either s !e t (with e observable) already exists, then we add (s; e; t; f ) as is to Nextobs while putting f marker to false (since this is a faultless path from s to t). Formally, this can be written: s !e t ^ o(e) ^ :f . As for U OReach, the origin state must be either the initial state (s = q0), or a state destination of an observable event (X(s"; e0; s; f 0)), which has been already captured in the N extobs relation, here.
Or there exists an intermediary state s0 such that s0 !e t where e is observable and s0 is reachable from s through a sequence of unobservable events ((s; s0; f 0) 2 U OReach). In this case, the fault marker f is a copy of f 0: indeed only unobservable sequences containing a fault can turn f into true. Formally, this case can be expressed as follows: U OReach(s; s0; f ) ^ s0 !e t ^ o(e).
Normal = X: (t):(9s)(9e) t = q0 (X(s) ^ N extobs(s; e; t; ?)) _ Normal is a unary relation ( (t)) containing the initial state q0 as well as all the states, destination of an observable transition and reachable from q0 by at least one normal path (cf. N extobs). This relation will be useful in the sequel as if a given state t is reachable only through faulty paths, then the faults will propagate and all the subsequent reached states will be consequently faulty (no anymore ambiguity). One may easily note that from the implementation point of view, sets N extobs and N ormal can be computed simultaneously using the same procedure, just by looking at the fault tagin N extobs.
Sameobs = X: (t; t0):(9s)(9s0)(9e) 0 N ormal(s) ^ N extobs(s; e; t; ?) B N extobs(s; e; t0; ?) ^ :(t = t0) @B X(s; s0) ^ N extobs(s; e; t; ?)
N extobs(s0; e; t0; ?) ^ :(t = t0) ^ ^ This relation catches all the couples (t; t0) such that states t and t0 are different states that could be reached respectively by two normal (faultless) paths P1 and P2 having the same projection on o. Sameobs allows us to keep all the states equivalent 1 _ C
C A in terms of observation; the goal being to examine ambiguity in the system behavior starting from such pairs of states, as will be shown in the Amb relation. Two cases are considered:
the first case holds when from the same “normal” state s, one can reach two different states t and t0 respectively by two unobservable normal sequences, both followed by the same observable event e (cf. Figure 10). This case can be written as: N ormal(s)^N extobs(s; e; t; ?)^N extobs(s; e; t0; ?)^ :(t = t0).
the second case corresponds to the recursion and consists in propagating the trace equivalence. Concretely from two indistinguishable states s and s0 already in Sameobs (X(s; s0)), one can reach two different states t and t0 while generating the same observable event e and without generating any fault for both paths (cf. Figure 11). This case can be expressed as: X(s; s0) ^ N extobs(s; e; t; ?) ^ N extobs(s0; e; t0; ?) ^ :(t = t0). or t and t0 come respectively from s and s0 by Sameobs through a same observable event e and without generating any fault such that (s; s0) is also in Sameobs (cf. Figure 13). faulty and not is the second. This can happen according to three cases:
In the second case, let us take back the computation of Sameobs as given in definition 9. Assume there are n couples (si; s0i) in Sameobs, i 2 [1; n] preceding (t; t0) after having bifurcated from the same normal state s, as shown in Figure 13. Then, according to N extobs definition, 9 n; n0 2 ( u n f ) : o such that P o ( n) = P o ( n0) = e ^ (sn = s) !n t ^ 0 (s0n = s0) !n t0. This is also true for each pair of couples (si; s0i); (si+1; s0i+1) for i 2 [1; n 1]. That is 8i 2 [1,n-1]; 9 i; i0 2 ( n f ) : o such that 0 P o ( i) = P o ( i0) ^ si !i si+1 ^ s0i !i s0i+1. Then by concatenating respectively i sequences and i0 sequences, one can state that: 9 1; 2 2 ( n f ) : o; 1 = 1 : : : n; 2 = 10 : : : n0 such that P o ( 1) = P o ( 2) ^ s1 !1 t ^ s01 !2 t0.
Moreover (s1; s01) falls in the first case, then 9 1; 2 2 ( n f ) ; 1 6= 2 such that q0 !1 s1 ^ q0 !2 s01 ^ P o ( 1) = P o ( 2) ^ q0 !1 s1 ^ q0 !2 s01. Finally, by taking 1 = 1: 1 and 2 = 2: 2, we obtain: 1; 2 2 ( n f ) : o, 1 6= 2, P o ( 1) = P o ( 2) ^ q0 !1 t ^ q0 !2 t0.
Amb = X: (t; t0):(9s)(9s0)(9e)(9f ) 0 N ormal(s) ^ N extobs(s; e; t; >) ^ B N extobs(s; e; t0; ?) BB Sameobs(s; s0) ^ N extobs(s; e; t; >) ^ BB N extobs(s0; e; t0; ?) @B X(s; s0) ^ N extobs(s; e; t; f ) ^
N extobs(s0; e; t0; ?) Amb relation is quite simple and consists in identifying pairs of states t and t0 locally ambiguous, i.e t and t0 can be reached from q0 by two sequences generating the same observation, but the first is 1 _ C
C
C _ C
C C A
pairs (t; t0) such that t and t0 can be reached from the same normal state s, respectively through an unobservable faulty path followed by an observable event e in one hand, and on the other hand through a normal unobservable path (may be ) followed by the same observable event e. This case can be expressed as: N ormal(s) ^ N extobs(s; e; t; >) ^ N extobs(s; e; t0; ?) (cf. Figure 15).
when from two states s and s0 such that Sameobs(s; s0), one can reach t and t0 respectively through two unobservable sequences, 1 faulty and 2 normal, both followed by the same observable event e (Sameobs(s; s0) ^ N extobs(s; e; t; >) ^ N extobs(s0; e; t0; ?)) as shown in Figure 16. This can be written: Sameobs(s; s0) ^ N extobs(s; e; t; >) ^ N extobs(s0; e; t0; ?).
the third case is when the ambiguity is obtained by “inheritence” from two ambiguous states s and s0 repectively by a faulty unobservable sequence (which may be either normal or faulty, and possibly empty) followed by an observable event e; and on the other hand by a normal unobservable sequence followed by the same observable event e (X(s; s0) ^ N extobs(s; e; t; f ) ^ N extobs(s0; e; t0; ?)). This case is depicted in Figure 17. In order to examine diagnosability, one has to check whether there exists a cycle of ambiguous states. Searching such a cycle is not simple if we use the smallest fix-point operator . One possible way is to add, one by one, the elements that we are sure they do not make part of a cycle: if the obtained relation (that we call Noteveramb) is equal to Amb, then there is no such a cycle. Conversely, the elements of Amb which are not in Noteveramb form at least one ambiguous cycle.
However, the -calculus offers another operator which will be very useful here: the greatest fix-point operator . Thanks to this operator, we will start from the maximal relation Q Q, then at each step we keep only the elements satisfying the equation until a fix-point is reached. Hence, defining Everamb becomes simpler because only one case is possible (cf. Figure 18): a couple (s; s0) is in Everamb iff s and s0 are ambiguous (Amb(s; s0)) and iff there is at least one successor couple (t; t0) by Nextobs which fulfills both of the following conditions: is also ambiguous: (Nextobs(s; e; t; >) ^ Nextobs(s0; e; t0; ?)), and is in Everamb as well (recursivity): (X(t; t0)) Such a recursive definition implies that either of the following two cases holds: 1. the number of ambiguous couples in Everamb is infinite, or 2. the ambiguous couples in Everamb form a cycle.
Hence, since we deal with a finite state system, only the second case is possible. Thereby, each ambiguous couple (s; s0) in Everamb belongs to at least one cycle of ambiguous couples.
Everamb = X: (s; s0):(9t)(9t0)(9e)(9f)
Amb(s; s0) ^ Nextobs(s; e; t; >) ^
Nextobs(s0; e; t0; ?) ^ X(t; t0) Figure 19 gives the Everamb relation for the considered model. Everamb is equal to Amb here, but for which we have shown in dotted line, some cycles in Nextobs that satisfy Amb.
partition of faults f iff for each part f in f ,
and those of Sa
It is proved in Huang (2004) that an LTS is
diagnosable in the sense of Sa
a, F a, F a, T
a, F
a, F
a, F
2
On one h
On the other hand, the computation of Sameobs together with Amb is equivalent to the composition procedure Gd = (GojjGo). Actually, Sameobs performs the composition between the normal paths which have an observational equivalence (both generate the same observation), whereas Amb performs the composition between a faulty path on one hand and a normal path on the other hand, when both paths have an observational equivalence. Also, the definition of Everamb does not allow multiple faults directly, but this does not break its generality: if there is more than one type of faults, i.e. if the partition f contains more than one set, it is sufficient to check the emptiness of Everamb for each of the sets individually, as stated in definition 8. In Gd, a couple (x; y) is ambiguous iff, for a given fault f, x = (q; F ) and f 2 F , while y = (q0; F 0) and f 62 F 0. As (x; y) is in Gd, this means that q and q0 are reachable by the same observable sequence. This corresponds to our definition of ambiguity. The couple of states (t; t0) is ambiguous if either of the following conditions holds:
there exists a state s belonging to Normal, i.e there exists a normal sequence 2 (( uo n f ) o) such that q0 ! s, and there exists an observable event e and two unobservable sequences 0 faulty and 00 normal, such that s 0:!e t and s 00:!e t0. This means we cannot decide, by only observing P o( ):e, whether a fault has occurred or not, hence the ambiguity.
there exists a couple (s; s0) of states in Sameobs, i.e there exist two normal sequences having the same projection on o, 1; 2 2 (( uo n f ) o) such that q0 !1 s and q0 !2 s0, and (s; s0) fulfills the following: from s there can be an observable step (in N extObs) s !e t generating a fault and from s0 there can be an observable step (in N extObs) s0 !e t0 with no fault. Like previously, this means one cannot decide by only observing P o ( ):e whether a fault has occurred or not, thus the ambiguity.
there exists a couple of states (s; s0) in Amb, which means there exists a faulty sequence 1 2 ( uo o) such that q0 !1 s and a normal sequence 2 2 (( uo n f ) o) such that q0 !1 s0 while 1 and 2 have the same observable projection, and (s; s0) fulfills the following: there exist an observable event e, two unobservable sequences either faulty or not (2 uo), and 0 normal (2 ( uo n f ) ) such that s :!e t and s0 0:!e t0. Thereby, t can be reached from q0 through a faulty path 1 e, and t0 can be reached from q0 through a normal path 2 0e and both paths generate the same observation (P o ( 1 e) = P o ( 2 0e)). Like previously, this means we cannot decide based on the observed events if a fault has actually occurred, hence the ambiguity.
For every sequence of events, once a state is faulty,
every successor is faulty as well. If a cycle is found in
Gd such that it contains at least one composite state
of a “faulty” and a “normal” states (i.e. ambiguity),
then every state in that cycle is ambiguous too.
This is why instead of finding cycles containing at
least one
We want to insist on the fact that the purpose of this article is not to propose a new algorithm. Indeed, even if the semantics is operational and allows computation, a direct implementation of that semantics would be far from being optimized. Nevertheless, we want to argue here that our formulation may be a good source for some new efficient algorithms. Indeed, where the other works systematically operate a product of the system to be diagnosed with itself (or a non-faulty version of itself), such a product is performed here according to some finer conditions. But before exploring what such an algorithm would look like, we wanted to explore the complexity of our approach, to see whether it is of the same complexity order, i.e. whether our formulation yields a polynomial complexity (if it is not, finding an efficient algorithm would have no sense!).
To estimate the complexity of the whole diagnosability decision process, we will seek for an upper bound on the complexity of each of the various formulas given in definitions 8 to 13.
Let us recall that these formulas are all based on fixed point operators. Because of their recursive nature and because the computation stops as soon as a new iteration does not change the result (the fixed point is reached), it is difficult to determine the worst case in a general way. Indeed, it is possible to find a worst case for a given (part of) formula, but it may very well be that this very worst case is at the same time the best case of another one (or at least, not its worst case), and the worst case of both formulas, when combined, generally cannot be the combination of the worst cases of each of the formulas.
Here we will take the worst case for each of the formulas for one single iteration and then, we will consider the maximum number of iterations leading to the fix point. This way, we are sure to get an upper bound of the complexity. Note that the result we will get is necessarily an overestimate of the real complexity. To picture that, let us consider the calculation of U OReach (Definition 3). With the operator one starts with an empty set, and at the first iteration the triples (s; t; f ) verifying the following conditions are added: s is either the initial state, or the target state of an observable transition; to check both conditions we must go through the whole transition relation (which has a -highly improbable- maximum of jQj:j j:jQj elements) and check for each triple (s; e; t) whether e is observable (j oj j j). At the end, these operations have the following complexity: jQj2:j j2. for all the states s found in the previous item (at most jQj states), (s; t; f ) is in U OReach at the first iteration if there exists (s; e; t) in the transition relation, such that e is not observable (e 2 u). Like previously, we will consider instead of u (j uj j j), to ease factorization. We obtain the following complexity: jQj3:j j2. f can be either true or false: the complexity of the previous item is then multiplied by 2.
This results in the following upper bound of the overall complexity: jQj2:j j2 + 2jQj3j j2 for the first iteration.
For the subsequent iterations, we start with the existing set of triples (s; s0; f ) (at most 2jQj2 triples), and for all the (target) states s0 of these triples, we determine the states t directly accessible by an unobservable transition e (complexity 2jQj2j j2). So this gives the following upper bound of complexity: 2jQj4j j2.
Regarding the number of iterations before reaching the fixed point, the worst case corresponds to the situation in which at each iteration, a single new triplet is added to U OReach: this means there are at most jQj2j j iterations.
We then obtain that an upper bound on the complexity of the U OReach computation is jQj6:j j3. It is obvious that this bound is far from being optimal, but it allows us to determine the complexity class of our formulation. In the same way, we find that each of the formulas, has a polynomial complexity. Thus, we can say that analyzing the diagnosability on the basis of our formulation is of a polynomial computational complexity.
This work offers a new way to formulate diagnosability of DES using -calculus logic that we advocate to be a good formalism for a single formal framework to deal with diagnosability. While it theoretically defines the logical perimeter of the problem, it also allows the use of model checking techniques. This means taking advantage of already efficient tools and of mature techniques to circumvent, the best it can, the problem of combinatorial explosion, which is a well-known problem in model-checking, also called the state space explosion problem. The developed formulation is quite flexible and some extensions are being developed in order to tackle diagnosability issues under different contexts. Moreover, based on our logical formulation, we intend to develop diagnosers for online monitoring.
From a technical point of view, developing an
on-the-fly algorithm to implement our formulation
shall improve the efficiency of the computational
complexity of the diagnosa
In addition, we believe that the flexibility of
calculus can be efficiently used for some other
problems gravitating around diagnosability, as for
f
The approach was tested with the MEC/ARC tools,
but a prototype was also implemented to tackle the
issue from the point of view of explicit exploration
of the behavior (which is not allowed by MEC),
but also to have a better understanding of the
formulation complexity, and to explore optimization
possibilities. As a side note, the prototype was
relatively easily implemented (using Standard ML),
and we think that this is in large part because of
the simplicity of the -calculus semantics. Besides
this direct implementation, we have also developed a
second prototype based on a database