Franck Cassez
email: franck.cassez@cnrs.irccyn.fr

Stavros Tripakis
email: tripakis@cadence.com

Fault Diagnosis with Static and Dynamic Observers *

We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider static observers where the set of observable events is not fixed, but needs to be optimized (e.g., minimized in size). We also consider dynamic observers, where the observer can "switch" sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. On the other hand, minimizing the number of (static) observable events required to achieve diagnosability is NP-complete. We show that this is true also in the case of mask-based observation, where some events are observable but not distinguishable. For dynamic observers' synthesis, we prove that a most permissive finite-state observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. We show how to compute an optimal observer using results on mean-payoff games by Zwick and Paterson.

Introduction

Monitoring, Testing, Fault Diagnosis and Control. Many problems concerning the monitoring, testing, fault diagnosis and control of embedded systems can be formalized using finite automata over a set of observable events Σ, plus a set of unobservable events [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF][START_REF] Tsitsiklis | On the Control of Discrete Event Dynamical Systems[END_REF]. The invisible actions can often be represented by a single unobservable event τ . Given a finite automaton over Σ ∪ {τ } which is a model of a plant (to be monitored, tested, diagnosed or controlled) and an objective (good behaviours, what to test for, faulty behaviours, control objective) we want to check if a monitor/tester/diagnoser/controller exists that achieves the objective, and if possible to synthesize one automatically.

The usual assumption in this setting is that the set of observable events is fixed (and this in turn, determines the set of unobservable events as well). Observing an event usually requires some detection mechanism, i.e., a sensor of some sort. Which sensors to use, how many of them, and where to place them are some of the design questions that are often difficult to answer, especially without knowing what these sensors are to be used for.

In this paper we study problems of sensor minimization. These problems are interesting since observing an event can be costly in terms of time or energy: computation time must be spent to read and process the information provided by the sensor, and power is required to operate the sensor (as well as perform the computations). It is then essential that the sensors used really provide useful information. It is also important for the computer to discard any information given by a sensor that is not really needed. In the case of a fixed set of observable events, it is not the case that all sensors always provide useful information and sometimes energy (used for sensor operation and computer treatment) is spent for nothing. As an example, consider the system described by the automaton M, Fig. 1. M models a system that has two possible behaviors, a faulty behavior that starts with the fault event f , and a non-faulty behavior that starts with event b. Events a and b are assumed to be observable, whereas events f and τ are unobservable. In this case, a simple way for an observer to detect fault f is to watch for both events a and b: if the sequence a.b is observed, then f must have occurred; if, on the other hand, b.a is observed, then we can be certain that f did not occur (assuming the system under observation behaves precisely as the model M).

• • • • • • τ τ f
Although this is a correct way of performing diagnosis in this case, there exists a "cheaper" way. Initially, the observer turns on only the a sensor (that is, is only able to observe a but not b). When a is observed (eventually it will, since a occurs in both behaviors) the observer turns off the a sensor and turns on the b sensor. If b is observed, then we can conclude that f occurred. As long as b is not observed, f has not occurred.

The former diagnosis method uses a "static" observer in the sense that it watches for the same set of events throughout the entire observation process. The latter method uses a dynamic observer, which turns sensors on and off as necessary. The latter method can be less costly, as in the example described above.

Sensor Minimization and Fault Diagnosis. We focus our attention on sensor minimization, without looking at problems related to sensor placement, choosing between different types of sensors, and so on. We also focus on a particular observation problem, that of fault diagnosis. We believe, however, that the results we obtain are applicable to other contexts as well.

Fault diagnosis consists in observing a plant and detecting whether a fault has occurred or not. We follow the discrete-event system (DES) setting of [START_REF] Sampath | Diagnosability of Discrete Event Systems[END_REF] where the behavior of the plant is assumed to be known: this includes both the nominal, non-faulty behavior of the plant, as well as the faulty behavior of the plant (after a fault occurs). In particular, we assume that we have a model of the plant in the form of a finite-state automaton over Σ ∪ {τ, f }, where Σ is the set of potentially observable events, τ represents the unobservable events, and f is a special unobservable event that corresponds to the faults. 1Checking diagnosability (whether a fault can be detected) for a given plant and a fixed set of observable events can be done in polynomial time [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 the general case, synthesizing a diagnoser involves determinization and thus cannot be done in polynomial time.

We examine sensor optimization problems with both static and dynamic observers. A static observer always observes the same set of events, whereas a dynamic observer can modify the set of events it wishes to observe during the course of the plant execution.

In the static observer case, we consider both the standard setting of observable/unobservable events as well as the setting where the observer is defined as a mask which allows some events to be observable but not distinguishable (e.g., see [START_REF] Cieslak | Supervisory control of discrete-event processes with partial observations[END_REF]). Our first contribution is to show that the problems of minimizing the number of observable events (or distinct observable outcomes in case of the mask) are NP-complete. Membership in NP can be easily derived by reducing these problems to the standard diagnosability problem, once a candidate minimal solution is chosen non-deterministically. NP-hardness can be shown using reductions of well-known NP-hard graphs problems, namely the clique and coloring problems.

In the dynamic observer case, we assume that an observer can decide after each new observation the set of events it is going to watch. We provide a definition of the dynamic observer synthesis problem and then show that computing a dynamic observer for a given plant, can be reduced to a problem of computing strategies in a game. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. Finally we show how to compute an optimal (cost-wise) dynamic observer.

Related work. In Section 3.1 we give a new polynomial time algorithm to check diagnosability. This result itself (testing diagnosability in polynomial time) is not new and was 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]. Nevertheless the proof we give is original and very simple and applies to plants that are specified by non-deterministic automata with no assumption on non observable loops as 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]. We can also derive easily a polynomial time algorithm to compute the minimum k such that a DES is k-diagnosable and thus improve a result from [START_REF] Yoo | Computation of Fault Detection Delay in Discrete-Event Systems[END_REF] but again with a very simple proof. NP-hardness of finding minimum-cardinality sets of observable events so that diagnosability holds under the standard, projection-based setting has been previously reported in [START_REF] Yoo | NP-completeness of sensor selection problems arising in partially observed discrete-event systems[END_REF]. Our result of section 3.2 can be viewed as an alternative shorter proof of this result. Masks have not been considered in [START_REF] Yoo | NP-completeness of sensor selection problems arising in partially observed discrete-event systems[END_REF]. As we show in section 4 a reduction from the mask version of the problem to the standard version is not straightforward. Thus the result in section 4 is useful and new.

The complexity of finding "optimal" observation masks, i.e., a set that cannot be reduced, has been considered in [START_REF] Jiang | Optimal Sensor Selection for Discrete Event Systems with Partial Observation[END_REF] where it was shown that the problem is NP-hard for general properties. [START_REF] Jiang | Optimal Sensor Selection for Discrete Event Systems with Partial Observation[END_REF] also shows that finding optimal observation masks is polynomial for "mask-monotonic" properties where increasing the set of observable (or distinguishable) events preserves the property in question. Diagnosability is a mask-monotonic property. However, the notion of "optimality" considered in this work differs from ours: [START_REF] Jiang | Optimal Sensor Selection for Discrete Event Systems with Partial Observation[END_REF] considers the computation of a minimal partition of the set of events w.r.t. partition refinement ordering, and not the computation of the minimum cardinality of the partitions that ensure diagnosability. Notice that optimal observation masks are not the same as minimum-cardinality masks that we consider in this paper.

In [START_REF] Debouk | On an Optimization Problem in Sensor Selection[END_REF], the authors investigate the problem of computing a minimal-cost strategy that allows to find a subset of the set of observable events such that the system is diagnosable. It is assumed that each such subset has a known associated cost, as well as a known a-priori probability for achieving diagnosability. Dynamic observers are not considered in this work.

Dynamic observers have received little attention in the context of fault diagnosis. The only work we are aware of is the one described in [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF]. Our work has been developed independently (Cf. previous versions of this paper [START_REF] Cassez | Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis[END_REF][START_REF] Cassez | Synthesis Of Optimal Dynamic Observers for Fault Diagnosis of Discrete-Event Systems[END_REF]). Although the general goals of this work and ours are the same, namely, dynamic on/off switching of sensors in order to achieve cost savings, the setting and the approach of [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF] are quite different from ours:

• The definitions of dynamic observers differ in the two settings: for instance, for the example of section 4.2.1 of [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF], there is no finite-cost solution for Problem CD of [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF] (which corresponds to Problem 5 in our paper). In our setting the same example admits a finite-cost solution.

• the purpose of [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF] is to compute one optimal observation policy (using dynamic programming).

In contrast, we solve two problems: first, we compute the set of all dynamic observers that can be used to diagnose a system; second we compute all the optimal observers. We do this using well-known game-theoretic approaches.

• there is no upper bound on the complexity of the procedures given in [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF]. We show that our solutions are in 2EXPTIME.

• in [START_REF] Thorsley | Active Acquisition of Information for Diagnosis and Supervisory Control of Discrete Event Systems[END_REF], the authors compute dynamic observers for stochastic systems which we do not consider. They also consider the control problem under dynamic observation which we do not consider. Notice that the control problem they consider is a Ramadge & Wonham control problem i.e., on languages on finite words, and thus, the method we propose in paragraph 5.4 could be applied as well.

Organisation of the paper. In Section 2 we fix notation and introduce finite automata with faults to model DES. In Section 3 we present a new algorithm for testing diagnosability. We also show NPcompleteness of the sensor minimization problem for the standard projection-based observation setting.

In Section 4 we show NP-completeness of the sensor minimization problem for the mask-based setting.

In Section 5 we introduce and study dynamic observers and show that the most permissive dynamic observer can be computed as the most permissive (finite-memory) winning strategy in a safety 2-player game.

We also define a notion of cost for dynamic observers in Section 6 and show that the cost of a given observer can be computed using Karp's algorithm. Finally, we define the optimal-cost observer synthesis problem and show it can be solved using Zwick and Paterson's result on graph games.

Preliminaries

Words and Languages

Let Σ be a finite alphabet and Σ τ = Σ ∪ {τ }. Σ * (resp. Σ ω ) is the set of finite (resp. infinite) words over Σ and contains ε which is the empty word. We let Σ + = Σ * \ {ε}. A language L is any subset of Σ * ∪ Σ ω . Given two words ρ ∈ Σ * and ρ ′ ∈ Σ * ∪ Σ ω we denote ρ.ρ ′ the concatenation of ρ and ρ ′ which is defined in the usual way. |ρ| stands for the length of the word ρ (the length of the empty word is zero, the length of an infinite word is ∞) and |ρ| λ with λ ∈ Σ stands for the number of occurrences of λ in ρ. We also use the notation |S| to denote the cardinality of a set S. Given Σ 1 ⊆ Σ, we define the projection operator on finite words, π /Σ 1 : Σ * → Σ * 1 , recursively as follows:

π /Σ 1 (ε) = ε and for a ∈ Σ, ρ ∈ Σ * , π /Σ 1 (a.ρ) = a.π /Σ 1 (ρ) if a ∈ Σ 1 and π /Σ 1 (ρ) otherwise.

Automata Definition 2.1. (Finite Automaton)

An automaton A is a tuple (Q, q 0 , Σ τ , δ, F, R) with Q a set of states, q 0 ∈ Q is the initial state, δ ⊆ Q × Σ τ × 2 Q is the transition relation and F ⊆ Q, R ⊆ Q are receptively the set of final and repeated states. We write q λ -→ q ′ if q ′ ∈ δ(q, λ). For q ∈ Q, Enabled(q) is the set of actions enabled at q, i.e., the set of λ such that q λ -→ q ′ for some q ′ . If Q is finite, A is a finite automaton. An automaton is deterministic if for any q ∈ Q, |δ(q, τ )| = 0 and for any λ ∈ Σ, |δ(q, λ)| ≤ 1. A labeled automaton is a pair (A, L) where A = (Q, q 0 , Σ τ , δ, F, R) is an automaton and L : Q → P where P is a finite set of observations. A run ρ from state s in A is a finite or infinite sequence of transitions

s 0 λ 1 --→ s 1 λ 2 --→ s 2 • • • s n-1 λn --→ s n • • • (1)
s.t. λ i ∈ Σ τ and s 0 = s. If ρ is finite, of length n, and ends in s n we let tgt(ρ) = s n . The set of finite (resp. infinite) runs from s in A is denoted Runs(s, A) (resp. Runs ω (s, A)) and we define Runs(A) = Runs(q 0 , A) and Runs ω (A) = Runs ω (q 0 , A). The trace of the run ρ, denoted tr(ρ), is the word obtained by concatenating the symbols λ i appearing in ρ, for those λ i different from τ . The finite word w ∈ Σ * is accepted by A if w = tr(ρ) for some ρ ∈ Runs(A) with tgt(ρ) ∈ F . The language of finite words L(A) of A is the set of words accepted by A. The infinite word w ∈ Σ ω is accepted by A if w = tr(ρ) for some ρ ∈ Runs ω (A) and there is an infinite set of indices

I = {i 0 , i 1 , • • • , i k , • • • } s.t. s l ∈ R for each l ∈ I.
The language of infinite words L ω (A) of A is the set of infinite words accepted by A.

Discrete-Event Systems

In this paper we use finite automata that generate prefix-closed languages of finite words to model discrete-event systems, hence we do not always need a set of final or repeated states (we assume F = Q and R = ∅ if not otherwise stated).

Let f ∈ Σ τ be a fresh letter that corresponds to the fault action. We also let

Σ τ,f = Σ τ ∪ {f } and A = (Q, q 0 , Σ τ,f , δ). Given V ⊆ Runs(A), Tr(V ) = {tr(ρ) for ρ ∈ V } is the set of traces of the runs in V . A run ρ as in equation (1) is k-faulty if there is some 1 ≤ i ≤ n s.t. λ i = f and n -i ≥ k.
Notice that ρ can be infinite and in this case n = ∞ and ni ≥ k always holds. Faulty ≥k (A) is the set of k-faulty runs of A. A run is faulty if it is k-faulty for some k ∈ N and Faulty(A) denotes the set of faulty runs. It follows that Faulty

≥k+1 (A) ⊆ Faulty ≥k (A) ⊆ • • • ⊆ Faulty ≥0 (A) = Faulty(A).
Finally, NonFaulty(A) = Runs(A) \ Faulty(A) is the set on non-faulty runs of A. We let Faulty tr ≥k (A) = Tr(Faulty ≥k (A)) and NonFaulty tr (A) = Tr(NonFaulty(A)) be the sets of traces of faulty and non-faulty runs.

We assume that each faulty run of A of length n can be extended into a run of length n + 1. This is required for technical reasons (in order to guarantee that the set of faulty runs where sufficient "logical" time has elapsed after the fault is well-defined) and can be achieved by adding τ loop-transitions to each deadlock state of A. Notice that this transformation does not change the observations produced by the plant, thus, any observer synthesized for the transformed plant also applies to the original one.

Product of Automata

The product of automata with τ -transitions is defined in the usual way: the automata synchronize on common labels except for τ . Let A 1 = (Q 1 , q 1 0 , Σ τ 1 , δ 1 ) and A 2 = (Q 2 , q 2 0 , Σ τ 2 , δ 2 ). The product of A 1 and A 2 is the automaton A 1 × A 2 = (Q, q 0 , Σ τ , δ) where:

• Q = Q 1 × Q 2 ,
• q 0 = (q 1 0 , q 2 0 ),

• Σ = Σ 1 ∪ Σ 2 , • δ ⊆ Q × Σ τ × Q is defined by (q 1 , q 2 ) σ -→ (q ′ 1 , q ′ 2 ) if: -either σ ∈ Σ 1 ∩ Σ 2 and q k σ -→ k q ′ k , for k = 1, 2, -or σ ∈ (Σ i \ Σ 3-i ) ∪ {τ } and q i σ -→ i q ′ i and q ′ 3-i = q 3-i , for i = 1 or i = 2.

Sensor Minimization with Static Observers

In this section we address the sensor minimization problem for static observers. We point out that the result in this section was already obtained in [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF] and we only give here an alternative shorter proof. We are given a finite automaton A = (Q, q 0 , Σ τ,f , δ). Such an automaton A models a plant. Notice that A is as in Definition 2.1 with the addition that its alphabet includes both the unobservable non-fault event τ and the unobservable fault event f .

A diagnoser is a device that observes the plant and raises an "alarm" whenever it detects a fault. We allow the diagnoser to raise an alarm not necessarily immediately after the fault occurs, but possibly some time later, as long as this time is bounded by some k ∈ N, where N is the set of non-negative integers. We model time by counting the "moves" the plant makes (including observable and unobservable ones). If the system generates a word ρ but only a subset Σ o ⊆ Σ is observable, the diagnoser can only see π /Σo (ρ).

Definition 3.1. ((Σ o , k)-Diagnoser) Let A be a finite automaton over Σ τ,f , k ∈ N, Σ o ⊆ Σ. A mapping D : Σ * o → {0, 1} is a (Σ o , k)- diagnoser for A if: • for each ρ ∈ NonFaulty(A), D(π /Σo (tr(ρ))) = 0, • for each ρ ∈ Faulty ≥k (A), D(π /Σo (tr(ρ))) = 1. A is (Σ o , k)-diagnosable if there is a (Σ o , k)-diagnoser for A. A is Σ o -diagnosable if there is some k ∈ N s.t. A is (Σ o , k)-diagnosable.
Remark 3.1. At this stage, we do not require the mapping D to be effectively computable or even regular.

Example 3.1. Let A be the automaton shown on Fig. 2. The run with one action f is in Faulty ≥0 (A), the run f.a is in Faulty ≥1 (A) and a.τ 2 is in NonFaulty(A). A is neither {a}-diagnosable, nor {b}-

• 0 • 1 • 2 • 3 • 4 τ τ f a b a b Figure 2. The automaton A.
diagnosable. This is because, for any k, the faulty run f.a.b.τ k gives the same observation as the nonfaulty run a.τ k (in case a is the observable event) or the non-faulty run b.τ k (in case b is the observable event). Consequently, the diagnoser cannot distinguish between the two no matter how long it waits. If both a and b are observable, however, we can define: D(a.b.ρ) = 1 for any ρ ∈ {a, b} * and D(ρ) = 0 otherwise. D is a ({a, b}, 2)-diagnoser for A, thus, A is {a, b}-diagnosable.

Checking Diagnosability

Let A = (Q, q 0 , Σ τ,f , →) be a finite automaton over Σ τ,f . In this subsection we give a polynomial time algorithm to check diagnosability. As 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], checking whether A is Σ-diagnosable can be done in polynomial time in the size of A, more precisely in O(|A| 2 ). We improve 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][START_REF] Yoo | Computation of Fault Detection Delay in Discrete-Event Systems[END_REF] on this subject with respect to the following directions:

• compared to [START_REF] Yoo | Polynomial-Time Verification of Diagnosability of Partially-Observed Discrete-Event Systems[END_REF], the product automaton (denoted A 1 × A 2 in the sequel) that we build has fewer states; moreover our result applies even if the plant is given by a non-deterministic automaton with non-observable loops.

• in [START_REF] Jiang | A Polynomial Algorithm for Testing Diagnosability of Discrete Event Systems[END_REF], in case there are many types of faults, the algorithm for checking diagnosability runs in exponential time. We can use our algorithm to check each fault at a time and obtain a polynomialtime algorithm for multiple types of faults.

• to compute the maximum delay k to diagnose a system, [START_REF] Yoo | Computation of Fault Detection Delay in Discrete-Event Systems[END_REF] computes the strongly connected components of a product automaton and then reduces the problem of computing k, to a shortestpath problem in a graph. This proves that k can be computed in cubic time in the size of the plant.

We improve this result with our construction and obtain a quadratic algorithm.

Altogether, this section provides a uniform and elegant setting to check diagnosability of discrete-event systems with multiple faults types and to compute the maximum delay. Moreover the proofs are very easy and short. It also reduces the diagnosability problem to the Büchi emptiness problem: very efficient algorithms [START_REF] Courcoubetis | Memory Efficient Algorithms for the Verification of Temporal Properties[END_REF] are known to solve this problem, for instance on-the-fly algorithms [START_REF] Holzmann | On nested depth-first search[END_REF]. In this respect, our algorithm can be very useful because it is implemented in very efficient tools like SPIN [START_REF] Holzmann | Software model checking with SPIN[END_REF] to check for Büchi emptiness.

An Algorithm to Check Diagnosability. Let A = (Q, q 0 , Σ τ,f , →) be a finite automaton over Σ τ,f . We assume that Σ o = Σ i.e., all the events in Σ are observable and thus τ is the only unobservable action.

By definition 3.1, A is diagnosable iff ∃k ∈ N * s.t. A is (Σ, k)-diagnosable. This is equivalent to: A is not diagnosable ⇐⇒ ∀k ∈ N * , A is not (Σ, k)-diagnosable (2)
⇐⇒ ∀k ∈ N * , ∃ρ ∈ NonFaulty(A) and ∃ρ ′ ∈ Faulty ≥k (A)

s.t. π /Σ (tr(ρ)) = π /Σ (tr(ρ ′ )) (3)
There is also a language-based definition of (Σ, k)-diagnosability:

A is (Σ, k)-diagnosable iff π /Σ (Faulty tr ≥k (A)) ∩ π /Σ (NonFaulty tr (A)) = ∅ (4)
or in other words, there is no pair of runs (ρ 1 , ρ 2 ) with ρ 1 ∈ Faulty ≥k (A), ρ 2 ∈ NonFaulty(A) s.t. ρ 1 and ρ 2 give the same observations on Σ. To check diagnosability, we build a product automaton A 1 ×A 2 such that A 1 behaves like A but records whether a fault occurred or not, and A 2 produces only the non-faulty runs of A. Define A 1 = (Q × {0, 1}, (q 0 , 0), Σ τ , → 1 ) s.t.

• (q, n) l -→ 1 (q ′ , n) iff q l -→ q ′ with l ∈ Σ; • (q, n) τ -→ 1 (q ′ , 1) iff q f -→ q ′ ,
(n is set to 1 after a fault occurs);

• (q, n) τ -→ 1 (q ′ , n) iff q τ -→ q ′ . Define A 2 = (Q, q 0 , Σ τ , → 2 ) with • q l -→ 2 q ′ if q l -→ q ′ and l ∈ Σ; • q τ -→ 2 q ′ if q τ -→ q ′ . Let A 1 × A 2 be
z ′ = 1 if A 1 Move(t)
, and z ′ = 0 otherwise. Define the set of states R B = {(((q, 1), q ′ ), 1) | ((q, 1), q ′ ) ∈ A 1 × A 2 }. The Büchi automaton B is the tuple ((Q × {0, 1} × Q) × {0, 1}, ((q 0 , 0), q 0 , 0), Σ τ , -→ B , ∅, R B ) with R B the set of repeated states. The following theorem holds:

Theorem 3.1. L ω (B) = ∅ ⇐⇒ A is not Σ-diagnosable. Proof: =⇒ Assume L ω (B) = ∅. Let ρ ∈ L ω (B)
: ρ has infinitely many faulty states and infinitely many A 1 -actions because of the definition of R B . Let k ∈ N. Let ρ[i k ] be a finite prefix of ρ that contains more than k A 1 -actions (for any k this i k exists because ρ contains infinitely many 3) is satisfied and A is not diagnosable. ⇐= Conversely assume A is not Σ-diagnosable. Then by equation (3) and Lemma 3.2, for any k ∈ N, there is a run ρ k ∈ Runs ≥k (A 1 × A 2 ). As A 1 × A 2 is finite, there must be a state (q 1 , 1), q 2 in A 1 × A 2 which is the source of an infinite number of runs ρ ′ k having more than k A 1 -actions. As A 1 × A 2 is of finite branching, by König's Lemma, there is a infinite run in A 1 × A 2 containing infinitely many A 1 -actions and thus L ω (B) = ∅.

