Member, IEEE Franck Cassez

A Note on Fault Diagnosis Algorithms

In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to the emptiness problem for (timed) B üchi automata. Moreover, it is known that, checking whether a discrete-event system is diagnosable, can also be reduced to checking bounded diagnosability. We establish a similar result for timed automata. We also provide a synthesis of the complexity results for the different fault diagnosis problems.

I. INTRODUCTION

Discrete-event systems [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF], [START_REF]The control of discrete event systems[END_REF] (DES) can be modelled by finite automata over an alphabet of observable events Σ. To address decision problems under partial observation of DES, it is sufficient to add a special event τ which represents all the unobservable actions.

The Fault diagnosis problem is a typical example of a problem under partial observation. We assume that the behavior of the DES is known and a model of it is available as a finite automaton over an alphabet Σ ∪ {τ, f }, where Σ is the set of observable events, τ represents the unobservable events, and f is a special unobservable event that corresponds to the faults: this is the original framework introduced by M. Sampath and al. [START_REF] Sampath | Diagnosability of discrete event systems[END_REF] and the reader is referred to this paper for a clear and exhaustive introduction to the subject 1 . The aim of fault diagnosis is to detect faulty sequences of the DES by observing only the events in Σ. A faulty sequence is a sequence of the DES containing an occurrence of event f . We assume that an observer which has to detect faults, knows the specification/model of the DES, and it is able to observe sequences of observable events. Based on this knowledge, it has to announce whether an observation (a word in Σ * ) was produced by a faulty sequence (in (Σ∪{τ, f }) * ) or not. A diagnoser (for a DES) is an observer which observes the sequences of observable events and is able to detect whether a fault event occurred, although it is not observable. If a diagnoser can detect a fault at most ∆ steps 2 after it occurred, the DES is said to be ∆-diagnosable. It is diagnosable if it is ∆-diagnosable for some ∆ ∈ N. Checking whether a DES is ∆-diagnosable for a given ∆ is Franck Cassez is with National ICT Australia & CNRS, Locked Bag 6016, The University of New South Wales, Sydney NSW 1466, Australia.

franck.cassez@cnrs.irccyn.fr,Franck.Cassez@nicta.com.au Author supported by a Marie Curie International Outgoing Fellowship within the 7th European Community Framework Programme. 1 The "companion paper" [START_REF]Failure diagnosis using discrete-event models[END_REF] focuses on a less stringent notion of diagnosability called I-diagnosability. 2 Steps are measured by the number of events, observable or not, which occur in the DES. called the bounded diagnosability problem; checking whether a DES is diagnosable is the diagnosability problem.

Checking diagnosability for a given DES and a fixed set of observable events can be done in polynomial time using the algorithms of [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]. Nevertheless the size of the diagnoser can be exponential as it involves a determinization step. The extension of this DES framework to timed automata [START_REF] Alur | A theory of timed automata[END_REF] (TA) has been proposed by S. Tripakis [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], and he proved that the problem of checking diagnosability of a timed automaton is PSPACE-complete. In the timed case, the diagnoser may be a Turing machine. In a subsequent work by P. Bouyer and al. [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF], the problem of checking whether a timed automaton is diagnosable by a diagnoser which is a deterministic timed automaton was studied (we will not refer to this work in this paper.)

The algorithms proposed in the DES framework [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF] and in the timed automata framework [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF] rely on different assumptions and use different techniques: for example [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF] assumes that the DES is live and contains no unobservable loops; the algorithm to check the diagnosability problem then consists in checking whether a cycle exists in a suitable product automaton; the algorithm of [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF] for timed automata consists in checking whether a infinite word can be accepted by a (product) Büchi automaton: the main reason for the use of a Büchi acceptance condition in this case is to ensure time divergence. Our Contribution. In this paper, we try to put into perspective the results of [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF], [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF] by giving a uniform presentation of the algorithms for fault diagnosis both in the DES and timed automata settings. We also establish a (not difficult but still) missing result for timed automata: diagnosability can be reduced to bounded diagnosability. Another contribution of this paper is to examine in details the complexity of the problems and this is summarized in Table I.

The results in this paper that are not new and have already been published are followed by the reference(s) in the core of the text of after the Theorem keyword.

One such result is Theorem 3 which already appeared in [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]. It generalizes the previous results of [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF] and shows that fault diagnosis reduces to Büchi emptiness for DES. This has some interesting consequences regarding the algorithmic aspects of the problem as well as the tools that can be used to verify diagnosability. These considerations (Section IV) might be of interest for the DES community. Organisation of the Paper. Section II recalls the definitions of timed automata. Section III introduces the fault diagnosis problems we are interested in. Sections IV and V describes the algorithms to solve the diagnosability problems respect-ively for DES and TA. Section VI summarizes the results.

II. PRELIMINARIES

Σ denotes a finite alphabet and Σ τ = Σ∪{τ } where τ ∈ Σ is the unobservable action. B = {TRUE, FALSE} is the set of boolean values, N the set of natural numbers, Z the set of integers and Q the set of rational numbers. R is the set of real numbers and R ≥0 is the non-negative real numbers.

A. Clock Constraints

Let X be a finite set of variables called clocks. A clock valuation is a mapping v : X → R ≥0 . We let R X ≥0 be the set of clock valuations over X. We let 0 X be the zero valuation where all the clocks in X are set to 0 (we use 0 when X is clear from the context). Given δ ∈ R, v + δ denotes the valuation defined by (v + δ)(x) = v(x) + δ. We let C(X) be the set of convex constraints on X, i.e., the set of conjunctions of constraints of the form x ⊲⊳ c with c ∈ Z and ⊲⊳∈ {≤, <, =, >, ≥}. Given a constraint g ∈ C(X) and a valuation v, we write v |= g if g is satisfied by v. Given R ⊆ X and a valuation v, v[R] is the valuation defined by

v[R](x) = v(x) if x ∈ R and v[R](x) = 0 otherwise.

B. Timed Words

The set of finite (resp. infinite) words over Σ is Σ * (resp. Σ ω ) and we let Σ ∞ = Σ * ∪ Σ ω . A language L is any subset of Σ ∞ . A finite (resp. infinite) timed word over Σ is a word in (R ≥0 .Σ) * .R ≥0 (resp. (R ≥0 .Σ) ω ). We let Dur(w) be the duration of a timed word w which is defined to be the sum of the durations (in R ≥0 ) which appear in w; if this sum is infinite, the duration is ∞. Note that the duration of an infinite word can be finite, and such words which contain an infinite number of letters, are called Zeno words. We let Unt(w) be the untimed version of w obtained by erasing all the durations in w, e.g., Unt(0. TW * (Σ) is the set of finite timed words over Σ, TW ω (Σ), the set of infinite timed words and TW ∞ (Σ) = TW * (Σ) ∪ TW ω (Σ). A timed language is any subset of TW ∞ (Σ).

Let π /Σ ′ be the projection of timed words of TW ∞ (Σ) over timed words of TW ∞ (Σ ′ ). When projecting a timed word w on a sub-alphabet Σ ′ ⊆ Σ, the durations elapsed between two events are set accordingly: for instance π /{a,c} (0.4 a 1.0 b 2.7 c) = 0.4 a 3.7 c (projection erases some letters but keep the time elapsed between two letters). Given a timed language L, we let

Unt(L) = {Unt(w) | w ∈ L}. Given Σ ′ ⊆ Σ, π /Σ ′ (L) = {π /Σ ′ (w) | w ∈ L}.

C. Timed Automata

Timed automata (TA) are finite automata extended with real-valued clocks to specify timing constraints between occurrences of events. For a detailed presentation of the fundamental results for timed automata, the reader is referred to the seminal paper of R. Alur and D. Dill [START_REF] Alur | A theory of timed automata[END_REF].

Definition 1 (Timed Automaton): A Timed Automaton A is a tuple (L, l 0 , X, Σ τ , E, Inv, F, R) where: L is a finite set of locations; l 0 is the initial location; X is a finite set of clocks; Σ is a finite set of actions; E ⊆ L × C(X) × Σ τ × 2 X × L is a finite set of transitions; for (ℓ, g, a, r, ℓ ′ ) ∈ E, g is the guard, a the action, and r the reset set; Inv ∈ C(X) L associates with each location an invariant; as usual we require the invariants to be conjunctions of constraints of the form x c with ∈ {<, ≤}. F ⊆ L and R ⊆ L are respectively the final and repeated sets of locations. An example of TA is given in Fig. 1

. A state of A is a pair (ℓ, v) ∈ L × R X ≥0 . A run ̺ of A from (ℓ 0 , v 0
) is a (finite or infinite) sequence of alternating delay and discrete moves:

̺ = (ℓ 0 , v 0 ) δ0 -→ (ℓ 0 , v 0 + δ 0 ) a0 -→ (ℓ 1 , v 1 ) • • • • • • an-1 ---→ (ℓ n , v n ) δn -→ (ℓ n , v n + δ n ) • • • s.t.
for every i ≥ 0:

• v i + δ |= Inv(ℓ i ) for 0 ≤ δ ≤ δ i ; • there is some transition (ℓ i , g i , a i , r i , ℓ i+1 ) ∈ E s.t. : (i) v i + δ i |= g i and (ii) v i+1 = (v i + δ i )[r i ].
The set of finite (resp. infinite) runs from a state s is denoted Runs * (s, A) (resp. Runs ω (s, A)) and we define Runs * (A) = Runs * ((l 0 , 0), A) and Runs ω (A) = Runs ω ((l 0 , 0), A). As before Runs(A) = Runs * (A) ∪ Runs ω (A). If ̺ is finite and ends in s n , we let last(̺) = s n . Because of the denseness of the time domain, the unfolding of A as a graph is infinite (uncountable number of states and delay edges). The trace, tr(̺), of a run ̺ is the timed word

π /Σ (δ 0 a 0 δ 1 a 1 • • • a n δ n • • • ). We let Dur(̺) = Dur(tr(̺)). For V ⊆ Runs(A), we let Tr(V ) = {tr(̺) | ̺ ∈ V }, which
is the set of traces of the runs in V .

A finite (resp. infinite) timed word w is accepted by A if it is the trace of a run of A that ends in an F -location (resp. a run that reaches infinitely often an R-location). L * (A) (resp. L ω (A)) is the set of traces of finite (resp. infinite) timed words accepted by A, and L(A) = L * (A) ∪ L ω (A) is the set of timed words accepted by A. In the sequel we often omit the sets R and F in TA and this implicitly means F = L and R = ∅.

A finite automaton (FA) is a particular TA with X = ∅. Consequently guards and invariants are vacuously true and time elapsing transitions do not exist. We write A = (L, l 0 , Σ τ , E, F, R) for a FA. A run is thus a sequence of the form:

̺ = ℓ 0 a0 -→ ℓ 1 • • • • • • an-1 ---→ ℓ n • • •
where for each i ≥ 0, (ℓ i , a i , ℓ i+1 ) ∈ E. Definitions of traces and languages are straightforward. In this case, the duration of a run ̺ is the number of steps (including τ -steps) of ̺: if ̺ is finite and ends in ℓ n , Dur(̺) = n and otherwise Dur(̺) = ∞.

D. Region Graph of a TA

The region graph RG(A) of a TA A is a finite quotient of the infinite graph of A which is time-abstract bisimilar to A [START_REF] Alur | A theory of timed automata[END_REF]. It is a FA on the alphabet E ′ = E ∪ {τ }. The states of RG(A) are pairs (ℓ, r) where ℓ ∈ L is a location of A and r is a region of R X ≥0 . More generally, the edges of the graph are tuples (s, t, s ′ ) where s, s ′ are states of RG(A) and t ∈ E ′ . Genuine unobservable moves of A labelled τ are labelled by tuples of the form (s, (g, τ, r), s ′ ) in RG(A). An edge (g, λ, R) in the region graph corresponds to a discrete transition of A with guard g, action λ and reset set R. A τ move in RG(A) stands for a delay move to the time-successor region. The initial state of RG(A) is (l 0 , 0). A final (resp. repeated) state of RG(A) is a state (ℓ, r) with ℓ ∈ F (resp. ℓ ∈ R). A fundamental property of the region graph [START_REF] Alur | A theory of timed automata[END_REF] is:

Theorem 1 ( [START_REF] Alur | A theory of timed automata[END_REF]): L(RG(A)) = Unt(L(A)). In other words:

1) if w is accepted by RG(A), then there is a timed word

