Lina Ye

Philippe Dague

Diagnosability Analysis for Self-observed Distributed Discrete Event Systems

Diagnosability is a crucial property that determines at design stage how accurate any diagnosis algorithm can be on a partially observable system and thus has a significant impact on the performance and reliability of complex systems. Most existing approaches assumed that observable events in the system are globally observed. But sometimes it is not possible to obtain global information. Thus a recent work has proposed a new framework to check diagnosability in a system where each component can only observe its own observable events to keep the internal structure private in terms of observations. However, the authors implicitly assume that local paths in components can be exhaustively enumerated, which is not true in a general case where there are embedded cycles. In this paper, we get some new results about diagnosability in such a system, i.e., what we call joint diagnosability in a self-observed distributed system. First we prove the undecidability of joint diagnosability with unobservable communication events by reducing Post's Correspondence Problem to an observation problem. Then we propose an algorithm to check a sufficient but not necessary condition of joint diagnosability. Finally we briefly discuss about the decidable case with observable communication events.

I. INTRODUCTION

Over the latest decades, with more performance requirements imposed on the complex systems, they are subject to more errors. However, it is unrealistic to detect faults manually for such systems. Automated diagnosis mechanisms are thus required for large distributed applications. Generally speaking, diagnosis reasoning aims at detecting possible faults explaining the observations. The efficiency of diagnosis reasoning depends on system diagnosability, which is a crucial property that determines at design stage how accurate any diagnosis algorithm can be on a partially observable system. The systems we discuss here are Discrete Event Systems (DES).

Some existing works analyzed diagnosability in a centralized way ( [START_REF] Sampath | Diagnosability of discrete event systems[END_REF], [START_REF] Jiang | A polynomial time algorithm for diagnosability of discrete event systems[END_REF], etc.), i.e., a monolithic model of a given system is hypothesized, which is unrealistic due to combinatorial explosion of state space. This is why very recently distributed approaches began to be investigated ( [START_REF] Pencolé | Diagnosability analysis of distributed discrete event systems[END_REF], [START_REF] Schumann | Scalable diagnosability checking of eventdriven systems[END_REF], etc.), relying on local objects. However, all these approaches assumed that observable events in the system are globally observed. But sometimes it is not possible to obtain global information. Then [START_REF] Ye | Diagnosability analysis of discrete event systems with autonomous components[END_REF] has proposed a new framework to check diagnosability in a system where each component can only observe its own observable events to keep the internal structure private in terms of observations. However, the authors implicitly assume that local paths can be exhaustively enumerated, which is not true in a general case where there are embedded cycles. In this paper, we generalize this work to get some new results about the diagnosability of what we call self-observed distributed systems, where observable events can only be observed by their own component.

We make several contributions in this paper. First, we extend diagnosability of globally observed systems to what we call joint diagnosability of self-observed systems and then to prove its undecidability with unobservable communication events. Secondly, we propose an algorithm for testing a sufficient condition, where we obtain pairs of local trajectories in the faulty component, such that for each pair only one trajectory contains the fault but both have the same observations, and then check their global consistency through two phases. We provide the proof that it is a sufficient condition and point out why it is not necessary. Thirdly, the decidable case where communication events are observable is discussed.

II. PRELIMINARIES

In this section, we model self-observed distributed DES and then recall joint diagnosability features [START_REF] Ye | Diagnosability analysis of discrete event systems with autonomous components[END_REF].

We consider a self-observed distributed DES composed of a set of components {G 1 , G 2 ,..., G n } that communicate by communication events, where each component can only observe its own observable events. Such a system is modeled by a set of finite state machines (FSM), each one representing the local model of one component. The local model of a component G i is a FSM, denoted by

G i = (Q i , Σ i , δ i , q 0 i )
, where Q i is the set of states; Σ i is the set of events; δ i ⊆ Q i ×Σ i ×Q i is the set of transitions; and q 0 i is the initial state. The set of events Σ i is partitioned into four subsets: Σ io , the set of locally observable events that can be observed only by their own component G i ; Σ iu , the set of unobservable normal events; Σ i f , the set of unobservable fault events; and Σ ic , the set of communication events shared by at least one other component, which are the only shared events between components. Figure 1 depicts a self-observed distributed system with two components: G 1 (left) and G 2 (right), where the events Oi denote locally observable events, the event F denotes an unobservable fault event, the events U i denote unobservable normal events and the events Ci denote communication events.

We denote the synchronized FSM of components G 1 , ..., G n by (G 1 , ..., G n ), where the synchronized events are the shared events between components and any one of them always occurs simultaneously in all components that define it. The global model of the entire system is implicitly defined as the synchronized FSM of all components based on their shared events, i.e., communication events. However, the global model will not be calculated since in a self-observed distributed system, the global occurrence order of observable events is not accessible. In the following, we call subsystem of G the synchronization of a subset of components of G, i.e., (G s1 , ..., G sm ), where {s 1 , ...s m } ⊆ {1, ...n}. One component or the entire system can be considered as a subsystem.

Given a system model G = (Q, Σ, δ, q 0 ), the set of words produced by the FSM G is a prefix-closed language L(G) that describes the normal and faulty behaviors of the system. Formally, L(G) = {s ∈ Σ * |∃q ∈ Q, (q 0 , s, q) ∈ δ}, where the transition δ has been extended from events to words. In the following, we call a word of L(G) also a trajectory in the system G and a sequence q 0 σ 0 q 1 σ 1 ... a path in G, where σ 0 σ 1 ... is a trajectory and for all i, we have (q i , σ i , q i+1 ) ∈ δ. Given s ∈ L(G), we denote the post-language of L(G) after s by L(G)/s and denote the projection of s to observable events of G (resp. G i ) by P (s) (resp. P i (s)). We adopt the assumption in [START_REF] Pencolé | Diagnosability analysis of distributed discrete event systems[END_REF], i.e., the projection of the global language on each local model is observable live, i.e., there is no unobservable cycle in any component. For the sake of simplicity, our approach is shown for only one fault, which can be extended to the case with multiple faults by running one time for each fault. Next we rephrase reconstructibility introduced in [START_REF] Cori | Recognizable subsets of some partially abelian monoids[END_REF].

Definition 1: (Reconstructibility). Given a system G that is composed of several subsystems, i.e., G = (G s1 , ..., G sm ), a set of trajectories in these subsystems is said to be reconstructible with respect to G if it is obtained by projection on this set of subsystems of a trajectory in G.

If there is no common communication event between two subsystems, then any trajectory in one subsystem and any one in the other subsystem are reconstructible.

For the sake of consistency, now we rename what is called cooperative diagnosability in [START_REF] Ye | Diagnosability analysis of discrete event systems with autonomous components[END_REF] as joint diagnosability. We denote a trajectory ending with the fault f by s f . Definition 2:

(Joint diagnosability). A fault f is jointly diagnosable in a self-observed distributed system G with components {G 1 , ...G n }, iff ∃k ∈ N, ∀s f ∈ L(G), ∀t ∈ L(G)/s f , (∀i ∈ {1, ..., n}, |P i (t)| ≥ k)⇒ (∀p ∈ L(G) (∀i ∈ {1, ..., n}, P i (p) = P i (s f .t)) ⇒ f ∈ p).
Joint diagnosability of f means that for each faulty trajectory s f in G, for each extension t with enough locally observable events in all components, every trajectory p in G that is equivalent to s f .t for local observations in each component should contain in it f . In other words, the fault can be detected after finite non bounded trajectory prolongation in at least one component. In a self-observed system, we call a pair of trajectories p and p′ satisfying the three conditions a (global) indeterminate pair: 1) p contains f and p′ does not; 2) p has arbitrarily long local observations in all components after the occurrence of f ; 3) ∀i ∈ {1, ..., n}, P i (p) = P i (p′). Here arbitrarily long local observations can be considered as infinite local observations. Now we have the following theorem [START_REF] Ye | Diagnosability analysis of discrete event systems with autonomous components[END_REF].

Theorem 1: Given a self-observed distributed system G, a fault f is jointly diagnosable in G iff there is no (global) indeterminate pair in G.

III. UNDECIDABLE CASE

To discuss about joint diagnosability, we consider two cases: communication events being unobservable and observable. We first consider the general case, i.e., communication events being unobservable.