A 1 -actions). ρ[i k ] ∈ Runs ≥k (A 1 × A 2 ) and by Lemma 3.1, it follows that ρ[i k ] |1 ∈ Faulty ≥k (A) and ρ[i k ] |2 ∈ NonFaulty(A) and π /Σ (tr(ρ |1 )) = π /Σ (tr(ρ |2 )). Thus equation (
⊓ ⊔

This gives a procedure to check whether an automaton A is diagnosable or not. The product (extended) system built from A 1 × A 2 has size 4 • |A|2 i.e., O(|A| 2 ). Checking emptiness of a Büchi automaton having n states and m transitions can be done in O(n + m). Thus, checking diagnosability of a finite (non-deterministic) automaton can be done in O(|A| 2 ) i.e., is also polynomial.

In the case of a finite number of failure types, it suffices to design A 1 × A 2 for each type of faults [START_REF] Yoo | Polynomial-Time Verification of Diagnosability of Partially-Observed Discrete-Event Systems[END_REF] and check for diagnosability. Thus checking diagnosability with multiple type of faults is also polynomial.

Computation of the Maximal Delay to Detect Faults.

To compute the smallest k s.t. A is (Σ, k)diagnosable we proceed as follows: in case A is Σ-diagnosable, there is no infinite faulty run with infinitely many A 1 -actions in A 1 × A 2 ; this implies that each run beginning in a faulty state of A 1 × A 2 is followed by a finite number of A 1 -actions and this number is bounded by a constant α. Indeed, otherwise, we could construct an infinite faulty run with a infinite number of A 1 -actions and A would not be diagnosable. Assume k is the maximum number of A 1 -actions that can follow a faulty state in A 1 × A 2 . Then A is (Σ, k + 1)-diagnosable: otherwise there would be a faulty run with k + 1 A 1 -actions after a faulty state in A 1 × A 2 . Also A is not (Σ, k)-diagnosable because there is faulty run with k A 1actions after a faulty state in A 1 × A 2 , which also means there is another non faulty run with the same observable actions. Thus k + 1 is the minimum value for which A is Σ-diagnosable or in other words, it is the maximal delay after which a fault will be announced. Computing k + 1 amounts to computing the maximum number of A 1 -actions that can follow a faulty state in

A 1 × A 2 .
The computation of k amounts to computing the length of a longest path 2 in a graph which can be done in linear time w.r.t. size of the graph. As the size of A 1 × A 2 is O(|Q| 2 ) we can compute k in quadratic time which is better than the bound O(|Q| 3 ) of [START_REF] Yoo | Computation of Fault Detection Delay in Discrete-Event Systems[END_REF].

Synthesis of a Diagnoser.

To compute the diagnoser we do the following: take A 1 and determinize it (using the standard subset construction). The deterministic automaton A ′ obtained this way has at most 2 O(|Q|) states. If a state S of the deterministic version A ′ contains only faulty states, i.e., every (q, k) ∈ S is such that k = 1 then declare S as faulty.

Define the diagnoser D as follows: for a run ρ ∈ Runs(A),

D(ρ) = 1 if S 0 tr(ρ)
--→ S ′ in A ′ and S ′ is faulty; otherwise D(ρ) = 0. D is a diagnoser for A and the maximum delay to announce a fault is k + 1 steps if k is the minimum value for which A is (Σ, k)-diagnosable. Computing the diagnoser is thus exponential in the size of A, i.e., can be done in 2 O(|A|) .

Minimum Cardinality Set for Static Observers

In this section we address the problem of finding a set of observable events Σ o that allows faults to be detected. We would like to detect faults using as few observable events as possible. We want to decide whether there is a subset Σ o Σ such that the fault can be detected by observing only events in Σ o . Moreover, we would like to find an "optimal" such Σ o (e.g., one with minimal number of events).

Problem 1. (Minimum Number of Observable Events)

INPUT: Plant model A = (Q, q 0 , Σ τ,f , δ), n ∈ N s.t. n ≤ |Σ|. PROBLEMS: (A) Is there any Σ o ⊆ Σ with |Σ o | = n, such that A is Σ o -diagnosable ? (B) If the answer to (A) is "yes", find the minimum n 0 such that there exists Σ o ⊆ Σ with |Σ o | = n 0 and A is Σ o -diagnosable.
If we know how to solve Problem 1(A) efficiently then we can also solve Problem 1(B) efficiently: we perform a binary search over n between 0 and |Σ|, and solve Problem 1(A) for each such n, until we find the minimum n 0 for which Problem 1(A) gives a positive answer. 3 Unfortunately, Problem 1(A) is a combinatorial problem, exponential in |Σ|, as we show next.

Theorem 3.2. Problem 1(A) is NP-complete.

Proof:

Membership in NP is proved using the result in section 3.1: if we guess a solution Σ o we can check that A is Σ o -diagnosable in time polynomial in |A|. Here we provide the proof of NP-hardness by giving a reduction of the n-clique problem. Let G = (V, E) be a (undirected) graph where V is set of vertices and

E ⊆ V × V is a set of edges (we assume that (v, v ′ ) ∈ E ⇐⇒ (v ′ , v) ∈ E). A clique in G is a subset V ′ ⊆ V such that for all v, v ′ ∈ V ′ , (v, v ′ ) ∈ E.
The n-clique problem asks the following: determine whether G contains a clique of n vertices.

The reduction is as follows. Given G, we build a finite automaton A G such that there is a n-clique in

G iff A G is Σ o -diagnosable, where |Σ \ Σ o | = n. Notice that since Σ o ⊆ Σ, |Σ \ Σ o | = n is equivalent to |Σ o | = |Σ| -n.
Thus, there is a n-clique in G iff n events from Σ do not need to be observed i.e., iff Problem 1(A) gives a positive answer for |Σ|n.

Starting from G we define Σ = V . Then we define A G as shown in Fig. 3: q 0 is the initial state and the "branches" f.a.b, f.a

′ .b ′ , • • • are obtained from the pairs of nodes (a, b), (a ′ , b ′ ), • • • that are not linked with an edge in G: (a, b), (a ′ , b ′ ), • • • ∈ E. q 0 • • • • • • • • • f a b τ f a ′ b ′ τ f a ′′ b ′′ τ Figure 3. The automaton A G .

If part. Assume Problem 1(A)

gives a positive answer for |Σ|-n. This means that there exists

Σ o ⊆ Σ such that |Σ o | = |Σ| -n, or |Σ \ Σ o | = n, and A G is Σ o -diagnosable. Then we claim that C = Σ \ Σ o is a clique in G. Assume C is not a clique.
Then there must be some {a, b} ⊆ C such that (a, b) ∈ E.

By the construction of Fig. 3, there is a branch f.a.b in A G and thus both ρ = ε and ρ ′ = f.a.b.τ k are runs of A G , for any k. As {a, b} ⊆ C, {a, b} ∩ Σ o = ∅ and the observation of both runs4 ρ and ρ ′ is ε, no diagnoser exists that can distinguish between the two runs, for any k.

Only if part. Assume there exists a n-clique in G. Let Σ o = Σ \ C. We claim that A G is (Σ o , 2)- diagnosable (thus also Σ o -diagnosable).
Suppose not. Then there exist two runs ρ and ρ ′ such that ρ ′ ∈ NonFaulty(A G ) and ρ = ρ 1 .f.ρ 2 , and |ρ 2 | ≥ 2, and π /Σo (ρ) = π /Σo (ρ ′ ). Then, ρ must be of the form ρ = f.a.b.τ k , with (a, b) ∈ E. Also, the only way ρ ′ can be non faulty is

ρ ′ = ε. Then π /Σo (ρ ′ ) = ε = π /Σo (ρ), thus, both a and b must be non-observable, thus {a, b} ∩ Σ o = ∅ which entails {a, b} ⊆ C. This implies that (a, b) ∈ E which is a contradiction. ⊓ ⊔ Remark 3.2.
Notice that in Problem 1, the maximum number of steps after which a fault has to be reported, k, is not specified as an input. Adding k to the set of inputs results in answers that may generally depend on k. For instance, in the automaton E of Fig. 4, if we impose that a fault be reported within k = 2 steps, then we need to observe both a and b; whereas if we leave k unspecified, we need only observe a and we can diagnose a fault after 3 steps (i.e., 2 a's).

• • • • • • τ τ f a

Sensor Minimization with Masks

So far we have assumed that observable events are also distinguishable. However, there are cases where two events a and b are observable but not distinguishable, that is, the diagnoser knows that a or b occurred, but not which of the two. This is not the same as considering a and b to be unobservable, since in that case the diagnoser would not be able to detect occurrence of a or b. Distinguishability of events is captured by the notion of a mask [START_REF] Cieslak | Supervisory control of discrete-event processes with partial observations[END_REF].

Definition 4.1. (Mask) A mask (M, n) over Σ is a total, surjective function M : Σ → {1, • • • , n} ∪ {ε}. M induces a morphism M * : Σ * → {1, • • • , n} * , where M * (ε) = ε and M * (a.ρ) = M (a).M * (ρ), for a ∈ Σ and ρ ∈ Σ * . For example, if Σ = {a, b, c, d}, n = 2 and M (a) = M (b) = 1, M (c) = 2, M (d) = ε, then we have M * (a.b.c.b.d) = 1.1.2.1 = M * (a.a.d.c.a). Definition 4.2. ((M, n), k)-diagnoser) Let (M, n) be a mask over Σ. A mapping D : {1, • • • , n} * → {0, 1} is a ((M, n), k)-diagnoser for A if: • for each ρ ∈ NonFaulty(A), D(M * (π /Σ (tr(ρ)))) = 0; • for each ρ ∈ Faulty ≥k (A), D(M * (π /Σ (tr(ρ)))) = 1. A is ((M, n), k)-diagnosable if there is a ((M, n), k)-diagnoser for A. A is said to be (M, n)- diagnosable if there is some k such that A is ((M, n), k)-diagnosable.
Given A and a mask (M, n), checking whether A is ((M, n)-diagnosable can be done in polynomial time. In fact it can be reduced to checking Σ o -diagnosability of a modified automaton A M , with

Σ o = {1, ..., n}. A M is obtained from A by renaming the actions a ∈ Σ by M (a) or τ if M (a) = ε. It can be seen that A is ((M, n)-diagnosable iff A M is {1, • • • , n}-diagnosable. Also notice that A is ((M, n), k)-diagnosable iff M * (π /Σ (Faulty tr ≥k (A))) ∩ M * (π /Σ (NonFaulty tr (A))) = ∅.
As in the previous section, we are mostly interested in minimizing the observability requirements while maintaining diagnosability. In the context of diagnosis with masks, this means minimizing the number n of distinct outputs of the mask M . We thus define the following problem:

Problem 2. (Minimum Mask) INPUT: Plant model A = (Q, q 0 , Σ τ,f , δ), n ∈ N s.t. n ≤ |Σ|. PROBLEM:
(A) Is there any mask (M, n) such that A is (M, n)-diagnosable ? (B) If the answer to (A) is "yes", find the minimum n 0 such that there is a mask (M, n 0 ) such that A is (M, n 0 )-diagnosable.

As with Problem 1, if we know how to solve Problem 2(A) efficiently we also know how to solve Problem 2(B) efficiently: again, a binary search on n suffices.

We will prove that Problem 2 is NP-complete. One might think that this result follows easily from Theorem 3.2. However, this is not the case. Obviously, a solution to Problem 1 provides a solution to Problem 2: assume there exists Then A is ((M, 1), 2)-diagnosable because we can build a diagnoser D defined by: D(ε) = 0, D(1) = 0, D(1 2 .ρ) = 1 for any ρ ∈ 1 * . However, as we said before, there is no strict subset of {a, b} that allows A to be diagnosed. 5Instead of using the previous result, we provide a direct proof of NP-hardness of Problem 2.

Σ o such that A is (Σ o , k)-diagnosable and Σ o = {a 1 , ..., a n }; define a mask M : Σ → {1, • • • , n} such that M (a i ) = i and for any a ∈ Σ \ Σ o , M (a) = ε. Then, A is ((M, n), k)-diagnosable.

Proof:

Membership in NP is again justified by the fact that checking whether a guessed mask works can be done in polynomial time (it suffices to rename the events of the system according to M and apply the algorithm of section 3.1). We show NP-hardness using a reduction of the n-coloring problem. The ncoloring problem asks the following: given an undirected graph G = (V, E), is it possible to color the vertices with colors in {1, 2, • • • , n} so that no two adjacent vertices have the same color ?

Let G = (V, E) be an undirected graph. Let E = {e 1 , e 2 , • • • , e j } be the set of edges with e i = (u i , v i ). We let Σ = V and define the automaton A G as pictured in Fig. 5. The initial state of

A G is q 0 . Widget for e 2 q 0 • • • • • • • • • • • • • • • • • • • u 1 f v 1 u 2 f v 2 u j f v j v 1 τ u 1 v 2 τ u 2 v j τ u j • • • τ τ τ τ Figure 5. Automaton A G for n-colorizability. We claim that G is n-colorizable iff A G is (M, n)-diagnosable. If part Assume A G is (M, n)-diagnosable for n ≥ 0.
We first show that for all i = 1, ..., j, M

(u i ) = ε, M (v i ) = ε and M (u i ) = M (v i ).
For any k, we can define the runs ρ

= v 1 .τ.u 1 .v 2 .τ.u 2 • • • u i .f.v i .τ k and ρ ′ = v 1 .τ.u 1 .v 2 .τ.u 2 • • • v i .τ.u i . If either M (u i ) = ε or M (v i ) = ε or M (u i ) = M (v i ) holds, then we have M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))
). Thus, for any k, there is a faulty run with more than k events after the fault, and a non-faulty run which gives the same observation through the mask. Hence, for any k, A cannot be ((M, n), k)-diagnosable. Thus A is not (M, n)-diagnosable which contradicts diagnosability of A. Note that the above implies in particular that n ≥ 1. We can now prove that G is n-colorizable. Let C be the color mapping defined by

C(v) = M (v). We need to prove that C(u i ) = C(v i ) for any (u i , v i ) ∈ E.
This holds by construction of A G and the fact that M (u i ) = M (v i ) as shown above.

Only if part Assume G is n-colorizable. There exists a color mapping

C : V → {1, 2, • • • , n} s.t. if (v, v ′ ) ∈ E then C(v) = C(v ′ ). Define the mask M by M (a) = C(a) for a ∈ V . We claim that A G is ((M, n), 1)-diagnosable (thus, also (M, n)-diagnosable). Assume on the contrary that A G is not ((M, n), 1)-diagnosable. Then there exist two runs ρ ∈ Faulty ≥1 (A G ) and ρ ′ ∈ NonFaulty(A G ) such that M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))). As ρ is 1-faulty it must be of the form ρ = v 1 .τ.u 1 • • • u i .f.v i .τ k with 1 ≤ i ≤ j and k ≥ 0. Notice that M (a) = ε for all a ∈ V . Hence it implies M * (π /Σ (tr(ρ))) = M (v 1 ).M (u 1 ) • • • M (u i ).M (v i ), and |M * (π /Σ (tr(ρ)))| = 2i. Consequently, |M * (π /Σ (ρ ′ ))| = 2i. The only possible such ρ ′ which is non-faulty is ρ ′ = v 1 .τ.u 1 • • • v i .τ.u i . Now, M * (π /Σ (tr(ρ))) = M * (π /Σ (tr(ρ ′ ))), which implies M (v i ) = M (u i ) i.e., C(v i ) = C(u i ). But (u i , v i ) ∈ E,
and this contradicts the assumption that C is a valid coloring.

⊓ ⊔

Fault Diagnosis with Dynamic Observers

In this section we introduce dynamic observers. They can choose after each new observation the set of events they are going to watch for. To illustrate why dynamic observers can be useful consider the following example.

Example 5.1. (Dynamic Observation)

Assume we want to detect faults in automaton B of Fig. 6. A static diagnoser that observes Σ = {a, b} works, however, no proper subset of Σ can be used to detect faults in B. Thus the minimum cardinality of the set of observable events for diagnosing B is 2 i.e., a static observer will have to monitor two events during the execution of the DES B. If we want to use a mask, the minimum-cardinality for a mask is 2 as well. This means that an observer will have to be receptive to at least two inputs at each point in time to detect a fault in B. One can think of being receptive as switching on a device to sense an event. This consumes energy. We can be more efficient using a dynamic observer, that only turns on sensors when needed, thus saving energy. In the case of B, this can be done as follows: in the beginning we only switch on the a-sensor; once an a occurs the a-sensor is switched off and the b-sensor is switched on. Compared to the previous diagnosers we use half as much energy.

• • • • • • τ τ f a b b a

Dynamic Observers

We formalize the above notion of dynamic observation using observers. The choice of the events to observe can depend on the choices the observer has made before and on the observations it has made. Moreover an observer may have unbounded memory.

Definition 5.1. (Observer)

An observer Obs over Σ is a deterministic labeled automaton 6 Obs = (S, s 0 , Σ, δ, L), where S is a (possibly infinite) set of states, s 0 ∈ S is the initial state, Σ is the set of observable events, δ : S × Σ → S is the transition function (a total function), and L : S → 2 Σ is a labeling function that specifies the set of events that the observer wishes to observe when it is at state s. We require for any state s and any a ∈ Σ, if a ∈ L(s) then δ(s, a) = s: this means the observer does not change its state when an event it has chosen not to observe occurs.

As an observer is deterministic we use the notation δ(s 0 , w) to denote the state s reached after reading the word w and L(δ(s 0 , w)) is the set of events Obs observes after w.

An observer implicitly defines a transducer that consumes an input event a ∈ Σ and, depending on the current state s, either outputs a (when a ∈ L(s)) and moves to a new state δ(s, a), or outputs ε, (when a ∈ L(s)) and remains in the same state waiting for a new event. Thus, an observer defines a mapping Obs from Σ * to Σ * (we use the same name "Obs" for the automaton and the mapping). Given a run ρ, Obs(π /Σ (tr(ρ))) is the output of the transducer on ρ. It is called the observation of ρ by Obs. We next provide an example of a particular case of observer which can be represented by a finite-state machine.

Checking Diagnosability with Dynamic Diagnosers Definition ((Obs, k)-diagnoser)

Let A be a finite automaton over Σ τ,f and Obs be an observer over Σ. D : Σ * → {0, 1} is an (Obs, k)diagnoser for A if

• ∀ρ ∈ NonFaulty(A), D(Obs(π /Σ (tr(ρ)))) = 0 and

• ∀ρ ∈ Faulty ≥k (A), D(Obs(π /Σ (tr(ρ)))) = 1. A is (Obs, k)-diagnosable if there is an (Obs, k)-diagnoser for A. A is Obs-diagnosable if there is some k such that A is (Obs, k)-diagnosable.
If a diagnoser always selects Σ as the set of observable events, it is a static observer and (Obs, k)diagnosability amounts to the standard (Σ, k)-diagnosis problem [START_REF] Sampath | Diagnosability of Discrete Event Systems[END_REF]. In this case A is (Σ, k)-diagnosable iff equation (4) holds.

As for Σ-diagnosability, (Obs, k)-diagnosability can be stated as a language-based equality:

A is (Obs, k)-diagnosable iff Obs(π /Σ (Faulty tr ≥k (A))) ∩ Obs(π /Σ (NonFaulty tr (A))) = ∅.
This follows directly from definition 5.2.

Problem 3. (Finite-State Obs-Diagnosability)

INPUT: Plant model A = (Q, q 0 , Σ τ,f , →), Obs = (S, s 0 , Σ, δ, L) a finite-state observer. PROBLEM:

(A) Is A Obs-diagnosable?

(B) If the answer to (A) is "yes", compute the minimum k such that A is (Obs, k)-diagnosable.

Theorem 5.1. Problem 3 is in P.

Proof:

We first prove that Problem 3(A) is in P. The proof runs as follows: we build a product automaton 7A ⊗ Obs such that:

A is (Obs, k)-diagnosable ⇐⇒ A ⊗ Obs is (Σ, k)-diagnosable.
Let A = (Q, q 0 , Σ τ,f , →) be a finite automaton and Obs = (S, s 0 , Σ, δ, L) be a finite-state observer. Define the automaton A ⊗ Obs = (Q × S, (q 0 , s 0 ), Σ τ,f , →) as follows:

• (q, s) β -→ (q ′ , s ′ ) iff ∃λ ∈ Σ s.t. q λ -→ q ′ , s ′ = δ(s, λ) and β = λ if λ ∈ L(s), β = τ otherwise; • (q, s) λ -→ (q ′ , s) iff ∃λ ∈ {τ, f } s.t. q λ -→ q ′ .
In this proof we use Obs(ρ) instead of Obs(π /Σ (tr(ρ))) to simplify notations. To prove Theorem 5.1 we use the following lemmas: Lemma 5.1.

Let ρ ∈ Faulty ≥k (A).

There is a word ν ∈ Faulty tr ≥k (A ⊗ Obs) s.t. Obs(ρ) = π /Σ (ν).

Let ρ ′ ∈ NonFaulty(A).

There is a word ν ′ ∈ NonFaulty tr (A ⊗ Obs) s.t. Obs(ρ ′ ) = π /Σ (ν ′ ).

