Karine Altisen
email: karine.altisen@imag.fr

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

Stavros Tripakis
email: stavros.tripakis@imag.fr

Verimag Laboratory

Monitoring and Fault-Diagnosis with Digital Clocks *

come

Introduction

Monitoring and Fault-Diagnosis. In this paper we study the problems of monitoring and fault diagnosis in the context of real-time systems. In both problems the objective is to synthesize an observer, that is, a device that observes a certain system (or plant) and infers some information about this system.

In the monitoring problem, we want to know whether the system satisfies a given specification. Here, the system is black-box, that is, we have no information about how the system behaves. Therefore, we cannot check that all be-haviors of the system satisfy the specification. Rather, we can observe the system during its execution and attempt to check whether the observed behavior satisfies the specification. This is the objective of the observer, which in this case is called a monitor. Our goal is to synthesize a monitor automatically from the specification.

In the fault-diagnosis problem, we have a model of the system, for instance, in the form of an (untimed or timed) automaton. We also know that the system may produce some faults. However, these faults are not directly observable, thus, their occurrence must be deduced from other observations (this can be seen as a grey-box setting). The objective of the observer, which in this case is called a diagnoser, is to detect whether a fault occurred or not, and this as soon as possible after the fault happened. In this case, before we attempt to synthesize a diagnoser, we must first check existence of a diagnoser, called diagnosability. Indeed, a diagnoser may not exist in cases where the system can produce two behaviors, one faulty and the other nonfaulty, which appear the same to an external observer.

Monitoring and fault-diagnosis have been extensively studied in "untimed" settings, for instance, where specifications and plants are given as finite automata. Then, synthesizing a monitor simply means determinizing the system (possibly after "hiding" unobservable events). Faultdiagnosis has been first introduced in [START_REF] Sampath | Diagnosability of discrete event systems[END_REF], where it was shown how to check diagnosability and, in the case it holds, synthesize a diagnoser.

More recently, these problems have also been studied in a real-time setting, where specifications and plants are given as timed automata [2]. In particular, the monitoring problem has been studied, as a special case of the conformance testing problem in [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF][START_REF] Krichen | Real-time testing with timed automata testers and coverage criteria[END_REF]. The fault-diagnosis problem has been studied in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF][START_REF] Bouyer | Fault diagnosis using timed automata[END_REF].

Implementability & Digital Clocks. Most of the above works, however, consider analog-clock observers, that is, observers that are capable of observing time as precisely as necessary. For instance, such observers can distinguish between an event occurring at time t = 1 or at time t > 1. Analog-clock observers are not implementable, since the above distinction cannot be made by any real clock. Indeed, real clocks are digital: they are counters that are updated by some physical process. These counter can be consulted (i.e., read) by the monitor. It is also possible to configure the clock so as to send an event (e.g., an interrupt) to the program at every "tick".

Our Contributions. In this paper, we study the monitoring and fault-diagnosis problems in the case where observers only have access to digital clocks. The architecture we consider is shown in Figure 1. The observer can be seen as an untimed "machine" reacting to discrete events produced by the plant and the discrete event "tick" produced by the digital clock.

In the monitoring problem, the specification is given as a timed automaton A over some alphabet Σ. The monitor observes a subset Σ o ⊆ Σ. The digital clock is modeled as a timed automaton A DC over the event tick. The objective is to synthesize a monitor which is sound and optimal. Soundness means intuitively that the monitor should not reject behaviors that are conforming to the specification. We show that care must be taken when formally defining this notion.

Optimality means that the monitor is as precise as possible, that is, does not accept behaviors that are nonconforming, except when it cannot do otherwise. Indeed, the digital-clock monitor cannot be "perfect" in the sense that it accepts precisely L(A) (the timed language of A). This is because digital clocks are less precise than analog clocks. Thus, two distinct timed behaviors ρ and ρ ′ may appear the same to the monitor: if ρ is conforming and ρ ′ is non-conforming, a sound monitor has no choice but accepting both. On the other hand, the monitor should not be trivial (i.e., accept everything). We define several notions of optimality and show how to synthesize automatically optimal monitors for each of these notions.

In the fault-diagnosis problem, the plant is given as a timed automaton A over Σ o ∪{τ, f }. Σ o models the observable events, τ the unobservable events, and f the (unobservable) fault. We consider three problems: (1) given plant A, digital clock A DC and time bound ∆, check whether there is a diagnoser that can detect any fault within ∆ time units;

(2) given A and A DC check whether there is a diagnoser for some ∆; (3) given A, check whether there is a diagnoser for some digital clock A DC and some ∆. We show how to solve problems (1) and (2). Problem ( 3) is open. However, we give an example that shows that existence of an analogclock diagnoser does not imply existence of a digital-clock diagnoser, and this for any digital-clock, no matter how precise it is. We also provide a sufficient (but not necessary) condition for existence of a digital-clock diagnoser.

Related Work.

The distinction between analog and digital clocks has been made in [START_REF] Henzinger | What good are digital clocks?[END_REF] and subsequent work on digitization of timed automata. Digitization studies how the "sampling" semantics of timed automata (that is, the semantics where only particular time delays are allowed, e.g., multiples of 1 n ) are related to its dense-time semantics. Although related, this is not the same as our problem, where we study the observational capabilities of digital-clocks.

Digital clocks have been used for monitoring and testing in [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF][START_REF] Bensalem | Testing conformance of real-time applications by automatic generation of observers[END_REF]. We borrow from these works the idea to model digital clocks as timed automata. Soundness and optimality of monitors is not considered in these works, neither are the problems of fault-diagnosis and synthesis of digital clocks. Finally, digital clocks have been also used in [START_REF] Altisen | Implementation of timed automata: an issue of semantics or modeling? In Formal and Analysis of Timed Systems[END_REF] in the context of timed automata implementation.

Fault diagnosis with digital clocks has recently been considered independently in [START_REF] Jiang | Diagnosis of dense-time systems using digital clocks[END_REF]. This work is restricted in several ways compared to ours. First, it only considers digital clocks that "tick" every [∆ ± δ] time units. In our framework digital clocks are modeled as timed automata, which can capture the above clocks and more (see Figure 2). Second, in [START_REF] Jiang | Diagnosis of dense-time systems using digital clocks[END_REF] the non-faulty behavior of the plant is modeled as a deterministic timed automaton, whereas we allow the plant to be non-deterministic (we also allow unobservable events other than faults). Finally, the synthesis of a digital clock (problem (3) above) is not considered in [START_REF] Jiang | Diagnosis of dense-time systems using digital clocks[END_REF].

Outline of the paper. In section 2, we recall the basic definitions of timed words, timed automata and monitors and diagnosers. In section 3, we study digital-clock monitoring. Section 4 is devoted to digital-clock fault-diagnosis. Section 5 concludes the paper.

Preliminaries

Clock constraints, timed words

Let N be the set of natural numbers, Z the set of integers, Q the set of rationals and R the set of non-negative reals.