Theorem 1 implies that checking joint diagnosability boils down to check the existence of indeterminate pairs that witnesses non joint diagnosability. Inspired from [START_REF] Tripakis | Undecidable problems of decentralized observation and control[END_REF], where undecidability of joint observability is proved by reducing the Post's Correspondence Problem (PCP) to an observation problem, we discuss first about whether joint diagnosability is decidable or not.

For the sake of simplicity, we give now a simplified proof for undecidability of joint diagnosability 1 .

Theorem 2: Given a self-observed distributed system where communication events are unobservable, checking joint diagnosability of a given fault is undecidable.

Proof: : 1)PCP: given a finite alphabet Σ, two sets of words

v 1 , v 2 , ..., v k and z 1 , z 2 , ..., z k over Σ, then a solution to PCP is a sequence of indices (i m ) 1≤m≤n with n ≥ 1 and 1 ≤ i m ≤ k for all m such that v i1 v i2 ...v in = z i1 z i2 ...z in .
2)Now consider the example depicted in figure 2, where the system is composed of two components G 1 and G 2 . In G 1 , each one of V i, i ∈ {1, ..., k}, and each one of Zi, i ∈ {1, ..., k}, denotes a sequence of observable events all different from O1, C1, ..., Ck are unobservable communication events, F denotes a fault event and O1 is an observable event. In G 2 , each one of Ai, i ∈ {1, ..., k}, denotes an observable event different from O2, C1, ..., Ck are unobservable communication events and O2 is an observable event. Then the observations in G 1 can be described as V i 1 V i 2 ...V i n O1 * without fault or Zi 1 Zi 2 ...Zi n O1 * with fault, where ∀i j , j ∈ {1, ..., n}, i j ∈ {1, ..., k}. In G 2 , the observations are Ai 1 Ai 2 ...Ai n O2 * . In this system, the occurrence of the fault can be confirmed by the observation of O1.

3) Without the observation of O1, the local observations are wO1 + for G 1 and Ai 1 Ai 2 ...Ai n O2 * for G 2 , where w = V i 1 V i 2 ...V i n when there is no fault or w = Zi 1 Zi 2 ...Zi n when there is a fault. Clearly, if PCP has a solution, i.e., ∃(i m ) 1≤m≤n such that V i 1 V i 2 ...V i n = Zi 1 Zi 2 ...Zi n , we have two trajectories p and p′ such that the observations of p in G 1 are V i 1 V i 2 ...V i n O1 + , which is a trajectory without fault, while the observations of p′ in G 1 are Zi 1 Zi 2 ...Zi n O1 + , which is a trajectory with a fault. And both p and p′ have the same observations for G 2 , i.e., Ai 1 Ai 2 ...Ai n O2 * . Thus we get that p and p′ have the same observations for both

G 1 and G 2 , i.e., V i 1 V i 2 ...V i n O1 + =Zi 1 Zi 2 ...Zi n O1 + for G 1 and Ai 1 Ai 2 ...Ai n O2 * for G 2 ,
then the fault is not jointly diagnosable. 4) On the other hand, if the fault is not jointly diagnosable, then we obtain at least one indeterminate pair, denoted by p and p′ such that the pro-

jection of p on G 1 is Ci 1 V i 1 Ci 2 V i 2 ...Ci n V i n O1 * , on G 2 is Ai 1 Ci 1 Ai 2 Ci 2 ...Ai n Ci n O2 * and that of p′ on G 1 is Cj 1 Zj 1 Cj 2 Zj 2 ...Cj m Zj m F O1 * and on G 2 is Aj 1 Cj 1 Aj 2 Cj 2 ...Aj m Cj m O2 * .
From the fact that p and p′ have the same observations for G 2 , we get Ai 1 Ai 2 ...Ai n O2 * = Aj 1 Aj 2 ...Aj m O2 * and thus we have m = n and i 1 = j 1 , ..., i n = j n . And then from the same observations of p and p′ on G 1 , we get

V i 1 V i 2 ...V i n O1 * = Zi 1 Zi 2 ...Zi n O1 * , i.e., V i 1 V i 2 ...V i n = Zi 1 Zi 2 ...Zi n ,
which means that there is a solution for PCP. 5) The above proves that the existence of a solution for PCP is equivalent to that of a fault being not jointly diagnosable. Since PCP is an undecidable problem, then checking joint diagnosability is undecidable.

There are two major differences between joint diagnosability in our framework and joint observability in [START_REF] Tripakis | Undecidable problems of decentralized observation and control[END_REF]. One is that the former assumes that local observers are attached to local components that are synchronized by common communication events to get a global model while the latter separates arbitrarily the observable events in the global model into several sets. The other one is that joint diagnosability consists in separating infinite trajectories while joint observability consists in separating finite ones. Thus, if any communication event is assumed to be unobservable, joint diagnosability checking boils down to infinite PCP. But this one has also been proved to be undecidable [START_REF] Halava | Undecidability of infinite post correspondence problem for instances of size 9[END_REF], which gives the result.

IV. SUFFICIENT ALGORITHM

We have proved that joint diagnosability with unobservable communication events is undecidable. We can nevertheless propose an algorithm to test a sufficient condition, which is still quite useful in some circumstances. We first construct the local diagnoser from a given local model to show fault information for any local trajectory. Then we show how to build a structure called local twin plant to obtain original information about indeterminate pairs (also called local indeterminate pairs in the following), based on the local diagnoser. The next step is to check the global consistency, i.e., to check whether the local indeterminate pairs can be extended into (global) indeterminate pairs, whose existence testifies non joint diagnosability. Actually our algorithm remains trivially applicable when the assumption of unobservability of communication events is partially relaxed, i.e., in the most general case where some communication events are observable and others unobservable.

A. Original diagnosability information

To check the existence of indeterminate pairs, in the distributed framework, we use the structure called local twin plant defined in [START_REF] Jiang | A polynomial time algorithm for diagnosability of discrete event systems[END_REF]. In particular, the considered fault is assumed to only occur in one component, denoted by G f . Then the local twin plant for G f contains original information of indeterminate pairs: actually this twin plant is a FSM that compares every pair of local trajectories to search for the pairs with the same arbitrarily long local observations, but exactly one of the two containing a fault, which are local indeterminate pairs. First, we define delay closure operation with respect to a subset Σ d of Σ to preserve only the information about the events in Σ d .

Definition 3: (Delay Closure). Given a FSM G = (Q, Σ, δ, q 0 ), its delay closure with respect to

Σ d ⊆ Σ is ∁ Σ d (G) = (Q, Σ d , δ d , q 0 ) where (q, σ, q ′ ) ∈ δ d iff ∃s ∈ (Σ\Σ d ) * , (q, sσ, q ′ ) ∈ δ.
We now describe how to construct the local diagnoser of a given component, based on which we build the local twin plant. Given a local model, we get a modified one by attaching fault label, denoted by l ∈ {N, F }, where N for normal and F for fault, to each state. In other words, before the occurrence of the fault, each state is labeled with label N and, after its occurrence, with label F .

Definition 4: (Local diagnoser). Given a local model G i , its local diagnoser D i is obtained by operating the delay closure with respect to the set of communication events and observable events on the modified model:

D i = ∁ Σi o ∪Σi c (G m i ), where G m i is the modified version of G i .
Based on the local diagnoser, the corresponding local twin plant is obtained by synchronizing the local diagnoser with itself based on the locally observable events, allowing one to obtain all pairs of local trajectories with the same observations to search for local indeterminate pairs. To simplify this synchronization, the two identical local diagnosers, denoted by D l i (left instance) and D r i (right instance), can be reduced as follows: D l i is obtained by retaining only paths with at least one fault cycle and D r i is obtained by retaining only paths with at least one non-fault cycle. This reduction keeps all original diagnosability information since what we are interested in are only local indeterminate pairs. However, this reduction is only applicable for the local diagnoser of the faulty component G f ; for other components, the local twin plant is obtained by synchronizing the non reduced left instance and the non reduced right instance since there is no fault information. Since this synchronization is based on observable events Σ io , the non-synchronized events are distinguished by the prefix L or R: in D l i (D r i ), each communication event c ∈ Σ ic from D i is renamed by L : c (R : c). The names of all locally observable events are left unchanged.