v with Unt(v) = w s.t. v is accepted by A. 2) if v is accepted by A, then Unt(w) is accepted RG(A).
The (maximum) size of the region graph is exponential in the number of clocks and in the maximum constant of the automaton A (see [START_REF] Alur | A theory of timed automata[END_REF]):

|RG(A)| = |L| • |X|! • 2 |X| • K |X|
where K is the largest constant used in A.

E. Product of TA Definition 2 (Product of TA):

Let A i = (L i , l i 0 , X i , Σ i τ , E i , Inv i ), i ∈ {1, 2}, be TA s.t. X 1 ∩ X 2 = ∅. The product of A 1 and A 2 is the TA A 1 × A 2 = (L, l 0 , X,Σ τ , E, Inv) given by: L = L 1 × L 2 ; l 0 = (l 1 0 , l 2 0 ); Σ = Σ 1 ∪ Σ 2 ; X = X 1 ∪ X 2 ; and E ⊆ L × C(X) × Σ τ × 2 X × L and ((ℓ 1 , ℓ 2 ), g 1,2 , σ, r, (ℓ ′ 1 , ℓ ′ 2 )) ∈ E if: • either σ ∈ (Σ 1 ∩ Σ 2 ) \ {τ }, and (i) (ℓ k , g k , σ, r k , ℓ ′ k ) ∈ E k for k = 1 and k = 2; (ii) g 1,2 = g 1 ∧ g 2 and (iii) r = r 1 ∪ r 2 ; • or for k = 1 or k = 2, σ ∈ (Σ k \ Σ 3-k ) ∪ {τ }, and (i) (ℓ k , g k , σ, r k , ℓ ′ k ) ∈ E k ; (ii) g 1,2 = g k and (iii) r = r k ; and finally Inv(ℓ 1 , ℓ 2 ) = Inv(ℓ 1 ) ∧ Inv(ℓ 2 ).
The definition of product also applies to finite automata.

III. FAULT DIAGNOSIS PROBLEMS

The material in this section is based on [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF], [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]. To model timed systems with faults, we use timed automata on the alphabet Σ τ,f = Σ τ ∪ {f } where f is the faulty (unobservable) event. We only consider one type of fault here, but the results we give are valid for many types of faults {f 1 , f 2 , • • • , f n }: indeed solving the many types diagnosability problem amounts to solving n one type diagnosability problems [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]. Other unobservable events are abstracted as a τ action (one τ suffices as these events are all unobservable).

The system we want to supervise is given as a TA A = (L, l 0 ,X, Σ τ,f , E, Inv). Fig. 1 gives an example of such a system (α ∈ N is a parameter). Invariants in the automaton A(α) are written within square brackets as in which are the traces 3 of ∆-faulty and non-faulty runs of A.

[x ≤ 3]. Let ∆ ∈ N. A run of A ̺ = (ℓ 0 , v 0 ) δ0 -→ (ℓ 0 , v 0 + δ 0 ) a0 -→ (ℓ 1 , v 1 ) • • • • • • an-1 ---→ (ℓ n , v n ) δn -→ (ℓ n , v n + δ) • • • is ∆-faulty if: (1) there is an index i s.t. a i = f and (2) the duration of the run ̺ ′ = (ℓ i , v i ) δi -→ • • • δn -→ (ℓ n , v n + δ n ) • • • is larger than ∆. We let Faulty ≥∆ (A) be the set l0 l1 [x ≤ 6] l2 [x ≤ 6] l4 [x ≤ 3]
The purpose of fault diagnosis is to detect a fault as soon as possible. Faults are unobservable and only the events in Σ can be observed as well as the time elapsed between these events. Whenever the system generates a timed word w, the observer can only see π /Σ (w). If an observer can detect faults in this way it is called a diagnoser. A diagnoser must detect a fault within a given delay ∆ ∈ N.

Definition 3 (∆-Diagnoser): Let A be a TA over the alphabet Σ τ,f and ∆ ∈ N. A ∆-diagnoser for A is a mapping D : TW * (Σ) → {0, 1} such that:

• for each ̺ ∈ NonFaulty(A), D(tr(̺)) = 0, • for each ̺ ∈ Faulty ≥∆ (A), D(tr(̺)) = 1. A is ∆-diagnosable if there exists a ∆-diagnoser for A. A is diagnosable if there is some ∆ ∈ N s.t. A est ∆-diagnosable.
Remark 1: Nothing is required for the ∆ ′ -faulty words with ∆ ′ < ∆. Thus a diagnoser could change its mind and answers 1 for a ∆ ′ -faulty word, and 0 for a ∆ ′′ -faulty word with ∆ ′ < ∆ ′′ < ∆.

Example 1: The TA A(3) in Fig. 1 taken from [8] is 3-diagnosable. For the timed words of the form t.a.δ.b.t ′ with δ ≤ 3, no fault has occurred, whereas when δ > 3 a fault must have occurred. A diagnoser can then be easily constructed. As we have to wait for a "b" action to detect a fault, D cannot detect a fault in 2 time units. If α = 2, in A(2) there are two runs:

ρ 1 (δ) = (l 0 , 0) a -→ (l 1 , 0) 2.5 --→ (l 1 , 2.5) f -→ (l 2 , 2.5) 0.2 --→ (l 2 , 2.7) b -→ (l 3 , 2.7) δ -→ (l 2 , 2.7 + δ) ρ 2 (δ) = (l 0 , 0) a -→ (l 1 , 0) 2.5 --→ (l 1 , 2.5) τ -→ (l 4 , 2.5) 0.2 --→ (l 4 , 2.7) b -→ (l 5 , 2.7) δ -→ (l 5 , 2.7 + δ)
3 Notice that tr(̺) erases τ and f . that satisfy tr(ρ 1 (δ)) = tr(ρ 2 (δ)), and this for every δ ≥ 0. For each ∆ ∈ N, there are two runs ρ 1 (∆) and ρ 2 (∆) which produce the same observations and thus no diagnoser can exist. A( 2) is not diagnosable. The classical fault diagnosis problems are the following: Problem 1 (Bounded or ∆-Diagnosability):

INPUTS: A TA A = (L, ℓ 0 , X, Σ τ,f , E, Inv) and ∆ ∈ N. PROBLEM: Is A ∆-diagnosable?
Problem 2 (Diagnosability):

INPUTS: A TA A = (L, ℓ 0 , X, Σ τ,f , E, Inv). PROBLEM: Is A diagnosable?
Problem 3 (Maximum delay):

INPUTS: A TA A = (L, ℓ 0 , X, Σ τ,f , E, Inv). PROBLEM: If A is diagnosable, what is the minimum ∆ s.t. A is ∆-diagnosable ?
We do not address here the problem of synthesizing a diagnoser and the reader is referred to [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF], [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF] for a detailed presentation.

A necessary and sufficient condition for diagnosability was already established in [START_REF] Sampath | Diagnosability of discrete event systems[END_REF], but was stated on a candidate diagnoser. We give here a simple language based condition, valid in both the discrete and timed cases. According to Definition 3, A is diagnosable, iff, there is some ∆ ∈ N s.t. A is ∆-diagnosable. Thus:

A is not diagnosable⇐⇒∀∆ ∈ N, A is not ∆-diagnosable.
Moreover a trace based definition of ∆-diagnosability can be stated as:

A is ∆-diagnosable iff Faulty tr ≥∆ (A) ∩ NonFaulty tr (A) = ∅. (1)
This gives a necessary and sufficient condition for nondiagnosability and thus diagnosability:

A is not diagnosable⇐⇒          ∀∆ ∈ N, ∃ρ ∈ NonFaulty(A) ∃ρ ′ ∈ Faulty ≥∆ (A) s.t. tr(ρ) = tr(ρ ′ ), (2)
or in other words, there is no pair of runs (ρ 1 , ρ 2 ) with ρ 1 ∈ Faulty ≥∆ (A), ρ 2 ∈ NonFaulty(A) the traces of which are equal.

IV. ALGORITHMS FOR DISCRETE EVENT SYSTEMS

In this section we briefly review the main results about diagnosability of discrete-event systems. We consider here that the DES is given by a FA A = (Q, q 0 , Σ τ,f , →).

Moreover we assume that the automaton A is such that every faulty run of length n can be extended to a run of length n + 1; this assumption simplifies the proofs (of some lemmas in [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]) and if A does not satisfy it, it is easy to add τ loops to deadlock states of A to ensure it holds. It does not modify the observation made by the external observer and thus does not modify the diagnosability status of A.

A. Problem 1

To check Problem 1 we have to decide whether there is a (∆ + 1)-faulty run ρ 1 and a non-faulty run ρ 2 that give the same observations when projected on Σ. An easy way to do this is to build a finite automaton B which accepts exactly those runs, and check whether L(B) is empty or not.

Let A 1 = (Q × {-1, 0, • • • , ∆ + 1}, (q 0 , -1), Σ τ , → 1 ) be the automaton with → 1 defined by:

• (q, n) λ --→ 1 (q ′ , n) if q λ --→ q ′ and n = -1 and λ ∈ Σ ∪ {τ }; • (q, n) λ --→ 1 (q ′ , min(n + 1, ∆ + 1)) if q λ --→ q ′ and n ≥ 0 and λ ∈ Σ ∪ {τ }; • (q, n) τ --→ 1 (q ′ , min(n + 1, ∆ + 1) if q f --→ q ′ . Let A 2 = (Q, q 0 , Σ τ , → 2 ) with: q λ --→ 2 q ′ if q λ --→ q ′ and λ ∈ Σ ∪ {τ }. Define B = A 1 × A 2 with the final states F B of B given by: F B = {((ℓ, ∆ + 1), ℓ ′ ) | (ℓ, ℓ ′ ) ∈ Q × Q}. We let R B = ∅. It is straightforward to see that: Theorem 2: A is ∆-diagnosable iff L * (B) = ∅.
As language emptiness for B amounts to reachability checking, it can be done in linear time in the size of B. Still strictly speaking, the automaton B has size (∆ + 1) • |A| 2 which is exponential in the size of the inputs of the problem A and ∆ because ∆ is given in binary. Thus Problem 1 can be solved in EXPTIME. As storing ∆ requires only polynomial space Problem 1 is in PSPACE. Actually checking Problem 1 can be done in PTIME (see the end of this section).

B. Problem 2

To check whether A is diagnosable, we build a synchronized product A 1 × A 2 , s.t. A 1 behaves exactly as A but records in its state whether a fault has occurred, and A 2 behaves like A without the faulty runs as before. It is then as if ∆ = 0 in the previous construction. We let → 1,2 be the transition relation of A 1 × A 2 . A faulty run of A 1 × A 2 is a run for which A 1 reaches a faulty state of the form (q, 1). To decide whether A is diagnosable we build an extended version of A 1 ×A 2 which is a Büchi automaton B as follows: B has a boolean variable z which records whether A 1 participated in the last transition fired by A 1 × A 2 . Assume we have a predicate 4 A 1 Move(t) which is true when A 1 participates in a transition t of the product A 1 ×A 2 . A state of B is a pair (s, z) where s is a state of A 1 ×A 2 . B is given by the tuple ((Q×{0, 1}×Q)×{0, 1}, ((q 0 , 0), q 0 , 0), Σ τ , -→ B , ∅, R B ) with:

• (s, z) σ --→ B (s ′ , z ′ ) if (i) there exists a transition t : s σ --→ 1,2 s ′ in A 1 × A 2 , and (ii) z ′ = 1 if A 1 Move(t) and z ′ = 0 otherwise; • R B = {(((q, 1), q ′ ), 1) | ((q, 1), q ′ ) ∈ A 1 × A 2 }.
B accepts the language L(B) = L ω (B) ⊆ Σ ω . Moreover this language satisfies a nice property:

Theorem 3 ([10]): A is diagnosable iff L ω (B) = ∅.
This theorem has for consequence that the diagnosability problem can be checked in quadratic time: the automaton B has size 4 • |A| 2 i.e., O(|A| 2 ) and checking emptiness for Büchi automaton can be done in linear time. Thus diagnosability can be checked in PTIME. Polynomial algorithms for checking diagnosability (Problem 2) were already reported in [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]. In these two papers, the plant cannot have unobservable loops i.e., loops that consist of τ actions. Our algorithm does not have this limitation (we even may have to add τ loops to ensure that each faulty run can be extended). Note also that in [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF], [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF], the product construction is symmetric in the sense that A 2 is a copy of A as well. Our A 2 does not contain the f transitions, which is a minor difference complexity-wise, but in practice this can be useful to reduce the size of the product.

Moreover, reducing Problem 2 to emptiness checking of Büchi automata is interesting in many respects:

• the proof (see [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]) of Theorem 3 is easy and short; algorithms for checking Büchi emptiness are wellknown and correctness follows easily as well; • this also implies that standard tools from the modelchecking/verification community can be used to check for diagnosability. There are very efficient tools to check for Büchi emptiness (e.g., SPIN [START_REF] Holzmann | Software model checking with spin[END_REF]). Numerous algorithms, like on-the-fly algorithms [START_REF] Couvreur | On-the-fly emptiness checks for generalized büchi automata[END_REF] have been designed to improve memory/time consumption (see [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF] for an overview). Also when the DES is not diagnosable a counter-example is provided by these tools. The input languages (like PROMELA for SPIN) that can be used to specify the DES are more expressive than the specification languages of some dedicated tools 5 like DESUMA/UMDES [START_REF] Ricker | Desuma: A tool integrating giddes and umdes[END_REF] (notice that the comparison with DESUMA/UMDES concerns only the diagnosability algorithms; DESUMA/UMDES can perform a lot more than checking diagnosability). From Theorem 3, one can also conclude that diagnosability amounts to bounded diagnosability: indeed if A is diagnosable, there can be no accepting cycles of faulty states in B; in this case there cannot be a faulty run of length more than 2 • |Q| 2 in B. Thus Problem 2 reduces to a particular instance of Problem 1 which was already stated in [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]:

Theorem 4 ([6]): A is diagnosable if and only if A is (2 • |Q| 2 )-diagnosable.
This appeals from some final remarks on the algorithms we should choose to check diagnosability: for the particular case of ∆ = 2 • |A| 2 , solving Problem 1 (a reachability problem) can be done in time 2•|A| 2 •|A| 2 i.e., O(|A| 4 ) whereas solving directly Problem 2 as a Büchi emptiness problem can be done in O(|A| 2 ). Thus the extra-cost of using a reachability algorithm is still reasonable.

The Büchi-emptiness algorithm used to solve Problem 2 can also be used to solve Problem 1 for a given ∆ and automaton A with set of states Q: if ∆ ≥ 2 • |Q| 2 , then we check wether A is diagnosable and this gives the answer to Problem 1; otherwise, if ∆ < 2 • |Q| 2 , we check wether A is ∆-diagnosable but in polynomial time. Hence Problem 1 5 UMDES was the only publicly available tool which could be found by a Google search. can be solved in polynomial time O(|A| 4 ).

Finally, solving Problem 3 can be done by a binary search solving iteratively ∆-diagnosability problems starting with ∆ = 2 • |A| 2 . Thus Problem 3 can be solved in O(|A| 4 ). Using a different approach, Problem 3 was reported to be solvable in O(|Q| 3 ) in [START_REF] Yoo | Computation of fault detection delay in discrete-event systems[END_REF].

In the sequel we recall the algorithm for checking diagnosability for TA and establish a counterpart of Theorem 4 for TA.

V. ALGORITHMS FOR TIMED AUTOMATA

We first recall how to check ∆-diagnosability for TA which first appeared in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF].

A. Problem 1

Let t be a fresh clock not in X.

Let A 1 (∆) = ((L × {0, 1}) ∪ {Bad}, (l 0 , 0), X ∪ {t}, Σ τ , E 1 , Inv 1 ) with: • ((ℓ, n), g, λ, r, (ℓ ′ , n)) ∈ E 1 if (ℓ, g, λ, r, ℓ ′ ) ∈ E, λ ∈ Σ ∪ {τ }; • ((ℓ, 0), g, τ, r ∪ {t}, (ℓ ′ , 1)) ∈ E 1 if (ℓ, g, f, r, ℓ ′ ) ∈ E; • Inv 1 ((ℓ, n)) = Inv(ℓ); • for ℓ ∈ L, ((ℓ, 1), t ≥ ∆, τ, ∅, Bad) ∈ E 1 and A 2 = (L, l 0 , X 2 , Σ τ , E 2 , Inv 2 ) with: • X 2 = {x 2 | x ∈ X} (clocks of A are renamed); • (ℓ, g 2 , λ, r 2 , ℓ ′ ) ∈ E 2 if (ℓ, g, λ, r, ℓ ′ ) ∈ E, λ ∈ Σ ∪ {τ }
with: g 2 is g where the clocks x in X are replaced by their counterpart x 2 ; r 2 is r with the same renaming;

• Inv 2 (ℓ) = Inv(ℓ). Consider A 1 (∆) × A 2 .
A faulty state of A 1 (∆) × A 2 is a state of the form (((ℓ, 1), v), (ℓ ′ , v ′ )) i.e., where the state of A 1 is faulty. Let Runs ≥∆ (A 1 (∆) × A 2 ) be the runs of A 1 (∆) × A 2 s.t. a faulty state of A 1 is encountered and s.t. at least ∆ time units have elapsed after this state. If this set is not empty, there are two runs, one ∆-faulty and one non-faulty which give the same observation. Moreover, because t is reset exactly when the first fault occurs, we have t ≥ ∆. Conversely, if a state of the form (((ℓ, 1), v), (ℓ ′ , v ′ )) with v(t) ≥ ∆ is reachable, then there are two runs, one ∆faulty and one non-faulty which give the same observation. Location Bad in A 1 is thus reachable exactly if A is not ∆-diagnosable. Let D be A 1 (∆) × A 2 with the final set of locations F D = {Bad} and R D = ∅.

Theorem 5 ([8]): A is ∆-diagnosable iff L * (D) = ∅. Checking reachability of a location for TA is PSPACEcomplete [START_REF] Alur | A theory of timed automata[END_REF]. More precisely, it can be done in linear time on the region graph. The size of the region graph of D is

(2 • |L| 2 + |L|) • (2|X| + 1)! • 2 2|X|+1 • K 2|X| • ∆
where K is the maximal constant appearing in A. Hence:

Corollary 1: Problem 1 can be solved in PSPACE for TA.

B. Problem 2

As for the untimed case, we build an automaton D, which is special version of A 1 (∆) × A 2 . Assume A 1 is defined as before omitting the clock t and the location Bad. In the timed case, we have to take care of the following real-time related problems [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]:

• some runs of A 2 might prevent time from elapsing from a given point in time. In this case, equation ( 1) cannot be satisfied but this is for an artificial reason: for ∆ large enough, there will be no ∆ faulty run in A 1 × A 2 because A 2 will block the time. In this case we can claim that A is diagnosable but it is not realistic; • a more tricky thing may happen: A 1 could produce a Zeno run 6 after a fault occurred. This could happen by firing infinitely many τ transitions in a bounded amount of time. If we declare that A is not diagnosable but the only witness run is a Zeno run, it does not have any physical meaning. Thus to declare that A is not diagnosable, we should find a non-Zeno witness which is realizable, and for which time diverges. To cope with the previous dense-time related problems we have to ensure that the two following conditions are met: C 1 : A 2 is timelock-free i.e., A 2 cannot prevent time from elapsing; this implies that every finite nonfaulty run of A 2 can be extended in a time divergent run. We can assume that A 2 satisfies this property or check it on A 2 before checking diagnosability; C 2 : for A to be non-diagnosable, we must find an infinite run in A 1 × A 2 for which time diverges. C 2 can be enforced by adding a third timed automaton Div(x) and synchronizing it with A 1 × A 2 . Let x be a fresh clock not in X. Let Div(x) = ({0, 1}, 0, {x}, E, Inv) be the TA given in Fig. 2. If we use F = ∅ and R = {1} for Div(x), any accepted run is time divergent. Let D = (A 1 × A 2 ) × Div(x) with F D = ∅ and R D is the set of states where A 1 is in a faulty state and Div(x) is location 1. The following theorem is the TA counterpart of Theorem 3: [START_REF] Alur | A theory of timed automata[END_REF]. Thus deciding diagnosability is in PSPACE.

Theorem 6 ([8]): A is diagnosable iff L ω (D) = ∅. Deciding whether L ω (A) = ∅ for TA is PSPACE- complete
The reachability problem for TA can be reduced to a diagnosability problem [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]. Let A be a TA on alphabet Σ and End a particular location of A. We want to check whether End is reachable in A. It suffices to build A ′ on the alphabet Σ τ,f by adding to A the following transitions: (End, TRUE, λ, ∅, End) for λ ∈ {τ, f }. Then: A ′ is not diagnosable iff End is reachable in A. It follows that:

Theorem 7 ( [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]): Problem 2 is PSPACE-complete for TA. We can draw another conclusion from the previous theorem: if a TA A is diagnosable, there cannot be any cycle with faulty states in the region graph of A 1 ×A 2 ×Div(x). Indeed, otherwise, by Theorem 1, there would be a non-Zeno word in A 1 × A 2 × Div(x) itself 7 . Let α(A) denote the size of the region graph RG(A 1 ×A 2 ×Div(x)). If A is diagnosable, then (P 1 ): a faulty state in RG(A 1 ×A 2 ×Div(x)) can be followed by at most α(A) (faulty) states. Notice that a faulty state cannot be followed by a state (s, r) where r is an unbounded region of A, as this would give rise to a non-Zeno word in A 1 × A 2 × Div(x). Hence (P 2 ): all the regions following a faulty state in RG(A 1 × A 2 × Div(x)) are bounded. As the amount of time which can elapse within a region is less than 1 time unit 8 , this implies that the duration of the longest faulty run in A 1 × A 2 × Div(x) is less than α(A). Actually as every other region is a singular region9 , it must be less than (α(A)/2) + 1. Thus we obtain the following result:

Theorem 8: A is diagnosable if and only if A is (α(A)/2) + 1-diagnosable.
As diagnosability can be reduced to ∆-diagnosability for TA:

Corollary 2: Problem 1 is PSPACE-complete for TA. Problem 3 can be solved by a binary search and is also in PSPACE for TA. Although Problem 1 and Problem 2 are PSPACE-complete for timed automata, the price to pay to solve Problem 2 as a reachability problem is much higher than solving it as a Büchi emptiness problem: indeed the size of the region graph of A 1 (α(A)) × A 2 is the square of the size of the region graph of A 1 × A 2 × Div(x) which is already exponential in the size of A. Time-wise this means a blow up from 2 n to 2 n 2 which is not negligible as in the discrete case.