Let X be a set of variables taking values in R. In the context of timed automata, a variable in X is called a clock. An atomic clock constraint over X is an expression of the form x#c, where x ∈ X, c is a rational constant and # ∈ {<, ≤, =, ≥, >}. A convex clock constraint over X is a conjunction of atomic clock constraints over X. A clock constraint over X is a boolean expression of atomic clock constraints over X. A valuation over X is a function v : X → R, assigning to each clock a value. Given r ⊆ X, v[r := 0] denotes the valuation v ′ such that for all x ∈ r, v ′ (x) = 0 and for all y ∈ Xr, v ′ (y) = v(y). 0 denotes the valuation assigning zero to each clock. A valuation v satisfies a clock constraint g, written v |= g, if substituting v(x) for every x appearing in g yields a valid constraint.

Let Σ be a finite alphabet. A timed word over Σ is a finite sequence of delays in R and letters in Σ: ρ ∈ (Σ ∪ R) * . Every such sequence can be put in a canonical form by summing up consecutive delays and adding initial and final zero delays if necessary:

ρ = t 0 • a 1 • t 1 • a 2 • t 2 • • • a n • t n .
We will define a set of projection functions on timed words. The first can be seen as a projection onto R: Time(ρ) denotes the total amount of time spent in ρ, that is, Time(ρ) = i=0,...,n t n . The second is the untiming projection: Unt(ρ) ∈ Σ * is the sequence of letters a 1 • • • a n . Conversely, given a sequence of letters

a 1 • • • a n , Unt -1 (a 1 • • • a n ) is the set of timed words t 0 .a 1 .t 1 . • • • .a n .t n with t i ∈ R. Finally, given Σ ′ ⊆ Σ, Π Σ ′ (ρ)
is the timed word over Σ ′ obtained from ρ by erasing all events not in Σ ′ . For example, if Σ = {a, b},

Σ ′ = {a} and ρ = 1 • a • 2 • b • 1 • b then Π Σ ′ (ρ) = 1 • a • 3.
Projections Unt and Π can be naturally extended to sets of timed words in the usual way.

Given two timed words

ρ 1 ∈ (Σ 1 ∪ R) * and ρ 2 ∈ (Σ 2 ∪ R) * ) the parallel composition ρ 1 ||ρ 2 is the set of words ρ ∈ (Σ 1 ∪ Σ 2 ∪ R) * s.t. Π Σ1 (ρ) = ρ 1 and Π Σ2 (ρ) = ρ 2 .
L 1 ⊆ (Σ 1 ∪ R) * and L 2 ⊆ (Σ 2 ∪ R) * , the parallel compo- sition of L 1 and L 2 is L 1 ||L 2 = {ρ 1 ||ρ 2 |ρ i ∈ L i }.

Timed automata

Let Σ be a finite alphabet. A timed automaton over Σ is a tuple A = (Σ, Q, Q 0 , Q f , X, I, E), where:

• Q is a finite set of locations, Q 0 ⊆ Q is the set of initial locations and Q f ⊆ Q is the set of final locations.
• X is a finite set of clocks.

• I is the invariant function, associating to each location q ∈ Q a clock constraint over X. We assume that 0 ∈ I(q 0 ) for all q 0 ∈ Q 0 .

• E is a finite set of edges. Each edge is a tuple (q, q ′ , a, g, r), where q and q ′ are the source and destination locations, a ∈ Σ is the label of the edge, g is a clock constraint over X, called the guard of the edge, and r ⊆ X is the set of clocks to reset to zero when the edge is crossed.

A state of A is a pair (q, v), where q ∈ Q and v is a valuation over X such that v |= I(q). The set of initial states of

A is S 0 = {(q 0 , 0) | q 0 ∈ Q 0 }. The set of final states of A is S f = {(q f , v) | q f ∈ Q f }. Let S A denote the set of all states of A.
A discrete transition of A is a triple (s, a, s ′ ), where s, s ′ ∈ S A and a ∈ Σ, such that: s = (q, v), s ′ = (q ′ , v ′ ) and there is an edge e = (q, q ′ , a, g, r

) ∈ E, such that v |= g and v ′ = v[r := 0]. If such a transition exists we write s a → s ′ . A time transition of A is a triple (s, t, s ′ ), where s, s ′ ∈ S A and t ∈ R, such that: s = (q, v), s ′ = (q, v + t) and for all 0 ≤ t ′ ≤ t, v + t ′ ∈ I(q). If such a transition exists we write s t → s ′ . Notice that for all states s ∈ S A , s 0 → s. A run of A is a finite sequence of transitions: σ = s 0 t0 → s 1 a1 → s ′ 1 t1 → • • • an → s ′ n tn → s n+1
, where n ≥ 0. We say that the run starts from state s 0 and reaches state s n+1 . If s 0 ∈ S 0 then we say that the state s n+1 is a reachable state. The set of all reachable states of A is denoted R A .

Every run like the one above has a corresponding timed word, namely, t 0 a 1 t 1 • • • a n t n . We denote by tw(σ) the timed word corresponding to run σ. If s 0 ∈ S 0 and s n+1 ∈ S f then the run is accepting and the corresponding timed word is accepted by A. The set of all timed words accepted by A is the (timed) language of A, denoted L(A). The untimed language of A, denoted Unt(A) is Unt(L(A)).

A state s of A is called non-Zeno if for all t ∈ R there exists a run σ starting at s such that Time(tw(σ)) ≥ t. A is called non-Zeno if all its reachable states are non-Zeno. Non-Zenoness means that A cannot "block time". Note that this does not mean that all runs of A let time progress (i.e., are non-Zeno) but rather that there is always the possibility of letting time progress.

Given two timed automata

A 1 = (Σ 1 , Q 1 , Q 0 1 , Q f 1 , X 1 , I 1 , E 1 ) and A 2 = (Σ 2 , Q 2 , Q 0 2 , Q f 2 , X 2 , I 2 , E 2 ), the par- allel composition of A 1 and A 2 denoted A 1 ||A 2 , is the timed automaton A = (Σ, Q, Q 0 , Q f , X, I, E) defined as follows 1 : • Σ = Σ 1 ∪ Σ 2 .
1 We assume neither Σ 1 nor Σ 2 contains the silent action τ .

• Q = Q 1 × Q 2 , Q 0 = Q 0 1 × Q 0 2 and Q f = Q f 1 × Q f 2 . • X = X 1 ∪ X 2 .
• I(q 1 , q 2 ) = I(q 1 ) ∧ I(q 2 ).

• E contains the following transitions:

-For each a ∈ Σ 1 ∩ Σ 2 , if (q 1 , q ′ 1 , a, g 1 , r 1 ) ∈ E 1 and (q 2 , q ′ 2 , a, g 2 , r 2 ) ∈ E 2 then e = ((q 1 , q 2 ), (q ′ 1 , q ′ 2 ), a, g 1 ∧ g 2 , r 1 ∪ r 2 ) ∈ E. That is, the two automata synchronize on Σ 1 ∩ Σ 2 . -For each a ∈ Σ 1 \ Σ 2 , if (q 1 , q ′ 1 , a, g 1 , r 1 ) ∈ E 1 then e = ((q 1 , q 2 ), (q ′ 1 , q 2 ), a, g 1 , r 1 ) ∈ E. -For each a ∈ Σ 2 \ Σ 1 , if (q 2 , q ′ 2 , a, g 2 , r 2 ) ∈ E 2 then e = ((q 1 , q 2 ), (q 1 , q ′ 2 ), a, g 2 , r 2 ) ∈ E. It can be checked that L(A 1 ||A 2 ) = L(A 1 )||L(A 2 ).