Definition 5: (Local twin plant). Given a local diagnoser D i for the component G i , the corresponding local twin plant is a FSM, denoted by T i = D l i D r i , where the synchronized events are locally observable events in G i . Each state of a local twin plant is a pair of local diagnoser states providing two possible diagnoses with the same local observations. Given a twin plant state ((q l , l l )(q r , l r )), if the considered fault f ∈ l l ∪ l r but f / ∈ l l ∩ l r , which means that the occurrence of f is not certain up to this state, then this state is called an ambiguous state with respect to the fault f . An ambiguous state cycle is a cycle containing only ambiguous states. In a local twin plant, if a path contains an ambiguous state cycle with at least one locally observable event, then it is called a local indeterminate path, which corresponds to a local indeterminate pair. Note that local indeterminate paths contain original diagnosability information and can be obtained only in the local twin plant of the component G f . If a local indeterminate pair can be extended into a global indeterminate pair, then we say that its corresponding local indeterminate path is globally consistent. Figure 3 shows the left and right instances of the local diagnoser for the faulty component G 1 of Figure 1 (top) as well as a part of the corresponding local twin plant (bottom). Clearly, in the local twin plant, we have local indeterminate paths since they have ambiguous state cycles with observable events.

B. Global consistency checking

Joint diagnosability verification consists in checking the existence of globally consistent local indeterminate paths, whose existence proves non joint diagnosability. To do this, we have to check the global consistency of the corresponding left trajectories of the local indeterminate paths in the local twin plants as well as that of their corresponding right trajectories, shortly called left consistency checking and right consistency checking.

Definition 6: (Left (Right) consistent plant). Given a subsystem G S composed of components G i1 , ..., G im and their corresponding local twin plants T i1 , ..., T im , to obtain a left (right) consistent plant with respect to the subsystem G S , denoted by T l f (T r f ), we perform the following two steps: 1) Distinguish right (left) communication events between local twin plants by renaming them with the prefix of component ID. For example, R:C2 (L:C2) in the local twin plant of G 2 is renamed as G 2 :R:C2 (G 2 :L:C2). 2) Synchronize the renamed local twin plants with the synchronized events being the common left (right) communication events, which works because observable events do not intersect between components and nonsynchronized right (left) communication events are distinguished by the prefix of component ID.

From definition 1, we know that in the left (right) consistent plant with respect to a subsystem G S , each path p corresponds to a set of paths p i1 , ..., p im in the local twin plants of all components in G S such that the set of left (right) trajectories of p i1 , ..., p im are reconstructible with respect to G S . For our example, the bottom part of figure 4 shows a part of the left consistent plant T l f , which is obtained by synchronizing the renamed local twin plant of G 1 and that of G 2 (top part of figure 4) based on the common left communication events.

C. Algorithm

Algorithm 1 presents the procedure to verify a sufficient condition of joint diagnosability. As shown in the pseudocode, algorithm 1 performs as follows. Given the input as the set of component models, the fault F that may occur in the component G f , we initialize the parameters as empty, i.e., G l S (G r S ), the subsystem for the left (right) consistency checking. The procedure of the algorithm can be separated into two parts: left consistency checking (line 3-12) and right consistency checking (line 13-24). Left consistency checking begins with the local twin plant construction of G f , the subsystem G l S being now G f (line 3-4). When both the left consistent plant T l f with respect to the current left subsystem G l S and DirectCC(G, G l S ) are not empty (line 5), where DirectCC(G, G l S ) is the set of directly connected components to G l S (a directly connected component being one sharing at least one common communication event with the subsystem), the algorithm repeatedly performs the following steps to further check left consistency. 1) Select one directly connected component G i to the subsystem G l S and construct its local twin plant T i (line 6-7). 2) Synchronize T l f with T i to obtain left consistent plant for this extended subsystem based on common left communication events (line 8). To do this, non-synchronized right communication events are distinguished by the prefix of component ID.

3) Update the subsystem G l S by adding G i and reduce the newly obtained T l f by retaining only paths with ambiguous state cycles containing observable events for all components in G l S (line 9-10).

Algorithm 1 Sufficient algorithm 1: INPUT: the system model G = (G 1 , ..., G n ); the fault F and the faulty component G f 2: Initializations: G l S ← ∅ (subsystem for left consistency checking); G r S ← ∅ (subsystem for right consistency checking) 3:

T l f ← ConstructLT P (G f ) 4: G l S ← G f 5: while T l f = ∅ and DirectCC(G, G l S ) = ∅ do 6: G i ← SelectDirectCC(G, G l S )
7:

T i ← ConstructLT P (G i ) 8: T l f ← T l f T i 9: G l S ← Add(G l S , G i ) 10: T l f ← RetainConsisP aths(T l f ) 11: if T l f = ∅ then 12:
return "F is jointly diagnosable in G" 13: else 14:

T r f ← AbstractRight(G f , T l f ) 15: G r S ← G f 16: while T r f = ∅ and G l S = G r S do 17: G i ← SelectDirectCC(G l S , G r S ) 18: T r f ← T r f AbstractRight(G i , T l f ) 19: G r S ← Add(G r S , G i ) 20: T r f ← RetainConsisP aths(T r f ) 21: if T r f = ∅ then 22:
return "F is jointly diagnosable in G"

23:

else 24:

return "Joint diagnosability cannot be determined"

If the left consistent plant T l f is empty, then there is no local indeterminate path that corresponds to a set of paths in the local twin plants of all components in the subsystem such that their left trajectories are reconstructible (definition 1), which implies the non existence of a globally consistent local indeterminate path. In this case joint diagnosability information is returned (line 11-12). Otherwise, if T l f is not empty (line 13), then we proceed to check right consistency of the corresponding paths in T l f that have been already verified to be left consistent in the whole system. Right consistency checking begins with the function AbstractRight(G f , T l f ) (line 14), which performs delay closure with respect to right communication events and observable events of G f . Then the subsystem G r S is assigned as G f (line 15). When the right consistent plant T r f for the current right subsystem G r S is not empty and G l S = G r S (line 16), we repeatedly perform the following steps to check right consistency in an extended subsystem (since left consistency checking does explore all connected components, for right consistency checking we only consider the subsystem G l S instead of the whole system). 1) Select a directly connected component G i to G r S from G l S (line 17).

2) Perform the function AbstractRight(G i , T l f ), which has been described as above, and then synchronize with T r f based on the common right communication events (line 18). To do this, we rename the right communication events by removing the prefix of component ID, e.g., G i :R:C2 renamed as R:C2.

3) Update the subsystem G r S by adding G i and reduce the newly obtained T r f by retaining only paths with ambiguous state cycles containing observable events for all components in G r S (line 19-20). If the right consistent plant T r f is empty, then there is no local indeterminate path that corresponds to a set of paths in the local twin plants such that their left trajectories and right trajectories are reconstructible respectively, i.e., there is no globally consistent local indeterminate path. In this case, the algorithm returns joint diagnosability information (line 21-22). Otherwise, if T r f is not empty, we cannot determine whether the fault is jointly diagnosable or not. Then the algorithm returns indetermination information (line 23-24). In other words, empty left consistent plant T l f or empty right consistent plant T r f is a sufficient condition but not a necessary condition of joint diagnosability.

Theorem 3: In algorithm 1, if the left consistent plant T l f or the right consistent plant T r f is empty, then the fault is jointly diagnosable, but the reverse is not true.