Proof: Let r ∈ Runs(A) s.t. r = q 0 a 1 -→ q 1 • • • q n-1 an -→ q n . By definition of A ⊗ Obs, the run r = (q 0 , s 0 ) b 1 -→ (q 1 , s 1 ) • • • (q n-1 , s n-1 ) bn -→ (q n , s n ) such that for 1 ≤ i ≤ n: • if a i ∈ {τ, f }, b i = a i and s i = s i-1 ; • if a i ∈ L(s i-1 ), b i = a i and s i = δ(s i-1 , a i ); • if a i ∈ L(s i-1 ), b i = τ and s i = s i-1 ; is in Runs(A ⊗ Obs). Moreover (i) a 1 a 2 • • • a n ∈ Faulty tr ≥k (A) ⇐⇒ b 1 b 2 • • • b n ∈ Faulty tr ≥k (A ⊗ Obs) and (ii) Obs(r) = π /Σ (b 1 b 2 • • • b n ) which means that Obs(r) = π /Σ (tr(r)).
By (i), if r ∈ Faulty ≥k (A), tr(r) ∈ Faulty tr ≥k (A ⊗ Obs) and if r ∈ NonFaulty(A), tr(r) ∈ NonFaulty tr (A ⊗ Obs) and in both cases Obs(r) = π /Σ (tr(r)) by (ii).

⊓ ⊔ Lemma 5.2.

1. Let ν ∈ Faulty tr ≥k (A ⊗ Obs). There is a run ρ ∈ Faulty ≥k (A) s.t. Obs(ρ) = π /Σ (ν).

2. Let ν ′ ∈ NonFaulty tr (A ⊗ Obs). There is a run ρ ′ ∈ NonFaulty(A) s.t. Obs(ρ ′ ) = π /Σ (ν ′ ).

Proof:

This proof is the counterpart of the proof of Lemma 5.1. Let r = (q 0 , s 0 )

b 1 -→ (q 1 , s 1 ) • • • (q n-1 , s n-1 ) bn -→ (q n , s n ) be in Runs(A ⊗ Obs). Define a run r = q 0 a 1 -→ q 1 • • • q n-1 an -→ q n with 1 ≤ i ≤ n: • if b i = f , then a i = f , • if b i ∈ Σ, then a i = b i , • if b i = τ , choose some a i ∈ {τ } ∪ Σ \ L(s i-1 ) s.t. q i-1 a i -→ q i .
r is a run in Runs(A) and Obs(r) = π /Σ (tr(r)). It is then easy to see that Lemma 5.2 holds.

⊓ ⊔

Now assume A is (Obs, k)-diagnosable and A ⊗ Obs is not (Σ, k)-diagnosable. There are two words ν ∈ Faulty tr ≥k (A ⊗ Obs) and ν ′ ∈ NonFaulty tr (A ⊗ Obs) s.t. π /Σ (ν) = π /Σ (ν ′ ). By Lemma 5.2, there are two runs ρ ∈ Faulty ≥k (A) and

ρ ′ ∈ NonFaulty(A) s.t. Obs(ρ) = π /Σ (ν) = π /Σ (ν ′ ) = Obs(ρ ′ ) and thus A is not (Obs, k)-diagnosable which is a contradiction. Assume A ⊗ Obs is (Σ, k)-diagnosable and A is not (Obs, k)-diagnosable.
There are two runs ρ ∈ Faulty ≥k (A) and ρ ′ ∈ NonFaulty(A) with Obs(ρ) = Obs(ρ ′ ). By Lemma 5.1, there are two words ν ∈ Faulty tr ≥k (A ⊗ Obs) and ν ′ ∈ NonFaulty tr (A ⊗ Obs) s.t. Obs(ρ) = π /Σ (ν) and π /Σ (ν ′ ) = Obs(ρ ′ ) and thus π /Σ (ν) = π /Σ (ν ′ ). This would imply that A ⊗ Obs is not (Σ, k)-diagnosable which is a contradiction.

The number of states of A ⊗ Obs is at most |Q| × |S| and the number of transitions is bounded by the number of transitions of A. Hence the size of the product is polynomial in the size of the input |A| + |Obs|. Checking that A ⊗ Obs is diagnosable can be done in polynomial time (section 3.1) thus Problem 3.(A) is in P.

To solve Problem 3(B), we can use the same algorithm as for finding the minimum k for a static diagnoser, explained in section 3.1. In this case we apply it to the product A ⊗ Obs. The algorithm is polynomial in the size of A ⊗ Obs, thus Problem 3(B) is also in P. This completes the proof.

⊓ ⊔ Example 5.3. Let A be the DES given in Fig. 2 and Obs the observer of Fig. 7. The product A ⊗ Obs used in the above proof is given in Fig. 8. (Notice that this is different from the synchronized product (see section 2.4) A × Obs since it uses the labeling information available in Obs.) Using an algorithm for checking Σ-diagnosability of A ⊗ Obs we obtain that it is (Σ, 2)-diagnosable (and 2 is the minimum value). Hence A is (Obs, 2)-diagnosable with 2 the minimum value.

For Problem 3, we have assumed that an observer was given. It would be even better if we could synthesize an observer Obs such that the plant is Obs-diagnosable. Before attempting to synthesize such an observer, we should first check that the plant is Σ-diagnosable: if it is not, then obviously no such observer exists; if the plant is Σ-diagnosable, then the trivial observer that observes all events in Σ at all times works 8 . As a first step towards synthesizing non-trivial observers, we can attempt to compute the set of all valid observers, which includes the trivial one but also non-trivial ones (if they exist).

INPUT: Plant model A = (Q, q 0 , Σ τ,f , δ), k ∈ N.
PROBLEM: Compute a set of observers O such that for any observer Obs, A is (Obs, k)-diagnosable iff Obs ∈ O. That is, O includes all observers (and only those) Obs for which A is (Obs, k)-diagnosable.

In the next subsection, we reduce Problem 5 to a safety control problem with partial information. Before giving a solution to Problem 5, we review some useful results on safety games that will be needed in the sequel.

Some Results on Safety Games Under Partial Observation

Computing controllers for system under partial observation has already been studied in [START_REF] Doyen | Algorithms for omega-regular games with imperfect information[END_REF][START_REF] Kupferman | Synthesis with Incomplete Informatio, 2nd International Conference on Temporal Logic[END_REF][START_REF] Lamouchi | Effective Control Synthesis for DES Under Partial Observations[END_REF]. These results apply to general alternating two-player games under partial observation and also for very powerful control objectives (Büchi control objectives). In the sequel we need to use results of the type of those presented in [START_REF] Doyen | Algorithms for omega-regular games with imperfect information[END_REF][START_REF] Kupferman | Synthesis with Incomplete Informatio, 2nd International Conference on Temporal Logic[END_REF][START_REF] Lamouchi | Effective Control Synthesis for DES Under Partial Observations[END_REF] but for a very particular type of two-player games, and only for safety objectives. This is why we provide hereafter the definitions and algorithms to solve this particular instance.

We model a control problem as a game problem between two players. In our setting, partial observation only comes from the fact that Player 1 cannot observe all Player 2 moves. Still Player 1 has to enforce a safety objective i.e., to force the system to stay in a designated set of (safe) states. Player 1 must also play according to the sequence of events it has observed so far: the strategy of Player 1 must be trace-based. In the sequel we formalize these assumptions and give some useful results on this type of games.

Games, Plays, Safety Objective

In each state of the game, it is either the turn of Player 1 to play or the turn of Player 2 to play, but not both (i.e., the moves of the two players alternate). The game starts in a Player 1 state. The rules of the game are as follows:

• Player 1 always plays one move (in the alphabet Σ 1 ) and hands it over to player 2;

• Player 2 can play two types of moves: invisible moves (τ is the invisible action) and visible moves (Σ 2 -actions). If Player 2 plays an invisible move τ , it is again his turn to play. Otherwise if he plays a visible move, the turn switches back to Player 1.

Let ⊎ denote the union of disjoint sets.

Definition 5.3. (Two-Player τ -Games)

A two-player τ -game G is a tuple

(Q 1 ⊎ Q 2 , q 0 , Σ 1 ⊎ Σ τ 2 , δ) with: • Q i , i = 1
, 2 is a finite set of states for player i;

• q 0 ∈ Q 1 is the initial state of the game;

• Σ i is a finite set of visible actions for player i, i = 1, 2;

• δ ⊆ (Q 1 × Σ 1 × Q 2 ) ∪ (Q 2 × {τ } × Q 2 ) ∪ (Q 2 × Σ 2 × Q 1 )
is the transition relation.

Remark 5.1. The type of δ is set according to the rules of the game.

We further assume that the game is deterministic w.r.t Player 1 moves, i.e., for all q 1 ∈ Q 1 , σ 1 ∈ Σ 1 there is at most one state q 2 ∈ Q 2 such that (q 1 , σ 1 , q 2 ) ∈ δ. For (q, a, q ′ ) ∈ δ we also use the notation q a q ′ to write sequences of transitions in a compact manner. If G contains no τ transitions, G is an alternating full-observation two-player game (we use the term two-player game in this case).

Definition 5.4. (Play, Trace)

A play in G is a finite or infinite sequence

ρ = q 0 ℓ 1 q 1 • • • q n ℓ n+1 q n+1 • • •
such that for each i, q i ℓ i+1

---→ q i+1 . We write q 0

ℓ 1 ℓ 2 •••ℓn -----→ q n if q 0 ℓ 1 q 1 • • • ℓ n q n is
a finite play in G. We let Runs(G) be the set of finite plays in G. Runs i (G), i = 1, 2 are the sets of finite plays ending in a Q i -state. The state sequence of a play ρ, denoted States(ρ) is the sequence

q 0 q 1 • • • q n • • • .
We let ρ(i) be the prefix of ρ up to state q i , so ρ(0) = q 0 , ρ(n) = q 0 ℓ 1 q 1 • • • q n , and so on.

Definition 5.5. (Player 1 Strategy)

A strategy for Player 1 is a mapping f :

Runs 1 (G) → Σ 1 . A strategy f is trace-based if for all ρ, ρ ′ ∈ Runs 1 (G), tr(ρ) = tr(ρ ′ ) implies f (ρ) = f (ρ ′ ). A strategy f is memoryless if tgt(ρ) = tgt(ρ ′ ) implies f (ρ) = f (ρ ′ ).

Definition 5.6. (Outcome)

Given a strategy f for Player 1, the outcome, Out(G, f ), of the game G under (or controlled by) f is the set of states sequences9 States(ρ) for the plays ρ = q 0 ℓ 1 q 1

• • • q n ℓ n+1 q n+1 • • • such that for each q i ∈ Q 1 , ℓ i+1 = f (ρ(i)).

Definition 5.7. (Safety Control Objective)

An objective φ for Player 1 is a subset of (Q

1 ∪ Q 2 ) ω ∪ (Q 1 ∪ Q 2 ) * . φ is a safety objective if there is a set F ⊆ Q 1 ∪ Q 2 such that φ = F ω ∪ F * (F is the base set of safe states).
Given a pair (G, φ), a strategy f is winning if Out(G, f ) ⊆ φ. If G is a τ -game and φ a safety objective based on the set F , we say that the pair (G, F ) is a safety game. A state q of G is winning if there is a winning strategy from q.

Safety Two-Player τ -Games

The usual control problem on two-player τ -games asks the following:

Problem 6. (Control Problem)

INPUT: A two-player τ -game G, a safety control objective F . PROBLEM: Is there a winning strategy for (G, F ) ?

To solve safety two-player τ -games we define the Cpre operator [START_REF] Thomas | On the Synthesis of Strategies in Infinite Games[END_REF]:

Cpre(S) = {s ∈ Q 1 | ∃σ 1 ∈ Σ 1 , s.t. δ(s, σ 1 ) ∈ S} (5) ∪ {s ∈ Q 2 | ∀σ 2 ∈ Σ τ 2 , δ(s, σ 2 ) ⊆ S} (6)
It is well-known [START_REF] Thomas | On the Synthesis of Strategies in Infinite Games[END_REF] that iterating Cpre and computing the fix-point Cpre * (F ) gives the set of winning states10 of the game. In case G is finite this computation terminates and can be done in linear time for safety games [START_REF] Thomas | On the Synthesis of Strategies in Infinite Games[END_REF]. If q 0 ∈ Cpre * (F ), there is a strategy for Player 1 to win. Moreover, for this type of games, memoryless strategies are sufficient to win. Indeed, as we can observe the state of the game, τ transitions are not totally unobservable (or invisible) and thus knowing the current state gives some useful information. Also there is a most permissive strategy11 F : Q 1 ∩ Cpre * (F ) → 2 Σ 1 \ ∅ defined by: F(q) = {σ | δ(q, σ) ∈ Cpre * (F )}. This is the most permissive strategy in the following sense: f is a winning strategy for (G, F ) iff for any finite run ρ ∈ Out(G, f ) ending in Q 1 -state, f (ρ) ∈ F(tgt(ρ)), i.e., every move defined by f is a move of the most permissive strategy and vice versa.

In our setting, τ is not observable. What we should ask for to win a game under partial observation, is to base our choice of move on the sole basis on the observable moves that have occurred so far. The problem we want to address is the following: This problem is more demanding than the usual Control Problem (Problem 6) that asks only for a winning strategy for Player 1, i.e., a strategy in which full observation of the state is assumed. To solve Problem 7, we reduce it to a full-observation two-player game (using a construction like the one given in [START_REF] Doyen | Algorithms for omega-regular games with imperfect information[END_REF]).

To do this, we first define the following operator for σ

∈ Σ τ 2 , s ∈ Q 2 , Next 2 (s, σ) = {s ′ | s τ * -→ s 1 σ -→ s ′ } (7) It follows that if σ ∈ Σ 2 , Next 2 (s, σ) ⊆ Q 1 and if σ = τ , Next 2 (s, σ) ⊆ Q 2 . Let σ ∈ Σ 1 and Q ⊆ Q 1 .
We define

Next 1 (Q, σ) = {s ′ ∈ Q 2 | s ′ = δ(s, σ) with s ∈ Q} (8)
To solve (G, F ), we build a full-observation two player game (G H , F H ) (which contains no τ transitions) such that:

Theorem 5.2. There is a winning strategy in (G H , F H ) iff there is a trace-based winning strategy in (G, F ).

The proof of Theorem 5.2 is given in Appendix A. The definition of the game (G H , F H ) is as follows:

Definition 5.8. Assume G = (Q 1 ⊎ Q 2 , q 0 , Σ 1 ⊎ Σ τ 2 δ).
The game G H = (W, s 0 , Σ ′ , ∆) is defined by:

• W = W 1 ⊎ W 2 with W 1 = 2 Q 1 ∪ {⊥ 1 } are the Player 1 states, W 2 = 2 Q 2 ∪ {⊥ 2 } are Player 2 states; • s 0 = {q 0 }, • Σ ′ = Σ 1 ∪ Σ u 2
where u is a fresh name, Σ 1 are Player 1 moves, and Σ u 2 Player 2 moves;

• ∆ ⊆ (W 1 × Σ 1 × W 2 ) ∪ (W 2 × Σ u 2 × W 1
) is defined by: (S, σ, S ′ ) ∈ ∆ iff one of the three conditions holds:

C 1 : S ⊆ Q 1 , σ ∈ Σ 1 and S ′ = Next 1 (S, σ) if for all s ∈ S, σ ∈ Enabled(s) and otherwise S ′ = ⊥ 2 ; C 2 : S ⊆ Q 2 , σ ∈ Σ 2 , S ′ = Next 2 (S, σ) and S ′ = ∅; C 3 : S ⊆ Q 2 , σ = u, Next 2 (S, τ ) ∩ (W \ F ) = ∅ and S ′ = ⊥ 1 .
We let [START_REF] Thomas | On the Synthesis of Strategies in Infinite Games[END_REF] by: let q ∈ W 1 , σ ∈ F H (q) if Next 1 (q, σ) ∈ W H . In other words, the most permissive strategy gives, for each state, the set of moves that keep the system into the set of winning states W H .

F H = {Q ∈ S | Q ⊆ F } i.e.,
Given F H , we can build a strategy for G. Let β(w) be the (unique) state s ′ s.t. q 0 w --→ s ′ in G H . We define the mapping F on Runs 1 (G) by: F(ρ) = F H (tgt(β(tr(ρ)))). Intuitively, this means that, given a run ρ in G ending in a Q 1 -state, to decide what to play, we compute the (unique) state q = tgt(β(tr(ρ))) that can be reached in G H ; then we can play any move from the ones allowed by the most permissive strategy F H (q). Theorem 5.4. F is the most permissive trace-based strategy for G.

Proof:

First F is trace-based 12 . Let f be a trace-based winning strategy. We define f H as in the If part proof of Theorem 5.2. f H is winning and thus for any run w, we have f

H (w) ∈ F H (tgt(w)). By definition of f H , f (ρ) = f H (β(tr(ρ))) and f (ρ) ∈ F H (tgt(β(tr(ρ)))) = F(ρ).
Now assume f is a trace-based strategy such that for each run ρ ∈ Runs 1 (G), f (ρ) ∈ F(ρ). Build f H as before. f H is winning. Indeed, f H (w) = f (ρ) for any ρ s.t. tr(ρ) = tr(w). Hence, f H (w) ∈ F H (tgt(w)) and thus f H is winning. Now from f H build a strategy f as in the Only If part of the proof of Theorem 5.2. It turns out that f = f and as f is winning, f is winning.

⊓ ⊔ Corollary 5.1. The most permissive trace-based strategy F for (G, F ) can be effectively computed and is represented by an automaton which has at most an exponential number of states in the size of G.

This follows from the fact that G H is exponential in the size of G. The most permissive trace-based strategy is obtained from G H by removing from each state q the transitions that are not in F H (q).

Problem 5 as a Game Problem

To solve Problem 5 we reduce it to a safety 2-player τ -game. In short, the reduction we propose is the following:

• Player 1 chooses the set of events it wishes to observe, then it hands over to Player 2;

• Player 2 chooses an event and tries to produce a run which is the observation of both a k-faulty run and a non-faulty run.

Player 2 wins if he can produce such a run. Otherwise Player 1 wins. Player 2 has complete information of Player 1's moves (i.e., it can observe the sets that Player 1 chooses to observe). Player 1, on the other hand, only has partial information of Player 2's moves because not all events are observable (details follow). Let A = (Q, q 0 , Σ τ,f , →) be a finite automaton. To define the game, we use two copies of automaton A: A k 1 and A 2 . The accepting states of A k 1 are those corresponding to runs of A which are faulty and where more than k steps occurred after the fault. A 2 is a copy of A where the f -transitions have been removed. The game we are going to play is the following (see Fig. 9, Player 1 states are depicted with square boxes and Player 2 states with round shapes): 1. the game starts in a state (q 1 , q 2 ) corresponding to the initial states the automata A k 1 and A 2 . Initially, it is Player 1's turn to play. Player 1 chooses a set of events he is going to observe i.e., a subset X of Σ and hands it over to Player 2;

(q 1 , q 2 ) (q 1 , q 2 ) • • • (q, q ′ ) • • • (q ′ 1 , q ′ 2 ) (q ′′ 1 , q ′′ 2 ) Player 1 chooses X ⊆ Σ λ 1 ∈ X σ 1 ∈ X λ 2 ∈ X λ 3 ∈ X σ 2 ∈ X λ 4 ∈ X

assume the automata A k

1 and A 2 are in states (q 1 , q 2 ). Player 2 can change the state of A k 1 and A 2 by: (a) firing an action which is not in X (like λ 1 , λ 2 , λ 3 , λ 4 in Fig. 9): it is an unobservable action and thus, it can be taken independently by either A k 1 or A 2 (they do not need to synchronise). In this case a new state (q, q ′ ) is reached and Player 2 can play again from this state. Notice that Player 2's moves do not change the set X;

(b) firing an action in X (like σ 1 , σ 2 in Fig. 9): to do this both A k 1 and A 2 must be in a state where such an action (e.g., σ 1 , σ 2 ) is enabled (synchronization); after the action is fired a new state (q ′ 1 , q ′ 2 ) is reached: now it is Player 1's turn to play, and the game continues as in step 1 above from the new state (q ′ 1 , q ′ 2 ).

Player 2 wins if he can reach a state (q 1 , q 2 ) in the product of A k 1 and A 2 where q 1 is an accepting state of A k 1 (this means that Player 1 wins if it can avoid ad infinitum this set of states). In this sense this is a safety game for Player 1 (and a reachability game for Player 2). Formally, the game G A = (S 1 ⊎ S 2 , s 0 , Σ 1 ⊎ Σ 2 , δ A ) is defined as follows (⊎ denotes union of disjoint sets):

• S 1 = (Q × {-1, • • • , k}) × Q is the set of Player 1 states; a state ((q 1 , j), q 2 ) ∈ S 1 indicates that A k
1 is in state q 1 , j steps have occurred after a fault, and q 2 is the current state of A 2 . If no fault has occurred, j = -1 and if more than k steps occurred after the fault, we use j = k.

• S 2 = (Q × {-1, • • • , k}) × Q × 2 Σ
is the set of Player 2 states. For a state ((q 1 , j), q 2 , X) ∈ S 2 , the triple ((q 1 , j), q 2 ) has the same meaning as for S 1 , and X is the set of moves Player 1 has chosen to observe on its last move.

• s 0 = ((q 0 , -1), q 0 ) is the initial state of the game belonging to Player 1;

• Σ 1 = 2 Σ is the set of moves of Player 1; Σ 2 = Σ τ is the set of moves of Player 2 (as we encode the fault into the state, we do not need to distinguish f from τ ).

• the transition relation

δ A ⊆ (S 1 × Σ 1 × S 2 ) ∪ (S 2 × {τ } × S 2 ) ∪ (S 2 × Σ × S 1
) is defined by:

-Player 1 moves: let σ ∈ Σ 1 and s 1 ∈ S 1 . Then (s 1 , σ, (s 1 , σ)) ∈ δ A .

-Player 2 moves: a move of Player 2 is either a silent move (τ ) i.e., a move of A k 1 or A 2 or a joint move of A k 1 and A 2 with an observable action in X. Consequently, a silent move ((q 1 , i), q 2 , X), τ, (q ′ 1 , j), q ′ 2 , X)) is in δ A if one of the following conditions holds:

1. either q ′ 2 = q 2 , q 1 ℓ -→ q ′ 1 is a step of A k 1 , ℓ ∈ X, and if i ≥ 0 then j = min(i + 1, k); if i = -1 and ℓ = f , then j = 0 otherwise j = i.

either q

′ 1 = q 1 , q 2 ℓ -→ q ′ 2 is a step of A 2 , ℓ ∈ X (and ℓ = f ), and if i ≥ 0 then j = min(i + 1, k), otherwise j = i.
A visible move can be taken by Player 2 if both A k 1 and A 2 agree on doing such a move. In this case the game proceeds to a Player 1 state:

((q 1 , i), q 2 , X), ℓ, ((q ′ 1 , j), q ′ 2 )) ∈ δ A if ℓ ∈ X, q 1 ℓ -→ q ′ 1 is a step of A k 1 , q 2 ℓ -→ q ′
2 is a step of A 2 , and if i ≥ 0 then j = min(i + 1, k), otherwise j = i.

We can show that for any observer

O s.t. A is (O, k)-diagnosable, there is a strategy f (O) for Player 1 in G A s.t. f (O) is trace-based and winning. A strategy for Player 1 is a mapping f : Runs(G A ) → Σ 1 that associates a move f (ρ) in Σ 1 with each run ρ in G A that ends in an S 1 -state. Remind that a strategy f is trace-based (see section 5.3 for details), if given two runs ρ, ρ ′ , if tr(ρ) = tr(ρ ′ ) then f (ρ) = f (ρ ′ ).
Conversely, for any trace-based winning strategy f (for Player 1), we can build an observer

O(f ) s.t. A is (O(f ), k)-diagnosable.
Let O = (S, s 0 , Σ, δ, L) be an observer for A. We define the strategy f (O) on finite runs of G A ending in a Player 1 state by: f (O)(ρ) = L(δ(s 0 , π /Σ (tr(ρ)))). The intuition is that we take the run ρ in G A , take the trace of ρ (choices of Player 1 and moves of Player 2) and remove the choices of Player 1. This gives a word in Σ * . The strategy for Player 1 for ρ is the set of events the observer O chooses to observe after reading π /Σ (tr(ρ)) i.e., L(δ(s 0 , π /Σ (tr(ρ)))).

Proof:

First f (O) is trace-based by definition. We have to prove that f (O) is winning. We denote Out(G, f ) the set of outcomes i.e., the set of possible runs of a game G when the strategy f is played by Player 1 (see section 5.3 for a formal definition of Out(G A , f )). Assume on the contrary that f (O) is not winning. This implies that there is a run ρ in Out(G A , f (O)) as defined by equations (9-11) below: Each step i of the run given by one of equations (9-11) consists of a choice of Player 1 (X i move) followed by a number of moves by Player 2 (λ j i actions). The last state encountered in ρ, ((q 1 n (α), k n (α)), q 2 n (α), X n ) is a losing state for Player 1, which means that k n (α) = k, by definition of losing states in G A . From the run ρ, we can build two runs ν and ν ′ defined by equations ( 12) and ( 13): By definition of G A , each λ j i is either a common visible action of A k 1 and A 2 and it is in Σ, or a silent action (τ ) i.e., it actually corresponds to an action of A k 1 or A 2 that is not in the current set of visible actions X i . To retrieve a run in A k 1 (resp. A 2 ) from ν (resp. ν ′ ) we can safely remove the unobservable actions of A 2 (resp. A k 1 ) because they leave the state of A k 1 (resp. A 2 ) unchanged. This way we obtain two runs ν and ν′ , which, when interleaved give a run of A k 1 × A 2 . By definition of G A , ν ∈ Faulty ≥k (A) and ν′ ∈ NonFaulty(A). We claim that O(ν) = O(ν ′ ). Indeed, each part of the runs from

q 1 i • • • q 1 i+1 and q 2 i • • • q 2 i+1 yields the ρ = (q 1 0 , -1), q 2 0 X 0 --→ (q 1 0 , 0), q 2 0 , X 0 λ 1 0 -→ (q 1 0 (1), k 0 (1)), q 2 0 (1), X 0 • • • (q 1 0 (j), k 0 (j)), q 2 0 (j), X 0 • • • λ n 0 0 --→ (9)
(q 1 1 , k 1 ), q 2 1 X 1 --→ (q 1 1 , k 1 ), q 2 1 , X 1 λ 1 1 -→ (q 1 1 (1), k 1 (1)), q 2 1 (1), X 1 • • • (q 1 1 (j), k 1 (j)), q 2 1 (j), X 1 • • • λ n 1 1 --→ (10)
. . . (. . .)

(q 1 n , k n ), q 2 n Xn --→ (q 1 n , k n ), q 2 n , X n • • • (q 1 n (j), k n (j)), q 2 n (j), X n • • • λ α 0 -→ (q 1 n (α), k n (α)), q 2 n (α), X n (11)
ν = q 1 0 λ 1 0 -→ q 1 0 (1)
λ 2 0 -→ • • • λ n 0 0 --→ q 1 1 λ 1 1 -→ • • • λ n 1 1 --→ q 1 2 • • • q 1 n λ 1 n -→ • • • λ α n -→ q 1 n (α) (12)
ν ′ = q 2 0 λ 1 0 -→ q 2 0 (1)
λ 2 0 -→ • • • λ n 0 0 --→ q 2 1 λ 1 1 -→ • • • λ n 1 1 --→ q 2 2 • • • q 2 n λ 1 n -→ • • • λ α n -→ q 2 n (α) (13)
same observation by O: it is the sequence of events λ j 1 • • • λ jn i s.t. each λ j l is a letter of both A k 1 and A 2 and is in X i . As there are two runs ν ∈ Faulty ≥k (A) and ν′ ∈ NonFaulty(A) with the same observation, A is not (O, k)-diagnosable which contradicts the assumption. Hence f (O) must be winning.

⊓ ⊔

Conversely, with each trace-based strategy f of the game G A we can associate an automaton O(f ) = (S, s 0 , Σ, δ, L) defined by:

• S = {π /Σ (tr(ρ)) | ρ ∈ Out(G A , f ) and tgt(ρ) ∈ S 1 }; • s 0 = ε; • δ(v, ℓ) = v ′ if v ∈ S, v ′ = v.ℓ and there is a run ρ ∈ Out(G A , f ) with ρ = q 0 X 0 --→ q 1 0 τ * -→ q n 0 0 λ 1 -→ q 1 X 1 --→ q 1 1 τ * -→ q n 1 1 λ 2 -→ q 2 • • • q k 1 τ * -→ q n k-1 k-1 λ k -→ q k with each q i ∈ S 1 , q j i ∈ S 2 , v = π /Σ (tr(ρ)), and ρ X k --→ q 1 k τ * -→ q n k k ℓ -→ q k+1 with q k+1 ∈ S 1 , ℓ ∈ X k . δ(v, l) = v if v ∈ S and ℓ ∈ f (ρ); • L(v) = f (ρ) if v = π /Σ (tr(ρ)).

Proof:

We first have to prove that O(f ) (more precisely L) is well defined. Assume v = π /Σ (tr(ρ)) and v ′ = π /Σ (tr(ρ ′ )). As f is trace-based, f (ρ) = f (ρ ′ ) and there is a unique value for L(v).

We also have to prove that the last requirement of Definition 5.1 is satisfied i.e., if a ∈ L(s) then δ(s, a) = s.

If ℓ ∈ L(v), then ℓ ∈ f (π /Σ (tr(ρ))) for any ρ s.t. v = π /Σ (tr(ρ)) because f is trace-based. Thus δ(v, ℓ) = v. ⊓ ⊔ Theorem 5.6. Let f be a trace-based winning strategy in G A . Then A is (O(f ), k)-diagnosable. Proof: Assume A is not (O(f ), k)-diagnosable.
There are two runs ν ∈ Faulty ≥k (A) and ν ′ ∈ NonFaulty(A)

s.t. O(f )(π /Σ (tr(ν))) = O(f )(π /Σ (tr(ν ′ ))
). Let ν (resp. ν′ ) be the sequence of labels that appear in ν (resp. ν ′ ). We can write ν and ν′ in the form