Monitoring

Digital-clock automata: models of digital clocks

A digital-clock automaton (DC-automaton for short)

A is a non-Zeno timed automaton ({tick}, Q, Q 0 , Q f = Q, X, I, E).
The tick event is a special event representing one "tick" of the digital clock.

The idea of using timed automata to model digital clocks has been introduced in [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF] where it has been used for realtime testing. The idea has also been used in [START_REF] Altisen | Implementation of timed automata: an issue of semantics or modeling? In Formal and Analysis of Timed Systems[END_REF] for implementation of timed automata.

To illustrate the concept, we borrow some examples of digital-clock automata from the above works. These are shown in Figure 2. A 1 DC models a perfectly periodic digital clock with period 1. A 2 DC (ǫ) is an automaton parameterized by ǫ, and models a clock with non-perfect period 1 ± ǫ. In this model errors may accumulate, so that the i-th tick of the clock may occur anywhere in the interval

[(1 -ǫ)i, (1 + ǫ)i]. A 3
DC (ǫ) models a more restricted behavior where errors do not accumulate: the i-th tick occurs in the interval [iǫ, i + ǫ], for all i.

Digital-clock monitors

Let Σ o be a finite alphabet such that tick ∈ Σ o . A digital- clock monitor over alphabet Σ o is a function D : (Σ o ∪ {tick}) * → {0, 1}. The untimed language of D is defined as Unt(D) = {π ∈ (Σ o ∪{tick}) * | D(π) = 1}. The timed language of D is defined as L(D) = Unt -1 (Unt(D)).
Digital-clock monitors accept or reject untimed words in (Σ o ∪ {tick}) * . Such words represent observations that the monitor receives during its execution. These observations are sequences of: (a) observable events received by the monitored plant; and (b) tick events received by the (digital) clock of the system (i.e., computer) where the monitor executes. More precisely, if ρ is a timed behavior generated by the system under observation, and if σ is a timed behavior generated by the digital clock, then D receives an untimed observation in Π Σo (Unt(ρ||σ)). Indeed, ρ ′ ∈ ρ||σ is a timed behavior corresponding to some (non-deterministically chosen) interleaving of ρ and σ. π = Π Σo (Unt(ρ ′ )) is the observation received by the monitor when ρ ′ occurs: real-time delays and unobservable events are removed from ρ ′ in order to obtain π.

Soundness of digital-clock monitors

The monitor is supposed to check conformance to a specification. The latter is modeled as a timed automaton A over Σ ⊇ Σ o . A crucial property for monitors is soundness: if ρ is a behavior in L(A), then the monitor should not reject it (i.e., announce non-conformance whereas the timed word is conforming). A first attempt to capture soundness for digital-clock monitors is given by the definition below. The definition can be read as follows: "if ρ is a timed word of the specification L(A), then the untimed observable version of ρ must be accepted by the digital-clock monitor D when the latter executes in parallel with the digital clock automaton A DC ". Definition 1 (A first attempt to define soundness) Given a timed automaton A, a digital-clock automaton A DC and a monitor D, the predicate sound 1 (A, A DC , D) holds iff:

Π Σo (L(A)) ⊆ Π Σo (L(D)||L(A DC )) (1)
This definition is not satisfactory as demonstrated by the following example:

Example 1 Let Σ o = Σ = {a}, L(A) = {2 • a • t | t ∈ R} (i.e.,
. Indeed, L(D) = {t 1 • tick • t 2 • a • t 3 | t i ∈ R}. Thus, L(D)||L(A DC ) = {t 1 • tick • t 2 • a • t 3 | t 1 ∈ {1, 3}, t 2 , t 3 ∈ R} and Π Σo (L(D)||L(A DC )) = {t 1 • t 2 • a • t 3 | t 1 ∈ {1, 3}, t 2 , t 3 ∈ R} = {t 1 • a • t 2 | t 1 ≥ 1, t 2 ∈ R}. (i.e.
, a occurs at some point later than time 1). Therefore, we have

Π Σo (L(A)) ⊆ Π Σo (L(D)||L(A DC ))
, as required by predicate sound 1 . However, the above monitor does not conform to our intuition of soundness (page 4). Indeed, consider the timed word of A DC , ρ ADC = 3 • tick. Executed together with the only timed word of A, ρ = 2 • a, this produces the the untimed digital observation Π Σo (Unt(ρ||ρ ADC )) = {a • tick}. The monitor D rejects it whereas it should have accepted it if it were "sound" as stated p. 4. Note also that Actually the definition of sound 1 captures the following fact: whenever a timed word ρ is in L(A), there is a behavior of A DC that generates tick so that the digital monitor will accept the untimed digital behavior. This means that if we have a timed automaton A DC that generates a unique timed word, sound 1 would be sufficient. But of course, we want to model non deterministic and drifting clocks and the previous definition is not what we are looking for. We want our digital monitor to be robust against the disturbances generated by the digital clock, i.e. that for any of its timed words, the monitor has a constant answer (in case of acceptance). To remedy this problem, we provide a robust definition of soundness.

• x ≤ 1 A 1 DC tick x = 1 x := 0 • x ≤ 1 + ǫ A 2 DC (ǫ) tick 1 -ǫ ≤ x ≤ 1 + ǫ x := 0 • x ≤ 1 A 3 DC (ǫ) • x ≤ 1 • x ≤ ǫ tick 1 -ǫ ≤ x ≤ 1 ε ; x = 1 ; x := 0 tick 0 ≤ x ≤ ǫ ε ; x = 1 ; x := 0
Definition 2 (Robust definition of soundness) Given a timed automaton A, a digital-clock automaton A DC and a monitor D, the predicate sound(A, A DC , D) holds iff:

∀ρ ∈ L(A).∀ρ ′ ∈ L(A DC ).Π Σo (Unt(ρ||ρ ′ )) ⊆ Unt(D)
This definition states precisely what we want, namely, that for any behavior ρ which conforms to the specification A, and for any possible behavior ρ ′ of the digital clock, the monitor D will accept any observation resulting from these two behaviors. It can be shown that sound is strictly stronger than sound 1 . The following results are immediate consequences of Definition 2: the first one states that if a monitor is sound for a certain digital-clock then it remains sound for a "more deterministic" digital-clock; the second one that a sound monitor should at least accept the untimed language of the product of A and A DC .

Proposition 1 For any timed automaton A, for any digitalclock automaton

Lemma 1 For any timed automaton A and digital-clock automata A 1

DC and A 2 DC , and for any monitor D

sound(A, A 1 DC , D) ∧ L(A 2 DC ) ⊆ L(A 1 DC ) ⇒ sound(A, A 2 DC , D).
Lemma 2 Let D be such that sound(A, A DC , D). Then Π Σo (Unt(L(A||A DC ))) ⊆ Unt(D).

Now that we have a definition of sound digital-clock monitors, it appears straightforward to define the following monitoring problem.

(First definition of a monitoring problem) Given a timed automaton A and a digital-clock automaton

A DC , synthesize a monitor D such that sound(A, A DC , D). This problem, however, has a trivial solution, namely, the monitor that accepts all behaviors: D(σ) = 1 for all σ. Therefore, we need to find some way to exclude such trivial monitors. We do this by introducing, in the section that follows, orders that allow us to speak of "better" or "worse" monitors, and also to synthesize optimal monitors w.r.t. those orders.

Orders on monitors

Our aim is to synthesize "optimal" monitors. For this, we need to introduce an order which captures that a monitor is "better" than another monitor. We explore some possible orders in this section.

A first possible choice is to compare the languages accepted by the monitors using standard subset relation. Given two monitors D and D ′ ,

D ⊆ D ′ ≡ Unt(D) ⊆ Unt(D ′ ).
Notice that this order is independent of the "application" in question, namely, the specification A and the digital clock A DC We proceed by defining an alternative order which depends on A and A DC .

We define D ≤ A,ADC D ′ iff for any ρ ∈ L(A) and any σ ∈ L(A DC ), we have

Π Σo (Unt(ρ||σ)) ∩ Unt(D ′ ) = ∅ ⇒ Π Σo (Unt(ρ||σ)) ∩ Unt(D) = ∅
The above formula states that an observation rejected by D ′ is also rejected by D, provided this observation can be generated by some behavior ρ of A and some behavior σ of A DC .

It can be easily shown that if D ⊆ D ′ then for any A and A DC , D ≤ A,ADC D ′ . Definition 3 (Minimal and optimal monitors) Let D be a class of monitors and let ≺ be a partial order on D. A monitor D ∈ D is said to be minimal in the class D with respect to order ≺ if it is a minimal element of (D, ≺). D is called optimal if it is the (unique) least element of (D, ≺).

Problem 2 (Optimal digital-clock monitoring problem) Given a timed automaton A, a digital-clock automaton

A DC , and ≺∈ {⊆, ≤ A,ADC }, check whether there exists and synthesize a monitor D such that sound(A, A DC , D) and D is minimal or optimal with respect to ≺.

Sound and optimal monitors

We now present a solution to the optimal digital-clock monitoring problem, namely, we show how to construct a monitor which is sound (with respect to the sound predicate) and also optimal with respect to any of the orders introduced above.

Consider a timed automaton A and a digital-clock automaton A DC . Define the automaton A 0 to be a finite state automaton that accepts the language Π Σo (Unt(A||A DC )). This automaton A 0 can be obtained in the following way:

1. Construct the parallel product A ′ = A||A DC . The final locations of A ′ are the pairs (l, l ′ ) with l a final location of A.

2. Build an abstract graph A 0 that preserves the untimed language of A ′ . A 0 can be the region graph [2], the time-abstracting bisimulation graph [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF], or the zone graph [4, 13] of A ′ . These graphs are finite-state automata. Their transitions are labeled with letters in Σ∪{tick}. In the case of the region or time-abstracting bisimulation graphs, some transitions are labeled with ǫ, a special label denoting the passage of time. Each state of A 0 is labeled with a location of timed automaton A ′ . The final states of A 0 are the states labeled by a final location of A ′ .

3. Replace all labels in Σ -Σ o by ǫ. This gives the projection onto Σ o .

We define the digital monitor D 0 as follows: D 0 (u) = 1 iff u is accepted by A 0 . A property of the region automaton Remark 2 The automaton A 0 described above can be determinised using the usual subsets construction. This way, D 0 is just a Moore version of A 0 where the final states of A 0 are labeled with 1 and the other states with 0.

A 0 is that u ∈ L(A 0 ) ⇔ ∃ρ ∈ L(A ′ ) s.t. Π Σo (Unt(ρ)) = u.

Fault diagnosis

The fault-diagnosis2 problem has been introduced and studied in the untimed setting of discrete-event systems in [START_REF] Sampath | Diagnosability of discrete event systems[END_REF] and extended to the timed automata setting with analog-clock (i.e., infinite-precision) diagnosers in [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF].

Here, we study the problem in the timed automata setting but with digital-clock diagnosers.

Fault diagnosis is similar to monitoring. The main differences are two. First, the plant under observation is not entirely black-box. A model of the plant is available, but this model contains unobservable actions. Some of these unobservable actions model faults that may occur in the plant. The goal of the diagnoser is to detect whether a fault has occurred and, in the case where there are many different types of faults, to identify which fault occurred. The second difference with monitoring is that the diagnoser must announce a fault within a bounded, albeit unknown a-priori, delay after the fault occurred. Thus, the plant is supposed to continue execution forever, and the diagnoser's task is to detect faults if possible, and as soon as possible.

These two differences imply that, contrary to monitoring, synthesis of a diagnoser is not always possible. This is the case when the plant contains two distinct behaviors, one faulty and the other non-faulty, which produce the same observation as far as the diagnoser is concerned. Thus, the first task is to check diagnosability, that is, the existence of a diagnoser. If diagnosability holds, then a diagnoser can be synthesized.

It should then be clear that knowing how to solve the monitoring problem does not imply we can solve the diagnosis problem: the latter requires us to check diagnosability, which does not exist in monitoring. On the other hand, one might think that the monitoring problem can be reduced to the diagnosis problem, by building a plant where non-faulty behaviors correspond to the "positive" monitoring specification and faulty behaviors to its negation. A first problem with this is that it assumes we can complement the specification, which is not always possible, neither easy, for timed automata. Even when the complement is available, the above construction may yield a plant automaton with non-accepting states: this is not allowed in our diagnosis framework (see below). For the above reasons, it is justified to treat the two problems separately.

For simplicity, we are going to consider the case of a single type of faults. The results can be easily extended to the case of multiple different types of faults.

Digital-clock diagnosers

The plant is modeled as a timed automaton A over Σ = Σ o ∪ {τ, f }, where τ, f ∈ Σ o : τ models unobservable events which are not faults; f models the faults, which are also unobservable; Σ o models the observable events. We assume that all locations of A are accepting. That is, the language of A is prefix-closed. This is in accordance with the interpretation given above, namely, that the plant is expected to continue execution and the objective is to detect faults after some bounded delay.

Let ρ be a timed word in (Σ ∪ R) * . ρ is said to be nonfaulty if the letter f does not appear in ρ, that is, Π {f } (ρ) = Time(ρ). Otherwise, ρ is said to be faulty. Let ∆ ∈ N. ρ is said to be ∆-faulty if there exist

ρ 1 ∈ ((Σ \ {f }) ∪ R) * and ρ 2 ∈ (Σ ∪ R) * such that ρ = ρ 1 • f • ρ 2 and Time(ρ 2 ) ≥ ∆.
That is, if ρ is ∆-faulty then at least ∆ time units have elapsed after the occurrence of the first fault in ρ.

Definition 4 (Digital-clock diagnoser) Let A DC be a digital-clock automaton and let

∆ ∈ N. A (A DC , ∆)- diagnoser for A is a total function D : (Σ o ∪ {tick}) * → {0, 1}
such that: -if ρ is non-faulty then ∀π ∈ Π Σo (Unt(ρ||σ)).D(π) = 0,

• for any π, π ′ ∈ (Σ o ∪ {tick}) * , if D(π) = 1 then D(π • π ′ ) = 1,
-if ρ is ∆-faulty then ∀π ∈ Π Σo (Unt(ρ||σ)).D(π) = 1.
In other words, a (A DC , ∆)-diagnoser must announce 0 (i.e., "no fault detected") for any behavior that is non-faulty, no matter what the behavior of the digital clock is: this is a soundness requirement. On the other hand, a (A DC , ∆)diagnoser must announce 1 (i.e., "fault detected") for any behavior that is faulty, provided at least ∆ time units have elapsed after the first fault: this is a liveness requirement.

No requirement is made for faulty behaviors where less than ∆ time units have elapsed after the fault. However, the first requirement ensures that the diagnoser does not "change its mind" once it has announced a fault.

A is said to be

(A DC , ∆)-diagnosable if there exists a (A DC , ∆)-diagnoser for A. A is said to be A DC - diagnosable if there exists ∆ ∈ N such that A is (A DC , ∆)- diagnosable. A is said to be digital-clock diagnosable if there exists A DC such that A is A DC -diagnosable.
The following result is the counterpart of Lemma 1 for diagnosis, and the proof is straightforward.

Lemma 3 For any timed automaton A, for any digitalclock automata A 1

DC and A 2 DC , for any

∆ 1 , ∆ 2 , if D is a (A 1 DC , ∆ 1 )-diagnoser for A, L(A 2 DC ) ⊆ L(A 1 DC ) and ∆ 2 ≥ ∆ 1 , then D is also a (A 2
DC , ∆ 2 )-diagnoser for A. Consider the digital-clock automaton A p DC shown in Figure 3. A p DC is a generalization of automaton A 1 DC of Figure 2. A p DC models a perfectly-periodic clock with period p. We say that A is p-diagnosable iff A is A p DCdiagnosable. The lemma below states that a periodic clock that "ticks" k times faster than another clock is better for diagnosability, that is, if diagnosability holds for the slower clock it will also hold for the fast clock.

Lemma 4 Consider the digital-clock automaton A p DC

shown in Figure 3. For any timed automaton A, for any

p 1 , p 2 , if p 1 = k • p 2 for some k ∈ N, and A is p 1 - diagnosable, then A is also p 2 -diagnosable.
With these definitions, we can define a set of problems. Problem 4 (A DC -diagnosability problem) Given A and A DC , check whether there exists ∆ such that there exists a (A DC , ∆)-diagnoser for A.

Problem 3 ((A DC , ∆)-diagnosability problem) Given

Problem 5 (Diagnosability problem) Given A, check whether there exist A DC and ∆ such that there exists a (A DC , ∆)-diagnoser for A.

In each of the problems above, in the case where a diagnoser exists, we would also like to synthesize one.

Solution to the (A DC , ∆)-diagnosability problem

Proposition 4 (Necessary and sufficient condition for (A DC , ∆)-diagnosability) Let A be any timed automaton, let A DC be a digital-clock automaton and let ∆ ∈ N. A is (A DC , ∆)-diagnosable iff for all non-faulty ρ ∈ L(A), ∆-faulty ρ ′ ∈ L(A), σ, σ ′ ∈ L(A DC ) the following holds:

Time(ρ) = Time(σ) ∧ Time(ρ ′ ) = Time(σ ′ ) ⇒ Π Σo (Unt(ρ||σ)) ∩ Π Σo (Unt(ρ ′ ||σ ′ )) = ∅
We now present an algorithmic method to check the necessary and sufficient condition given above. First, let Obs(∆) be the timed automaton of Figure 4. It is an automaton parameterized by ∆ and the accepting state is bad. Second, let A = (Σ, Q, q 0 , Q, X, I, E). We define the timed automaton A f over Σ as follows:

1. the locations of A f are {q f | q ∈ Q} ∪ {q ¬f | q ∈ Q};

Let Q f be the set of faulty locations (q f locations) and Q ¬f be the set of non-faulty locations (q locations). The idea is that locations in Q f encode the fact that a fault has occurred. The initial locations of A f are the non-faulty locations. The accepting locations of A f are the faulty locations.

2. the set of clocks of A f is X;

3. the initial state of A f is q 0¬f ; 4. the transition function is defined as follows: for each edge (q, q ′ , a, g, r) ∈ E with a = f we create two edges in A f , (q f , q ′ f , a, g, r) and (q ¬f , q ′ ¬f , a, g, r). If a = f we create (q f , q ′ f , f, g, r) and (q ¬f , q ′ f , a, g, r) (the target location must be a faulty location); 5. the invariant of A f for q p is the same as for q in A.

Third, let P = (A f ||Obs(∆))||A DC . That is, P is the parallel composition of A f , Obs(∆) and A DC , where A f and Obs(∆) synchronize on the f label, while all three automata synchronize on the passage of time. P accepts all the interleavings of (1) ∆-faulty timed words of A and (2) timed words of A DC . Fourth, let A ¬f be a copy of A with all f -labeled transitions removed. Finally, let P ′ = A ¬f ||A DC . P ′ accepts all the interleavings of (1) non faulty timed words of A and (2) timed words of A DC .

Proposition 5 A is (A DC , ∆)-diagnosable if and only if Π Σo (Unt(P )) ∩ Π Σo (Unt(P ′ )) = ∅.
The condition of Proposition 5 can be checked algorithmically. Indeed, Unt(P ) and Unt(P ′ ) are regular languages accepted by finite-state automata which can be constructed as explained in subsection 3.5. The projection Π Σo (L) of a regular language L is regular and it is accepted by an automaton obtained from the automaton accepting L by replacing τ and f labels by ǫ.

Solution to the A DC -diagnosability problem

The above algorithm works for a given ∆. However, as mentioned in the introduction, ∆ is a-priori unknown. In this section, we show how to check A DC -diagnosability, where ∆ is unknown. To do this, we need some definitions first.

An infinite timed word over Σ is an infinite sequence of delays in R and letters in Σ: ρ ∈ (Σ ∪ R) ω . Every such sequence can be put in a canonical form where delays and letters alternate:

ρ = t 0 • a 1 • t 1 • a 2 • t 2 • • • .
Terminology and operators that we introduced for finite words can be extended to infinite words in a straightforward way. For instance, we can speak about faulty infinite timed words, if f appears in them. We can also extend the projection and untiming operators.

Consider a timed automaton A. An infinite run of A is an infinite sequence of transitions, σ = s 0

t0 → s 1 a1 → s ′ 1 t1 → • • • , such that every finite prefix of σ is a run of A and s 0 is an initial state of A. The run is called non-Zeno if i t i = ∞.
The run is called accepting if it visits accepting locations infinitely often. The set of all infinite timed words corresponding to infinite, non-Zeno, accepting runs of A is denoted L ∞ (A).

Proposition 6 (Necessary and sufficient condition for

A DC -diagnosability) Let A be a non-Zeno timed automaton and let A DC be a digital-clock automaton. A is A DCdiagnosable iff there do not exist ρ, ρ ′ ∈ L ∞ (A) and σ, σ ′ ∈ L ∞ (A DC ) such that the following hold:

• • x ≤ 1 • • • x ≤ 1 • x := 0 f ; x > 1 a τ a Figure 5
. A plant which is not digital-clock diagnosable.

• ρ is faulty and ρ ′ is non-faulty,

• Π Σo (Unt(ρ||σ)) ∩ Π Σo (Unt(ρ ′ ||σ ′ )) = ∅.
As previously, the above necessary and sufficient condition serves as the basis for an algorithm. Let P = A f ||A DC and P ′ = A ¬f ||A DC , where A f and A ¬f are constructed as described above.

Proposition 7 A is A DC -diagnosable if and only if Π Σo (Unt(L ∞ (P ))) ∩ Π Σo (Unt(L ∞ (P ′ ))) = ∅.
The condition of Proposition 7 can be checked algorithmically, using a similar method as the one for checking the condition of Proposition 5.

On the existence of digital-clock diagnosers

To illustrate the interest of Problem 5, consider the timed automaton shown in Figure 5. This automaton is diagnosable in the sense of [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF], that is, with analog clock diagnosers. Indeed, the diagnoser expects a to occur at most 1 time unit after the beginning of operation. If it does not, the diagnoser is certain that a fault has occurred. Notice that, since the diagnoser is analog-clock, it can distinguish between any two observations t 1 • a and t 2 • a, where t 1 ≤ 1 and t 2 > 1, no matter how close t 1 and t 2 are. The first observation is the result of a non-faulty behavior, whereas the second observation is the result of a faulty behavior.

Proposition 8

The timed automaton shown in Figure 5 is not digital-clock diagnosable.

Proof: Let ∆ ≥ 2. Consider a digital-clock automaton A DC and let ρ ′ ∈ L(A DC ) such that Time(ρ ′ ) = ∆. Let n be the number of tick events appearing in ρ ′ until time 1 (including time 1) and let m be the number of tick events appearing in ρ ′ strictly later than time 1. There are two cases to consider: either m 0, that is, no tick appears after time 1 in ρ ′ ; or m > 0.

In the case m = 0, we set t ′ = 1.5. In the case m > 0, let t > 1 be the first moment after time 1 that a tick event appears in ρ ′ and let 1 < t ′ < t. the following two behaviors of the timed automaton of Figure 5:

ρ 1 = t ′ • f • a • ∆, (2) ρ 2 = 1 • τ • a • ∆. (3)
We claim that:

tick n • a • tick m ∈ Π Σo (Unt(ρ 1 ||ρ ′ )) ∩ Π Σo (Unt(ρ 2 ||ρ ′ )). It is clear that tick n • a • tick m ∈ Π Σo (Unt(ρ 1 ||ρ ′ )). It is also true that tick n • a • tick m ∈ Π Σo (Unt(ρ 2 ||ρ ′ ))
. Indeed, even if the n-th tick occurs exactly at time 1, the semantics of || are such that both interleavings a • tick and tick • a are included.

The point is that the digital-clock diagnoser cannot tell whether a occurred exactly at time 1 or at time strictly greater than 1, that is, it cannot distinguish between ρ 1 and ρ 2 . Thus, according to Proposition 4, the timed automaton of Figure 5 is not (A DC , ∆)-diagnosable.

We do not know whether Problem 5 is decidable. In the rest of this section, we provide a sufficient condition for existence of digital-clock diagnosers.

Consider a TA A and let ρ, ρ ′ ∈ L ∞ (A).

Let Π Σo (ρ) = t 0 • a 1 • t 1 • a 2 • t 2 • • • and Π Σo (ρ ′ ) = t ′ 0 • a ′ 1 • t ′ 1 • a ′ 2 • t ′ 2 • • • . Suppose Π Σo (Unt(ρ)) = Π Σo (Unt(ρ ′ )), that is, a 1 = a ′
1 , a 2 = a ′ 2 , .... Let date(i, ρ) denote the absolute time that the observable event a i occurs, that is, date(i, ρ) = k=0,...,i-1 t k . Similarly, date(i, ρ ′ ) = k=0,...,i-1 t ′ k . Given ǫ > 0, we define the following predicate: close ǫ (ρ, ρ ′ ) = ∀i . |date(a i , ρ)date(a i , ρ ′ )| ≤ ǫ. (4) That is, close ǫ (ρ, ρ ′ ) holds iff the corresponding observable events in ρ and ρ ′ are not separated by more than ǫ time units.

Proposition 9 (Sufficient condition for digital-clock diagnosability)

A is digital-clock-diagnosable if the following condition holds: there exists ǫ ∈ R, ǫ > 0, such that for all ρ, ρ ′ ∈ L ∞ (A), if ρ is non-faulty, ρ ′ is non-faulty and Π Σo (Unt(ρ)) = Π Σo (Unt(ρ ′ )), then ¬close ǫ (ρ, ρ ′ ). In particular, A is ǫ 2 -diagnosable.

If the condition of Proposition 9 is true, then "sampling" with a period ǫ 2 is sufficient to diagnose A. Intuitively, this is because for every two behaviors that yield identical observations on Σ o , there will be a tick "separates" the observable events in the two behaviors, thus allowing to distinguish them. The condition of Proposition 9 is sufficient but not necessary. Indeed, consider the example of Figure 6, which is a slight modification of the example of Figure 5. This automaton is digital-clock diagnosable: it suffices to take a digital-clock that produces tick at time 1. Then, if a • tick is observed, the diagnoser knows that no fault occurred; if tick • a is observed, a fault occurred. However, the condition of Proposition 9 does not hold for this example. Indeed, for any ǫ > 0, we can take ρ = τ • (1 -ǫ 2 ) • a and

ρ ′ = f • (1 + ǫ 2 )
• a, such that close ǫ (ρ, ρ ′ ).

Conclusions and perspectives

We have studied monitoring and fault-diagnosis problems for real-time systems, where observers only have access to digital (i.e., finite-precision) clocks. We have presented a framework where digital clocks are modeled as timed automata, and so are specifications (for monitoring) or plants (for fault-diagnosis). We have shown how sound and optimal monitors can be automatically synthesized, given specification and digital-clock models. We have also shown how to check diagnosability and, in case it holds, automatically synthesize a diagnoser, for given plant and digital-clock models. Finally, we have shown that there are cases where no digital clock, no matter how precise, can be used to diagnose a plant, even though the latter is diagnosable with an analog-clock.

An interesting question remains, namely, whether the problem of checking existence of such a digital clock is decidable. Another research direction is to study controller synthesis with digital-clock controllers.

Figure 1 .

 1 Figure 1. Digital-clock observation architecture.

  For example 2.a||3.b = {2.a.1.b} and 2.a||2.b = {2.a.b, 2.b.a}. Given two sets of timed words

Figure 2 .

 2 Figure 2. Digital-clock Automata

  A DC such that L(A DC ) = ∅, and for any monitor D sound(A, A DC , D) ⇒ sound 1 (A, A DC , D).

Proposition 3 (Remark 1

 31 It is then easy to prove that:Proposition 2 (Soundness) For any timed automaton A, for any digital-clock automaton A DC , sound(A, A DC , D 0 ). Optimality) Consider a timed automaton A and a digital-clock automaton A DC . Let D be a monitor such that sound(A, A DC , D). Then D 0 ⊆ D and D 0 ≤ A,ADC D Proposition 3 does not hold for predicate sound 1 . Indeed, consider the monitor D described in Example 1, which is sound w.r.t. sound 1 . We have L(D 0 ) = {tick•a, a•tick}, whereas L(D) = {tick•a}. Thus, D ⊆ D 0 , which means that D 0 is not optimal w.r.t. ⊆ and sound 1 .

Figure 3 .

 3 Figure 3. The digital-clock A p DC : a perfectly periodic clock with period p.

Figure 4 .

 4 Figure 4. Observer automaton Obs(∆).

Figure 6 .

 6 Figure 6. The condition of Proposition 9 is not necessary for digital-clock diagnosability.

A better term would be fault detection, but we use the term introduced in[START_REF] Sampath | Diagnosability of discrete event systems[END_REF] for reasons of tradition.


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

Stavros Tripakis
email: tripa-kis@cadence.com.

Fault Diagnosis with Dynamic Observers *

In this paper, we review some recent results about the use of dynamic observers for fault diagnosis of discrete event systems. Dynamic observers can switch sensors on or off, thus dynamically changing the set of events they wish to observe. We study the dynamic diagnoser synthesis problem and some related optimization problems.

I. INTRODUCTION

A. Monitoring, Testing, Fault Diagnosis and Control

Many problems concerning the monitoring, testing, fault diagnosis and control of discrete event systems (DES) 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 review some recent results about sensor minimization. These results 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.

Given 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 wasted. For example, to detect a fault f in the system described by the automaton B, Figure 1, page 3, an observer needs to watch only for event a initially, and watch for event b only after a has occurred. If the sequence a.b occurs, for sure f has occurred and the observer can raise an alarm. If, on the other hand, event b is not observed after a, f has not occurred. It is then not useful to switch on sensor b before observing event a.

B. 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 discreteevent system (DES) setting of [START_REF] Sampath | Diagnosability of discrete event systems[END_REF] where the behavior of the plant is known and a model of it is available as 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 1 . Checking 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] Sampath | Diagnosability of discrete event systems[END_REF], [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF], [START_REF] Jiang | A polynomial algorithm for testing diagnosability of discrete event systems[END_REF]. In the general case, synthesizing a diagnoser involves determinization and thus cannot be done in polynomial time.