Proof: : (⇒) Suppose that T l f or T r f is empty and that the fault is not jointly diagnosable. From non joint diagnosability, it follows that there exists at least one globally consistent local indeterminate path. Since global consistency of a local indeterminate path implies both left consistency and right consistency, from algorithm 1 we know that, after left and right consistency checking, this local indeterminate path must correspond to a path both in T l f and in T r f . Thus neither T l f nor T r f is empty, which contradicts the assumption. ( ) Now we explain why non emptiness of both T l f and T r f does not necessarily imply that the fault is not jointly diagnosable. Suppose that T l f is not empty and that it contains two paths, denoted by ρ1 and ρ2, corresponding to two local indeterminate paths. ρ1 corresponds to a set of paths ρ 1 i , 1 ≤ i ≤ n in the local twin plants of all components and ρ2 corresponds to a set of paths ρ 2 i , 1 ≤ i ≤ n in all local twin plants. Now suppose that the right trajectories of the set of paths ρ 1 i , 1 ≤ i ≤ n are not reconstructible and the same for that of the set of paths ρ 2 i , 1 ≤ i ≤ n. It follows that the two local indeterminate paths cannot be extended into global indeterminate pairs and thus are not globally consistent. Then we further suppose that the right trajectories of the set of paths ρ 1 1 , ..., ρ 1 n-1 , ρ 2 n are reconstructible or the same for the set of paths ρ 2 1 , ..., ρ 2 n-1 , ρ 1 n . In this case, from algorithm 1, it follows that finally the right consistent plant T r f is not empty. Now both T l f and T r f are not empty but there is no globally consistent local indeterminate paths, i.e., the fault is jointly diagnosable. Now illustrate on our example the fact that the condition is not necessary. The top part of figure 5 shows the results of performing delay closure with respect to right communication events and observable events both for G 1 and G 2 on the left consistent plant depicted in figure 4. Then, to check right consistency, we rename again the right communication events by removing the component ID such that they can be synchronized. The bottom part of figure 5 shows a part of the right consistent plant, which is not empty. with its left consistent pair ((O4.C2.O5 * ), (O4.C2.O5 * )) in G 2 . While the right consistent plant shown here corresponds to one local indeterminate pair in G 1 , which is ((C1.O1.F.O1 * ), (O1.C2.O1 * )), with its right consistent pair in G 2 , i.e., ((O4.C2.O5 * ), (O4.C2.O5 * )). Thus we can see that the same local indeterminate pair does not correspond to the same consistent pair in G 2 in the left consistent plant and in the right consistent plant, which means that this local indeterminate pair cannot be extended into a global indeterminate pair. Our algorithm gives indeterminate information for joint diagnosable systems that satisfy the following condition: for any set of paths including one path in the local twin plant of each non faulty component and one local indeterminate path in that for faulty component, if they are left consistent and right consistent respectively, then their corresponding local trajectories in the components cannot constitute an indeterminate pair through synchronization. Our illustrated example is quite tricky to show the possibility of indeterminate decision given by our algorithm for a joint diagnosable system. However, in reality, a system satisfying the above condition is quite rare and thus this algorithm is suitable to be applicable for a large number of complex systems.

V. DECIDABLE CASE

We have proved the undecidability of joint diagnosability with unobservable communication events. If we assume their observability, then this problem becomes decidable. Because when any communication event is observable, in the local twin plant, we obtain all pairs of local trajectories with the same observations, including the same observable communication events. Thus each path in the local twin plant corresponds to a pair of local trajectories with the same sequence of communication events. It follows that during global consistency checking, the separate checkings for left and right consistency becomes now only one checking. While in algorithm 1, the checking into two separate phases is the reason why it gives only a sufficient but not necessary condition. Actually, the observability of communication events makes joint diagnosability equivalent to classical diagnosability since only one checking for global consistency implies the same global occurrence order of observations for global indeterminate pairs.

VI. CONCLUSION

In this paper, we consider self-observed distributed systems where observable events can only be observed by their own component and thus the distributed and private (w.r.t. observation) nature of real systems is taken into account. Then we prove the undecidability of joint diagnosability checking when communication events are unobservable, before proposing an algorithm to test a sufficient condition. We start from local indeterminate paths and then we check both in sequence left consistency and right consistency. Due to the observationprivacy, the global occurrence order of observable events between different components is not known, which is taken into account through constructing left and right consistent plants separately. At the opposite, in the approaches for DES with globally observable events, twin plant is constructed by incrementally synchronizing local twin plants via both left and right communication events at the same time, which means that in their case, knowledge of the global occurrence order is required. Then we briefly discuss the decidable case where communication events are observable. There is a gap between these two cases as the unobservable case is undecidable and the observable case is decidable. Next interesting work is to investigate where is the frontier between the two cases, i.e., to study the decidability of joint diagnosability for partial observability of communication events.

Fig. 1 .

 1 Fig. 1. A system with two components G 1 (left) and G 2 (right).

Fig. 2 .

 2 Fig. 2. A system with two components G 1 (top) and G 2 (bottom) for proving undecidability of joint diagnosability.

Fig. 3 .

 3 Fig. 3. Two reduced instances of the diagnoser for G 1 (top) and part of the corresponding local twin plant (bottom).

Fig. 4 .

 4 Fig. 4. Part of the renamed local twin plants for G 1 and G 2 (top) and part of the left consistent plant T l f (bottom).

Fig. 5 .

 5 Fig. 5. FSM after delay closure on the left consistent plant (figure 4) for G 1 and G 2 (top) and part of the right consistent plant (bottom).

  Now both left and right consistent plants are not empty, but this does not imply the existence of global indeterminate pairs that witnesses non joint diagnosability. Actually the part of the left consistent plant depicted here corresponds to two local indeterminate pairs in G 1 with their corresponding left consistent pairs in G 2 , i.e., one local indeterminate pair is ((C1.O1.F.O1

* ), (O1.C2.O1 * )) in G 1 with its left consistent pair ((C1.O3.O5 * ), (O3.U 2.O5 * )) in G 2 and the other local indeterminate pair is ((O2.U 1.C2.F.O1 * ), (C1.O2.C2.O1 * )) in G 1


Lina Ye
email: lina.ye@lri.fr

Philippe Dague
email: philippe.dague@lri.fr

A General Algorithm for Pattern Diagnosability of Distributed Discrete Event Systems

Diagnosability is an important system property that determines at design stage how accurate any diagnostic reasoning can be on a partially observed system. A fault in a system is diagnosable iff its occurrence can always be deduced from enough observations. The centralized diagnosability approaches lead to state explosion since they assume the existence of a monolithic model of the system. This is why very recently the distributed approaches for diagnosability began to be investigated, relying on local objects. On the other hand, diagnosis objectives are generalized from fault event to fault pattern that can represent multiple faults, repeating fault, sequences of significant events, etc. For pattern case, most existing approaches are centralized. In this paper, we propose a new distributed framework for pattern diagnosability. We first show how to recognize patterns by incrementally constructing local pattern recognizers. Then we propose a structure called regional pattern verifier constructed from the subsystem where the pattern is completely recognized before showing how to abstract the necessary and sufficient diagnosability information to further save the search space. Then the global consistency checking is based on another local structure called abstracted local twin checker to analyze pattern diagnosability. The correctness of our distributed algorithm is theoretically proved and its efficiency experimentally demonstrated by the results of the implementation.

INTRODUCTION

Fault diagnosis is a crucial and challenging task in the automatic control of large complex systems. However, it can happen that, with the observation means available, deciding about the occurrence of a given fault is impossible even by observing the system as long as we want. If it is important to detect this fault, running a diagnosis engine on line will be of no help. So it is important to decide at design stage how accurate any diagnosis algorithm can be on a given partially observable system. This problem is called diagnosability analysis and is the basic question that underlies diagnosis.

The diagnosability analysis problem has received considerable attention in the literature. Some existing works analyze diagnosability in a centralized way [START_REF] Sampath | Diagnosability of discrete event systems[END_REF], [START_REF] Jiang | A polynomial time algorithm for diagnosability of discrete event systems[END_REF] and [START_REF] Cimatti | Formal verification of diagnosability via symbolic model checking[END_REF]), i.e., the knowledge of the monolithic model of a given system is hypothesized, which is a very powerful information but leading to combinatorial explosion and not always available. This is why very recently the distributed approaches for diagnosability began to be investigated ( (Pencolé, 2004), [START_REF] Schumann | A scalable jointree algorithm for diagnosability[END_REF], etc.), relying on local objects. More precisely, original diagnosability information can be obtained from the component where the fault may occur and then the global decision is calculated by checking its global consistency. All above approaches assume that the fault is a predefined event resulting in unexpected system behavior. However, sometimes the fault can be a sequence of some important events while any single one of them is not the fault by itself. A new proposal in the centralized case is provided by [START_REF] Jéron | Supervision patterns in discrete event systems diagnosis[END_REF], who formally introduce the notion of supervision pattern, simply called pattern, that is general enough to cover an important class of diagnosis objectives, e.g. diagnosing multiple faults, repeating faults, sequences of significant events, etc.