ν = w -1 λ 0 w 0 λ 1 w 1 • • • λ n w n (14) ν′ = w ′ -1 λ 0 w ′ 0 λ 1 w ′ 1 • • • λ n w ′ n ( 15
)
with w i , w ′ i ∈ (Σ \ O(f )(λ 0 λ 1 • • • λ i ) * for i ≥ 0 and w -1 , w ′ -1 ∈ (Σ \ O(f )(ε)) * , and λ i+1 ∈ O(f )(λ 0 λ 1 • • • λ i ).
We build a run in Out(G A , f ) as follows:

1. Player 1 chooses the set X 0 = O(f )(ε) which is by definition equal to f ((q 1 0 , -1), q 2 0 ) where ((q 1 0 , -1), q 2 0 ) is the initial state of the game.

2. Player 2 plays the sequence of actions in w 1 and w ′ 1 synchronizing on the common actions of w 1 and w ′ 1 . The game moves through S 2 states because each action is an invisible move. Finally Player 2 chooses λ 0 ∈ O(f )(ε). The game reaches a new S 1 -state ((q 1 1 , k 1 ), q 2 1 ).

3. from ((q 1 1 , k 1 ), q 2 1 ), the strategy f is to play X 1 which by definition is O(f )(λ 0 ). Thus Player 2 can play the sequence of actions given in w 2 and w ′ 2 synchronizing again on common action. In the end, Player 2 plays λ 1 ∈ O(f )(λ 0 ).

We can iterate the previous algorithm and build a run in Out(G A , f ) that reaches a state ((q 1 n , k n ), q 2 n ) with k n = k and thus Out(G A , f ) contains a losing run. Hence f is not winning which contradicts the assumption. This way we conclude that A is (O(f ), k)-diagnosable.

⊓ ⊔

The result on G A (section 5.3) is that, if there is a winning trace-based strategy for Player 1, then there is a most permissive strategy F A which has finite memory. It can be represented by a finite automaton

S F A = (W 1 ⊎ W 2 , s 0 , Σ ∪ 2 Σ , ∆ A ) s.t. ∆ A ⊆ (W 1 × 2 Σ × W 2 ) ∪ (W 2 × Σ × W 1 ) which has size exponential in the size of G A . For a given run ρ ∈ (Σ ∪ 2 Σ ) * ending in a W 1 -state, we have F A (w) = Enabled(∆ A (s 0 , w)).

Most Permissive Observer

We now define the notion of most permissive observer and show the existence of a most permissive observer for a system in case A is diagnosable. F A is the mapping defined at the end of the previous section.

For an observer O = (S, s 0 , Σ, δ, L) and w ∈ Σ * we let L(w) be the set L(δ(s 0 , w)): this is the set of events O chooses to observe on input w. Given a word ρ ∈ π /Σ (L(A)), we recall that O(ρ) is the observation of

ρ by O. Assume O(ρ) = a 0 • • • a k . Let ρ = L(ε).a 0 .L(a 0 ).a 1 . • • • a k .L(O(ρ)(k)) i.e., ρ
contains the history of what O has chosen to observe at each step and the events that occurred after each choice.

Let

O : 2 Σ .(Σ τ × 2 Σ ) + → 2 2 Σ
. By definition O is the most permissive observer for (A, k) if the following holds:

O = (S, s 0 , Σ, δ, L) is an observer and A is (O, k)-diagnosable ⇐⇒ ∀w ∈ Σ * , L(δ(s 0 , w)) ∈ O(w)
The definition of the most permissive observer states that:

• any good observer O (one such that A is (O, k)-diagnosable) must choose a set of observable events in O(w) on input w;

• if an observer chooses its set of observable events in O(w) on input w, then it is a good observer.

Assume A is (Σ, k)-diagnosable. Then there is an observer O s.t. A is (O, k)-diagnosable because the constant observer that observes Σ is a solution. By Theorem 5.5, there is a trace-based winning strategy for Player 1 in G A . As said at the end of the previous subsection, in this case there is a most permissive trace-based winning strategy which is F A .

Theorem 5.7. F A is the most permissive observer.

Proof:

Let O = (S, s 0 , Σ, δ, L) be an observer such that A is (O, k)-diagnosable. We have to prove that L(δ(s 0 , w)) ∈ F A (w) for any w ∈ Σ * . By Theorem 5.5, the strategy f (O) is a winning tracebased strategy and this implies that f (O)(ν) ∈ F A (ν) for any run ν of G A . By definition of w, π /Σ (w) = w. By definition of f (O), f (O)(w) = L(δ(s 0 , π /Σ (tr(w)))) = L(δ(s 0 , w)) and thus L(δ(s 0 , w)) ∈ F A (w).

Conversely, assume O is such that ∀w ∈ Σ * , L(s 0 , w) ∈ F A (w). We have to prove that A is

(O, k)-diagnosable. Again, we build f (O). As before, f (O) is a winning trace-based strategy in G A and thus O(f (O)) is such that A is (O(f (O)), k)-diagnosable by Theorem 5.6. Assume O(f (O)) = (S ′ , s ′ 0 , Σ, δ ′ , L ′ )). By construction of O(f (O)), L ′ (δ ′ (s ′ 0 , w)) = f (O)(ρ) if w = π /Σ (tr(ρ)). Hence O(f (O)) = O and A is (O, k)-diagnosable. ⊓ ⊔
This enables us to solve Problem 5 and compute a finite representation of the set O of all observers such that A is Example 5.4. For the automaton A of Fig. 2, we obtain the most permissive observer F A shown in Fig. 10. In the even states, depicted as a square, the observer chooses (non-deterministically) what to observe and in the odd states, depicted as a circle, it moves according to what it observes. For odd states we have not shown the component X that has last been picked up by the observer. X is the label of the unique incoming transition. Initially, the observer may choose to observe either {a, b} or {a}. If it observes a, then it moves to state 2, where it can choose any subset containing b. If it observes b instead, then it moves to state 4, where it can choose to observe anything, including the empty set.

(O, k)-diagnosable iff O ∈ O. Computing F A can be done in O(2 |G A | ) (section 5.3). The size of G A is quadratic in |A|,
We point out that from an odd state (2k + 1, X), outgoing transitions are labeled by elements of X. This does not mean that the DES under observation cannot do other actions than those in X: it might be able to do so but these actions are unobservable for the observer.

Computation of the Most Permissive Diagnoser

We conclude this section by showing how to compute a generic diagnoser. This diagnoser is the most permissive dynamic diagnoser and contains all the choices a dynamic diagnoser can make to be able to diagnose a plant. The construction of the most permissive dynamic diagnoser follows easily from the construction of the most permissive observer and the construction of a synchronized product (using the ⊗ defined operator defined in section 5.2). The steps to build it are:

1. from the plant A, build à which behaves like A but where the states which are after a faulty event are tagged i.e., each state of à is of the form (q, k) where k = 0 (non faulty states) or k = 1 (faulty states);

2. determinize à assuming f and τ are unobservable and obtain det( Ã); the final states S of det( Ã) are the the set of states of the form S = {(q 1 , 1), (q 2 , 1), • • • , (q n , 1)} i.e., all the states in S are faulty;

3. write the most permissive observer as a non-deterministic observer (like in Definition 5.1) and obtain O;

4. synchronize O and det( Ã) to obtain the most permissive dynamic diagnoser: announce a fault when O ⊗ det( Ã) reaches a final state, and otherwise no fault can be announced.

We now define precisely the previous steps. Let A = (Q, q 0 , Σ τ,f , →) be a finite automaton over Σ τ,f .

Definition of det( Ã)

. Define à = (Q × {0, 1}, (q 0 , 0), Σ τ , → ˜) s.t.

• (q, n) l -→ ˜(q ′ , n ′ ) iff q l -→ q ′ and l ∈ Σ and n = n ′ ;

• (q, n) τ -→ ˜(q ′ , 1) iff q f -→ q ′ , (n is set to 1 after a fault);

• (q, n) τ -→ ˜(q ′ , n) iff q τ -→ q ′ .
We equip à with the set of final states F = Q × {1}. For the example of Fig. 2

Definition of O ⊗ det( Ã).

To compute the most permissive dynamic diagnoser, we first write the most permissive observer as a non-deterministic observer i.e., following Definition 5.1.

To obtain a "generic" dynamic diagnoser it suffices to synchronize it (using the ⊗ operator defined in section 5.2). The most permissive (non-deterministic) dynamic diagnoser D A for the automaton A of when it reaches its final state F A . In state F A and F ′ A , D A can choose to observe any subset of {a, b} but no event can occur anymore. F A is a final state whereas F ′ A is not. Notice also that D A starts either from 0 or 1. As the size of det( Ã) is also exponential in the size of A, D A has size exponential in the size of A (and k) and doubly exponential in the size of Σ.

Optimal Dynamic Observers

In this section we define a notion of cost for observers. This will allow us to compare observers w.r.t. to this criterion and later on to synthesize an optimal observer.

Weighted Automata & Karp's Algorithm

Before introducing the optimal dynamic observer and diagnoser synthesis problem, we present a set of tools that we are going to use in that process. These deal with the notion of cost in a model of dynamic behaviors such as a finite automaton model. The notion of cost for automata has already been defined and algorithms to compute some optimal values related to this model are described in many papers. For our purposes, the model of weighted automata is appropriate. We recall here this model and the results of [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF] which will be used later.

Definition 6.1. (Weighted Automaton)

A weighted automaton is a pair (A, w) s.t. A = (Q, q 0 , Σ, δ) is a finite automaton and w : Q → N associates a weight with each state.

Definition 6.2. (Mean Cost)

Let ρ = q 0 a 1 -→ q 1 a 2 -→ • • • an -→ q n be a run of A. The mean cost of ρ is µ(ρ) = 1 n + 1 × n i=0
w(q i ) .

We remind that the length of ρ = q 0

a 1 -→ q 1 a 2 -→ • • • an -→ q n is |ρ| = n.
We assume that A is complete w.r.t. Σ (and Σ = ∅) and thus contains at least one run for any arbitrary length n. Let Runs n (A) be the set of runs of length n in Runs(A). The maximum mean-weight of the runs of length n for A is ν(A, n) = max{µ(ρ) for ρ ∈ Runs n (A)}. The maximum mean weight of A is ν(A) = lim sup n→∞ ν(A, n). Actually the value ν(A) can be computed using Karp's maximum mean-weight cycle algorithm [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF] on weighted graphs. If c = s 0

a 1 -→ s 1 a 2 -→ • • • an -→ s n is a cycle of A i.e., s 0 = s n , the mean weight of the cycle c is µ(c) = 1 n+1 • n i=0 w(s i ).
The maximum mean-weight cycle of A is the value ν * (A) = max{µ(c) for c a cycle of A}. As stated in [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF], for weighted automata, the mean-weight cycle value is the value that determines the mean-weight value (the transient behaviors of the system are not contributing to this value). It follows that ν(A) = lim sup n→∞ ν(A, n) = lim n→∞ ν(A, n) = ν * (A).

The original Karp's maximum mean cycle algorithm [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF] works for weighted automaton where the weights are on the edges. We give the version where weights are on vertices. Let ν * = max c µ(c) where c ranges over all cycles in A. A cycle c with µ(c) = ν * is a maximum mean-weight cycle. Let D(q) be the weight of a most expensive path from q 0 to q and D k (q) be the weight of a most expensive path which has exactly k edges (if there is no such path D k (v) = -∞). Assume |Q| = n. Karp's algorithm is based on the fact that

ν * = max q∈Q min 0≤k≤n-1 D n (q) -D k (q) n -k
The values D k (q) can be computed iteratively:

D 0 (q 0 ) = w(q 0 ) (16) D 0 (q) = -∞ for q = q 0 (17) D k+1 (q) = max q∈δ(q ′ ,a) {D k (q ′ ) + w(q)} (18)
Thus for each state q we can compute min(q) = min 0≤k≤n-1

Dn(q)-D k (q) n-k
and then compute the value max q∈Q min(q) to obtain ν * . This algorithm runs in O(n.m) where |Q| = n and |δ| = m (where |δ| denotes the number of transitions in δ). Improvements [START_REF] Dasdan | Efficient algorithms for optimum cycle mean and optimum cost to time ratio problems[END_REF] can be made to this algorithm still the worst case run-time is O(n.m).

Cost of a Dynamic Observer

Let Obs = (S, s 0 , Σ, δ, L) be an observer and A = (Q, q 0 , Σ τ,f , →). We would like to define a notion of cost for observers in order to select an optimal one among all of those which are valid, i.e., s.t. A is (Obs, k)-diagnosable. Intuitively this notion of cost should capture the fact that the more events we observe at each time, the more expensive it is.

Definition of Cost.

Given a word w = a 0 a 1 • • • a n , we let w(i) = a 0 • • a i be the prefix up to a i of w. In the sequel Obs(w)(i) thus denotes the prefix up to the ith letter of Obs(w).

There is not one way of defining a notion of cost for observers and we first discuss two different notions:

• the first one is to define the cost of a word w generated by the DES w.r.t. to Obs(w):

Cost 1 (w) = i=n i=0 |L(δ(s 0 , Obs(w)(i)))| n + 1
with n = |Obs(w)|. Using the observer of Fig. 12, we obtain that Cost 1 (b n .a) = 1+0 2 = 1 2 . And this regardless of the value of n.

• the second one is to define the cost of w w.r.t. to w itself: The example of Fig. 12 shows that the two notions are different. In the sequel we will use the second one, Cost 2 , because Cost 2 also captures the notion of the time we have been observing a set of events. Indeed, if the word b n+1 occurs, we have been observing the set L(0) n + 1 times in a logical time. It is natural that this is more expensive than observing L(0) n times. Thus Cost 2 is more satisfying than abstracting away the length of the input word as in Cost Cost of an Observer. We now show how to define and compute the cost of an observer Obs operating on a DES A.

Given a run ρ ∈ Runs(A), the observer only processes π /Σ (tr(ρ)) (τ and f -transitions are not processed). To have a consistent notion of costs that takes into account the logical time elapsed from the beginning, we need to take into account one way or another the number of steps of ρ (the length of ρ) even if some of them are non observable. A simple way to do this is to consider that τ and f are now observable events, let's say u, but that the observer never chooses to observe them. Indeed we assume we have already checked that A is (Obs, k)-diagnosable, and the problem is now to compute the cost of the observer we have used.

Definition 6.3. (Cost of a Run

) Given a run ρ = q 0 a 1 -→ q 1 • • • q n-1 an -→ q n ∈ Runs(A), let w i = π /Σ (tr(ρ(i))), 0 ≤ i ≤ n. The cost of ρ ∈ Runs(A) is defined by: Cost 2 (ρ, A, Obs) = 1 n + 1 • n i=0 |L(δ(s 0 , w i ))|.
We recall that Runs n (A) is the set of runs of length n in Runs(A). The cost of the runs of length n of A is defined by: Cost 2 (n, A, Obs) = max{Cost 2 (ρ, A, Obs) for ρ ∈ Runs n (A)}.

And finally, the cost of the pair (Obs, A) is Notice that Cost 2 (n, A, Obs) is defined for each n because we have assumed A generates runs of arbitrary large length.

As emphasised previously, in order to compute Cost 2 (n, A, Obs) we consider that τ and f are now observable events, say u, but that the observer never chooses to observe them. Let Obs + = (S, s 0 , Σ u , δ ′ , L) where δ ′ is δ augmented with u-transitions that loop on each state s ∈ S. Let A + be A where τ and f transitions are renamed u. Let A + × Obs + be the synchronized product of A + and Obs + . A + × Obs + = (Z, z 0 , Σ u , ∆) is complete w.r.t. Σ u and we let w(q, s) = |L(s)| so that (A + × Obs + , w) is a weighted automaton. Theorem 6.1. Cost 2 (A, Obs) = ν * (A + × Obs + ).