In this paper, we focus on dynamic observers. For results about sensor optimization with static observers, we refer the reader to [START_REF]Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF].

In the dynamic observer framework, we assume that an observer can decide after each new observation the set of events it is going to watch. We first prove that checking diagnosability with dynamic observers that are given by finite automata can be done in polynomial time. As a second aspect, we focus on the dynamic observer synthesis problem. We show that computing a dynamic observer for a given plant, can be reduced to a game problem. 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.

C. Related Work

To our knowledge, the problems of synthesizing dynamic observers for diagnosability that we study in this paper have not been addressed in the literature. Due to lack of space, we omit a discussion of previous work on related problems, and refer the reader to [START_REF] Cassez | Synthesis of optimal dynamic observers for fault diagnosis of discrete-event systems[END_REF], [START_REF]Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF], [START_REF] Cassez | Fault diagnosis with static and dynamic observers[END_REF].

D. Organisation of the paper.

In Section II we fix notation and introduce finite automata with faults to model DES.

In Section III we introduce and study dynamic observers and show that the most permissive dynamic observer can be computed as the strategy in a safety 2-player game.

We also define a notion of cost for dynamic observers in Section IV 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 how it can be solved using Zwick and Paterson's result on graph games.

This paper contains no proofs and the interested reader may refer to [START_REF] Cassez | Synthesis of optimal dynamic observers for fault diagnosis of discrete-event systems[END_REF], [START_REF]Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF], [START_REF] Cassez | Fault diagnosis with static and dynamic observers[END_REF] for the details.