VI. CONCLUSION

The main conclusions we can draw from the previous presentation are two-fold.

From a theoretical viewpoint, it shows that the fault diagnosis algorithms for DES and for TA are essentially the same: in both cases, diagnosability can be reduced to Büchi emptiness; and also to bounded diagnosability. The interesting point is that the complexity of the algorithms are the same for DES and TA except that for timed automata, the complexity measure is space (Table I). From a practical viewpoint, it clearly shows that the model-checking algorithms and tools developed in the model-checking/verification community can be used to solve the diagnosability problems; these tools usually have a very expressive specification language (e.g., Promela/Spin [START_REF] Holzmann | Software model checking with spin[END_REF], UPPAAL [START_REF] Behrmann | A tutorial on UPPAAL[END_REF] or KRONOS [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF]) and very efficient data structures/implementations (e.g., [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF] or [START_REF] Behrmann | UPPAAL implementation secrets[END_REF]).

We can also use the results in Table I to guide our choice of algorithms for checking diagnosability. Let Reach denote the reachability algorithm for checking ∆-diagnosability and Buchi denote the Büchi emptiness algorithm for checking diagnosability:

• time-wise, solving the diagnosability problem for a finite automaton using Reach is a bit more expensive than using Buchi, but the difference is not drastic; • for a timed automaton A it is totally different: spacewise the amount of space required by Reach is the square of the amount of space required by Buchi. Time-wise this means a worst case blow up from 2 |A| 2 to 2 |A| 4 . It is thus clear that one should use the Büchi emptiness algorithm in this case. Checking Büchi emptiness for TA is efficiently implemented in a version of KRONOS (Profounder) [START_REF] Tripakis | Checking timed buchi automata emptiness on simulation graphs[END_REF] and in UPPAAL-TiGA [START_REF] Behrmann | Uppaal-tiga: Time for playing games![END_REF], the game version of UPPAAL [START_REF] David | UPPAAL-TiGA 2009 -Towards Realizable Strategies[END_REF].

The previous results show that model-checking tools (both for finite and timed automata) are suitable to solve the diagnosis problems, and provide expressive specification languages and efficient algorithms and tools.

  4 a 1.0 b 2.7 c) = abc. In this paper we write timed words as 0.4 a 1.0 b 2.7 c • • • where the real values are the durations elapsed between two letters: thus c occurs at global time 4.1.

Figure 1 .

 1 Figure 1. The Timed Automaton A(α)

Figure 2 .

 2 Figure 2. Timed Automaton Div(x)

This is easy to define when building A 1 × A 2 .

A Zeno run is a run with infinitely many discrete steps the duration of which is bounded.

Note that this is true because we add the automaton Div(x). Otherwise an infinite run in the region graph of a TA does not imply a time divergent run in the TA A itself.

We assume the constants are integers.

A singular region is a region in which time elapsing is not possible e.g., defined by x = 0 ∧ y ≥ 1.


Franck Cassez

The Complexity of Codiagnosability for Discrete Event and Timed Systems

In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.

Introduction

Discrete-event systems [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Ramadge | The control of discrete event systems[END_REF] (DES) can be modelled by finite automata (FA) over an alphabet of observable events Σ.

The fault diagnosis problem is a typical example of a problem under partial observation. The aim of fault diagnosis is to detect faulty sequences of the DES. The assumptions are that the behavior of the DES is known and a model of it is available as a finite automaton over an alphabet Σ ∪ {τ, f }, where Σ is the set of observable events, τ represents the unobservable events, and f is a special unobservable event that corresponds to the faults: this is the original framework introduced by M. Sampath et al. [3] and the reader is referred to this paper for a clear and exhaustive introduction to the subject. A faulty sequence is a sequence of the DES containing an occurrence of event f . An observer which has to detect faults, knows the specification/model of the DES, and it is able to observe sequences of observable events. Based on this knowledge, it has to announce whether an observation it makes (in Σ * ) was produced by a faulty sequence (in (Σ ∪ {τ, f }) * ) of the DES or not. A diagnoser (for a DES) is an observer which observes the sequences of observable events and is able to detect whether a fault event has occurred, although it is not observable. If a diagnoser can detect a fault at most ∆ steps 1 after it has occurred, the DES is said to be ∆-diagnosable. It is diagnosable if it is ∆-diagnosable for some ∆ ∈ N. Checking whether a DES is ∆-diagnosable for a given ∆ is called the bounded diagnosability problem; checking whether a DES is diagnosable is the diagnosability problem.

Checking diagnosability for a given DES and a fixed set of observable events can be done in polynomial time using the algorithms of [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF][START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]. If a diagnoser exists there is a finite state one. Nevertheless the size of the diagnoser can be exponential as it involves a determinization step. The extension of this DES framework to timed automata (TA) has been proposed by S. Tripakis in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], and he proved that the problem of checking diagnosability of a timed automaton is PSPACE-complete. In the timed case however, the diagnoser may be a Turing machine. The problem of checking whether a timed automaton is diagnosable by a diagnoser which is a deterministic timed automaton was studied by P. Bouyer et al. [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF].

Codiagnosability generalizes diagnosability by considering decentralized architectures. Such decentralized architectures have been introduced in [START_REF] Debouk | Coordinated decentralized protocols for failure diagnosis of discrete event systems[END_REF] and later refined in [START_REF] Wang | Diagnosis of discrete event systems using decentralized architectures[END_REF][START_REF] Qiu | Decentralized failure diagnosis of discrete event systems[END_REF]. In these architectures, local diagnosers (with their own partial view of the system) can send some information to a coordinator, summarizing their observations. The coordinator then computes a result from the partial results of the local diagnosers. The goal is to obtain a coordinator that can detect the faults in the system. When local diagnosers do not communicate with each other nor with a coordinator (protocol 3 in [START_REF] Debouk | Coordinated decentralized protocols for failure diagnosis of discrete event systems[END_REF]), the decentralized diagnosis problem is called codiagnosis [START_REF] Qiu | Decentralized failure diagnosis of discrete event systems[END_REF][START_REF] Wang | Diagnosis of discrete event systems using decentralized architectures[END_REF]. In this case, codiagnosis means that each fault can be detected by at least one local diagnoser. In the paper [START_REF] Qiu | Decentralized failure diagnosis of discrete event systems[END_REF], codiagnosability is considered and an algorithm to check codiagnosability is presented for discrete event systems (FA). An upper bound for the complexity of the algorithm is EXPTIME. In [START_REF] Wang | Diagnosis of discrete event systems using decentralized architectures[END_REF], the authors consider a hierarchical framework for decentralized diagnosis. In [START_REF] Basilio | Robust codiagnosability of discrete event systems[END_REF] a notion of robust codiagnosability is introduced, which can be thought of as a fault tolerant (local diagnosers can fail) version of codiagnosability. None of the previous papers has addressed the codiagnosability problems for timed automata. Moreover, the exact complexity of the codiagnosis problems is left unsettled for discrete event systems (FA).

Our Contribution. In this paper, we study the codiagnosability problems for FA and TA. We settle the complexity of the problems for FA (PSPACE-complete), improving on the best known upper bound (EXPTIME). We also address the codiagnosability problems for TA and provide new results: algorithms to check codiagnosability and also codiagnosability under bounded resources. Our contribution is both of theoretical and practical interests. The algorithms we provide are optimal, and can also be implemented using standard model-checking tools like SPIN [START_REF] Holzmann | Software model checking with spin[END_REF] for FA, or UPPAAL [START_REF] Behrmann | A tutorial on UPPAAL[END_REF] for TA. This means that very expressive languages can be used to specify the systems to codiagnose and very efficient implementations and data structures are readily available.

Organisation of the Paper. Section 2 recalls the definitions of finite automata and timed automata. We also give some results on the Intersection Emptiness Problems (section 2.6) that will be used in the next sections. Section 3 introduces the fault codiagnosis problems we are interested in, and a necessary and sufficient condition that characterizes codiagnosability for FA and TA. Section 4 contains the first main results: optimal algorithms for the codiagnosability problems for FA and TA. Section 5 describes how to synthesize the codiagnosers and the limitations of this technique for TA. Section 6 is devoted to the codiagnosability problem under bounded resources for TA and contains the second main result of the paper.

Omitted proofs can be found in the full version of this paper [START_REF] Cassez | The complexity of codiagnosability for discrete event and timed systems. Research report[END_REF].

Preliminaries

Σ denotes a finite alphabet and Σ τ = Σ ∪{τ } where τ ∈ Σ is the unobservable action. B = {TRUE, FALSE} is the set of boolean values, N the set of natural numbers, Z the set of integers and Q the set of rational numbers. R is the set of real numbers and R ≥0 (resp. R >0 ) is the set of non-negative (resp. positive) real numbers. We denote tuples (or vectors) by

d = (d 1 , • • • , d k ) and write d[i] for d i .

Clock Constraints

Let X be a finite set of variables called clocks. A clock valuation is a mapping v : X → R ≥0 . We let R X ≥0 be the set of clock valuations over X. We let 0 X be the zero valuation where all the clocks in X are set to 0 (we use 0 when X is clear from the context). Given δ ∈ R, v + δ is the valuation defined by (v + δ)(x) = v(x) + δ. We let C(X) be the set of convex constraints on X, i.e., the set of conjunctions of constraints of the form x ⊲⊳ c with c ∈ Z and ⊲⊳∈ {≤, <, =, >, ≥}. Given a constraint g ∈ C(X) and a valuation v, we write v |= g if g is satisfied by the valuation v. We also write

[[g]] for the set {v | v |= g}. Given a set R ⊆ X and a valuation v of the clocks in X, v[R] is the valuation defined by v[R](x) = v(x) if x ∈ R and v[R](x) = 0 otherwise.

Timed Words

The set of finite (resp. infinite) words over Σ is Σ * (resp. Σ ω ) and we let Σ ∞ = Σ * ∪ Σ ω . A language L is any subset of Σ ∞ . A finite (resp. infinite) timed word over Σ is a word in (R ≥0 .Σ) * .R ≥0 (resp. (R ≥0 .Σ) ω ). Duration(w) is the duration of a timed word w which is defined to be the sum of the durations (in R ≥0 ) which appear in w; if this sum is infinite, the duration is ∞. Note that the duration of an infinite word can be finite, and such words which contain an infinite number of letters, are called Zeno words. We let Unt(w) be the untimed version of w obtained by erasing all the durations in w. An example of untiming is Unt(0.4 a 1.0 b 2.7 c) = abc. In this paper we write timed words as 0. TW * (Σ) is the set of finite timed words over Σ, TW ω (Σ), the set of infinite timed words and TW(Σ) = TW * (Σ) ∪ TW ω (Σ). A timed language is any subset of TW(Σ).

Let π Σ ′ be the projection of timed words of TW(Σ) over timed words of TW(Σ ′ ). When projecting a timed word w on a sub-alphabet Σ ′ ⊆ Σ, the durations elapsed between two events are set accordingly: for instance for the timed word 0.4 a 1.0 b 2.7 c, we have π {a,c} (0.4 a 1.0 b 2.7 c) = 0.4 a 3.7 c (note that projection erases some letters but keep the time elapsed between two letters). Given a timed language L, we let

Unt(L) = {Unt(w) | w ∈ L}. Given Σ ′ ⊆ Σ, π Σ ′ (L) = {π Σ ′ (w) | w ∈ L}.

Timed Automata

Timed automata are finite automata extended with real-valued clocks to specify timing constraints between occurrences of events. For a detailed presentation of the fundamental results for timed automata, the reader is referred to the seminal paper of R. Alur and D. Dill [START_REF] Alur | A theory of timed automata[END_REF].

Definition 1 (Timed Automaton).