In this paper, we propose a new and efficient distributed method for pattern diagnosability analysis of discrete event systems. First we extend pattern diagnosability problem from centralized framework to distributed one. Then we show how to recognize patterns by incrementally constructing local pattern recognizers for extended subsystems. More precisely, the subsystem is extended by synchronizing the diagnosability relative part with next selected component. In this way we can avoid global model. Next we propose a structure called regional pattern verifier that is constructed from the subsystem where the pattern is completely recognized before showing how to abstract just the necessary and sufficient diagnosability 1 information to further save the search space. Then the global consistency checking of the retained part is based on another local structure called abstracted local twin checker to check pattern diagnosability. In this way, we avoid constructing global objects both for pattern recognition and for pattern diagnosability verification. Our idea is to find an equivalent alternative to the centralized pattern diagnosability checking that is more efficient in order to improve the scalability of the problem.

PRELIMINARIES

In this section, we define the system model, recall pattern diagnosability of discrete event systems as well as the centralized approach.

System Model

We consider a distributed discrete event system G composed of a set of components G 1 , ..., G n that communicate with each other by communication events. Each component is modeled by a F SM , denoted by

G i = (Q i , Σ i , δ i , q 0 i ), where Q i is the set of states, Σ i is the set of events, δ i ⊆ Q i × Σ i × Q i is
the set of transitions (the same notation will be kept for its natural extension to words of Σ * i ) and q 0 i is the initial state. The set of events Σ i is divided into three disjoint parts: Σ io the set of observable events, Σ iu the set of unobservable events and Σ ic the set of unobservable communication events that are shared by at least one other component (communication events are assumed to be unobservable because we target general systems with a mixture of observable and unobservable communication events but, for sake of simplicity, we deal here with the case where all communication events are unobservable, as the observable case is easy and so the general case can be easily derived from our work ((Pencolé, 2004) and [START_REF] Schumann | A scalable jointree algorithm for diagnosability[END_REF]). For any pair of distinct local components G i and G j , we have Σ io ∩ Σ jo = ∅ and Σ iu ∩ Σ ju = ∅, which means that any two different components only share communication events and their observable events and unobservable events are disjoint.

It is important to notice that, if the model is distributed, the observations are centralized, i.e. accessible to one global observer: the case with several partial observers is completely different for diagnosability analysis, which becomes in particular undecidable ( (Ye, 2011)).

Two composition operations are defined as follows. For the sake of simplicity, they are presented for two FSMs but it is easy to generalize them for a set of FSMs using the associativity properties.

Definition 1 (Synchronization). Given two FSMs

G 1 = (Q 1 , Σ 1 , δ 1 , q 0 1 ) and G 2 = (Q 2 , Σ 2 , δ 2 , q 0 2 ), their synchronization is G 1 Σs G 2 =(Q 1 ×Q 2 , Σ 1 ∪Σ 2 , δ 1 2 , (q 0 1 , q 0
2 )), where Σ s = Σ 1 ∩Σ 2 is the set of shared events, which can be omitted when there is no ambiguity in the context, and δ 1 2 is defined as follows:

• ((q 1 , q 2 ), σ,

(q ′ 1 , q ′ 2 )) ∈ δ 1 2 , if σ ∈ Σ s , (q 1 , σ, q ′ 1 ) ∈ δ 1 and (q 2 , σ, q ′ 2 ) ∈ δ 2 ; • ((q 1 , q 2 ), σ, (q ′ 1 , q 2 )) ∈ δ 1 2 , if σ ∈ Σ 1 \Σ s and (q 1 , σ, q ′ 1 ) ∈ δ 1 ; • ((q 1 , q 2 ), σ, (q 1 , q ′ 2 )) ∈ δ 1 2 , if σ ∈ Σ 2 \Σ s and (q 2 , σ, q ′ 2 ) ∈ δ 2 . Definition 2 (Product). Given two FSMs G 1 and G 2 , their product is G 1 × G 2 = (Q 1 × Q 2 , Σ 1 ∪ Σ 2 , δ 1×2 , (q 0 1 , q 0 2 ))
, where ((q 1 , q 2 ), σ, (q ′ 1 , q ′ 2 )) ∈ δ 1×2 iff (q 1 , σ, q ′ 1 ) ∈ δ 1 and (q 2 , σ, q ′ 2 ) ∈ δ 2 . The operation of product is sometimes called complete synchronization. The main difference between the two operations is how the private events, i.e., the events not in Σ 1 ∩ Σ 2 , are handled. In the product, the transitions of the two FSMs must always be synchronized on a shared event, σ ∈ Σ 1 ∩ Σ 2 . In other words, an event in the product occurs iff it occurs in both FSMs. In the synchronization, the two FSMs are still synchronized on the shared events but the private events can independently be executed whenever possible. We denote the synchronized FSM of components G 1 , ..., G n as (G 1 , ..., G n ), which is actually the monolithic model of the entire system with Σ = ∪ i Σ i and Σ o = ∪ i Σ io , also called the global model in the following. Then we define the operation called delay closure with respect to a set of events, that preserves all information about this set by abstracting away irrelevant parts.

Definition 3 (Delay Closure). Given a FSM G = (Q, Σ, δ, q 0 ), its delay closure with respect to a set of events

Σ d ⊆ Σ is ∁ Σ d (G) = (Q, Σ d , δ d , q 0 ) where (q, σ, q ′ ) ∈ δ d iff ∃s ∈ (Σ\Σ d ) * , (q, sσ, q ′ ) ∈ δ.
Figure 1 presents a simple distributed system composed of three components, where observable events are denoted by Oi, unobservable events by U i and unobservable communication events by Ci. The global model, denoted by G, is implicitly defined as the synchronization of the three components, where the set of synchronized events are communication events, denoted by G = (G 1 , G 2 , G 3 ). Given a system model G, the prefix-closed language L(G) ⊆ Σ * of words produced by the FSM G describes the normal and faulty behaviors of the system. Formally, L(G) = {s ∈ Σ * |∃q ∈ Q, (q 0 , s, q) ∈ δ}. If there is a set F of final states in the FSM, then we denote the marked language generated by G by L m (G) = {s ∈ L(G)|∃q ∈ F, (q 0 , s, q) ∈ δ}.

In the following, we call a word of L(G) a trajectory in the system G and a sequence q 0 σ 0 q 1 σ 1 ... a path in G, where σ 0 σ 1 ... is a trajectory and, for all i, (q i , σ i , q i+1 ) ∈ δ. Given s ∈ L(G), we denote the post-language of L(G) after s by L(G)/s and denote the projection of the trajectory s to observable events by P (s). In our approach, we adopt the following assumption: the language of each component is observable live, i.e. it is live and there is no cycle with only unobservable events.

Pattern Diagnosability of Discrete Event

Systems Now we recall the notion of pattern for diagnosis problem and pattern diagnosability of discrete event systems ( [START_REF] Jéron | Supervision patterns in discrete event systems diagnosis[END_REF]).

Definition 4 (Pattern). A pattern is a deterministic, complete FSM Ω with a stable set F Ω of final states, Ω = (Q Ω , Σ Ω , δ Ω , q 0 Ω , F Ω ). Since F Ω is stable, the marked language generated by Ω is "extension-closed", formally described as: ∀s ∈ L m (Ω), ∀s′ ∈ Σ * Ω , ss′ ∈ L m (Ω). So once Ω arrives in a final state, it will always be in a final state in the future. With pattern definition, the diagnosis problem can be generalized from detecting fault events to recognizing event sequences that can describe more general objectives, like ordered occurrence of significant events, multiple occurrences of the same fault, the repair of a fault, etc [START_REF] Jéron | Supervision patterns in discrete event systems diagnosis[END_REF]). The fault event case is a special one of the pattern case.

In a given pattern Ω, we call an event σ a significant event of Ω if ∃(q, σ, q′) ∈ δ Ω with q = q′, i.e., any event that can change pattern state. We use Θ Ω to denote the set of significant events of Ω and ̟ q to denote the set of events σ ∈ Σ such that ∃(q, σ, q′) ∈ δ Ω , q = q′. Thus ̟ q is actually the set of significant events of Ω that change the state q.

