Incremental Diagnosis of Discrete-Event Systems

1 Introduction

It is established that diagnosing dynamical systems, represented as discrete-event systems amounts to finding what happened to the system from existing observations. In this context, the diagnostic task consists in determining the trajectories (a sequence of states and events) compatible with the observations. The diagnosis is generally defined as resulting from the synchronization of the automaton modelling the behavior of the system with the automaton that represents the observations sent by the system during the diagnosis period.

In this article, we are interested in avoiding the global computation by slicing the automaton of observations and building the diagnosis on successive slices of observations.

We introduce the concept of automata chain to represent an automaton by a sequence of automata slices. We then provide the properties such an automata chain has to satisfy to be a correct slicing and define a reconstruction operation to get the global automaton back. We demonstrate that, given a correct slicing of the observations, we can compute a global and correct diagnosis from the reconstruction of a diagnosis automata chain.

2 Automata chain

In this section we introduce the concept of automata chain whose goal is to enable us to slice an automaton into pieces. We use the well-known definitions of automata (with I the set of initial states and F the set of final states), path and trajectories (paths between an initial and a final state). The main property of an automata chain (first bullet) is that a state is not allowed to appear in two distinct automata of the chain, except if it is a frontier state between two successive automata, i.e it is a final state of the former and an initial state of the later. More generally, if a state belongs to the ith automata and also to the jth automata, with j > i, it appears also in all the automata between the ith and the jth as a frontier state.

Definition 1 (Automata chain) A sequence of automata (A1 , . . . ,An ) with Ai = (Qi ,E, T i , I i , F i ) is called automata chain, and denoted EA, if:

• ∀i, j, j > i, ∀q, q ∈ Qi ∩Qj ⇒ q ∈ F i ∧ q ∈ I i+1 ,
• ∀i, j, ∀q, q′ , if {q, q′} ⊆ Qi ∩ Qj then ∀p, path of Ai between q and q′ , p is also a path of Aj .

An automata chain is given in Figure 1.

Let EA be an automata chain (A1 , . . . , An). A trajectory of EA is defined as being the ordered (from 1 to n) concatenation of n trajectories, one for each automaton. For instance, the path going from state 1 to state 6 through the states 3 and 5 is a trajectory of the automata chain of Figure 1. Conversely, the path going from state 8 to 6 through 9 is not a trajectory.

Definition 2 (Correct slicing) Let A be an automaton and EA = (A1 , . . . , An) an automata chain. EA is a correct slicing of A, denoted EA = Sli(A), iff the set of trajectories of EA is equal to the set of trajectories of A.

Definition 3 (Automaton reconstruction) Let

EA = (A1 , . . . ,An) be an automata chain with Ai = (Qi ,E, T i , I i , F i ). We call reconstruction of the chain EA, the simplified automaton obtained from (Q1 ∪ . . . ∪ Qn, E, T 1 ∪ . . . ∪ T n, I 1 , F n).

Theorem 1 Let A be an automaton and EA an automata chain. If EA is a correct slicing of A, then A is obtained by the reconstruction of EA. The proof is not given here.

The reconstruction of EA is denoted Sli-1 (EA). If EA is a correct slicing of A, then A = Sli-1 (EA).

We call prefix-closed automaton of A (resp. suffix-closed automaton of A) denoted A+ (resp. A-) the automaton A whose all states are final (resp. initial). We denote A#, the automaton which is both prefix-closed and suffix-closed.