Proof:

The proof follows easily from the definitions. Let ρ be a run of A. There exists a run ρ in A + × Obs + s.t. Cost 2 (ρ, A, Obs) = µ(ρ) (µ is the mean cost as stated in Definition 6.3). ρ is obtained from ρ by replacing τ and f transitions by some u transitions. Conversely for any run ρ in A + × Obs + there is a run ρ in A s.t. µ(ρ) = Cost 2 (ρ, A, Obs).

⊓ ⊔

We can compute the cost of a given pair (A, Obs): this can be done using Karp's maximum mean weight cycle algorithm [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF] on weighted graphs. This algorithm is polynomial in the size of the weighted graph and thus we have:

0 1 2 3 4 D 0 1 -∞ -∞ -∞ -∞ D 1 -∞ 4 -∞ -∞ 4 D 2 -∞ -∞ 6 -∞ 6 D 3 -∞ -∞ -∞ 8 8 D 4 -∞ -∞ -∞ 10 10 min -∞ -∞ -∞ 2 2 Table 1. Iterations for A + × O + 1 . 0 1 2 3 4 5 D 0 1 -∞ -∞ -∞ -∞ -∞ D 1 -∞ 2 -∞ -∞ 2 2 D 2 -∞ -∞ 3 -∞ 3 3 D 3 -∞ -∞ -∞ 4 4 4 D 4 -∞ -∞ -∞ 4 5 5 D 5 -∞ -∞ -∞ 4 6 6 min -∞ -∞ -∞ 0 1 1 Table 2. Iterations for A + × O + 2 .
One of the result of [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF] is that there is a rational value ν ∈ Q s.t. Player 1 has a strategy to ensure lim inf n→∞ 1 n • n i=1 w(e i ) ≥ ν and Player 2 has a strategy to ensure that lim sup n→∞ 1 n • n i=1 w(e i ) ≤ ν. ν is called the value of the game. Let n = |V |. To compute ν, proceed as follows [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]:

1. Let ν 0 (v) = 0 for v ∈ V . For v ∈ V and k ≥ 1, ν k (v) is defined by: ν k (v) = max (v,w)∈E {w(v, w) + ν k-1 (w)} if v ∈ V 1 min (v,w)∈E {w(v, w) + ν k-1 (w)} if v ∈ V 2
This is the equivalent of the D k (v) values for Karp's algorithm using a min max strategy depending on which player is playing;

2. for each v ∈ V , compute ν ′ (v) = ν k (v)/k for k = 4 • n 3 • W .
3. for each vertex, the value of the game from v is the only rational number with a denominator at most n that lies in the interval ]ν

′ (v) -α, ν ′ (v) + α[ with α = 1 2n(n-1) .
The value of the game is ν = ν(v 0 ) where v 0 is the initial vertex. To compute an optimal strategy for Player 1, proceed as follows:

1. compute the values ν(v) for each v ∈ V ;

2. if all the vertices of V 1 have outgoing degree 1, there is a unique strategy and it is positional and optimal;

3. otherwise, take a vertex v ∈ V 1 with outgoing degree d ≥ 2. Remove ⌈ d 2 ⌉ edges from v leaving at least one. Recompute the value m v for each v. If m v = ν(v), there is an optimal positional strategy which uses the remaining edges from v. Otherwise there is a positional strategy that uses one of the removed edges.

We can iterate the previous scheme to find an optimal strategy for Player 1. In summary some of the results by Zwick and Paterson [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF] we are going to use are:

• there is a value ν ∈ Q, called the value of the game s.t. Player 1 has a strategy to ensure that lim inf n→∞ • there are optimal memoryless strategies for both players that can be computed in O

(|V | 4 × |E| × log(|E|/|V |) × W ).

Synthesis of an Optimal Observer

To solve the Problem 8, we use the most permissive observer F A we computed in section 5.5. Given A and F A , we build a weighted graph game G(A, F A ) s.t. the value of the game is the optimal cost for the set of all observers. Moreover an optimal observer can be obtained by taking an optimal memoryless strategy in G(A, F A ).

To build G(A, F A ) we use the same idea as in section 6.2: we replace τ and f transitions in A by u obtaining A + . We also modify F A to obtain a weighted graph game (F + A , w) by adding transitions so that each state 2k + 1 is complete w.r.t. Σ u . This is done as follows:

• from each (2i + 1, X) state, create a new even state i.e., pick some 2i ′ that has not already been used. Add transitions ((2i + 1, X), σ, 2i ′ ) for each σ ∈ Σ u \ Enabled(2i + 1, X). Add also a transition (2i ′ , X, (2i + 1, X)). This step means that if a A produces an event and it is not observable, F + A just reads the event and makes the same choice again.

• the weight of a transition (2i, X, (2i ′ + 1, X)) is |X|.

The automaton F + A obtained from F A is depicted on Fig. 15. The game G(A, F A ) is then A + ×F + A . This way we can obtain a weighted graph game W G(A, F A ) by abstracting away the labels of the transitions. Notice that it still enables us to convert any strategy in W G(A, F A ) to a strategy in F A . A strategy in W G(A, F A ) will define an edge (2i, (2i ′ + 1, X)) to take. As the target vertex contains the set of events we chose to observe we can define a corresponding strategy in F A . By construction of G(A, F A ) and the definition of the value of a weighted graph game, the value of the game is the optimal cost for the set of all observers O s.t. A is (O, k)-diagnosable.

Assume A has n states and m transitions. From Theorem 5.7 we know that

F A has at most O(2 n 2 × 2 k × 2 2 |Σ| ) states and O(2 n 2 × 2 k × 2 2 |Σ| × n 2 × k × m) transitions. Hence G(A, F A ) has at most O(n × 2 n 2 × 2 k × 2 2 |Σ| ) vertices and O(m × 2 n 2 × 2 k × 2 2 |Σ|
) edges. To make the game complete we may add at most half the number of states and hence W G(A, F A ) has the same size. We thus obtain the following results: A consequence of Theorem 6.4 and Zwick and Paterson's results is that the cost of the optimal observer is a rational number. Example 6.2. For the example A of Fig. 8 andF + A of Fig. 15, using Zwick and Paterson's algorithm we obtain that the optimal cost is 1 and the optimal strategy is to use the observer Obs of Fig. 7.

Conclusions

In this paper we have addressed sensor minimization problems in the context of fault diagnosis, using both static and dynamic observers. We showed that computing the smallest number of observable events necessary to achieve diagnosis with a static observer is NP-complete: this result also holds in the mask-based setting which allows to consider events that are observable but not distinguishable. We then focused on dynamic observers and proved that, for a given such observer, diagnosability can be checked in polynomial time (as in the case of static observers). We also solved a synthesis problem of dynamic observers and showed that a most-permissive dynamic observer can be computed in doubly-exponential time, provided an upper bound on the delay needed to detect a fault is given. Finally we have defined a notion of cost for dynamic observers and shown how to compute the minimal-cost observer that can be used to detect faults within a given delay.

There are several directions we are currently investigating:

• Problem 4 has not been solved so far. The major impediment to solve it is that the reduction we propose in section 5 yields a Büchi game. The algorithm we give in section 5.3 does not work for Büchi games and cannot be extended trivially. More generally we plan to extend the framework we have introduced for fault diagnosis to control under dynamic partial observation and this will enable us to solve Problem 4.

• Problem 5 is solved in doubly exponential time. To reduce the number of states of the most permissive observer, we point out that only minimal sets of events need to be observed. Indeed, if we can diagnose a system by observing only A from some point on, we surely can diagnose it using any superset A ′ ⊇ A. So far we keep all the sets that can be used to diagnose the system. We could possibly take advantage of the previous property using techniques described in [START_REF] Doyen | Algorithms for omega-regular games with imperfect information[END_REF].

• ρ ′ H ∈ Out(G H , f H ) and P 1 and P 2 hold;

• as ρ ′ H satisfies P 2 :

-either it satisfies P 2 .(a) and tgt(ρ ′ H ) ∈ {⊥ ----→ S 2(k+1)+1 . This means that S 2(k+1)+1 = ⊥ 2 . In this case q 1 2(k+1)+1 ∈ S 2(k+1)+1 . Again two cases arise:

(a) either there is some 2 ≤ j ≤ n 2(k+1)+1 s.t. q j 2(k+1)+1 ∈ F and in this case This completes the proof of Lemma A.1.

⊓ ⊔ Now assume f is not winning, we can build a run ρ ∈ Out(G, f ) with tgt(ρ) ∈ F . Applying Lemma A.1 we obtain: there is a run ρ H ∈ Out(G H , f H ) that satisfies P 1 and P 2 :

• either tgt(ρ H ) ∈ {⊥ 1 , ⊥ 2 } and in this case ρ H is a losing run for Player 1 and thus f H is not winning which contradicts the assumption;

• or ρ H contains no state in {⊥ 1 , ⊥ 2 }. Two cases arise depending on the parity of the length of ρ H :

-either ρ H = S 0 • • • S 2k . In this case tgt(ρ) ∈ S 2k (P 2 .(b)) and thus ρ H ends in a losing state and f H is not winning.

-or ρ H = S 0 • • • S 2k+1 and again tgt(ρ) ∈ S 2k+1 and ρ H is losing and f is not winning.

This contradicts the assumption that f H is winning.

This concludes the proof of the Only If part.

If Part.

Let w be a run of G H ending in W 1 -state. If w does not contain any u action, there is a run ρ ∈ Runs 1 (G) s.t. tr(ρ) = tr(w) by construction of G H (Definition 5.8). We let f H (w) = f (ρ).

If w = S 0 • • • S k u⊥ 1 , we let f H (w) = f H (S 0 • • • S k ).
f H is well defined as if ρ, ρ ′ are such that tr(ρ) = tr(ρ ′ ) then f (ρ) = f (ρ ′ ) because f is trace-based. f H is winning. To prove this we use the following lemma:

Lemma A.2. Let w = S 0 σ 0 S k be a run in Out(G H , f H ). Then one of two following conditions hold:

D 1 : S k ∈ {⊥ 1 , ⊥ 2 }
and there is a run q 0 0 • • • q in Out(G, f ) such that either (i) with q ∈ F or (ii) f (q 0 0 • • • q) = σ and σ ∈ Enabled(q); D 2 : S i ∈ {⊥ 1 , ⊥ 2 } for 0 ≤ i ≤ k and for any q ∈ S k , there is a run ρ = q 0 0 • • • q in Out(G, f ) s.t. tr(ρ) = tr(w).

Proof:

We prove Lemma A.2 by induction of the number of Player 1 moves in w. If w contains 0 moves clearly it holds.

Assume w is a run of Out(G H , f H ) that contains k + 1 Player 1 moves. There are two possible forms for w:

• w ends in a W 2 -state. w = S 0 σ 0 • • • S 2k σ 2k S 2k+1 . All the states S i , 0 ≤ i ≤ 2k must be different from {⊥ 1 , ⊥ 2 }. Then either S 2k+1 = ⊥ 2 or not.

-if S 2k+1 = ⊥ 2 , there is some state q ∈ S 2k s.t. σ 2k ∈ Enabled(q) by definition of G H . We can apply the induction assumption on the run w ′ = S 0 σ 0 • • • S 2k that contains k Player 1 moves. This leads: there is a run ρ ′ = q 0 0 • • • q in Out(G, f ) s.t. tr(ρ ′ ) = tr(w ′ ) (because w ′ does not contain any ⊥ 1,2 state). Moreover f (ρ ′ ) = f (w ′ ) = σ 2k , σ 2k ∈ Enabled(q) and and thus condition D 1 .(ii) holds for w.

-otherwise S 2k+1 = ⊥ 2 . By definition of G H , this implies that S 2k+1 = Next 1 (S 2k , σ 2k ). For any q ∈ S 2k+1 there is some q ′ ∈ S 2k s.t. q ′ σ 2k --→ q in G H . We can again apply the induction assumption on the run w ′ = S 0 σ 0 • • • S 2k that contains k Player 1 moves. This leads: there is a run ρ ′ = q 0 0 • • • q ′ in Out(G, f ) s.t. tr(ρ ′ ) = tr(w ′ ) and f (ρ ′ ) = f (w ′ ) = σ 2k . Hence ρ = ρ ′ σ 2k --→ q is a run of Out(G, f ) and tr(ρ) = tr(w). w satisfies D 2 .

• w ends in a W 1 -state. Let w = S 0 σ 0 • • • S 2k S 2k+1 λ 2k+1 S 2(k+1) . It must be the case that S 2k+1 = ⊥ 2 . Two cases arise:

1. λ 2k+1 = u. By definition of G H , S 2(k+1) = Next 2 (S 2k+1 , λ 2k+1 ). Let q ∈ S 2(k+1) . By definition of Next 2 , there is a state q ′ ∈ S 2k+1 s.t.

q ′ τ -→ • • • λ 2k+1
---→ q. As in the previous case for any q ′ ∈ S 2k+1 we can build a run ρ ′ = q 0 0 • • • q ′ in Out(G, f ) with tr(ρ ′ ) = tr(S 0 • • • S 2k+1 ). Hence ρ = ρ ′ λ 2k+1 ---→ q is a run of Out(G, f ) and satisfies D 2 .

2. λ 2k+1 = u. In this case S 2(k+1) = ⊥ 1 . This mean that there is a state q ′ ∈ S 2k+1 s.t. q ′ τ -→ • • • τ -→ q and q ∈ F . Again we can build a run ρ ′ = q 0 0 • • • q ′ in Out(G, f ) with tr(ρ ′ ) = tr(S 0 • • • S 2k+1 ) and clearly ρ = ρ ′ τ -→ • • • τ -→ q is run of Out(G, f ) and thus w satisfies D 1 .(i).

Figure 1 .

 1 Figure 1. The automaton M.

Figure 4 .

 4 Figure 4. The automaton E.

  However, a positive answer to Problem 2(A) does not necessarily imply a positive answer to Problem 1(A), as shown by the example that follows.

Example 4 . 1 .

 41 Consider again the automaton A of Fig. 2. Let M (a) = M (b) = 1.

Theorem 4 . 1 .

 41 Problem 2 is NP-complete.

Figure 6 .

 6 Figure 6. The automaton B.

Example 5 . 2 .L(0) = {a} 1 L( 1 ) = {b} 2 LFigure 7 .

 521127 Figure 7. A finite-state observer Obs.

Fig. 6 and

 6 Fig. 6 and B generates f.a.b, Obs will have as input π /Σ (f.a.b) = a.b with Σ = {a, b}. Consequently the observation of Obs is Obs(π /Σ (f.a.b)) = a.b.

Figure 8 . 7 .

 87 Figure 8. The product A ⊗ Obs of the automaton of Fig. 2 and the observer of Fig. 7.

Problem 7 .

 7 (Trace-Based Control Problem) INPUT: a game G, a safety objective F . PROBLEM: Is there a trace-based winning strategy for (G, F ) ?

Figure 9 .

 9 Figure 9. Game reduction for problem 5.

Theorem 5 . 5 .

 55 Let O be an observer s.t. A is (O, k)-diagnosable. Then f (O) is a trace-based winning strategy in G A .

Lemma 5 . 3 .

 53 O(f ) is an observer.

  linear in the size of k, and exponential in the size of Σ i.e., |G A | = O(|A| 2 × 2 |Σ| × |k|). This means that computing F A can be done in exponential time in the size of A and k and doubly exponential time in the size of Σ.

Figure 10 .

 10 Figure 10. Most permissive observer for the automaton A of Fig. 2.

Fig. 2 Figure 11 .

 211 Figure 11. Most permissive dynamic diagnoser D A .

Cost 2

 2 (w) = i=n i=0 |L(δ(s 0 , w(i)))| n + 1 with n = |w|. Using the observer of Fig. 12, we obtain Cost 2 (b n .a) = n+1+0 n+2 = n+1 n+2 . And by simple arithmetic, it is true that Cost 2 (b n .a) < Cost 2 (b n+1 .a).

Figure 12 .

 12 Figure 12. The Finite-State Observer Obs.

Cost 2 (

 2 A, Obs) = lim sup n→∞ Cost 2 (n, A, Obs).

  e i ) ≥ ν and Player 2 has a strategy to ensure that lim sup n→∞ 1 n n i=1 w(e i ) ≤ ν; this value can be computed in O(|V | 3 × |E| × W ) where W is the range of the weight function (assuming the weights are in the interval [-W..W ]). Note that deciding whether this value satisfies ν ⊲⊳ c for ⊲⊳∈ {=, <, >} for c ∈ Q can be done in O(|V | 2 × |E| × W ).

Figure 15 .

 15 Figure 15. The Automaton F + A .

Theorem 6 . 3 .Theorem 6 . 4 .

 6364 Problem 8 can be solved in time O(|Σ| × m × 2 n 2 × 2 k × 2 2 |Σ| ).We can even solve the optimal cost computation problem: Problem 9. (Optimal Cost Observer)INPUT: Plant model A = (Q, q 0 , Σ τ,f , δ), k ∈ N. PROBLEM: Compute the least value m s.t. there exists an observer Obs s.t. A is (Obs,k)-diagnosable and Cost 2 (Obs) ≤ m. Problem 9 can be solved in time O(|Σ| × m × 2 n 2 × 2 k × 2 2 |Σ| ).

  ) , the set Next 2 (S 2k+1 , λ 2k+1 ) is not empty and thus= S 0 • • • S 2k σ 2k S 2k+1 λ 2k+1 S 2(k+1) is in Out(G H , f H ) and S 2(k+1) = ⊥ 2 . f H (S 0 • • • σ 2k S 2k+1 λ 2k+1 S 2(k+1) ) = f (q 0 0 • • • q 0 2(k+1) ) by definition of f and S 0 σ 0 • • • σ 2k S 2(k+1) = β(tr(q 0 0 σ 0 • • • q 0 2(k+1))). Two cases arise:1. either S 2(k+1)σ 2(k+1) ----→ ⊥ 2 : in this case ρ H = S 0 • • • S 2k • • • λ 2k+1 S 2(k+1) σ 2(k+1) ⊥ 2 and ρ H ∈ Out(G H , f H ) and satisfies P 1 and P 2 .(a); 2. or S 2(k+1) σ 2(k+1)