Given a system G and a pattern Ω, it is assumed that Σ = Σ Ω , Σ o = Σ Ωo , Σ u = Σ Ωu . We say that Ω is recognized by a trajectory in the system s ∈ L(G) iff s ∈ L m (Ω). The property of pattern diagnosability concerns the ability of a system to detect a trajectory recognizing the pattern with certainty, based on a sequence of observations. We assume that ∃σ ∈ Θ Ω such that σ is unobservable, which means that at least one significant event is unobservable: otherwise, the diagnosability problem would be trivial. For example, figure 1 depicts an example of such a system and a pattern. Here in the pattern (bottom right) Σ Ω = {C1, C2, U 1, U 2, O1, O2, O3, O4, O5, O6}, which is the same set of events as that of the system. And the final state set of the pattern is {P 2}. We can see that the recognition of this pattern requires the ordered occurrences of the significant events U 1, O3, where any event except U 2 is allowed between them and any event is allowed before and after them.

Definition 5 (Pattern Diagnosability). A pattern

Ω is diagnosable in a system G (we say that G is Ω- diagnosable) iff ∃n ∈ N, ∀s ∈ L(G) ∩ L m (Ω), ∀t ∈ L(G)/s, if |t| ≥ n, then ∀p ∈ L(G), P (p) = P (s.t) ⇒ p ∈ L m (Ω).
A system G is Ω-diagnosable iff for any trajectory s in G recognizing the pattern and for any extension t of s with enough events, any trajectory with the same observations as s.t also recognizes the pattern. A pair of trajectories p, p′ satisfying the following conditions is called a critical pair, also a global critical pair in the following considering that it relates to the global model: 1) p ∈ L m (Ω) and p′ / ∈ L m (Ω); 2) p is of arbitrarily long length after pattern recognition; 3) P (p) = P (p′). The existence of such a global critical pair witnesses non Ω-diagnosability of the system. Thus pattern diagnosability checking is to search for global critical pairs.

Centralized Method

A centralized method for pattern diagnosability checking is proposed in [START_REF] Jéron | Supervision patterns in discrete event systems diagnosis[END_REF], where the existence of the global model is assumed. Then the pattern recognition is based on the construction of global pattern recognizer. Definition 6 (Global Pattern Recognizer). Given a global model G = (Q, Σ, δ, q 0 ) and a pattern Ω, then the global pattern recognizer is R G = G × Ω, where the initial state is (q 0 , q 0 Ω ) and the set

F RG of final states is (Q × F Ω ) ∩ Q RG (Q RG is the set of states in R G ).
Since Ω is a complete deterministic FSM, we have

L(Ω) = Σ * and L(R G ) = L(G) ∩ L(Ω) = L(G).
So the global pattern recognizer shows which part of the pattern can be recognized by any trajectory in the system. If F RG = ∅, we say that the pattern can be recognized in the system. After pattern recognition, pattern diagnosability is analyzed based on the structure called global pattern verifier.

Definition 7 (Global Pattern Verifier). The global pattern verifier for a given global pattern recognizer

R G , denoted by V G , can be obtained by V G = ∁ Σo (R G ) Σo ∁ Σo (R G ).
To construct the global pattern verifier, the delay closure with respect to the set of observable events is first performed on the global pattern recognizer and then the resulted FSM is synchronized with itself based on the set of observable events. The idea is to obtain all pairs of trajectories with the same observations. In V G , each state is a pair of recognizer states that provide two possible pattern recognitions. Given a verifier state composed of two recognizer states, if only one of them is a final state, which means that the recognition of the pattern is not certain up to this state with the same observations, this verifier state is called an ambiguous state. An ambiguous state cycle is a cycle containing only ambiguous states. As any event in V G is observable, then a path in V G containing an ambiguous state cycle corresponds to a global critical pair, which is called a global critical path in the following. So pattern diagnosability testing consists in checking the existence of global critical paths in V G . Thus we have the following theorem. Theorem 1 A pattern Ω is diagnosable in a system G iff there is no global critical path in the global pattern verifier.

DISTRIBUTED FRAMEWORK

As said before, the centralized approach is impractical due to its assumption of the monolithic model. In this section, we show how to recognize a given pattern by incrementally extending a subsystem to avoid the global model and then show how to analyze pattern diagnosability through global consistency checking of the diagnosability relative parts to avoid the global pattern verifier.

Pattern Recognition

Before showing how to recognize a given pattern, for the sake of simplicity, we first modify final states in the pattern as follows: ∀ρ, where ρ is a path in Ω, such that ρ = q σ1 -→ q 1 ... σn --→ q n σ′ -→ q′, where {q 1 , ..., q n , q′} ⊆ F Ω , q / ∈ F Ω , it is modified as a path

ρ′ = q σ1 -→ q 1 ΣΩ --→ q 1 .
This means that we replace the stable final states set F Ω with its transitions by the stable final states set

F ′ Ω = {(q, Σ Ω , q) | q ∈ F Ω and ∃(q′, σ, q), q′ / ∈ F Ω }.
Since F Ω is stable, this operation has no impact on the correctness of the diagnosability algorithm, except to make it more simpler.

Given a subsystem, following the same idea as in definition 6, we construct the local pattern recognizer as follows.

Definition 8 (Local Pattern Recognizer). Given a subsystem G S = (Q S , Σ S , δ S , q 0 S ) and a pattern Ω, then the local pattern recognizer of G S is R GS = G S × Ω, where the initial state is (q 0 S , q 0 Ω ) and the set

F RG S of final states is (Q S × F Ω ) ∩ Q RG S (Q RG S is the set of states in R GS ).
Similar to the global pattern recognizer, the local pattern recognizer shows which part of the pattern is recognized by any trajectory in the subsystem. If the pattern cannot be completely recognized, i.e., the recognizer is not a complete recognizer that will be described later, we need to choose another component to extend the subsystem for further recognition. Before choosing the next component, we first define the following notations.

Definition 9 (Recognition Relative Path and Diagnosability Relative Path).

• Given a path ρ in the pattern recognizer R GS of the subsystem G S , if ρ contains at least one state q r = (q, q Ω ), such that either q Ω is a final state of the pattern Ω or ∃σ ∈ ̟ qΩ such that σ ∈ Σ\Σ S (where Σ S is the set of events of G S and Σ is that of the entire system G), then ρ is called a recognition relative path. And σ, if any, is called a next recognizable event with respect to the subsystem G S . The set of next recognizable events with respect to G S is denoted by Λ GS . • Given a path ρ in R GS , if it is a recognition relative path or it has the same observations as some recognition relative path of R GS , then it is called a diagnosability relative path.

A recognition relative path contains either at least one final state of the recognizer or at least one state that is the source state of a significant event in the pattern such that this significant event is contained outside of the current subsystem, which is called a next recognizable event. Only such kind of paths can possibly recognize the rest of the pattern after synchronization with other components. Then the next component to be chosen should contain at least one next recognizable event. The set of recognition relative paths contains the projections on the subsystem of all the global trajectories that recognize the pattern (called the corresponding subparts of these trajectories in the subsystem). The local pattern recognizer R G S can then be reduced by only retaining its diagnosability relative paths. Let denote R Ω G S this reduced recognizer. Figure 2 shows the local pattern recognizer R GS , where G S is the component G 1 (left part) and the reduced recognizer R Ω GS (right part), where the gray nodes represent the recognizer states whose pattern state is the source state of a next recognizable event in the pattern. Here we have only one next recognizable event O3 with respect to G S . Thus we get the reduced part R Ω GS by deleting one path which concerns neither pattern recognition nor pattern diagnosability. So it is easy to prove the following lemma since the set of diagnosability relative paths includes not only recognition relative paths but also all the paths with the same observations as some recognition relative path.

Lemma 1 The reduced pattern recognizer R Ω G S contains the corresponding subpart in the subsystem G S (projection on G S ) of all global critical pairs. We define a complete recognizer as a local reduced pattern recognizer with at least one final state and without next recognizable event with respect to its corresponding subsystem. The existence of a complete recognizer implies that the pattern can be recognized in the current subsystem and there is no other component that should be further exploited for next recognition.

If a local reduced recognizer R Ω

GS is not a complete recognizer, then there could be three cases:

1. there is no final state in R Ω G S and the set of next recognizable events is not empty Λ GS = ∅; 2. there exists at least one final state in R Ω G S and the set of next recognizable events is not empty Λ GS = ∅; 3. there is no final state in R Ω GS and the set of next recognizable events is empty Λ GS = ∅. In case 1, the pattern is not yet recognized in the current subsystem and there exists at least one next recognizable event. And in case 2, at least one sequence of ordered significant events of the pattern is recognized in the current subsystem but there exists at least one next recognizable event for next recognition (considering there could be not only one such sequence in the pattern to be recognized). So in the first two cases, there exists at least one component G j such that Σ j ∩ Λ GS = ∅ and thus we select G j that contains at least one next recognizable event for next recognition. Then we extend G S by G j through constructing R Ω GS Σc G j , where synchronization is based on the shared communication events, and we extend accordingly the pattern recognizer for this extended subsystem by product with Ω and we reduce it. Note that the number of events in Λ GS is not necessarily only one, so G j is not unique in general but the order of selection is not influential for pattern recognition. Case 3 means that the pattern is not recognized in the current subsystem and there is no next recognizable event. In other words, case 3 implies that the pattern cannot be recognized in the whole system.

In figure 2 (right), R Ω GS is in case 1 with Λ GS = {O3}. As O3 ∈ Σ 2 , G 2 is selected for extension. Figure 3 depicts this extension of G S by G 2 through synchronization based on the shared communication events (left part) and the according reduced extended pattern recognizer (right part) which is actually a complete recognizer since it contains final states and there is no next recognizable event. Here we use gray nodes to show final states of the recognizer.

Pattern Diagnosability Verification

Once a complete recognizer is calculated, then we construct the regional pattern verifier based on this complete recognizer. Since unobservable events do not intersect between components and there is no cycle of unobservable events, the information about unobservable events is not useful during global consistency checking. But, different from the global pattern verifier defined in definition 7, for local version we need, to check global consistency, to retain not only observable events but also communication events. So first we refine the complete recognizer by the delay closure with respect to the set of communication events and observable events. The refined recognizer is denoted as R r . We obtain left instance of R r , denoted by R l r , by prefixing the communication events with L. Then we get the right instance of R r , denoted by R r r , by prefixing the communication events with R. This is because we need to keep track of the origin (left or right instance) of the communication events for further synchronization. The regional pattern verifier is constructed by synchronizing the left instance with the right instance based on all observable events in R r . The idea is to obtain all pairs of trajectories with the same observations in the subsystem. Definition 10 (Regional Pattern Verifier). Given the refined recognizer R r , the regional pattern verifier is

V = R l r Σr o R r r
, where Σ ro is the set of observable events in R r .

In the regional pattern verifier, any path containing an ambiguous state is called a partial critical path. A part of the regional pattern verifier based on the complete recognizer partly depicted in the right part of figure 3 is shown in the left part of figure 4, where gray nodes are used for ambiguous states. Here we have partial critical paths since they contain ambiguous states.

Global consistency checking consists in verifying whether a partial critical path corresponds to a global critical path. Recall that a global critical path is a path in the global pattern verifier containing an ambiguous state cycle with at least one observable event. As this presence of an observable event is guaranteed from our assumption of observable liveness for each component, the information in a partial critical path important for global consistency checking is all the ambiguous states. And this consistency checking consists in verifying whether there exist ambiguous cycles in the global critical path after synchronization process. Since synchronization between components is based on common communication events, then it is also necessary to retain communication information. In other words, the regional pattern verifier can be abstracted by only retaining information about all its ambiguous states as well as its communication events.

Definition 11 (Abstracted Pattern Verifier). A given regional pattern verifier V is abstracted in V a , called abstracted pattern verifier, by the following steps, where {G s1 , ...G sm } are the components involved in V :

(Retaining only communication events) Delay

Closure with respect to the set of communication events is operated on the pattern verifier V , V a = ∁ Σc (V ).

(Adding qualitative description of the ambiguous state cycles without communication event, which have been lost in step 1) If there exists a local path in

V : q 0 e1 -→ q 1 ... en -→ q n
, where q 0 is the initial state of V , ∃j ∈ {0, ..., n -1}, q j = q n , ∀p ∈ {j, ..., n}, q p is an ambiguous state, ∀k ∈ {j + 1, ..., n}, e k ∈ Σ o , i.e. all events in this ambiguous state cycle are observable events, then the corresponding local path in

V a p = q ′ 0 c1 -→ q ′ 1 ... cm --→ q ′ m is modified as p′ = q ′ 0 c1 -→ q ′ 1 ... cm --→ q ′ m obs --→ q Ω obs --→ q Ω ,
where obs represents the existence of observable events of the subsystem corresponding to V and q Ω represents a verifier state that is ambiguous with respect to the pattern Ω.

For each communication transition (q i e1

-→ q j ) in V a such that only one of the two states is ambiguous, we check its corresponding part in V . If q i is ambiguous and in this corresponding part of V , there is an ambiguous state after e 1 , then this transition in V a becomes (q i e1 -→ q Ω σ -→ q j ). And if q j is ambiguous and in this corresponding part, there is an ambiguous state before e 1 , then this transition in V a becomes (q i σ -→ q Ω e1 -→ q j ), where σ represents an event of the system but which one is not important. The abstracted pattern verifier retains the corresponding parts of all partial critical paths in the regional pattern verifier, which are also called partial critical paths in the following for the sake of simplicity. All ambiguous state cycles are kept in a qualitative way: those with both observable and communication events are kept with their only communication events in the first step of definition 11 while those with only observable events, which are lost in this first step, are recuperated by the second step. The left part of figure 5 shows a part of the abstracted pattern verifier obtained from the regional verifier depicted in figure 4, where ambiguous states are represented by gray nodes. To each global critical path corresponds a partial critical path in the abstracted pattern verifier but the inverse is not true. The reason is that up to now we did not take into account the communication of partial critical paths with their neighborhood in the whole system. In other words, a partial critical path is not necessarily extensible into a global critical path during synchronization. To check the global consistency, given a component, we define as follows a structure called local twin checker, which aims at getting all pairs of local trajectories with the same observations.

Definition 12 (Local Twin Checker). The local twin checker of G

i is C i = (∁ Σ d (G i )) l Σi o (∁ Σ d (G i )) r , where Σ d = Σ io ∪ Σ ic .
The local twin checker of a component is obtained first by operating delay closure with respect to the set of communication events and observable events on its local model and then by distinguishing nonsynchronized communication events with the prefix L and R (left and right instances) before synchronizing the resulted local model with itself based on the observable events. The right part of figure 4 shows part of the local twin checker for the component G 3 .

The local twin checker is used to check whether a partial critical path can be extended into a global crit-ical path through synchronization with the abstracted pattern verifier. As only communication events can block an ambiguous state cycle during synchronization process, then only communication events need to be kept in the local twin checker. Thus the abstracted local twin checker is defined as follows. Definition 13 (Abstracted Local Twin Checker-ALTC). A given local twin checker C i is abstracted in C a i , called abstracted local twin checker (ALTC), by operating Delay Closure with respect to the set of communication events on C i , C a i = ∁ Σi c (C i ) and then by the following step: if there exists a local path in C i : q 0 e1 -→ q 1 ... en -→ q n , where q 0 is the initial state of C i , ∃j ∈ {0, ..., n -1}, q j = q n , ∀k ∈ {j + 1, ..., n}, e k is an observable event, suppose that the corresponding local path in

C a i is p = q ′ 0 c1 -→ q ′ 1 ... cm --→ q ′ m , then it is modified as p′ = q ′ 0 c1 -→ q ′ 1 ... cm --→ q ′ m obs --→ q ′ m .
Thus ALTC preserves all communication events as well as observable cycles. The idea is to check whether the partial critical paths can be extended to global ones after synchronization with all other ALTCs.

During the pattern recognition, by keeping only diagnosability relative paths during the subsystem extension, the search space has been already reduced. Now we will further save space by checking the global consistency of only partial critical paths through synchronization of the abstracted pattern verifier with the ALTCs to avoid building the global pattern verifier.

To check their global consistency, the partial critical paths are synchronized with the ALTCs of the connected components, i.e., those components which are not involved in the subsystem G S corresponding to the abstracted pattern verifier but are neighboring with G S (contain at least one shared communication event with G S ). Now we define the global consistency of a partial critical path as follows. Definition 14 (Global Consistency). A partial critical path is globally consistent if after synchronization with the ALTCs of all connected components, it either contains an ambiguous state cycle or contains an ambiguous state and there exists at least one independent component, i.e., non connected component.