A Timed Automaton A is a tuple (L, l 0 , X, Σ τ , E, Inv, F, R) where: L is a finite set of locations; l 0 is the initial location; X is a finite set of clocks; Σ is a finite set of actions; E ⊆ L × C(X) × Σ τ × 2 X × L is a finite set of transitions; in a transition (ℓ, g, a, r, ℓ ′ ), g is the guard, a the action, and r the reset set; as usual we often write a transition ℓ g,a,r ----→ ℓ ′ ; Inv ∈ C(X) L associates with each location an invariant; as usual we require the invariants to be conjunctions of constraints of the form x c with ∈ {<, ≤}; F ⊆ L is the set of final locations and R ⊆ L is the set of repeated locations.

The size of a TA A is denoted |A| and is the size of the clock constraints i.e., the size of the transition relation

E. A state of A is a pair (ℓ, v) ∈ L × R X ≥0 . A run ̺ of A from (ℓ 0 , v 0 )
is a (finite or infinite) sequence of alternating delay and discrete moves:

̺ = (ℓ 0 , v 0 ) δ0 -→ (ℓ 0 , v 0 + δ 0 ) a0 -→ (ℓ 1 , v 1 ) • • • an-1 ---→ (ℓ n , v n ) δn -→ (ℓ n , v n + δ n ) • • • s.t. for every i ≥ 0: -v i + δ |= Inv(ℓ i ) for 0 ≤ δ ≤ δ i ; -there is some transition (ℓ i , g i , a i , r i , ℓ i+1 ) ∈ E s.t. : (i) v i + δ i |= g i , (ii) v i+1 = (v i + δ i )[r i ].
The set of finite (resp. infinite) runs in A from a state s is denoted Runs * (s, A) (resp. Runs ω (s, A)). We let Runs * (A) = Runs * (s 0 , A), Runs ω (A) = Runs ω (s 0 , A) with s 0 = (l 0 , 0), and Runs(A) = Runs * (A) ∪ Runs ω (A). If ̺ is finite and ends in s n , we let last(̺) = s n . Because of the denseness of the time domain, the unfolding of A as a graph is infinite (uncountable number of states and delay edges). The trace, tr(̺), of a run ̺ is the timed word π Σ (δ

0 a 0 δ 1 a 1 • • • a n δ n • • • ). The duration of the run ̺ is Duration(̺) = Duration(tr(̺)). For V ⊆ Runs(A), we let Tr(V ) = {tr(̺) | ̺ ∈ V },
which is the set of traces of the runs in V . A finite (resp. infinite) timed word w is accepted by A if it is the trace of a run of A that ends in an F -location (resp. a run that reaches infinitely often an R-location). L * (A) (resp. L ω (A)) is the set of traces of finite (resp. infinite) timed words accepted by A, and L(A) = L * (A) ∪ L ω (A) is the set of timed words accepted by A.

In the sequel we often omit the sets R and F in TA and this implicitly means F = L and R = ∅.

A timed automaton A is deterministic if there is no τ labelled transition in A, and if, whenever (ℓ, g, a, r, ℓ ′ ) and (ℓ, g ′ , a, r ′ , ℓ ′′ ) are transitions of A, g ∧ g ′ ≡ FALSE. A is complete if from each state (ℓ, v), and for each action a, there is a transition (ℓ, g, a, r, ℓ ′ ) such that v |= g. We note DTA the class of deterministic timed automata.

A finite automaton is a particular TA with X = ∅. Consequently guards and invariants are vacuously true and time elapsing transitions do not exist. We write A = (Q, q 0 , Σ τ , E, F, R) for a finite automaton. A run is thus a sequence of the form:

̺ = ℓ 0 a0 -→ ℓ 1 • • • • • • an-1 ---→ ℓ n • • •
where for each i ≥ 0, (ℓ i , a i , ℓ i+1 ) ∈ E. Definitions of traces and languages are the same as for TA. For FA, the duration of a run ̺ is the number of steps (including τ -steps) of ̺: if ̺ is finite and ends in ℓ n , Duration(̺) = n and otherwise Duration(̺) = ∞.

Region Graph of a Timed Automaton

A region of R X ≥0 is a conjunction of atomic constraints of the form x ⊲⊳ c or x -y ⊲⊳ c with c ∈ Z, ⊲⊳∈ {≤, <, =, >, ≥} and x, y ∈ X. The region graph RG(A) of a TA A is a finite quotient of the infinite graph of A which is time-abstract bisimilar to A [START_REF] Alur | A theory of timed automata[END_REF]. It is a finite automaton on the alphabet E ′ = E ∪ {τ }. The states of RG(A) are pairs (ℓ, r) where ℓ ∈ L is a location of A and r is a region of R X ≥0 . More generally, the edges of the graph are tuples (s, t, s ′ ) where s, s ′ are states of RG(A) and t ∈ E ′ . Genuine unobservable moves of A labelled τ are labelled by tuples of the form (s, (g, τ, r), s ′ ) in RG(A). An edge (g, λ, R) in the region graph corresponds to a discrete transition of A with guard g, action λ and reset set R. A τ move in RG(A) stands for a delay move to the time-successor region. The initial state of RG(A) is (l 0 , 0). A final (resp. repeated) state of RG(A) is a state (ℓ, r) with ℓ ∈ F (resp. ℓ ∈ R). A fundamental property of the region graph [START_REF] Alur | A theory of timed automata[END_REF] is:

Theorem 1 (R. Alur and D. Dill, [15]). L(RG(A)) = Unt(L(A)).

The (maximum) size of the region graph is exponential in the number of clocks and in the maximum constant of the automaton A (see [START_REF] Alur | A theory of timed automata[END_REF]):

|RG(A)| = |L| • |X|! • 2 |X| • K |X|
where K is the largest constant used in A.

Product of Timed Automata

Given a n locations ℓ 1 , • • • , ℓ n , we write ℓ for the tuple

(ℓ 1 , • • • , ℓ n ) and let ℓ[i] = ℓ i . Given a letter a ∈ Σ 1 ∪ • • • ∪ Σ n , we let I(a) = {k | a ∈ Σ k }.

Definition 2 (Product of TA). Let

A i = (L i , l i 0 , X i , Σ i τ , E i , Inv i ), i ∈ {1, • • • , n}, be n TA s.t. X i ∩ X j = ∅ for i = j. The product of the A i is the TA A = A 1 × • • • × A n = (L, l 0 , X, Σ τ , E, Inv) given by: L = L 1 × • • • × L n ; l 0 = (l 1 0 , • • • , l n 0 ); Σ = Σ 1 ∪ • • • ∪ Σ n ; X = X 1 ∪ • • • ∪ X n ; E ⊆ L × C(X) × Σ τ × 2 X × L and (ℓ, g, a, r, ℓ ′ ) ∈ E if: -either a ∈ Σ \ {τ }, and 1. for each k ∈ I(a), (ℓ[k], g k , a, r k , ℓ ′ [k]) ∈ E k , 2. g = ∧ k∈I(a) g k and r = ∪ k∈I(a) r k ; 3. for k ∈ I(a), ℓ ′ [k] = ℓ[k]; -or a = τ and ∃j s.t. (ℓ[j], g j , τ, r j , ℓ ′ [j]) ∈ E j , g = g j , r = r j and for k = j, ℓ ′ [k] = ℓ[k]. Inv(ℓ) = ∧ n k=1 Inv(ℓ[k]).
This definition of product also applies to finite automata (no clock constraints).

If the automaton A i has the set of final locations F i then the set of final locations for

A is F 1 ו • •×F n .
For Büchi acceptance, we add a counter c to A which is incremented every time the product automaton A encounters an R i -location in A i , following the standard construction for product of Büchi automata. The automaton constructed with the counter c is A + . The repeated set of states of

A + is L 1 × • • • × L n-1 × L n × {n}.
As the sets of clocks of the A i 's are disjoint2 , the following holds:

Fact 1 L * (A) = ∩ n i=1 L * (A i ) and L ω (A + ) = ∩ n i=1 L ω (A i ).

Intersection Emptiness Problem

In this section we give some complexity results for the emptiness problem on products of FA and TA.

First consider the following problem on deterministic finite automata (DFA):

Problem 1 (Intersection Emptiness for DFA)

INPUTS: n deterministic finite automata A i , 1 ≤ i ≤ n, over the alphabet Σ. PROBLEM: Check whether ∩ n i=1 L * (A i ) = ∅. The size of the input for Problem 1 is n i=1 |A i |. Theorem 2 (D. Kozen, [16]). Problem 1 is PSPACE-complete.
D. Kozen's Theorem also holds for Büchi languages:

Theorem 3. Checking whether ∩ n i=1 L ω (A i ) = ∅ is PSPACE-complete. Problem 1 is PSPACE-hard even if A 2 , • • • , A n are
automata where all the states are accepting and A 1 is the only automaton with a proper set of accepting states (actually one accepting state is enough).

Proposition 1. Let

A i , 1 ≤ i ≤ n be n DFA over the alphabet Σ. If for all A i , 2 ≤ i ≤ n, all states of A i are accepting, Problem 1 is already PSPACE-hard.
The next results are counterparts of D. Kozen's results for TA.

Problem 2 (Intersection Emptiness for TA) INPUTS: n TA

A i = (L i , l i 0 , X i , Σ i τ , E i , Inv i , F i ), 1 ≤ i ≤ n with X k ∩ X j = ∅ for k = j. PROBLEM: Check whether ∩ n i=1 L * (A i ) = ∅. Theorem 4. Problem 2 is PSPACE-complete.
The previous theorem extends to Büchi languages:

Problem 3 (B üchi Intersection Emptiness for TA) INPUTS: n TA A i = (L i , l i 0 , X i , Σ i τ , E i , Inv i , R i ), 1 ≤ i ≤ n with X k ∩ X j = ∅ for k = j. PROBLEM: Check whether ∩ n i=1 L ω (A i ) = ∅. Theorem 5. Problem 3 is PSPACE-complete.

Fault Codiagnosis Problems

We first recall the basics of fault diagnosis. The purpose of fault diagnosis [3] is to detect a fault in a system as soon as possible. The assumption is that the model of the system is known, but only a subset Σ o of the set of events Σ generated by the system are observable. Faults are also unobservable.

Whenever the system generates a timed word w ∈ TW * (Σ), an external observer can only see π Σo (w). If an observer can detect faults under this partial observation of the outputs of A, it is called a diagnoser. We require a diagnoser to detect a fault within a given delay ∆ ∈ N.

To model timed systems with faults, we use timed automata on the alphabet Σ τ,f = Σ τ ∪ {f } where f is the faulty (and unobservable) event. We only consider one type of fault, but the results we give are valid for many-types of faults {f 1 , f 2 , • • • , f n }: indeed solving the many-types diagnosability problem amounts to solving n one-type diagnosability problems [START_REF] Yoo | Polynomial-time verification of diagnosability of partially-observed discrete-event systems[END_REF]. The observable events are given by Σ o ⊆ Σ and τ is always unobservable.

The idea of decentralized or distributed diagnosis was introduced in [START_REF] Debouk | Coordinated decentralized protocols for failure diagnosis of discrete event systems[END_REF]. It is based on decentralized architectures: local diagnosers and a communication protocol. In these architectures, local diagnosers (with their own partial view of the system) can send to a coordinator some information, using a given communication protocol. The coordinator then computes a result from the partial results of the local diagnosers. The goal is to obtain a coordinator that can detect the faults in the system. When local diagnosers do not communicate with each other nor with a coordinator (protocol 3 in [START_REF] Debouk | Coordinated decentralized protocols for failure diagnosis of discrete event systems[END_REF]), the decentralized diagnosis problem is called codiagnosis [START_REF] Qiu | Decentralized failure diagnosis of discrete event systems[END_REF][START_REF] Wang | Diagnosis of discrete event systems using decentralized architectures[END_REF]. In this section we formalize the notion of codiagnosability introduced in [START_REF] Qiu | Decentralized failure diagnosis of discrete event systems[END_REF] in a style similar to [START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]. This allows us to obtain a necessary and sufficient condition for codiagnosability of FA but also to extend the definition of codiagnosability to timed automata.