S 2 (

 2 k+1)+1 u -→ ⊥ 1 is in ∆ and ρ H = S 0 • • • S 2(k+1) σ 2(k+1) S 2(k+1)+1 u⊥ 1 is in Out(G H , f H ).ρ H satisfies P 1 and P 2 .(a); (b) or q j 2(k+1)+1 ∈ F for 1 ≤ j ≤ n 2(k+1)+1 and in this case ρ H = S 0 • • • S 2(k+1) σ 2(k+1) S 2(k+1)+1 is in Out(G H , f H ) and satisfies P 1 and P 2 .(b).

Lemma 3.1. Let

  the synchronized product of A 1 and A 2 : synchronization happens on common actions except τ , i.e., actions in Σ and otherwise interleaving (Cf. section 2.4). → 1,2 stands for the transition relation of A 1 × A 2 . We assume we have a predicate A 1 Move (resp. A 2 Move) on transitions of A 1 × A 2 which is true when A 1 (resp. A 2 ) participates in an A 1 × A 2 transition (i.e., A 1 Move(t) is true for all transitions except τ transitions taken by A 2 ). For a run ρ ∈ Runs(A 1 × A 2 ) we let ρ |1 , be the run of A 1 defined by the sequence of A 1 Move transitions of ρ and ρ |2 be the sequence of A 2 Move moves. Notice that π /Σ (tr(ρ |1 )) = π /Σ (tr(ρ |2 )) by definition of A 1 × A 2 . Let Runs ≥k (A 1 × A 2 )be the set of runs in A 1 × A 2 s.t. a (faulty) state ((q 1 , 1), q 2 ) is followed by at least k A 1 -actions. Then we have the following lemmas:ρ ∈ Runs ≥k (A 1 × A 2 ). Then ρ |1 ∈ Faulty ≥k (A) and ρ |2 ∈ NonFaulty(A). Moreover π /Σ (tr(ρ |1 )) = π /Σ (tr(ρ |2 )). Let ρ 1 ∈ Faulty ≥k (A) and ρ 2 ∈ NonFaulty(A) s.t. π /Σ (tr(ρ 1 )) = π /Σ (tr(ρ 2 )). Then there is some ρ ∈ Runs ≥k (A 1 × A 2 ) s.t. ρ |1 = ρ 1 and ρ |2 = ρ 2 . By definition of A 1 × A 2 ,it suffices to notice that a run in Runs ≥k (A 1 × A 2 ) can be split into a run of A 1 and a run of A 2 having the same projection on Σ.⊓ ⊔We can define an automaton B which is an extended version of A 1 × A 2 : we add a boolean variable z that is set to 0 in the initial state of B. An extended state of B is a pair (s, z) with s a state of A 1 × A 2 . Whenever A 1 participates in an A 1 × A 2 -action, z is set to 1, and when only A 2 makes a move in A 1 × A 2 , z is set 0. We denote -→ B the new transition relation between extended states;

	Lemma 3.2. Proof:
	(s, z)

σ

--→ B (s ′ , z ′ ) if there is a transition t : s σ --→ 1,2 s ′ , and

  F H is the set of safe states for G H . ⊥ 1 and ⊥ 2 are not safe states. (G H , F H ) is a safety game as well. Notice also that G H is a full-observation turn-based two-player game in which the moves of the two players alternate. To solve Problem 7 we can first solve the game (G H , F H ). This can be done in linear time in the size of (G H , F H ). From this obtain obtain an algorithm for Problem 7 i.e., compute the set of winning states of G H . As the size of G H is exponential in the size G: Indeed, to solve Problem 7, we compute the set of winning states W H of (G H , F H ) and check that the initial state of G H is winning. For safety games like G

	Theorem 5.3. Problem 7 is in EXPTIME.

H , with full observation, we can also compute the most permissive strategy as emphasised earlier. Given G H and F H let F H be the most permissive strategy. This memoryless (state-based) strategy is given

  page 7, F = {1, 2, 3} × {1}. Let det( Ã) be the determinization of Ã. A state S = {s 1 , s 2 , • • • , s n } in det( Ã) is final if every state s i is final in Ã.

  1 , ⊥ 2 }; in this case ρ ′ H cannot be extended in G H and thus ρ H = ρ ′ H and ρ H satisfies P 1 and P 2 .(a); -or P 2 .(b) holds and ρ ′ H does not contain any state in {⊥ 1 , ⊥ 2 }; Then ρ ′ H = S 0 • • • S 2k σ 2k S 2k+1 satisfies P 1 and P 2 .(b) and we have in particular q 0 2k ∈ S 2k and q 1 2k+1 ∈ S 2k+1 . Because q 1

Different types of faults could also be considered, by having different fault events f1, f2, and so on. Our methods can be extended in a straightforward way to deal with multiple faults. We restrict our presentation to a single fault event for the sake of simplicity. Also note that f is assumed to be unobservable. In the case where f can be directly observed, the task of fault diagnosis becomes trivial, since it suffices to report f as soon as it is observed.

Actually it amounts to computing the maximum number of A1-actions following a faulty state in A1 × A2. This can be done using a depth-first search algorithm and a tag on each faulty state s that gives the maximal number of A1-actions following s.

Notice that knowing n0 does not imply we know the required set of observable events Σo. We can find (one of the possibly many) Σo by searching over all possible subsets Σo ⊆ Σ of size n0 (there are C(|Σ|, n0) such combinations) and check for each such Σo whether A is Σo-diagnosable, using the methods described in section 3.1.

When a run can be uniquely defined by its sequence of actions, we omit the intermediate states and we can use the trace to characterize the run.

Note that automaton B of Fig.

6, although looking very similar to A, is not (M, 1)-diagnosable.

We write (S, s0, Σ, δ, L) instead of ((S, s0, Σ, δ, S, ∅), L).

We use ⊗ to clearly distinguish this product from the synchronous product ×.

Notice that this also shows that existence of an observer implies existence of a finite-state observer, since the trivial observer is finite-state.

In the sequel we assume that the game objectives are states sequences and do not refer to the labels of the transitions.

Notice that by definition of Cpre, Player 1 cannot win by refusing to play.

According to Definition 5.5, it is not a strategy as it prescribes a set of moves for a given state instead of one move.

Even if F is not strictly speaking a strategy, the trace-based property extends to sets of moves with set equality.

Acknowledgments

We would like to thank Karine Altisen for her contribution during earlier phases of this work. We would also like to thank the anonymous reviewers for their careful reading, helpful comments and pointers to related work.

* Preliminary versions of parts of this paper appeared in [2] and [1]. † Work supported by the French Government under grant ANR-SETI-06-003.

Theorem 6.2. Computing the cost of (A, Obs) is in P.

Proof:

The size of A + × Obs + is polynomial in the size of A and Obs.

⊓ ⊔ Remark 6.1. Notice that instead of the values |L(s)| we could use any mapping from states of Obs to Z and consider that the cost of observing {a, b} is less than observing a.

Example 6.1. We give the results for the computation of the cost of two observers for the DES A given in Fig. 2. Let O 1 be the most powerful observer that observes {a, b} at each step, and O 2 be the observer given in Fig. 7.

The automata A + ×O + 1 and A + ×O + 2 are given in Fig. 13 and Fig. 14. The weight function is pictured above each state. Notice that to compute ν * (A + × O + i ) we do not need the labels of the transitions as we are dealing with weighted graphs: if two transitions (s, a, s ′ ) and (s, b, s ′ ) are in A + × O + i we only need one of them. For instance in Fig. 13 one of the transitions (0, a, 4) and (0, b, 4) is redundant. The values D k (v) and min(v) for each state v of A + × O + i are given in Table 1 and Table 2. The maximum meanweight value ν * is the maximum value max v min(v) for v ranging over the set of states of

Optimal Dynamic Diagnosers

In this section, we focus on the problem of computing a best observer in the sense that diagnosing the DES with it has minimal cost. We address the following problem: . If the answer to (A) is "yes", compute a witness observer Obs, that satisfies Cost 2 (Obs) ≤ c.

Theorem 5.7, page 28 establishes that there is a most permissive observer F A in case A is (Σ, k)diagnosable and it can be computed in exponential time in the size of A and k, doubly exponential time in |Σ|, and has size exponential in A and k, and doubly exponential in |Σ|. Moreover the most permissive observer F A can be represented by a finite state machine

δ) which has the following properties:

• even states are states where the observer chooses a set of events to observe;

• odd states (2i + 1, X) are states where the observer waits for an observable event in X to occur;

it means that from an even state 2i, the automaton S F A can select a set X of events to observe. The successor state is an odd state together with the set X of events that are being observed;

• if δ((2i + 1, X), a) = 2i ′ with a ∈ X, it means that from (2i + 1, X), S F A is waiting for an observable event to occur. When some occurs it switches to an even state.

By definition of F A , any observer O s.t. A is (O, k)-diagnosable must select a set of observable events in F A (tr(w)) after having observed w ∈ π /Σ (L(A)).

To compute an optimal observer, we use a result by Zwick and Paterson [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF] on weighted graph games. The next subsection summarizes the results we are going to use.

Zwick and Paterson's Algorithm Definition 6.4. (Weighted Graph)

A weighted directed graph is a pair (G, w) s.t. G = (V, E) is a directed graph and w :

assigns an integral weight to each edge of G with W ∈ N. We assume that each vertex v ∈ V is reachable from a unique source vertex v 0 and has at least one outgoing transition.

Definition 6.5. (Weighted Graph Game) A weighted graph game

Vertices V i are Player i's vertices. A weighted graph game is a turn based game in which the turn alternates between Player 1 and Player 2. The game starts at a vertex v 0 ∈ V 1 . Player 1 chooses an edge e 1 = (v 0 , v 1 ) and then Player 2 chooses an edge e 2 = (v 1 , v 2 ) and so on and they build an infinite sequence of edges. Player 1 wants to maximise lim inf n→∞

A. Proof of Theorem 5.2

The following fact holds for G H : f is also winning. To prove this we use the following Lemma: Given ρ a run of Out(G, f ), we can build a run ρ H = S 0 σ 0 • • • S nρ in G H , such that ρ H is the longest run that can match ρ. It is defined as follows:

Lemma A.1. This run ρ H is in Out(G H , f H ) and has the properties:

2i ∈ S 2i and for 1 ≤ 2i + 1 < n ρ , q 1 2i+1 ∈ S 2i+1 ; P 2 : either (a) tgt(ρ H ) = S nρ ∈ {⊥ 1 , ⊥ 2 } or (b) if n ρ = 2k, q 0 2k ∈ S nρ , and if n ρ = 2k + 1, q 1 2k+1 ∈ S nρ .

Proof:

We prove properties Lemma A.1 by induction on the number of Player 1 moves in ρ. Assume k = 0. Clearly the run ρ H = {q 0 0 } is in Out(G H , f H ) and Lemma A.1 holds. Assume the property holds for k Player 1 moves. Let ρ be a run with k + 1 Player 1 moves σ 0 , σ 2 , • • • , σ 2k . We write

2k+1 . ρ ′ has k -1 Player 1 moves and by induction hypothesis on ρ ′ , we obtain:

This completes the proof of Lemma A.2.

⊓ ⊔

Now assume f H is not winning. There is a run S 0 • • • S k in Out(G H , f H ) such that either (i) S k ∈ {⊥ 1 , ⊥ 2 } or (ii) there is some q ∈ S k such that q ∈ F . Applying Lemma A.2 we obtain:

• if (i) holds, D 1 holds and there is a run ρ ∈ Out(G, f ) s.t. either (a) tgt(ρ) ∈ F or (b) f (ρ) ∈ Enabled(tgt(ρ)). If (a) holds f is not a winning strategy. If (b) holds f is not a strategy. In any case this contradicts the fact that f is a winning strategy.

• if (ii) holds, as S k contains a state q ∈ F , there is a run q 0 0 • • • q in Out(G, f ) and q ∈ F which again contradicts the fact that f is winning. This completes the proof of Theorem 5.2.