Now we describe the procedure to check the global consistency, given the abstracted pattern verifier V a with its corresponding subsystem G S . V a is first reduced by only retaining all its partial critical paths. When the reduced V a is not empty and there exist connected component to the current subsystem, then the global consistency checking repeatedly performs the following steps:

1. Select one connected component G j and construct its ALTC C a j . 2. Synchronize C a j with the reduced V a , where the set of synchronized events is the set of common left and right communication events of G S and G j . 3. Reduce the newly obtained abstracted pattern verifier by only retaining all its partial critical paths.

If the reduced verifier is not empty and there does exist other connected components, then we turn to step 1.

If there is no other connected component, any path obtained in the final FSM that contains an ambiguous state if there exists an independent component or any path containing an ambiguous cycle if there is no independent component is globally consistent. In this case, non diagnosability information is returned by the algorithm. Otherwise, the system is diagnosable with respect to the pattern. Now we are ready to state and prove the following lemma. Lemma 2 A partial critical path is globally consistent iff it corresponds to (i.e., is the projection of) a global critical path.

Proof : (⇒) Suppose that a partial critical path ρ is globally consistent. After synchronization with the ALTCs of all connected components, if it contains an ambiguous state cycle, then it is easy to deduce that, when ρ is synchronized with all ALTCs, it must contains an ambiguous state cycle. Otherwise, if it contains an ambiguous state and there exists at least one independent component, then after synchronizing with ALTCs of independent components, we get ambiguous cycles. From the assumption of observable liveness of each component, there must exist in this cycle at least one observable event. This means that ρ can be extended into a global critical path. (⇐) Suppose that a partial critical path ρ corresponds to a global critical path ρ′, i.e., the projection of ρ′ on the abstracted pattern verifier is ρ. Since global critical path contains an ambiguous state cycle and ρ contains at least one ambiguous state, then it follows that after synchronization with the ALTCs of all connected components, it either contains an ambiguous state cycle or contains an ambiguous state with at least one independent component. which means that ρ is globally consistent.

From lemma 2 and theorem 1, we can directly obtain the following theorem to verify pattern diagnosability in a distributed way. Theorem 2 A pattern Ω is diagnosable in a system G iff there is no partial critical path that is globally consistent.

For our example, after global consistency checking of the partial critical paths of the abstracted pattern verifier for {G 1 , G 2 } (see figure 5, left), i.e., after synchronizing these paths with the ALTC for G 3 (see figure 5, right), at least one partial critical path does not disappear and contains an ambiguous state cycle. In other words, there does exist a globally consistent partial critical path. Thus this system is not Ωdiagnosable.

Distributed Algorithm

The algorithm 1 describes the procedure of the distributed diagnosability verification for a given pattern. With the set of component models and the pattern under consideration as input, the parameters of the algorithm are initialized. As long as there exists at least one next recognizable event with respect to the current subsystem (line 3), which means that there are other components that should be further exploited for next Algorithm 1 Pattern Diagnosability Algorithm for Distributed System 1: INPUT: component models G 1 , ..., G n of the system G: G = {G 1 , ...G n }; the pattern Ω to be diagnosed in G 2: Initializations: G S ← ∅ (the current subsystem, initially empty); R ← ∅ (the current pattern recognizer, initially empty); Λ GS ← ̟ q 0 Ω (the set of next recognizable events with respect to the current subsystem, initially the set of significant events of Ω that change its initial state q 0 Ω ); 3: while

Λ GS = ∅ do 4: R ← REDU CE(R) 5: G i ← SelectComp(Λ GS , G) 6: G i ← G i R,
where the synchronized events are the common communication events of G S and G i 7:

R ← ConstructLP R(G i , Ω) 8: G S ← Add(G S , G i ) 9: Λ GS ← CollectN RE(R, G S , G, Ω) 10: if R is not a complete recognizer then 11:
return "Ω cannot be recognized in G" 12: else 13:

R ← Ref ine(R) 14: V a ← ConstructAP V (R) 15: CheckGlobalConsistency(G, V a , G S )
pattern recognition, the following steps are repeatedly performed.

1. The current pattern recognizer is reduced by only retaining its diagnosability relative paths (for the first time doing nothing since the current recognizer is empty) and then one component containing at least one next recognizable event is selected (line 4-5).

2. The reduced recognizer is then synchronized with the selected component, based on the set of common communication events of the current subsystem and the selected component (for the first time doing nothing since the current subsystem is empty), and then the local pattern recognizer for this synchronized FSM is again constructed (line 6-7).

3. The current subsystem is now updated by adding the selected component, and then the set of next recognizable events with respect to this current subsystem is updated as described in definition 9 (line 8-9).

When there is no more next recognizable event and the current pattern recognizer is not a complete one, which means that there is no final state in this recognizer, it can be deduced that the pattern can never be recognized in the system. In this case, our algorithm returns the information about non recognizability of the pattern (line 10-11). Otherwise (line 12), i.e., the current pattern recognizer is a complete one, based on which we construct the abstracted pattern verifier (line 13-14) before checking its global consistency (line 15) according to the procedure which steps have been precisely described in the precedent section. 7

IMPLEMENTATION

To illustrate experimentally the correctness of our proposed distributed algorithm and demonstrate its efficiency, we have compared it to the centralized algorithm of [START_REF] Jéron | Supervision patterns in discrete event systems diagnosis[END_REF] after having implemented both. Our results emphasize that the search space of our distributed algorithm is much smaller than that of the centralized one in most cases. Considering that if the number of faults is high we will face a significant increase in complexity, it is better to check the diagnosability individually for each fault, as it is usually done.

The test case that we adopt is a simple example of an office system composed of several components (please see more details about the example in (Ye, 2011)). Then the figure 6 shows the growth of states number and of transitions number in the global pattern recognizer, the global pattern verifier, the distributed complete pattern recognizer and the distributed pattern verifier when the system is extended by adding more independent components. We can see that, since the added components are independent, then for our distributed approach, the search spaces of the complete pattern recognizer (distributed PR) and of the distributed pattern verifier (distributed PV) never increase, while for the centralized approach, the search spaces of the global pattern recognizer (global PR) and of the global pattern verifier (global PV) dramatically increase. This is obviously the case the most favorable to distributed approaches and further experiments to evaluate the gain for intermediate scenarios, depending in particular of the degree of connectedness of the components, are planned. Furthermore, we also compared two distributed approaches for several small systems where all components are connected: normal distributed approach without abstraction and distributed approach with abstraction as described in this paper. The idea was to check how much space can be saved with the abstraction. And the results show that for all these examples (which will have to be completed by larger ones), we can save space between thirty and sixty percentage.

CONCLUSION

In this paper we first showed how to incrementally recognize the pattern by synchronizing the diagnosability relative paths with other components to avoid building a global model. Then, for diagnosability checking, we abstracted just the necessary and sufficient information from local objects to further save the search space. Our approach is general enough to be applicable to any pattern, i.e., both to only one sequence of events or several, even infinite, sequences of events. The correctness and efficiency of our algorithm have been not only theoretically but also practically proved through implementation. To the sake of comparison, we also implemented the centralized algorithm. Our results emphasize that our proposed approach leads to the same conclusions as the centralized one but with a much smaller search space. To the best of our knowledge, these are the first experimental results for pattern diagnosability, even in the centralized case. One perspective of this work is that when a diagnosable subsystem is returned by our approach, it is possible to investigate whether the observations (i.e., observable events) in this subsystem can be reduced while keeping it diagnosable and, if yes, how to reduce them ( [START_REF] Briones | Optimizing the system observability level for diagnosability[END_REF]).

Figure 1 :

 1 Figure 1: A distributed system composed of three components: G1(top left), G2(top right), G3(bottom left), and a pattern Ω to be diagnosed (bottom right).

Figure 2 :

 2 Figure 2: The local pattern recognizer RG S for the initial subsystem, i.e., G1(left), and the reduced one R Ω G S (right).

Figure 3 :

 3 Figure 3: Part of the extended subsystem R Ω G S G2 (left) and part of its corresponding reduced pattern recognizer (right).

Figure 4 :

 4 Figure 4: Part of the regional pattern verifier for {G1, G2} (left) and part of the local twin checker for G3 (right).

Figure 5 :

 5 Figure 5: Part of the abstracted pattern verifier for {G1, G2} (left) and part of the ALTC for G3 (right).

Figure 6 :

 6 Figure 6: The search space growth when adding simple independent components.