In the sequel we assume that the model of the system is a TA A = (L, l 0 , X, Σ τ,f , E, Inv) and is fixed. We also make the assumption that the TA A cannot prevent time from elapsing. For FA, this assumption is that from any state, a discrete transition can be taken. If it is not case, τ loop actions can be added with no impact on the (co)diagnosability status of the system. This is a standard assumption in diagnosability and is required to avoid taking into account these cases that are not interesting in practice.

Faulty Runs

Let ∆ ∈ N. A run ̺ = (ℓ 0 , v 0 ) δ0 -→ (ℓ 0 , v 0 + δ 0 ) a0 -→ (ℓ 1 , v 1 ) • • • an-1 ---→ (ℓ n , v n ) δn -→ (ℓ n , v n + δ) • • • of A is ∆-faulty if: (1) there is an index i s.t. a i = f and (2) the duration of ̺ ′ = (ℓ i , v i ) δi -→ • • • δn -→ (ℓ n , v n + δ n ) • • • is larger or equal to ∆. We let Faulty ≥∆ (A) be the set of ∆-faulty runs of A. Note that by definition, if ∆ ′ ≥ ∆ then Faulty ≥∆ ′ (A) ⊆ Faulty ≥∆ (A). We let Faulty(A) = ∪ ∆≥0 Faulty ≥∆ (A) = Faulty ≥0 (A)
For discrete event systems (FA), the notion of time is the number of transitions (discrete steps) in the system. A ∆-faulty run is thus a run with a fault action f followed by at least ∆ discrete steps (some of them can be τ or even f actions). When we consider codiagnosability problems for discrete event systems, this definition of ∆faulty runs apply. The other definitions are unchanged.

Remark 1. A timed automaton where discrete actions are separated by one time unit is not equivalent to using a finite automaton when solving a fault diagnosis problem. For instance, a timed automaton can generate the timed words 1.f.1.a and 1.τ.1.τ.1.a. In this case, it is 1-diagnosable: after reading the timed word 2.a we announce a fault. If we do not see the 1-time unit durations, the timed words f.a and τ 2 .a give the same observation. And thus it is not diagnosable if we cannot measure time. Using a timed automaton where discrete actions are separated by one time unit gives to the diagnoser the ability to count/measure time and this is not equivalent to the fault diagnosis problem for FA (discrete event systems).

Codiagnosers and Codiagnosability Problems

A codiagnoser is a tuple of diagnosers, each of which has its own set of observable events Σ i , and whenever a fault occurs, at least one diagnoser is able to detect it. In the sequel we write π i in place of π Σi for readability reasons. A codiagnoser can be formally defined as follows:

Definition 3 ((∆, E)-Codiagnoser). Let A be a timed automaton over the alphabet Σ τ,f , ∆ ∈ N and E = (Σ i ) 1≤i≤n be a family of subsets of Σ. A (∆, E)-codiagnoser for A is a mapping

D = (D 1 , • • • , D n ) with D i : TW * (Σ i ) → {0, 1} such that: -for each ̺ ∈ NonFaulty(A), n i=1 D[i](π i (tr(̺))) = 0, -for each ̺ ∈ Faulty ≥∆ (A), n i=1 D[i](π i (tr(̺))) ≥ 1.
As for diagnosability, the intuition of this definition is that (i) the codiagnoser will raise an alarm (D outputs a value different from 0) when a ∆-faulty run has been identified, and that (ii) it can identify those ∆-faulty runs unambiguously. The codiagnoser is not required to do anything special for ∆ ′ -faulty runs with ∆ ′ < ∆ (although it is usually required that once it has announced a fault, it does not change its mind and keep outputting 1).

A is (∆, E)-codiagnosable if there exists a (∆, E)-codiagnoser for

A. A is E-codia- gnosable if there is some ∆ ∈ N s.t. A is (∆, E)-codiagnosable.
The standard notions [3] of ∆-diagnosability and ∆-diagnoser are obtained when the family E is the singleton E = {Σ}. The fundamental codiagnosability problems for timed automata are the following:

Problem 4 ((∆, E)-Codiagnosability) INPUTS: A TA A = (L, l 0 , X, Σ τ,f , E, Inv), ∆ ∈ N and E = (Σ i ) 1≤i≤n . PROBLEM: Is A (∆, E)-codiagnosable? Problem 5 (Codiagnosability) INPUTS: A TA A = (L, l 0 , X, Σ τ,f , E, Inv) and E = (Σ i ) 1≤i≤n . PROBLEM: Is A E-codiagnosable? Problem 6 (Optimal delay) INPUTS: A TA A = (L, l 0 , X, Σ τ,f , E, Inv) and E = (Σ i ) 1≤i≤n . PROBLEM: What is the minimum ∆ s.t. A is (∆, E)-codiagnosable?
The size of the input for Problem 4 is |A| + log ∆ + n • |Σ|, and for Problems 5 and 6 it is |A| + n • |Σ|.

In addition to the previous problems, we will consider the construction of a (∆, E)codiagnoser when A is (∆, E)-codiagnosable in section 5.

Necessary and Sufficient Condition for Codiagnosability

In this section we generalize the necessary and sufficient condition for diagnosability [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF][START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF] to codiagnosability. Lemma 1. A is not (∆, E)-codiagnosable if and only if ∃̺ ∈ Faulty ≥∆ (A) and

∀1 ≤ i ≤ n, ∃̺ i ∈ NonFaulty(A) s.t. π i (tr(̺)) = π i (tr(̺ i )). (1)
Using Lemma 1, we obtain a language based characterisation of codiagnosability extending the one given in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF][START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF]

. Let π -1 i (X) = {w ∈ TW * (Σ) | π i (w) ∈ X}. Lemma 2. A is (∆, E)-codiagnosable if and only if Faulty tr ≥∆ (A) ∩ n i=1 π -1 i π i (NonFaulty tr (A)) = ∅. (2)
4 Algorithms for Codiagnosability Problems

(∆, E)-Codiagnosability (Problem 4)

Deciding Problem 4 amounts to checking whether equation 2 holds or not. Recall that A = (L, l 0 , X, Σ τ,f , E, Inv). Let t be a fresh clock not in X.

Let A f (∆) = ((L × {0, 1}) ∪ {Bad}, (l 0 , 0), X ∪ {t}, Σ τ , E f , Inv f ) with: -((ℓ, n), g, λ, r, (ℓ ′ , n)) ∈ E f if (ℓ, g, λ, r, ℓ ′ ) ∈ E, λ ∈ Σ ∪ {τ }; -((ℓ, 0), g, τ, r ∪ {t}, (ℓ ′ , 1)) ∈ E f if (ℓ, g, f, r, ℓ ′ ) ∈ E; -for ℓ ∈ L, ((ℓ, 1), t ≥ ∆, τ, ∅, Bad) ∈ E f ; -Inv f ((ℓ, n)) = Inv(ℓ).
A f (∆) is similar to A but when a fault occurs it switches to a copy of A (encoded by n = 1). When sufficient time has elapsed in the copy (more than ∆ time units), location Bad can be reached. The language accepted by A f (∆) with the set of final states {Bad} is thus L * (A f (∆)) = Faulty tr ≥∆ (A). Define A i = (L, l 0 , X i , Σ τ , E i , Inv i ) with:

-X i = {x i | x ∈ X} (create copies of clocks of A); -(ℓ, g i , λ, r i , ℓ ′ ) ∈ E i if (ℓ, g, λ, r, ℓ ′ ) ∈ E, λ ∈ Σ i ∪ {τ } with: g i is g
where the clocks x in X are replaced by their counterparts x i in X i ; r i is r with the same renaming;

-(ℓ, g i , τ, r i , ℓ ′ ) ∈ E i if (ℓ, g, λ, r, ℓ ′ ) ∈ E, λ ∈ Σ \ Σ i -Inv i (ℓ) = Inv(ℓ) with clock renaming (x i in place of x).
Each A i accepts only non-faulty traces as the f -transitions are not in A i . If the set of final locations is L for each A i , then L * (A i ) = π i (NonFaulty tr (A)). To accept π -1 i π i (NonFaulty tr (A)) we add transitions (ℓ, TRUE, λ, ∅, ℓ) for each location ℓ of E i and for each λ ∈ Σ \ Σ i . Let A * i be the automaton on the alphabet Σ constructed this way. By definition of

A * i , L * (A * i ) = π -1 i π i (NonFaulty tr (A)) . Define B = A f (∆) × A * 1 × A * 2 × • • • × A * n with the set of final locations F B = {Bad} × L × • • • × L. We let R B = ∅.
Using equation 2 we obtain:

Lemma 3. A is (∆, E)-codiagnosable iff L * (B) = ∅.
The size of the input for problem 4 is |A| + log ∆ + n • |Σ|. The size of A f (∆) is (linear in) the size of A and log ∆, i.e., O(|A| + log ∆). The size of A * i is also bounded by the size of A.

It follows that |A f (∆)| + n i=1 |A * i | is bounded by (n + 1)
|A| and is polynomial in the size of the input of problem 4. We thus have a polynomial reduction from Problem 4 to the intersection emptiness problem for TA. We can now establish the following result: Theorem 6.Problem 4 is PSPACE-complete for Timed Automata. It is already PSPACEhard for Deterministic Finite Automata.

E-Codiagnosability (Problem 5)

In this section we show how to solve the E-codiagnosability problem. The algorithm is a generalisation of the procedure for deciding diagnosability of discrete event and timed systems (see [START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF] for a recent presentation).

For standard fault diagnosis (one diagnoser and E = {Σ}), A is not diagnosable if there is an infinite faulty run in A the projection of which is the same as the projection of a non-faulty one [START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF].

The procedure for checking diagnosability of FA and TA slightly differ due to specific features of timed systems. We recall here the algorithms to check diagnosability of FA and TA [START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF][START_REF] Tripakis | Fault diagnosis for timed automata[END_REF] and extend them to codiagnosability.

Codiagnosability for Finite Automata.

To check whether a FA A is diagnosable, we build a synchronized product A f × A 1 , s.t. A f behaves exactly like A but records in its state whether a fault has occurred, and A 1 behaves like A without the faulty runs (transitions labelled f are cut off). This corresponds to A f (∆) defined in section 4.1 without the clock ∆.

A faulty run in the product A f × A 1 is a run for which A f reaches a faulty state of the form (q, 1). To decide whether A is diagnosable we build an extended version of A f × A 1 which is a Büchi automaton B [START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF]: B has a boolean variable z which records whether A f participated in the last transition fired by A f × A 1 . A state of B is a pair (s, z) where s is a state of A f × A 1 . B is given by the tuple ((Q × {0, 1} × Q) × {0, 1}, ((q 0 , 0), q 0 , 0), Σ τ , -→ B , ∅, R B ) with:

-(s, z) λ --→ B (s ′ , z ′ ) if (i) there exists a transition t : s λ --→ s ′ in A f × A 1 , and (ii) z ′ = 1 if λ is a move of A f and z ′ = 0 otherwise; -R B = {(((q, 1), q ′ ), 1) | ((q, 1), q ′ ) ∈ A f × A 1 }.
The important part of the previous construction relies on the fact that, for A to be non Σdiagnosable, A f should have an infinite faulty run (and take infinitely many transitions) and A 1 a corresponding non-faulty run (note that this one can be finite) giving the same observation. With the previous construction, we have [START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF]:

A is diagnosable iff L ω (B) = ∅.
The construction for codiagnosability is an extension of the previous one adding