Definition 4 (Automata chain synchronization) We call synchronization of an automata chain EA = (A1 , . . . ,An ) with an automaton M the sequence denoted EA ⊗M defined by: EA ⊗ M = (A1 ⊗ M +,A2 ⊗ M #, . . . ,An-1 ⊗ M #, An ⊗ M -).

Theorem 2 Let EA be an automata chain and M an automaton, then EA ⊗M is an automata chain and EA ⊗M is a correct slicing of Sli-1 (EA) ⊗M. The proof is not given.

3 Diagnosis by slices

Let us first recall the definitions used in the domain of discrete-event systems diagnosis where the model of the system is traditionnally represented by an automaton. The model of the system describes its behaviour and the trajectories of Mod represent the evolutions of the system.

Definition 5 (Model) The model of the system, denoted Mod, is an automaton (QMod ,EMod , T Mod , I Mod , F Mod ). I Mod is the set of possible states at t0. All the states of the system may be final, thus F Mod = QMod , Mod + = Mod and Mod # = Mod -.

Let us turn to observations and diagnosis definitions. Generally, we don't know the total order on the observations emitted by the system. Consequently, the observations are represented by an automaton, each trajectory of which represents a possible order of emission of the observations.

Definition 6 (Observations) The observations, denoted Obsn, is an automaton describing the observations emitted by the system during the period [t0, tn].

Definition 7 (Diagnosis) The diagnosis, denoted ∆n, is an automaton describing the possible trajectories on the model of the system compatible with the observations sent by the system during the period [t0, tn].

The diagnosis is defined (see [Sampath et al., 1996]) as resulting from the synchronization of the automata representing the system model and the observations: ∆n = Mod ⊗Obsn. Using Theo. 2, it is possible to compute the diagnosis by slices. The idea is to compute diagnosis slices, corresponding to observations slices. The global diagnosis can then be reconstructed from the diagnosis automata chain which is obtained.

Definition 8 (Diagnosis by slices - Diagnosis slice) Let

Mod be the system model. Let EObsn = (Obs 1 , . . . ,Obs n), be a correct slicing of Obs n, the observations emitted during the period [t0, tn]. The synchronization of EObsn with Mod, i.e EObsn ⊗ Mod = (Obs 1 ⊗ Mod,Obs 2 ⊗ Mod #, . . . ,Obs n ⊗ Mod #) is the diagnosis by slices of the system. It can be denoted by the diagnosis automata chain (∆1 , . . . ,∆n), where ∆i is called the ith diagnosis slice of the system.

It can be proved (using Theo. 2) that the diagnosis by slices of a system, here EObsn ⊗Mod, correctly represents the diagnosis computed on the global observations since the reconstruction of EObsn ⊗Mod equals the global diagnosis:

Result 1 ∆n = Mod ⊗Obsn = Sli-1 (EObsn ⊗Mod)

4 Incremental diagnosis

In the diagnosis by slices as presented above, the ith diagnosis slice, ∆i , is computed independently from the others, by synchronizing the ith observation slice from the chain EObsn , Obsi , with the systemmodel Mod #. In the incremental synchronization, noted ⊙, (see [Grastien et al., 2005] for more details), the set of initial states of an automaton of the chain is restricted by the set of final states of its predecessor.

Theorem 3 Let EA be an automata chain and M be an automaton. We have Sli-1 (EA ⊙M) = Sli-1 (EA ⊗M). The proof is not given.

Provided that EObsn = (Obs 1 , . . . , Obs n ) is a correct slicing of Obsn we have: ∆n = Sli-1 (EObsn ⊙ Mod ).

We note ∀i, EObsi = (Obs 1 , . . . ,Obs i ), the automata chain of the first i observations automata. Let i < n, and E∆i = (∆1 , . . . ,∆i ) the automata chain resulting from the incremental synchronisation of EObsi with the system model Mod. We can incrementally compute E∆i+1 = EObsi+1 ⊙ Mod as follows:

Result 2 E∆i+1 = (∆1 , . . . ,∆i ,∆i+1 ) where ∆i+1 is the automaton (Obs i+1 ⊗ Mod #) whose initial states are restricted by the set of final states of ∆i .

Let Obsi be the automaton provided by the reconstruction operation on EObsi , and let ∆i be the reconstruction of E∆i .

Result 3 ∆i =Obsi ⊗Mod.

5 Conclusion

In this paper, we formalized the computation by slices of diagnosis for discrete-event systems. We introduced and defined the concept of automata chain that enables us to handle slices of observations and slices of diagnosis rather than global observations and global diagnosis. In the diagnosis by slices, the ith diagnosis slice, ∆i , is computed independently from the others. In [Grastien et al., 2005], we show that this result can be instantiated to the case where the observation automaton is sliced according to time, according to temporal windows.

Our study exhibits the (non trivial) correctness properties that the observation slicing, in an automata chain, has to satisfy in order to guarantee the completeness of the diagnosis computation. This first step is then essential before considering the incrementality of on-line diagnosis computation.