II. PRELIMINARIES

A. Words and Languages

Let Σ be a finite alphabet and Σ ε = Σ ∪ {ε}. Σ * is the set of finite words over Σ and contains ε which is also the empty word and Σ + = Σ * \ {ε}. A language L is any subset of Σ * . Given two words ρ, ρ 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) 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 words, π /Σ1 : Σ * → Σ * 1 , recursively as follows: π /Σ1 (ε) = ε and for a ∈ Σ, ρ ∈ Σ * , π /Σ1 (a.ρ) = a.π /Σ1 (ρ) if a ∈ Σ 1 and π /Σ1 (ρ) otherwise.

B. Finite Automata

Definition 1 (Finite Automaton)

An automaton A is a tuple (Q, q 0 , Σ ε , δ) with Q a set of states 2 , q 0 ∈ Q is the initial state, δ ⊆ Q × Σ ε × 2 Q is
the transition relation. We write q λ -→ q if q ∈ δ(q, λ). For q ∈ Q, en(q) is the set of actions enabled at 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 A is a tuple (Q, q 0 , Σ, δ, L) where (Q, q 0 , Σ, δ) 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 • • • s.t. λ i ∈ Σ ε and s 0 = s.
If ρ is finite and ends in s n we let tgt(ρ) = s n . The set of finite runs from s in A is denoted Runs(s, A) and we define 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 ε. A word w is accepted by A if w = tr(ρ) for some ρ ∈ Runs(A). The language L(A) of A is the set of words accepted by A.