A 2 , • • • , A n to the product. Let B co = A f ×A 1 ו • •×A n with A i defined in section 4.1.
In B co we again use the variable z to indicate whether A f participated in the last move. Define the set of repeated states of B co by: R B co = {(((q, 1), q), 1) | ((q, 1),

q) ∈ A f × A 1 ו • •×A n }.
By construction, a state in R B co is: (1) faulty as it contains a component (q, 1) for the state of A f and (2) A f participated in the last move as z = 1. It follows that:

Lemma 4. A is E-codiagnosable iff L ω (B co ) = ∅.

Theorem 7. Problem 5 is PSPACE-complete for Deterministic Finite Automata.

Codiagnosability for Timed Automata. Checking diagnosability for timed automata requires an extra step in the construction of the equivalent of automaton B defined above: indeed, for TA, a run having infinitely many discrete steps could well be zeno, i.e., the duration of such a run can be finite. This extra step in the construction was first presented in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]. It can be carried out by adding a special timed automaton Div with two locations {0, 1} and synchronizing it with A f × A 1 . If we use F = ∅ and R = {1} for Div, any accepted run is time divergent and thus cannot be zeno. Let D = A f ×Div×A 1 and let F D = ∅ and R D be the set of states where A f is in a faulty location and Div is in location 1. For standard fault diagnosis, the following holds [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF][START_REF] Cassez | A Note on Fault Diagnosis Algorithms[END_REF]:

A is diagnosable iff L ω (D) = ∅.
The construction to check codiagnosability is obtained by adding

A 2 , • • • , A n in the product. Let D co = A f × Div × A 1 × • • • ×A n . Lemma 5. A is E-codiagnosable iff L ω (D co ) = ∅.
Theorem 8. Problem 5 is PSPACE-complete for Timed Automata.

Optimal Delay (Problem 6)

Using the results for checking E-codiagnosability and (∆, E)-codiagnosability, we obtain algorithms for computing the optimal delay. Lemma 4 reduces codiagnosability of FA to Büchi emptiness on a product automaton. The number of states of the automaton B co is bounded by 4 • |A| n , and the number of faulty states by 2 • |A| n . This implies that:

Proposition 2. Let A be a FA. If A is E-codiagnosable, then A is (2 • |A| n , E)-codia- gnosable.
From Proposition 2, we can conclude that: Theorem 9. Problem 6 can be solved in PSPACE for FA.

For timed automata, a similar reasoning can be done on the region graph of D co . If a TA A is E-codiagnosable, there cannot be any cycle with faulty locations in RG(D co ). Otherwise there would be a non-zeno infinite word in L(D co ) and thus an infinite timediverging faulty run in A, with corresponding non-faulty runs in each A i , giving the same observation. Let K be the size of RG(D co ). If A is E-codiagnosable, then a faulty state in RG(D co ) can be followed by at most K states. Otherwise a cycle in the region graph would occur and thus L ω (D co ) would not be empty. This also implies that all the states (s, r) in RG(D co ) that can follow a faulty state must have a bounded region. As the amount of time that can elapse in one region is at most 1 time unit 4 , the maximum duration of a faulty run in D co is bounded by K. This implies that:

Proposition 3. Let A be a TA. If A is E-codiagnosable, then A is (K, E)-codiagnosable with K = |RG(D co )|.
The size of the region graph of D co is bounded by

|L| n+1 •((n+1)|X|+1)!•2 (n+1)|X|+1 • M (n+1)|X|+1 . Thus the encoding of constant K has size O(n • |A|).
Theorem 10. Problem 6 can be solved in PSPACE for Timed Automata.

Synthesis of Codiagnosers

The reader is referred to the extended version of this paper [START_REF] Cassez | The complexity of codiagnosability for discrete event and timed systems. Research report[END_REF] for a detailed presentation of this section. The synthesis of codiagnosers for FA and TA can be carried out by extending the known construction for diagnosers [3].

The construction of a diagnoser for timed automata [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF] consists in computing onthe-fly the current possible states of the timed automaton A f after reading a timed word w. This procedure is effective but gives a diagnoser which is a Turing machine. The machine computes a state estimate of A after each observable event, and if it contains only faulty states, it announces a fault.

Obviously the same construction can be carried out for codiagnosis: we define the Turing machines M i , 1 ≤ i ≤ n that estimate the state of A. When one M i 's estimate on an input Σ i -trace w contains only faulty states, we set D i (w) = 1 and 0 otherwise. This tuple of Turing machines is a (∆, E)-codiagnoser.

Computing the estimates with Turing machines might be too expensive to be implemented at runtime. More efficient and compact codiagnosers might be needed with reasonable computation times. In the next section, we address the problem of codiagnosis for TA under bounded resources.

Codiagnosis with Deterministic Timed Automata

The fault diagnosis problem using timed automata has been introduced and solved by P. Bouyer et al. in [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF]. The problem is to determine, given a TA A, whether there exists a diagnoser D for A, that can be represented by a deterministic timed automaton.

Fault Diagnosis with Deterministic Timed Automata

When synthesizing (deterministic) timed automata, an important issue is the amount of resources the timed automaton can use: this can be formally defined [START_REF] Bouyer | Timed control with partial observability[END_REF] by the (number of) clocks, Z, that the automaton can use, the maximal constant max, and a granularity 1 m . As an example, a TA of resource µ = ({c, d}, 2, 1 3 ) can use two clocks, c and d, and the clocks constraints using the rationals -2 ≤ k/m ≤ 2 where k ∈ Z and m = 3. A resource µ is thus a triple µ = (Z, max, 1 m ) where Z is finite set of clocks, max ∈ N and 1 m ∈ Q >0 is the granularity. DTA µ is the class of DTA of resource µ.

Remark 2. Notice that the number of locations of the DTA in DTA µ is not bounded and hence this family has an infinite (yet countable) number of elements.

If a TA A is ∆-diagnosable with a diagnoser that can be represented by a DTA D with resource µ, we say that A is (∆, D)-diagnosable. P. Bouyer et al. in [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF] considered the problem of deciding whether there exists a DTA diagnoser with resource µ:

Problem 7 (∆-DTA-Diagnosability [7]) INPUTS: A TA A = (L, l 0 , X, Σ τ,f , E, Inv), ∆ ∈ N, a resource µ = (Z, max, 1 m )
. PROBLEM: Is there any D ∈ DTA µ s.t. A is (∆, D)-diagnosable ? Theorem 11 (P. Bouyer et al., [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF]). Problem 7 is 2EXPTIME-complete.

The solution to the previous problem is based on the construction of a two-player safety game, G A,∆,µ . In this game a set of states, Bad, must be avoided for A to be ∆diagnosable. The most permissive winning strategy gives the set of all DTA µ diagnosers (the most permissive diagnosers) which can diagnose A (or ∅ is there is none). We refer to the extended version [START_REF] Cassez | The complexity of codiagnosability for discrete event and timed systems. Research report[END_REF], section 6.1 for a detailed presentation of this construction.

Algorithm for Codiagnosability

In this section we include the alphabet Σ of a DTA in the resource µ and write µ = (Σ, Z, max, 1 m ).

Problem 8 (∆-DTA-Codiagnosability) INPUTS:

A TA A = (L, l 0 , X, Σ τ,f , E, Inv), ∆ ∈ N, and a family of resources To solve Problem 8, we extend the algorithm given in [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF] for DTA-diagnosability. Let G i be the game G A,∆,µi and Bad i the set of bad states. Given a strategy f i , we let f i (G i ) be the outcome5 of G i when f i is played by Player 0. Given w ∈ TW * (Σ) and a DTA A on Σ, we let last(w, A) be the location reached when w is read by A. Lemma 6. A is (∆, D)-codiagnosable iff there is a tuple of strategies f s.t.

µ i = (Σ i , Z i , max i , 1 mi ), 1 ≤ i ≤ n with Σ i ⊆ Σ. PROBLEM: Is there any codiagnoser D = (D 1 , D 2 , • • • , D n ) with D i ∈ DTA µi s.t. A is (∆, D)-codiagnosable ? ∆-
(1) ∀1 ≤ i ≤ n, f [i] is state-based on the game G i , and

(2) ∀w ∈ Tr(A) If S i = last(π Σi (w), f i (G i )), 1 ≤ i ≤ n, then ∃1 ≤ j ≤ n, s.t. S j ∈ Bad j .
Item (2) of Lemma 6 states that there is no word in A for which all the Player 0 in the games G i are in bad states. The strategies for each Player 0 are not necessarily winning in each G i , but there is always one Player 0 who has not lost the game G i . From the previous Lemma, we can obtain the following result:

Theorem 12. Problem 8 is 2EXPTIME-complete.

Conclusion & Future Work

Table 1 gives an overview of the results described in this paper (bold face) for the codiagnosis problems in comparison with the results for the diagnosis problems (second line, normal face). Our ongoing work is to extend the results on diagnosis using dynamic observers [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF][START_REF] Cassez | Fault diagnosis with static or dynamic diagnosers[END_REF] to the codiagnosis framework.

Ackowledgements. The author would like to thank the anonymous reviewers for their helpful comments.

A Proofs for Section 2

A.1 Proof of Proposition 1

Proof. Let A 1 , A 2 , • • • , A n be n deterministic automata with accepting states F 1 , F 2 , • • • , F n on the alphabet Σ. Let λ be a fresh letter not in Σ. Define automaton A ′ i by: from any state q in F i , add a transition (q, λ, ⊥) where ⊥ is new state. Let F ′ 1 = {⊥} and F ′ i be all the states of

A ′ i . It is clear that L * (A ′ 1 ) = L * (A 1 ).λ. We can prove that ∩ n i=1 L * (A i ) = ∅ ⇐⇒ ∩ n i=1 L * (A ′ i ) = ∅. Indeed, assume w ∈ ∩ n i=1 L * (A i ) = ∅. Then A 1 × A 2 × • • • × A n reaches the state (q 1 , q 2 , • • • , q n ) after reading w and ∀1 ≤ i ≤ n, q i ∈ F i . Thus in A ′ 1 × A ′ 2 × • • • × A ′
n the same state can be reached and then λ can be fired in the product leading to (⊥, ⊥, • • • , ⊥). Conversely, if a word w is accepted by the product

A ′ 1 × • • • × A ′ n , w must end with λ. Let w = u.λ ∈ ∩ n i=1 L * (A ′ i ) = ∅.
After reading u the state of the product must be (q 1 , q 2 , • • • , q n ) with ∀1 ≤ i ≤ n, q i ∈ F i , and the transitions fired when reading u are also in

A 1 × A 2 × • • • × A n which implies u ∈ ∩ n i=1 L * (A i ). ⊓ ⊔

A.2 Proof of Theorem 4

Proof. PSPACE-hardness follows from the fact that checking ∩ n i=1 L * (A i ) = ∅ on finite automata is already PSPACE-hard [START_REF] Kozen | Lower bounds for natural proof systems[END_REF] or alternatively because reachability for timed automata is PSPACE-hard [START_REF] Alur | A theory of timed automata[END_REF]. PSPACE-easiness can be established as Theorem 31 (section 4.1) of [START_REF] Aceto | Is your model checker on time? on the complexity of model checking for timed modal logics[END_REF]: the regions of the product of TA A i can be encoded in polynomial space in the size of the clock constraints of the product automaton. An algorithm to check emptiness is obtained by: 1) guessing a sequence of pairs (location,region) in the product automaton and 2) checking whether it is accepted. This can be done in NPSPACE and by Savitch's Theorem in PSPACE.

⊓ ⊔

A.3 Proof of Theorem 5