Let f ∈ Σ ε be a fresh letter that corresponds to the fault action,

Σ ε,f = Σ ε ∪ {f } and A = (Q, q 0 , Σ ε,f , δ). Given R ⊆ Runs(A), Tr(R) = {tr(ρ) for ρ ∈ R} is the set of traces of the runs in R. A run ρ is k-faulty if there is some 1 ≤ i ≤ n s.t. λ i = f and n-i ≥ k. Notice that ρ can be either finite or infinite: if it is infinite, n = ∞ and n-i ≥ 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 nonfaulty 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 time has elapsed after the fault is welldefined) 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.

C. 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.

III. 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 1 (Dynamic Observation) Assume we want to detect faults in automaton B of Figure 1. A static diagnoser that observes Σ = {a, b} can detect faults. 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.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 beginning we only switch on the asensor; 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

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 2 (Observer) An observer Obs over Σ is a deterministic labeled automaton 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. 0 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.

L(0) = {a} 1 L(1) = {b} 2 L(2) = ∅
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].

As for Σ-diagnosability, we have the following equivalence for dynamic observers:

A is (Obs, k)-diagnosable iff Obs(π /Σ (Faulty tr ≥k (A))) ∩ Obs(π /Σ (NonFaulty tr (A))) = ∅.

Problem 1 (Finite-State Obs-Diagnosability)

INPUT: A, a finite automaton and Obs 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 1 Problem 1 is in P.

To prove Theorem 1 we build a product automaton 3 A⊗ Obs such that:

A is (Obs, k)-diagnosable ⇐⇒ A⊗Obs is (Σ, k)- diagnosable. Given two finite automata A = (Q, q 0 , Σ ε,f , →)
and Obs = (S, s 0 , Σ, δ, L), the automaton A ⊗ Obs = (Q × S, (q 0 , s 0 ), Σ ε,f , →) is defined 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 .
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 and Problem 1.(A) is in P.

Example 3 Let B be the DES given in Figure 1 and Obs the observer of Figure 2. The product B ⊗ Obs used in the above proof is given in Figure 3.

For Problem 1, 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

• • • • • • ε ε f a b ε a
Fig. 3. The product B ⊗ Obs 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 4 . 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).

C. Problem 3 as a Game Problem

To solve Problem 3 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 a k-faulty run and a nonfaulty 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 Figure 4; Player 1 states are depicted with square boxes and Player 2 states with round shapes): 1) the game starts in an state (q 1 , q 2 ) corresponding to the initial state of the product of A k 1 and A 2 . Initially, it is Player 1's turn to play. Player 1 chooses a set of events 4 Notice that this also shows that existence of an observer implies existence of a finite-state observer, since the trivial observer is finite-state. he is going to observe i.e., a subset X of Σ and hands it over to Player 2; 2) 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 (like λ 1 , λ 2 , λ 3 , λ 4 in Figure 4) which is not in X. This action can be fired either in A k 1 or A 2 (no synchronization). In this case a new state (q, q ) is reached and Player 2 can play again from this state; b) firing an action λ in X (like σ 1 , σ 2 in Figure 4): to do this both A k 1 and A 2 must be in a state where λ 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 A k 1 ×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). This game can be defined formally (see [START_REF]Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]), as a game

G A = (S 1 S 2 , s 0 , Σ 1 Σ 2 , δ). 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 to each run ρ in G A that ends in an S 1 -state. A strategy f is trace-based if given two runs ρ, ρ , if tr(ρ) = tr(ρ ) then f (ρ) = f (ρ ).
Conversely, for any trace-based winning strategy f (for Player 1) in G A , 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 after ρ is the set of events the observer O chooses to observe after reading π /Σ (tr(ρ)) i.e., L(δ(s 0 , π /Σ (tr(ρ)))). 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 X0 --→ q 1 0 ε * -→ q n0 0 λ1 -→ q 1 X1 --→ q 1 1 ε * -→ q n1 1 λ2 -→ q 2 • • • q k1 ε * -→ 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(ρ)).
Using the previous definitions and constructions we obtain the following theorems: Known results [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF] on a game like G A imply 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

Theorem 2 Let O be an observer s.t. A is (O, k)-diagno- sable. Then f (O) is a trace-based winning strategy in G A . (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
S FA = (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) = en(∆ A (s 0 , w)). We can also prove (Cf. [START_REF]Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF]) that: Theorem 4 F A is the most permissive observer.

IV. 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. The notion of cost we are going to use is inspired by weighted automata.

A. 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 imply that the more events we observe at each step, the more expensive it is.

There is not one way of defining a notion of cost and the reader is referred to [START_REF] Cassez | Synthesis of optimal dynamic observers for fault diagnosis of discrete-event systems[END_REF], [START_REF] Cassez | Fault diagnosis with static and dynamic observers[END_REF] for a discussion on this subject.

The cost of a word w is given by:

Cost(w) = i=n i=0 |L(δ(s 0 , w(i)))| n + 1 with n = |w|.
We now show how to define and compute the cost of an observer Obs that observes 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 4 (Cost of a Run

) Let ρ = q 0 a1 ---→ q 1 a2 ---→ • • • q n-1
an ---→ q n be in Runs(A) and w i = Obs(π /Σ (tr(ρ(i)))), 0 ≤ i ≤ n. The cost of ρ is defined by: Notice that Cost(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(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 [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF]. Thus 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:

Cost(ρ, A, Obs) = 1 n + 1 • n i=0 |L(δ(s 0 , w i )|. Let Runs n (A)

Theorem 5 Computing Cost(A, Obs) is in P.

Remark 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.

B. Optimal Dynamic Diagnosers

We now 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: 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.

To solve Problem 4, we use the most permissive observer F A we computed in section III-C. Given A and F A , we build a weighted graph game W 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 W G(A, F A ). By construction of W 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 4 we know that A consequence of Theorem 7 and Zwick and Paterson's results is that the cost of the optimal observer is a rational number.

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 |Σ|

V. CONCLUSIONS

In this paper we have reviewed recent results on sensor minimization problems in the context of fault diagnosis, using dynamic observers. We proved that, for an observer given by a finite automaton, 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 obervers 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 2 has not been solved so far. The major impediment to solve it is that the reduction we propose in section III yields a Büchi game in this case. 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 2.

Problem 3 is solved in doubly exponential time. Nevertheless to reduce in practice 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 Σ from some point on, we surely can diagnose it using any superset Σ ⊇ Σ. 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].

Fig. 1 .

 1 Fig. 1. The automaton B

Fig. 2 .

 2 Fig. 2. A finite-state observer ObsExample 2 Let Obs be the observer of Figure2. Obs maps the following inputs as follows: Obs(baab) = ab,

Problem 2 (Problem 3 (

 23 Dynamic-Diagnosability) INPUT: A. PROBLEM: Compute the set O of all observers such that A is Obs-diagnosable iff Obs ∈ O. We do not have a solution to the above general problem. Instead, we introduce a restricted variant: Dynamic-k-Diagnosability) INPUT: A, k ∈ N. PROBLEM: Compute the set O of all observers such that A is (Obs, k)-diagnosable iff Obs ∈ O.

Fig. 4 . 3 Theorem 3

 433 Fig. 4. Game reduction for problem 3

  be the set of runs of length n in Runs(A). The cost of the runs of length n of A is Cost(n, A, Obs) = max ρ∈Runs n (A) {Cost(ρ, A, Obs)}. The cost of the pair (Obs, A) is Cost(A, Obs) = lim sup n→∞ Cost(n, A, Obs).

Problem 4 (

 4 Bounded Cost Observer) INPUT: A, k ∈ N and c ∈ N. PROBLEM: (A). Is there an observer Obs s.t. A is (Obs,k)-diagnosable and Cost(A, Obs) ≤ c ? (B). If the answer to (A) is "yes", compute a witness optimal observer Obs with Cost(A, Obs) ≤ c.

Theorem 6 Problem 5 (Theorem 7

 657 ) 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:Problem 4 can be solved in time O(|Σ| × m × 2 n 2 × 2 k × 2 2 |Σ| ).We can even solve the optimal cost computation problem: Optimal Cost Observer)INPUT: A, k ∈ N. PROBLEM:Compute the least value m s.t. there exists an observer Obs with Cost(A, Obs) ≤ m. Problem 5 can be solved in time O(|Σ| × m × 2 n 2 × 2 k × 2 2 |Σ| ).

Different types of faults could also be considered, by having different fault events f 1 , f

, and so on. Our results 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.

In this paper we often use finite automata that generate prefix-closed languages, hence we do not need to use a set of final or accepting states.

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

Acknowledgements:

The authors would like to thank Karine Altisen for her contribution in the early stage of this work.

Work suported by the French government under grant ANR-SETI-06-003.