Proof. PSPACE-hardness follows from the reduction of Problem 2 to Problem 3 or again because checking Büchi emptiness for timed automata is PSPACE-hard [START_REF] Alur | A theory of timed automata[END_REF]. Consider the product automaton A + the construction of which is described at the end of section 2.5. PSPACE-easiness is established by: 1) guessing a state of RG(A + ) of the form ((ℓ, n), r) and 2) checking it is reachable from the initial state (PSPACE) and reachable from itself (PSPACE). As n is encoded in binary the result follows. ⊓ ⊔

B Proofs for Section 3 B.1 Proof of Lemma 1

Proof.

-If part. Assume equation (1) holds and A is (∆, E)-codiagnosable. Then there is a codiagnoser D

= (D 1 , • • • , D n ) satisfying Definition 3.
For each ̺ i we must have D i (π i (tr(̺ i ))) = 0 because each ̺ i is non faulty. But we must also have for at least one index i, D i (π i (tr

(̺ i ))) = D i (π i (tr(̺))) = 1 because ̺ is ∆-faulty, which is impossible.
-Only If part. Assume A is not (∆, E)-codiagnosable and ∀̺ ∈ Faulty ≥∆ (A), equation (1) does not hold. In this case, there is an index 1 ≤ i ≤ n s.t. :

∀̺ ′ ∈ NonFaulty(A), π i (tr(̺)) = π i (tr(̺ ′ )).
Define D i (w) = 1 when w ∈ π i (Faulty tr ≥∆ (A)) \ π i (NonFaulty tr (A)) and 0 otherwise. Then D = (D 1 , • • • , D n ) is a ∆-codiagnoser for A. Indeed, let ̺ ∈ NonFaulty(A). Then π i (tr(̺)) ∈ π i (NonFaulty tr (A)) and thus D i (π i (tr(̺))) = 0. Let ̺ ∈ Faulty ≥∆ (A) and assume D i (π i (tr(̺))) = 0 for each 1 ≤ i ≤ n. By definition of D i we must have π i (tr(̺)) ∈ π i (NonFaulty tr (A)). In this case, there is some run ̺ i ∈ NonFaulty(A) s.t. π i (tr(̺)) = π i (tr(̺ i )) and thus equation [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF] holds which contradicts the initial assumption.

⊓ ⊔

B.2 Proof of Lemma 2

Proof. Assume equation 2 does not hold and let w ∈ Faulty tr ≥∆ (A), and for each 1 ≤ i ≤ n, w ∈ π -1 i π i (NonFaulty tr (A)) . This implies that:

-∃̺ ∈ Faulty ≥∆ (A) s.t. tr(̺) = w; -for each i, w ∈ π -1 i π i (NonFaulty tr (A)) and π i (w) ∈ π i (NonFaulty tr (A)). Thus, there is a run ̺ i ∈ NonFaulty(A), s.t. π i (w) = π i (tr(̺)) = π i (tr(̺ i )) and as equation (1) of Lemma 1 is satisfied, A is not (∆, E)-codiagnosable.
For the converse, assume A is not (∆, E)-codiagnosable. By Lemma 1, equation ( 1) is satisfied and:

-there is a run ̺ with tr(̺) ∈ Faulty tr ≥∆ (A); -for each i, there is some ̺ i ∈ NonFaulty(A) s.t. π i (tr(̺)) = π i (tr(̺ i )). Hence tr(̺) ∈ π -1 i (π i (NonFaulty tr (A))) for each i, and this implies that equation 2 does not hold.

⊓ ⊔

C Proofs for Section 4 C.1 Proof of Lemma 3

Proof. The sets of clocks of the A i 's and A f (∆) are disjoint: for each

1 ≤ i < j ≤ n, X i ∩ X j = ∅ and X i ∩ X = ∅. It follows from Fact 1 that L * (B) = L * (A f (∆)) ∩ n i=1 L * (A * i )
. By Lemma 2 and the construction of A f (∆) and the A i 's, the result follows.

⊓ ⊔

C.2 Proof of Theorem 6

Proof. PSPACE-easiness follows from the polynomial reduction above and Lemma 3. PSPACE-hardness is obtained by reducing the variant of the intersection emptiness problem for DTA to the (∆, E)-codiagnosability problem. This problem is PSPACEhard (Proposition 1).

Let A i , 1 ≤ i ≤ n, be n deterministic finite automata over the alphabet Σ. Assume A 1 has one accepting state and for A 2 , • • • , A n all states are accepting.

We construct B as shown on Figure 1: a 2 , • • • , a n are fresh letters not in Σ; the target state of a i is the initial state of A i . The initial state of B is ι. Let Σ i = Σ \ {a i } for each 2 ≤ i ≤ n. From the final state of A 1 there is a transition labeled f to a new state e.

We can prove that B is (1, E)-codiagnosable if and only if

∩ n i=1 L * (A i ) = ∅ with E = (Σ i ) 1≤i≤n . Assume w ∈ ∩ n i=1 L * (A i ) = ∅.
Take the run of trace τ.w.f.τ in B. This run is 1-faulty. For each 2 ≤ i ≤ n, there is a run of trace a i .w which is non faulty. Moreover, π i (a i .w) = w and thus B is not (1, E)-codiagnosable. Now, assume B is not (1, E)-codiagnosable. There is a 1-faulty run, and this must be a run of trace τ.w.f.τ with w ∈ L * (A 1 ), and for each 2 ≤ i ≤ n, there is a non-faulty run ̺ i the trace of which is u i , with π i (u i ) = w. It must be the case that u i = a i .w i as otherwise π i (u i ) would start with a k , k = i and thus it would be impossible to have Proof. PSPACE-easiness follows form the fact that checking whether L ω (B co ) = ∅ can be done in PSPACE (Theorem 3). PSPACE-hardness follows from a reduction of given w ∈ Tr(A), if π Σi (w) ∈ L(G i,c ), let D i (π Σi (w)) = 1 and otherwise 0. D is a ∆-codiagnoser for A. Indeed, let w ∈ NonFaulty tr (A). In each game G i,c , we cannot reach a ∆-faulty state because of (2). Hence In each G i,c we must reach a state q i containing a ∆-faulty state. By [START_REF] Ramadge | The control of discrete event systems[END_REF], there is some j s.t. q j ∈ Bad j and this implies that q j is made only of ∆-faulty states and q j is accepting, thus D[j](π Σj (w)) = 1.

π i (u i ) = w. As u i = a i .w i , π i (u i ) = w i = w,
Only If part. For this part we first show that a tuple of strategies f exists and then address the state-based problem. Let D = (D 1 , D 2 , • • • , D n ) be the tuple of DTA that diagnoses A. For each game G i , define the strategy f i by: let ̺ = (g 1 , λ 1 )(g 1 , λ 1 , Y 1 ) • • • (g k-1 , λ k-1 )(g k-1 , λ k-1 , Y k-1 )(g k , λ k ) be a run in G i ; f i (̺) = (g, a, Y ) if in D i the symbolic sequence (g 1 , λ 1 ) • • • (g k , λ k ) reaches a location ℓ and there is a transition (ℓ, (g, a, Y ), ℓ ′ ) in D i . By assumption, as D is a ∆-codiagnoser, for each w ∈ Faulty tr ≥∆ (A), there is at least one D j which reaches an accepting state after reading π Σj (w).

As a consequence, in the corresponding game, G j , the state reached is made only of ∆-faulty states. Indeed, if a non-faulty state is reachable, then the word w is also the projection of a non faulty run. Hence D j should announce 0 which is a contradiction.

If w ∈ NonFaulty tr (A), all the states reached in each G i are non faulty. Now assume we have the strategies f i , 1 ≤ i ≤ n. We can construct state-based strategies on each game G i . Given f 1 , (not necessarily winning) on G 1 , let T 1 be the set of bad states reachable in f 1 (G 1 ). Define the language L 1 to be the set of words w ∈ Tr(A) s.t. a state in T 1 is reachable in f 1 (G 1 ) when reading π Σ1 (w). These are the words on which f 1 is not winning in G 1 .

Let Reach(f 1 (G 1 )) be the set of states reachable in G 1 . There is a strategy (f 1 ) to avoid B 1 = Reach(G 1 ) \ Reach(f 1 (G 1 )). Hence there is a state-based strategy f ′ 1 that avoids B 1 .

Let 1 ≤ i < n. Consider the game f i+1 (G i+1 ) restricted to the (projections of the) words w ∈ L i . The idea is that on L i , a strategy f j , j ≤ i is winning in G j . In this restricted game, we define the set T i+1 of bad states that are still reachable. Let L i+1 be the set of words w ∈ Tr(A) s.t. a state in T i+1 is reachable in the restricted timed transition system f i+1 (G i+1 ).

Notice that we can construct a state-based strategy f ′ i which avoids the same states as f i does. For each restricted game f ′ i (G i ) we define the diagnoser D i as before. If for some i, L i = ∅, we can define the diagnosers D k , k ≥ i to always announce 0 for each word.

f ′ is a (∆, E)-codiagnoser for A and all the f ′ [i] are state-based on G i . ⊓ ⊔

D.2 Proof of Theorem 12

Proof. 2EXPTIME-hardness follows from Theorem 11, from [START_REF] Bouyer | Fault diagnosis using timed automata[END_REF]. 2EXPTIME easiness is obtained using the following algorithm:

1. compute the games G i , 1 ≤ i ≤ n; 2. select a state-based strategy on each game G i ;

  4 a 1.0 b 2.7 c • • • where the real values are the durations elapsed between two letters: thus c occurs at global time 4.1.

  be the set of faulty runs of A, and NonFaulty(A) = Runs(A) \ Faulty(A) be the set of non-faulty runs of A. Finally, we let Faulty tr ≥∆ (A) = Tr(Faulty ≥∆ (A)) and NonFaulty tr (A) = Tr(NonFaulty(A)) which are the traces 3 of ∆-faulty and non-faulty runs of A.

Fig. 1 .C. 3

 13 Fig. 1. Reduction for Theorem 6: Automaton B

  n i=1 D[i] = 0. Now assume w ∈ Faulty tr ≥∆ (A):

Table 1 .

 1 Summary of the Results

		Codiagnosability Codiagnosability Optimal Delay	Synthesis (Bounded Resources)
	FA	PSPACE-C. PTIME [5,4]	PSPACE-C. PTIME [5,4]	PSPACE PTIME [5,4]	EXPTIME EXPTIME [3]
	TA	PSPACE-C. PSPACE-C. [6]	PSPACE-C. PSPACE-C. [6]	PSPACE PSPACE [18]	2EXPTIME-C. 2EXPTIME-C. [7]

  and w ∈ L * (A i ), it follows that w ∈ ∩ n i=1 L * (A i ) and thus ∩ n i=1 L * (A i ) is not empty. Finally ∩ n i=1 L * (A i ) = ∅ if and only if B is not (1, E)-codiagnosable. The size of B is in O(

For finite automata, this is is vacuously true.

Notice that tr(̺) erases τ and f .

The constants in the automata are integers.

fi(G i ) is a timed transition system.

⋆ Author supported by a Marie Curie International Outgoing Fellowship within the 7th European Community Framework Programme.

Problem 1 to Problem 5 using the same encoding as the one given in the proof of Theorem 6: the automaton B of Fig. 1 is not (∆, E)-codiagnosable for any ∆ ∈ N. ⊓ ⊔ C. [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF] 2) is satisfied. From (1), each choice of Player 0 in G i determines one transition from each square state (see the definition of G i and square states in section 6.1). Thus the graph of G i can be folded into a set of transitions q g,a,Y ---→ q ′ if the choice of Player 0 is g, a, Y in square state (q, g, a). This gives a DTA G i,c . We can then build a diagnoser D i defined by the DTA as follows: (i) for each state q = {(ℓ 1 , r 1 ), • • • , (ℓ k , r k )} in G i,c , if all the ℓ j are ∆-faulty, q is accepting; (ii)