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

Stavros Tripakis
email: tripakis@cadence.com

Karine Altisen

Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems *

Keywords:

Fault diagnosis consists in synthesizing a diagnoser that observes a given plant through a set of observable events, and identifies faults which are not observable as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe. We define a notion of cost for such dynamic observers and show that (i) the cost of a given dynamic observer can be computed and (ii) an optimal dynamic observer can be synthesized.

Introduction

Fault Diagnosis. Discrete-event systems (DES) can be formalized by 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].

Fault diagnosis consists in observing a DES and detecting whether a fault has occurred or not. We follow the DES setting of [START_REF] Sampath | Teneketzis. 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 observable events, ε represents the unobservable events, and f is a special unobservable event that corresponds to the faults. 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 | Teneketzis. 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]. (Notice that synthesizing a di-agnoser involves determinization in general, thus cannot be done in polynomial time.)

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. Dynamic Observers. Dynamic sensors' selection consist in selecting the sensors to switch on after each new observation, thus dynamically changing the set of events to observe. A device that chooses the set of events to observe dynamically is a dynamic observer. We are interested in synthesizing a dynamic observer in the hope that not all the observable events are always needed to diagnose a DES.

This problem is 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 to 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 (sensor operation and computer treatment) is spent for nothing. For example, to diagnose a fault in the system described by the automaton B, Figure 1, a diagnoser only has to watch event a, and when a has occurred, to watch event b: if the sequence a.b occurs, for sure a fault has occurred and the diagnoser can raise an alarm. It is then not useful to switch on sensor b before an a has occurred.

Optimal-Cost Dynamic Sensors' Selection.

Given an observer we can define a notion of cost (i.e. how expensive it is) to diagnose a DES using this observer. The first problem we address in this paper is to compute the cost of diagnosing the DES with a given observer. We then focus on a more challenging problem which is to synthesize an optimal observer, in the sense that the cost of diagnosing a DES with such an observer is minimal.

Related work.

In the case of static observers where the set of observable events is fixed a priori some papers have already considered optimization problems. NP-hardness of finding minimum-cardinality sets of observable events so that diagnosability holds under the standard, projectionbased setting has been previously reported in [START_REF] Yoo | On the computational complexity of some problems arising in partially-observed discrete event systems[END_REF].

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. Computing an optimal observation masks is not the same as finding a minimumcardinality mask. We have recently considered this latter problem in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] and proved it is NP-complete.

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 s.t. 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.

To our knowledge, dynamic observers have not been considered up to now. Consequently, the problem of synthesizing optimal-cost dynamic observers for diagnosability purposes, have not been addressed previously in the literature. In a recent paper [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF], we have adressed the problem of synthesizing dynamic observers. No optimization criterion is used in this work. The present paper is a follow-up of [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] and extends it by considering optimization problems. A full version with proofs is available as a research report [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF].

Organisation of the paper.

In Section 2 we fix notations and introduce finite automata with faults to model DES. In Section 3 we introduce dynamic observers and define the cost of a dynamic observer. We also show how to compute it. In Section 4, we address the problem of computing an optimal observer.

Preliminaries

Words and Languages

Let Σ be a finite alphabet and Σ ε = Σ ∪ {ε}. Σ * is the set of finite words over Σ and contains ε which is also the empty word 1 . A language L is any subset of 1 We use ε both for the unobservable event and the empty word as the type is always clear from the context. Σ * . Σ + = Σ * \ {ε}. Given two words ρ, ρ ′ we denote ρ.ρ ′ the concatenation of ρ and ρ ′ (which is defined in the usual way). |ρ| stands for the length of the word ρ and |ρ| λ with λ ∈ Σ stands for the number of occurrences of λ in ρ. Given Σ 1 ⊆ Σ, we define the projection π /Σ1 : Σ * → Σ * 1 by: π /Σ1 (ε) = ε and for a ∈ Σ, ρ ∈ Σ * , π /Σ1 (a.ρ) = a.π /Σ1 (ρ) if a ∈ Σ 1 and π /Σ1 (ρ) otherwise.

Finite Automata

Let f ∈ Σ ε be a fresh letter that corresponds to the fault action. An automaton A is a tuple 2

(Q, q 0 , Σ ε,f , →) with Q a set of states, q 0 ∈ Q is the initial state, →⊆ Q × Σ ε,f × Q is the transition relation. If Q is finite, A is a finite automa- ton. We write q λ -→ q ′ if (q, λ, q ′ ) ∈ → . For q ∈ Q, en(q) is the set of actions enabled at q. A run ρ from state s in A is a sequence of transitions s 0 λ1 --→ s 1 λ2 --→ s 2 • • • s n-1 λn --→ s n s.t. λ i ∈ Σ ε,
f and s 0 = s. We let tgt(ρ) = s n . The set of 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 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.

λ i different from ε. Given a set 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. 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
We assume that each run of A of length n can be extended into a run of length n + 1. This is required for technical reasons 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

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 σ ∈ Σ i \ Σ 3-i and q i σ -→ i q ′ i and q ′ 3-i = q 3-i or -σ ∈ Σ 1 ∩ Σ 2 and q k σ -→ k q ′ k for k = 1, 2.

Sensor Minimization & Dynamic Observers

In this section we introduce dynamic observers. 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 Fig. 1. 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. 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 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 twice as less energy.

• • • • • • ε ε f a b b a Figure 1.
The automaton B

Dynamic Observers

We now formalize the above notion of dynamic observation. 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 1 (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 chose not to observe occurs. We use the notation δ(s 0 , w) to denote the state s reached by reading the word w and L(δ(s 0 , w)) for 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 nothing or ε, (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.

Fault Diagnosis with Dynamic Diagnosers

Definition 2 ((Obs, k)-diagnoser) Let Obs be an observer over Σ.

D : Σ * → {0, 1} is an (Obs, k)-diagnoser for A if (i) ∀ρ ∈ NonFaulty(A), D(Obs(π /Σ (tr(ρ)))) = 0 and (ii) ∀ρ ∈ 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 | Teneketzis. Diagnosability of discrete event systems[END_REF]. In

this case A is (Σ, k)-diagnosable iff π /Σ (Faulty tr ≥k (A)) ∩ π /Σ (NonFaulty tr (A)) = ∅.
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))) = ∅. This follows directly from definition 2.

If an observer is given as a finite state automaton we can state the following problem: Problem 1 (Finite-State Obs-Diagnosability) INPUT: A, 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.
As proved in [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] Problem 1 can be solved in polynomial time. To solve it we build a product automaton 3 A ⊗ Obs such that:

A is (Obs, k)-diagnosable ⇐⇒ A ⊗ Obs is (Σ, k)-diagnosable.
As (Σ, k)-diagnosability can be checked in polynomial time and A ⊗ Obs has polynomial size in the size of A and Obs the result follows.

The automaton A ⊗ Obs = (Q × S, (q 0 , s 0 ), Σ ε,f , →) is defined as follows:

1. (q, s)

β -→ (q ′ , s ′ ) iff ∃λ ∈ Σ s.t. q λ -→ q ′ , s ′ = δ(s, λ) and β = λ if λ ∈ L(s), β = ε otherwise; 2. (q, s) λ -→ (q ′ , s) iff ∃λ ∈ {ε, f } s.t. q λ -→ q ′ .
Example 3 Let A be the DES given in Fig. 3 and Obs the observer of Fig. 2. The product A ⊗ Obs is given in Fig. 4. 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.

• • • • • ε ε f a b a b

Figure 3. The automaton A

We are going to define a notion of cost for observers. This notion is inspired by weighted automata. 3 We use ⊗ to clearly distinguish this product from the synchronous product ×.

Weighted Automata

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. We recall here the results of [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF] which will be used later.

Definition 3 (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 4 (Mean Cost

) Let ρ = q 0 a2 -→ q 1 a1 -→ • • • 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 a1 -→ q 1 a2 -→ • • • 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 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 a1 -→ s 1 a2 -→ • • • an --→ s n is a cycle of A i.e. s 0 = s n , the mean weight of 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}. K As stated in [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF], for weighted automata, ν(A) = lim sup n→∞ ν(A, n) = lim n→∞ ν(A, n) = ν * (A). 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 is explained in Appendix 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 capture the fact that the more events we observe at each time, the more expensive it is.

Definition of Cost.

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. 5, 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. 5 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.

Cost 2 (w) = Σ i=n i=0 |L(δ(s 0 , w(i)))| n + 1 with n = |w|.
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 ρ 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 5 (Cost of a Run) Given a run

ρ = q 0 a1 -→ q 1 • • • q n-1 an --→ q n ∈ Runs(A), let w i = Obs(π /Σ (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 Cost 2 (n, A, Obs) = max{Cost 2 (ρ, A, Obs) for ρ ∈ Runs n (A)}.
The cost of the pair (Obs, A) is Cost 2 (A, Obs) = lim sup n→∞ Cost 2 (n, A, ρ). Notice that Cost 2 (n, A, Obs) is defined for each n because we have assumed A generates runs of arbitrary large length.

To compute Cost 2 (n, A, Obs) we consider that ε and f are now observable events, let's 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 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 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: Theorem 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.

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 4

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

The automata A + ×O + 1 and A + ×O + 2 are given in Fig. 6 and Fig. 7. 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. 3 one of the transitions (0, a, 4) and (0, b, 4) is redundant. We apply the algorithm of Appendix A. 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 mean-weight value ν * is the maximum value max v min(v) for v ranging over the set of states of

A + × O + i . We obtain Cost 2 (A, O 1 ) = 2 and Cost 2 (A, O 2 ) = 1. 0 w = 2 1 w = 2 2 w = 2 3 w = 2 4 w = 2 u a b a b u u Figure 6. A + × O + 1 0 w = 1 1 w = 1 2 w = 1 3 w = 0 4 w = 1 5 w = 1 u a b a b u u u Figure 7. A + × O + 2 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

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: Before dealing with Problem 2 we recall some results from [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF].

Problem 2 (Bounded Cost Observer) INPUT: A, k ∈ N and c ∈ N. PROBLEM: 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

Most Permissive Observer

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 observa- tion of ρ by O. Assume O(ρ) = a 0 • • • a k . Let ρ = L(ε).ε.L(a 0 ).a 0 . • • • L(O(ρ)(k))
.a 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 Σ .
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 Obs (one such that A is (Obs, 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.

Theorem 6 of [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] 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

S FA = ({0, 2 • • • , l} ∪ ({1, 3, • • • , 2l ′ + 1} × 2 Σ
), 0, Σ ∪ 2 Σ , δ) 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;

• if δ(2i, X) = (2i ′ + 1, X) with X ∈ 2 Σ , it means that from an even state 2i, the automaton S FA 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 FA 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)).

Example 5 For the automaton A of Fig. 3, we obtain the most permissive observer F A of Fig. 8. For odd states we have not mentionned the component X that has last been picked up by the observer. X is the label of the unique incoming transition. In the even states, the observer chooses what to observe and in the odd states it moves according to what it observes. When the system starts, it can choose either {a, b} or {a}. Once an a has been observed it can choose any subset containing b. When a b has been observed the observer can choose to observe the empty set. We point out that from an odd state (2i + 1, X), outgoing transitions are labeled by elements of X. This does not mean that the DES under observation cannot do other actions from state 2i + 1: it might be able to do so but there are unobservable for the observer.

Optimal Dynamic Observers

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 (see Appendix B for Zwick and Paterson algorithm). These are graphs (V, E) with the set of nodes partitioned into two sets: V 1 for Player 1 and V 2 for Player 2. In a V i state it is Player i's turn to play. There is a weight function that associates with each edge e the weight w(e). The players build paths e 1 . • • • .e n by choosing an edge when it is their turn to play. The goal of the game is for Player 1 to maximize the value lim inf n→∞ • there are optimal memoryless strategies for both players that can be computed in

O(|V | 4 × |E| × log(|E|/|V |) × W ).
To solve the Problem 2, we use the most permissive observer we computed in section 4.1. 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 3.4: 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 \ en(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. 9. 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 [START_REF] Cassez | Sensor minimization problems with static or dynamic observers for fault diagnosis[END_REF] 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 3 is that the cost of the optimal observer is a rational number (see Appendix B).

Example 6

For the example A of Fig. 4 andF + A of Fig. 9, using Zwick and Paterson's algorithm (Appendix B) we obtain that the optimal cost is 1 and the optimal strategy is to use the observer Obs of Fig. 2.

Conclusion & Future Work

In this paper we have addressed sensor optimization problems in the context of fault diagnosis, using dynamic observers. We have defined a suitable notion of cost for such observers. Then we have proved that, given such observer, we could compute the cost of diagnosing a DES. This is done by reducing this problem to the computation of a maximum mean-weight cycle in a weighted graph. Hence we can solve it in polynomial time. We have also solved the optimal observer synthesis problem i.e. compute an observer of optimal cost by reducing it to an optimization on weighted graph game.

Further work will include:

• finding the exact complexity class of Problems 2 and 3;

• dealing with more realistic examples. This requires an implementation of our algorithms and of the algorithms described in Appendix A and B.

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

Figure 2 .

 2 Figure 2. A Finite-State Observer Obs Example 2 Let Obs be the observer of Fig. 2. Obs maps the following inputs as follows: Obs(baab) = ab, Obs(bababbaab) = ab, Obs(bbbbba) = a and Obs(bbaaa) = a. If Obs operates on the DES B of Fig 1 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 4 .

 4 Figure 4. The automaton A ⊗ Obs

  Using the observer of Fig. 5, 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 5 .

 5 Figure 5. The Finite-State Observer Obs

  e i ) and for Player 2 to minimize lim sup n→∞ 1 n n i=1 w(e i ). One of the results by Zwick and Paterson[START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF] is that:• there is a value ν ∈ Q, called the value of the game s.t. Player 1 has a strategy to ensure that 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 ) ≤ ν; 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 8 .

 8 Figure 8. Most Permissive Observer for the Automaton A of Fig. 3

Figure 9 .Theorem 3 Problem 3 (Theorem 4

 9334 Figure 9. The Automaton F + A

Table 2 .

 2 Iterations forA + ⊗ O +

	2

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

* Work supported by the project CORTOS, a program of the french government. http://www.lsv.ens-cachan.fr/aci-cortos

A. Karp's Maximum Mean Cycle Algorithm

In this section, we recall Karp's maximum mean cycle algorithm [START_REF] Karp | A characterization of the minimum mean cycle in a digraph[END_REF]. The original algorithm works for weighted graph where the weights are on the edges. We give a version where weights are on vertices. Definition 6 (Weighted Graph) A weighted directed graph is a pair (G, w) s.t. G = (V, E) is a directed graph and w : V → R. We assume that each vertex v ∈ V is reachable from a unique source vertex s 0 .

Definition 7 (Mean Weight of a Cycle

Let D(v) be the weight of a most expensive path from s 0 to v and D k (v) be the weight of a most expensive path which has exactly k edges (if there is no such path

Thus for each vertex we can compute min(v) = min 0≤k≤n-1

and then compute the value max v∈V min(v) to obtain ν * . This algorithm runs in O(n.m) where |V | = n and |E| = m. 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).

B. Zwick and Paterson's Algorithm

In this section we give an overview of some results of [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]. Assume G = (V, E) is a weighted graph as in definition 6 except that the weight function is defined on edges:

assigns an integral weight to each edge of G with W ∈ N. We assume each vertex has at least one outgoing transition.

Definition 8 (Weighted Graph Game

Vertices V i are Player i's vertex. 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→∞ w(e i ). 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→∞ Let n = |V |. To compute ν, proceed as follows ( [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]):

is defined by:

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;

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.


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

Thomas Chatain
email: thomas.chatain@irisa.fr

Claude Jard
email: claude.jard@irisa.fr

Symbolic Unfoldings for Networks of Timed Automata

In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Extended symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.

Work supported by the project CORTOS, a

Introduction

Concurrent Semantics for Finite State Systems. The analysis of distributed or concurrent finite state systems has been dramatically improved thanks to partial-order methods (see e.g. [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF]) that take advantage of the independence between actions, and to the unfolding based methods [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF][START_REF] Kenneth | A technique of state space search based on unfolding[END_REF] that improve the partial order methods by taking advantage of the locality of actions. Timed Systems. The main models that include timing information and are used to specify distributed timed systems are networks of timed automata (NTA) [START_REF] Alur | A theory of timed automata[END_REF], and time Petri nets (TPN) [START_REF] Merlin | Recoverability of communication protocols -implications of a theorical study[END_REF]. There are a number of theoretical results about NTA and TPN and efficient tools to analyze them have been developed. Nevertheless the analysis of these models is always based on the exploration of a graph which is a single large automaton that produces the same behaviours as the NTA or the TPN; this induces an exponential blow up in the size of the system to be analysed.

Related Work.

In [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Minea | Partial order reduction for model checking of timed automata[END_REF], the authors define an alternative semantics for NTA based on local time elapsing. The efficiency of this method depends on two opposite factors: local time semantics generate more states but the independence relation restricts the exploration. In [START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF] (a generalization of [START_REF] Belluomini | Verification of timed systems using posets[END_REF]), the independence between transitions in a TA is exploited in a different way: the key observation is that the occurrences of two independent transitions do no need to be ordered and consequently nor do the occurrences of the clock resets. The relative drawback of the method is that, before their exploration, the symbolic states include more variables than the clock variables. Partial order methods for TPNs are studied in [START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF], where the authors generalize the concept of stubborn set to time Petri nets, calling it a ready set. They apply it to the state class graph construction of [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF]. The efficiency of the method depends on whether the (dynamical) timing coupling between transitions is weak or not. Unfortunately the urgent semantics of this model entails a strong timing coupling. The previous partial order methods only take advantage of the independence of actions and not of any locality property. We are interested in a true concurrent semantics for NTA and this has not been developed in the aforementioned work.

Process semantics for time Petri nets which is a generalization of the unfolding semantics for time Petri nets has been developed by different researchers. From a semantical point of view, Aura and Lilius have studied in [START_REF] Aura | A causal semantics for time petri nets[END_REF] the realizability problem of a non branching process in a TPN. They build an unfolding of the untimed Petri net underlying a safe TPN, and add constraints on the dates of occurrence of the events. It is then possible to check that a timed configuration is valid or not. In [START_REF] Fleischhack | Computing a finite prefix of a time Petri net[END_REF] the authors consider bounded TPN and a discrete time domain: the elapsing of one time unit is a special transition of the net. Thus the global synchronization related to this transition heavily decreases the locality property of the unfolding. Furthermore, when the intervals associated with the transitions involve large integers, this method suffers the usual combinatorial explosion related to the discrete time approach.

Section 3 of this paper can be viewed as the counterpart of the work of Aura and Lilius [START_REF] Aura | A causal semantics for time petri nets[END_REF] in the framework of NTA: we define similar notions for NTA and build a symbolic unfolding which is a symbolic net. We have to extend the results of Aura and Lilius because there is no urgency for firing a transition1 in a NTA. As stated in [START_REF] Aura | A causal semantics for time petri nets[END_REF] those unfoldings are satisfactory for free choice nets which are a strict subclass of TPN. Our NTA are not free choice nets and in section 4 we refine our symbolic unfolding to obtain an extended symbolic unfolding which is a symbolic net with read arcs.

Following our recent approach [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] using the notion of symbolic unfolding to capture the partial order behaviors of TPN, we propose in this paper a similar notion for NTA, but we cannot directly apply the framework of [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF]. Indeed TA and TPN have different expressive powers [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF][START_REF] Cassez | Structural translation from time petri nets to timed automata[END_REF] and as stated earlier NTA do not have the nice urgency features that TPN have.

Up to our knowledge, this is the first attempt to equip NTA with a concurrent semantics, which can be finitely represented by a prefix of an unfolding. In this paper we answer the following questions:

1. What can be a good model for a concurrent semantics of NTA? The result is an extension of the model of symbolic nets we have proposed in [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF]; 2. How to define a concurrent semantics for NTA, i.e. how to define a symbolic unfolding that captures the essential properties of a NTA while preserving concurrency information? This is achieved in two steps: first build a symbolic unfolding and use this object to build a proper extended symbolic unfolding of the NTA. By proper unfolding, we mean a symbolic Petri net on which we can check that a local configuration is valid using only the extended causal past of an event. 3. Is there a complete finite prefix for NTA? This result is rather easy to obtain on the symbolic unfolding object and carries over to the extended symbolic unfolding.

About point 3 above, we are not addressing the problem of building such a prefix efficiently but our work is concerned with identifying the key issues in the construction of a prefix for NTA. The solution proposed in [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF] builds a complete finite prefix for safe TPNs, but with no guarantee that this prefix is one of the smallest, which is a very difficult problem to solve. Based on this work, we address more basic questions about NTA, which are in a sense easier to study than safe TPNs because the concurrent structure is explicit.

Key Issues.

In this section we present informally the problem and the key issues raised by the three previous questions. In the case of networks of finite automata, finite complete prefixes exist. For example, for the network2 of Fig. 1(a), a finite complete prefix is given on Fig. 1(b). Finite complete prefixes contain full information about the reachable states of the network and about the set of events that are feasible in the network. A set of events (labels) is feasible iff it is a word that can be generated by the network. For example, {t 1 } is not a feasible set of events in the network N 1 , because t 1 must be

0 1 2 t0 t1 A x ≤ 10 B x ≤ 2 C t2; x := 0 t1; x ≤ 2 U y ≤ 3 V t2; y ≤ 3 (a) The NTA N1 ⊥ δ ⊥ = 0 0 A U δU ≤ 3 e2 t2, δe 2 ≤ 3 B δB -δe 2 ≤ 2 V e3 t1, δe 3 -δe 2 ≤ 2 2 C e1 t0 δe 1 -δ ⊥ ≤ 5 1
(b) Symbolic unfolding for the network N1 Fig. 1. A NTA and its Symbolic Unfolding preceded by t 2 . And this appears in the unfolding as event e 3 (labelled by t 1 ) must be preceded by e 2 (labelled by t 2 ). In an unfolding, a set of events K is a configuration if there is a reachable marking obtained by firing each event in K. For example {⊥, e 1 } is a configuration, {⊥, e 1 , e 2 } as well, but {⊥, e 3 } is not as e 3 must be preceded by e 2 before it occurs. The minimal set of events necessary for an event e to occur is called the causal past (or local configuration) of e. Note that by definition a configuration contains the causal past of each of its event. A complete prefix is an unfolding that satisfies property (P ): a set of events is feasible in the NTA iff it is a configuration of the unfolding 3 . This property of unfoldings is the key point in the untimed case and allows one to do model-checking on the complete finite prefix. This unfolding can also be used for fault diagnosis purposes which is a very important application area.

In the case of networks of timed automata, we deal with timed events which are pairs (e, δ) where δ ∈ R ≥0 . A set of timed events E is feasible iff there is a run in the NTA that generates a timed word that contains all the timed events in E. To decide whether a set of timed events is feasible in a network of timed automata, we can build a symbolic unfolding. For this, we add a symbolic timing constraint g(e) to each event of the previous unfolding. For example, with e 1 we can associate the constraint

g(e 1 ) def = δ e1 -δ ⊥ ≤ 5,
where δ e is the variable that represents the date of occurrence of e. A set of timed events {(e 1 , d 1 ),

• • • , (e k , d k )} is a timed configuration if {e 1 , e 2 , • • • , e k } is a configuration and the constraint g(e 1 ) ∧ • • • ∧ g(e k
) is satisfied when replacing each δ ei by d i . For example {(⊥, 0), (e 1 , 4)} is a timed configuration with g(⊥) def = δ ⊥ = 0. Thus the property we would like to have for symbolic unfoldings is (P

): {(e 1 , d 1 ), • • • , (e k , d k )} is a timed configuration iff there is a run (e f (1) , d f (1) ), • • • , (e f (k) , d f (k)
) in the NTA with f a one-to-one mapping from 1..k to 1..k. In the untimed case, one can check that an event is fireable in the unfolding using only the causal past of the event. We want this property to hold for the timed unfoldings as well and then a formula associated with an event e should only involve variables that are associated with events in the causal past of e (the local configuration of e). Now assume we want to decide whether {(⊥, 0), (e 1 , d 1 ), (e 2 , d 2 )} is a timed configuration. It is actually if d 1d 2 ≤ 2. But this cannot be captured by any conjunction g(⊥) ∧ g(e 1 ) ∧ g(e 2 ) because e 1 is not in the causal past of e 2 and e 2 not in the causal past of e 1 . A symbolic unfolding built by associating constraints with each event e, with the property that each constraint g(e) uses only variables in the causal past of e, does not always contain enough information for property (P ) to hold. In this paper we show 1) how to build an unfolding that contains enough information so that (P ) holds; 2) how to build a finite and complete prefix of the unfolding satisfying (P ).

Organization of the Paper. The paper is organized as follows. Section 2 presents the model of NTA and its usual sequential semantics. Section 3 gives a concurrent semantics for NTA in terms of symbolic branching processes (SBP) and proves the existence of complete finite prefixes. The SBP is a first step towards a complete finite prefix having property (P ). In section 4, we show how to build an extended SBP, using read-arcs, which is a complete finite prefix satisfying property (P ). Section 5 gives a summary of the paper and directions for future work. The proofs of the theorems are omitted and can be found in the extended version of the paper [START_REF] Cassez | Symbolic Unfoldings for Networks of Timed Automata[END_REF].

Networks of Timed Automata

Notations . Given a set B we use

B ε for the set B ∪ {ε} (assuming ε ∈ B). Let X = {x 1 , • • • , x n } be a finite set of clock variables. A valuation ν is a mapping from X to R ≥0 . Let X ⊆ X. The valuation ν[X ] is defined by: ν[X ](x) = 0 if x ∈ X and ν[X ](x) = ν(x) otherwise. ν |X
is the restriction (projection) of ν to X and is defined by ν |X (x) = ν(x) for x ∈ X . We denote 0 the valuation defined by 0(x) = 0 for each x ∈ X. For δ ∈ R, ν + δ is the valuation defined by (ν + δ)(x) = ν(x) + δ. C(X) is defined to be the set of conjunctions of terms of the form xx c or x c for x, x ∈ X and c ∈ N and ∈ {<, ≤, =, ≥, >}. C(X) is called the set of diagonal constraints over X. The set of rectangular constraints, C r (X) is the subset of C(X) where only constraints of the form x c appear. Given a formula ϕ ∈ C(X) and a valuation ν ∈ R X ≥0 , we use ϕ[x/ν(x)] for ϕ where x is replaced by ν(x). we denote

ϕ(ν) ∈ {tt, ff} the truth value of ϕ[x/ν(x)]. We let [[ϕ]] = {ν ∈ R ≥0 | ϕ(ν) = tt}. A subset Z of R X ≥0 is a zone if Z = [[ϕ Z ]] for some ϕ Z ∈ C(X).
Note that the intersection of two zones is a zone. Two operators are defined on zones: the time successor operator,

Z = {v+δ | v ∈ Z, δ ∈ R ≥0 } and the R-reset operator, Z[R] = {v | ∃v ∈ Z s.t. v = v [R]}. Both Z and Z[R] are zones if Z is a zone.
Timed Automata. Timed automata were introduced in [START_REF] Alur | A theory of timed automata[END_REF] to model systems which combine discrete and continuous evolutions.

Definition 1. A timed automaton A is a tuple (L, 0 , Σ, X, T, Inv) where: L is a finite set of locations; 0 is the initial location; Σ is a finite set of discrete actions; X = {x 1 , • • • , x n } is a finite set of (positive real-valued) clocks; T ⊆ L × C r (X) × Σ × 2 X × L is a finite set of transitions: ( , g, a, R, ) ∈ T represents
a transition from the location to , labeled by a, with the guard g and the reset set R ⊆ X; we write

SRC(t) = , TGT(t) = , G(t) = g, λ(t) = a and R(t) = R. Inv ∈ C r (X)
L assigns an invariant to any location. We require that Inv be a conjunction of terms of the form x c with ∈ {<, ≤} and c ∈ N.

A state of a timed automaton is a pair

( , v) ∈ L × R X ≥0 . A timed automaton is bounded if there exists a constant k ∈ N s.t. for each ∈ L, Inv( ) ⊆ [[0 ≤ x 1 ≤ k ∧ • • • ∧ 0 ≤ x n ≤ k]].
Examples of timed automata are given in Fig. 1(a). In the sequel we require that for any valuation v and any transition t = ( , g, a, R,

), g(v) =⇒ Inv( )(v[R]).

Definition 2. The semantics of a timed automaton

A = (L, 0 , Σ, X, T, Inv) is a la- beled timed transition system (TTS) S A = (Q, q 0 , T ∪ R ≥0 , →) with Q = L × (R ≤0 ) X , q 0 = ( 0 , 0)

is the initial state and → consists of the discrete and continuous transition relations: i) the discrete transition relation is defined for all

t ∈ T by: ( , v) t -→ ( , v ) ⇐⇒ ∃t = ( , g, a, R, ) ∈ T s.t. g(v) = tt, v = v[R → 0]; ii) the continuous tran- sition relation is defined for all δ ∈ R ≥0 by: ( , v) δ -→ ( , v ) iff = , v = v + δ and ∀0 ≤ δ ≤ δ, Inv( )(v + δ ) = tt. A run of a timed automaton A is a path in S A
starting in q 0 where continuous and discrete transitions alternate 4 . The set of runs of A is denoted by

[[A]]. A state q is reachable in A if there is a run from q 0 to q. REACH(A) is the set of reachable states of A. A timed word w ∈ (T × R ≥0 ) * is accepted by A if there is a run ρ ∈ [[A]] s.t. the trace of ρ is w.
The analysis of timed automata is based on the exploration of a (finite) graph, the simulation graph, where the nodes are symbolic states. A symbolic state is a pair ( , Z) where is a location and Z a zone over the set R X ≥0 .

Definition 3. The simulation graph SG(A) of a timed automaton A is given by: i) the set of states is the set of symbolic states of the form ( , Z) where Z is a zone; ii) the initial state is

( 0 , Z 0 ) with Z 0 = 0 ∩ [[Inv( 0 )]]; iii) ( , Z) a -→ ( , Z ) if there is a transition ( , g, a, R, ) in A s.t. Z ∩ [[g]] = ∅ (this ensures Z is not empty) and Z = (Z ∩ [[g]])[R] ∩ [[Inv( )]].
We assume that the timed automata are bounded i.e. in each location , Inv( ) is bounded 5 . In this case the number of zones of the simulation graph is finite [START_REF] Kim | Efficient verification of realtime systems: Compact data structure and state-space reduction[END_REF][START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF].

Network of Timed Automata. We use the classical composition notion based on a synchronization function. Let A 1 , . . . , A n be n timed automata with

A i = (L i , l i,0 , Σ i , X i , T i , Inv i ). We assume that for each i = j, L i ∩L j = ∅ and X i ∩X j = ∅ (clocks are not shared). A synchronization constraint I is a subset of Σ ε 1 × Σ ε 2 • • • × Σ ε n \(ε, • • • , ε). The (synchronization) vectors of a synchronization constraint I indicate which actions synchronize. For (t 1 , • • • , t n ) ∈ T ε 1 × • • • T ε n we write λ(t 1 , • • • , t n ) = (λ 1 (t 1 ), • • • , λ n (t n )) with λ i (ε) = ε. λ -1 (I) ⊆ T ε 1 × • • • T ε n indicates how the tran- sitions synchronize. For t ∈ λ -1 (I), we let: SRC * (t) = {l ∈ SRC(t[i]) | t[i] = ε}, TGT * (t) = {l ∈ TGT(t[i]) | t[i] = ε}, R(t) = {x | x ∈ R(t[i]) and t[i] = ε}, G(t) = ∧ t[i] =ε G(t[i]).

Definition 4. The network of timed automata (NTA)

(A 1 | . . . |A n ) I is the timed au- tomaton B = (L, l 0 , Σ, X, T, Inv) defined by: L = L 1 ו • •×L n , l 0 = ( 1,0 , • • • , n,0 ), Σ = Σ 1 × • • • × Σ n , X = ∪ n i=1 X i ; (l, g, a, R, l ) ∈ T iff ∃t ∈ λ -1 (I) s.t.: (1) if t[i] = ε then l i = SRC(t[i]) and otherwise l i = TGT(t[i]), (2) a = λ(t), g = G(t) and R = R(t) and Inv(l) = ∧ n i=1 Inv i ( i ) if l = ( 1 , • • • , n ).
This definition implies that if each A i is bounded (resp. simple) then the NTA is bounded (resp. simple).

Symbolic Unfolding for Network of Timed Automata

In this section we define the symbolic semantics of a NTA in terms of symbolic branching processes. Those processes contain timing constraints both on places and events. We do not recall the definitions of occurrence nets, branching processes (BP) for untimed network of automata. The reader is referred to [START_REF] Esparza | An unfolding algorithm for synchronous products of transition systems[END_REF] for a detailed presentation of these notions.

Let (A 1 | . . . |A n ) I be a synchronous product of TA. In a first step, we build the untimed branching processes (UBPs) of (A 1 | . . . |A n ) I . For each timed automaton A i we let UNTIME(A i ) be the automaton obtained by removing all the timing constraints and clocks in A i . An UBP of a NTA is a BP of the network of untimed automata (UNTIME(A 1 )| . . . |UNTIME(A n )) I in the sense of [START_REF] Esparza | An unfolding algorithm for synchronous products of transition systems[END_REF]. The set of UBPs is defined inductively over two sets E and P by: i) ⊥ ∈ E, ii) if e ∈ E and s ∈ L then (e, s) ∈ P, iii) if S ⊆ P and t ∈ λ -1 (I) then (S, t) ∈ E. On those two sets we define the mappings • (), ()

• :

-for E,

↑ J = ∪ e∈J e • \ ∪ e∈J • e . For a set J ⊆ E ∪ P J = {e ∈ E ∪ P | e
e for some e ∈ J}. A set of events J is causally closed if J = J. A configuration of a BP is a set of events K ⊆ E which is causally closed and conflict-free. A set A is a co-set iff A ⊆ ↑K where K is a configuration. A cut S ⊆ P is a set of places which is a maximal co-set. To each configuration K, we can associate a unique cut ↑ K which is denoted CUT(K). A place p = (e, s) ∈ P is a i-place if s ∈ L i . We can define the union of two branching processes (E 1 , P 1 ) and (E 2 , P 2 ) component-wise on events and places. BPs are closed under countable union and the unfolding of (UNTIME(A 1 )| . . . |UNTIME(A n )) I is be the maximal branching process. The next two properties are taken from [START_REF] Esparza | An unfolding algorithm for synchronous products of transition systems[END_REF]: Proposition 1. Two i-places of a UBP are either causally related or in conflict.

Proposition 2. Let C be a cut of a UBP. C contains one i-place for each 1 ≤ i ≤ n.
Thus given a configuration K, CUT(K) corresponds to a unique state of the product of untimed automata.

The symbolic branching processes of a NTA are built from the UBP. The intuition is that we associate with places and events a time variable. For an event e, the variable δ e stands for the (global) time at which event e fired. For a place p, δ p stands for the most recent (global) time for which a token was in p. We define δ(E ∪ P ) to be the set of variables

{δ x | x ∈ E ∪ P }. A symbolic branching process (SBP) (E, P, γ) of (A 1 | . . . |A n ) I is a UBP (E, P ) of (UNTIME(A 1 )| . . . |UNTIME(A n )) I with γ : E ∪ P → C(δ(E ∪ P ))
a mapping that associates to each node a timing constraint. The constraint on a node x should only refer to variables in x .

The constraint γ(x) is computed by rewriting the timing constraints of the NTA in terms of the variables δ y for y ∈ x . For the event ⊥ we just set δ ⊥ = 0 stating that the system started at time 0. On the example of Fig. 1(b), to compute the timing constraint γ(U ) we just rewrite the invariant y ≤ 3 in terms of the firing times of the events in the past of place U : if the current (global) time at which a token is in

U is δ U we must have x = δ U -δ ⊥ ≤ 3 i.e. δ U ≤ 3.
For event e 3 , we must have x ≤ 2 and the value of x is given by δ e3δ e2 which yields δ e3δ e2 ≤ 2. The result for the NTA of Fig. 1(a) is depicted on Fig. 1(b). The important point is that each constraint γ(x) is entirely determined by x. Hence to each UBP (E, P ) we can associate a unique SBP (E, P, γ). We can thus define the symbolic unfolding TBP(A 1 | . . . |A n ) I of (A 1 | . . . |A n ) I to be the symbolic branching process associated with the unfolding of (UNTIME(A 1 )| . . . |UNTIME(A n )) I .

To define cuts for SBP we need to take into account the timing constraints: for instance in Fig. 1(b),(0,A,U) is a cut iff δ 0 = δ A = δ U ≤ 3 meaning that the global time in each place is the same and the constraints on the places are satisfied. For an event the same strategy applies. We can define a formula that characterizes all the timed cuts of a SBP:

Definition 5. (M, Φ) is a symbolic co-set of (E, P, γ) if: 1) M is a co-set of (E, P ), 2) Φ = Φ 1 (M ) ∧ Φ 2 (M ) ∧ Φ 3 (M ) ∧ Φ 4 (M ) with: Φ 1 (M ) = x∈ M γ(x)
(1)

Φ 2 (M ) = e∈ M ∩E ∧ p∈ • e δ p = δ e (2)
Φ 3 (M ) = p∈M δ• p ≤ δ p (3) Φ 4 (M ) = p,p ∈M δ p = δ p ( 4
)
If M is a cut of (E, P ), (M, Φ) is a symbolic cut. The meaning of formula ( 2) is that the last date δ p at which a token was in p is the time at which an event removed a token in p.

(3) imposes that if a token is in p and p is in a co-set, the current time in p which is δ p is larger than the date of occurrence of the event that put a token in p. Finally ( 4) requires that all the places in the co-set have reached the same global time. The reason why we need to use variables associated with places is because there is no urgency in NTA. Notice that the formula Φ of a symbolic co-set is entirely determined by the co-set M and unique; we denote it by Φ M . Moreover the form of the constraints on δ(E ∪ P ) in the SBP is such that Φ M is a zone for each symbolic cut M :

Theorem 1. For each symbolic cut (M, Φ M ) Φ M is a zone.
Given a SBP (E, P, γ), a set M ⊆ P , and a mapping Θ : δ( M ) → R ≥0 that associates with each node a date, (M, Θ) is a timed cut iff (M, Φ M ) is a symbolic cut and Θ ∈ [[Φ M ]]. Given a timed cut (M, Θ) we can associate a unique state of the NTA GS(M, Θ): it suffices to compute the values of each clock variables in X from the values of the nodes variables in the SBP. Conversely, given a state (l, v) of the product, we can associate a timed cut to (l, v) as stated by Theorem 3 below.

Theorem 2. If K is a configuration of TBP(A 1 | . . . |A n ) I and Θ ∈ [[Φ CUT(K) ]] then a) GS(CUT(K), Θ) = (l, v) for some (l, v) reachable in (A 1 | . . . |A n ) I , and b) if K ∪{e} is a configuration and Θ ∈ [[Φ CUT(K) ∧γ(e) ∧ p∈ • e δ p = δ e ]] then (l, v) λ(e) ---→ (l , v ) with GS(K ∪ {e}, Θ ) = (l , v ) and Θ |CUT(K) = Θ and Θ (x) = Θ(p) for some p ∈ CUT(K) otherwise.
The formula Φ CUT(K) ∧ γ(e) ∧ p∈ • e δ p = δ e asserts that the global time is the same in every automata which is also equal to the firing time of e and that the guard of the transition t holds.

Theorem 3. Let (l, v) be a reachable state in

(A 1 | . . . |A n ) I . There is a configuration K of TBP(A 1 | . . . |A n ) I and Θ ∈ [[Φ CUT(K) ]] s.t.: a) GS(CUT(K), Θ) = (l, v), and b) if (l, v) t -→ (l , v ) there is a configuration K ∪ {e} s.t. λ(e) = t and a valuation Θ ∈ [[Φ CUT(K∪{e}) ]] s.t. GS(K ∪ {e}, θ ) = (l , v ).
If a TBP T satisfies the conditions of Theorem 3, we say that T is complete. Theorem 2, corresponds to a correctness property. For network of finite untimed automata, complete and correct finite branching processes exist, and are called complete finite prefixes [START_REF] Kenneth | A technique of state space search based on unfolding[END_REF][START_REF] Esparza | An unfolding algorithm for synchronous products of transition systems[END_REF]. In the case of network of timed automata we can construct a finite complete prefix that preserves the reachability information of the simulation graph.

Theorems 3 and 2 have two consequences. They follow from the fact that each Φ CUT(K) is a zone for a configuration K. This means that the set of valuations reachable by all the linearizations of the events in K defines a zone as well. In the symbolic unfolding we construct, we obtain one zone for all the linearizations of the events in K whereas in SG((A 1 | . . . |A n ) I ) they could be two distinct states for two different linearizations. The first consequence is that the union of the zones reachable by all the linearization in SG((A 1 | . . . |A n ) I ) is a zone. Indeed computing global states preserves zones. This result was obtained recently by Ramzi Ben Salah, Marius Bozga and Oded Maler in [START_REF] Ben Salah | On interleaving in timed automata[END_REF] and has useful consequences. Our framework gives an alternative proof of this result and accounts for it in terms of partial order. The second consequence is that finite complete prefixes exist for NTA.

Assume the two configurations K 1 and K 2 lead to the same symbolic state GS(CUT(K 1 ), Φ CUT(K1) ) = GS(CUT(K 2 ), Φ CUT(K2) ), then they have the same future. Thus we can discard the events that extend one of them, for instance the smallest w.r.t. the order defined as:

K 1 K 2 iff GS(CUT(K 1 ), Φ CUT(K1) ) = GS(CUT(K 2 ), Φ CUT(K2) ) ∧ |K 1 | < |K 2 |.
As the simulation graph contains a finite number of (union of) zones and because each Φ CUT(K) is a union of zones, we can not have an infinite number of different symbolic states. This allows us to construct a complete finite prefix by keeping only the events e such that there exists a configuration K that enables e and is minimal w.r.t. . We let PREF((A 1 | . . . |A n ) I ) be the complete symbolic finite prefix obtained from (A 1 | . . . |A n ) I . So far we are able to answer the question whether a set of timed events is a timed configuration: given the set of events K and the valuation Θ we can check whether Θ ∈ [[Φ CUT(K) ]]. What we would like to do is to check whether a set of events K can be extended to a configuration i.e. if ↑(K) is a co-set. We cannot do this directly with the SBP we have constructed so far. In the next section we refine our unfolding so that we do not need to look at the global state of the system to decide whether a set of events can be extended to a timed configuration.

Extended Finite Complete Prefixes

In the case of finite automata, any cut containing a co-set that enables an event, still enables the same event. This is not the case for network of timed automata as can be seen on the example of Fig. 1(b). If e 2 has not fired, e 1 can fire because nothing can prevent it from doing so (e 3 is not enabled). The fact that e 2 has not fired can be inferred from the fact that either place A or U contains a token. But this implies that the date δ e1 at which e 1 fires satisfies δ e1 ≤ 3. If e 2 has fired at δ e2 , e 3 and e 1 are in conflict. Thus e 1 can only occur at a date when a token can be in B, i.e. to fire we must have δ B = δ e1 and the constraint on the date at which a token can be in B which is δ Bδ e2 ≤ 2. This implies δ e1δ e2 ≤ 2. Thus the timing constraints associated with e 1 are not the same in the cuts (0, A, U) and (0, B, V ) although they are both cuts that contain • e 1 .

To encode this timing dependency structurally we can use symbolic occurrence nets with read arcs. For instance the symbolic net of Fig. 1(b) can be "transformed" into the symbolic extended net of Fig. 2 (a read arc is a dash line). Read arcs enable us to point to the missing timing information in the net that is needed to ensure an event can fire. This also means that we duplicate the event e 1 into e 1 and e 1 because the constraints are different depending on whether e 2 has occurred or not. Read arcs enlarge the causal past of the events. In the extended occurrence net, the constraint between the dates of occurrence of e 1 and e 2 can be inferred from the past of e 1 : indeed, to fire, we must have δ e1 = δ B and thus δ e1δ e2 ≤ 2. Read arcs enable us to differentiate the two cuts (0, A, U) and (0, B, V ) that generate different timing constraints on e 1 and e 2 .

Extended Branching

Processes. An extended net N is a tuple (E, P, • (), ()

• , • ())
where (E, P, • (), ()

• ) is a net, and • () : E → 2 P . If • e = ∅ for each e ∈ E then
N is a net. The set • e represents the input places of an event that are to be read without removing a token. The Extended symbolic branching processes (ESBP) of a network are defined as in section 3: the only change we need to do is to define the set of events so that it includes the read-only places of an event denoted • e. To this end, if S, S ⊆ P and t ∈ T , (S, S , t) is in E and if e = (S, S , t), • e = S . The causality relation is now defined by:

x → y if x ∈ • y ∪ • y or y ∈ x • .
is the reflexive and transitive closure of →. The weak causality relation is given by: x y if either x → y or • x ∩ • y = ∅ (if x needs a token in one of the input place of y this implies a causality relation, even if x is not in the past of y in the sense of →.). We let the reflexive and transitive closure of . Two nodes x and y are weakly causally related if either x y or y x. x and y are in conflict, x#y, if there is a place p s.t. there exist w and u, w = u, p ∈ • u ∩ • w and w x and u y. x and y are concurrent if they are not weakly causally related nor in conflict. For J ⊆ E ∪ P , the definitions of ↑J and J are unchanged (we use the new ). A set of events is now causally closed if J = J. Co-sets, configurations and cuts are defined as before.

Safe Co-sets. Let ENABLE(e) denote the enabling cuts of e = ⊥ in a finite symbolic branching process N : ENABLE(e) = {C | • e ⊆ C and C is a cut of N }. As a running example we take the prefix N 1 built in Fig. 1(b) and δ ⊥ is always replaced by 0 (zero). For this example the enabling cuts are: ENABLE(e 1 ) = {(0, A, U), (0, B, V )}, ENABLE(e 2 ) = {(0, A, U), (1, A, U)}, ENABLE(e 3 ) = {(0, B, V )}. Now assume an event e is in conflict with another event e in the symbolic unfolding. As we pointed out at the end of section 3, the timing constraints given by • e on the firing time of e do not always contain enough information to ensure event e can fire: event e 1 in N 1 can fire if a) e 2 has not fired (this must be at time δ ≤ 3), or b) e 2 has fired, and the time elapsed since it has occurred is less than 2 time units (i.e. at time δ with δδ e2 ≤ 2), or c) e 2 has been disabled by another event in conflict with it and cannot occur in the future. To ensure e can fire, we should add to the conditions in • e some information about the events in conflict with e. This is the purpose of safe co-sets. They extend the co-sets of the symbolic unfolding with some information about the conflicting events. In terms of occurrence nets, a safe co-set for an event e will be the set of places • e, extended with a set a read only places, • e. The information contained in a safe co-set should be such that, if the timing constraints obtained by Φ• e∪ • e are satisfied, then there is a cut C ⊇ • e ∪ • e s.t. Φ C is satisfied.

⊥ δ ⊥ = 0 0 A U δU ≤ 3 e2 t2, δe 2 ≤ 3 B δB -δe 2 ≤ 2 V e3 t1, δe 3 -δe 2 ≤ 2 2 C e1 t0 δe 1 ≥ 0 e 1 t0 δ e 1 ≥ 0 1 1
Fig. 2. Extended symbolic unfolding for the example of Fig. 1(a) For any cut C, the formula Φ C (Def. 5, equations ( 1)-( 4)) is a formula over δ(C ∪ ( C ∩ E)). Indeed all the intermediate places p, not in the cut, are constrained by a formula of the form δ e = δ p because of equation 2 of Def. 5. For instance

Φ (0,B,V ) = δ B -δ e2 ≤ 2 ∧ 0 ≤ δ e2 ≤ 3 ∧ δ B ≥ δ e2 ∧ δ 0 = δ B = δ V .
Because of the term Φ 4 , if we use an extra variable δ and the formula (δ = δ p ) ∧ Φ C for any 6 p ∈ C, we obtain a formula over δ( C ∩ E) ∪ {δ}: δ stands for the current global time (since the system started) and the constraint on δ in Φ C defines the set of instants for which the cut C is reachable i.e. there are tokens in each place p ∈ C. We write Φ δ C for the projection on ( C ∩ E) ∪ {δ} of the formula Φ C ∧ (δ = δ p ). In our example,

Φ δ (0,A,U) = δ ≤ 3, Φ δ (1,A,U) = δ e1 ≤ 3 ∧ δ e1 ≤ δ ≤ 3 and Φ δ (0,B,V ) = δ -δ e2 ≤ 2 ∧ 0 ≤ δ e2 ≤ 3 ∧ δ ≥ δ e2 .
( C ∩ E) ∪ {δ} → R ≥0 if ν |δ( S ∩E)∪{δ} ∈ [[Φ δ S ]] and ν |δ( C\S ∩E)∪{δ} ∈ [[Φ δ C\S ]] then ν ∈ [[Φ δ C ]]. S is a safe representative of e if S is a safe representative of each pair (e, C) with C ∈ ENABLE(e).
If S is a safe representative of (e, C), then if γ(e) holds together with Φ S , e can be added to the unfolding. For example, (0, A) is not a safe representative of (0, A, U) because Φ δ (0,A) = δ ≥ 0 and Φ δ (0,A,U) = δ ≤ 3. (0, U) is a safe representative of (0, A, U) as well as (0, A, U) itself. (0, B) is a safe representative of (0, B, V ). As each cut C ∈ ENABLE(e) is a safe representative of itself, there is always one safe representatives for any C which is ENABLE(e). We can state a theorem which is a variant of Theorem 2 using only safe representatives of an event (item b) of the theorem is altered):

Theorem 4. If K is a configuration of TBP(A 1 | . . . |A n ) I and Θ ∈ [[Φ CUT(K) ]] then a) GS(CUT(K), Θ) = (l, v) for some (l, v) reachable in (A 1 | . . . |A n ) I , and b) if K ∪ {e} is a configuration and S is a safe representative of CUT(K) and Θ ∈ [[Φ S ∧ γ(e) ∧ p∈ • e δ p = δ e ]] then (l, v) λ(e) ---→ (l , v ) with GS(K ∪ {e}, Θ ) = (l , v ) and Θ |CUT(K) = Θ and Θ (x) = Θ(p) for some p ∈ CUT(K) otherwise.
This theorem is a direct consequence of Theorem 2 and Def. 6. It states that a safe representative for e contains enough information to decide whether event e can be fired or not. As a consequence, if whenever we add a new event e to a (finite) extended symbolic branching process of a NTA (A 1 | . . . |A n ) I , we use a safe representative S = • e∪ • e and add read-arcs to the places of • e, then e (including S ) gives the accurate constraints on the date δ e at which e can fire.

To build an extended complete finite prefix for a NTA we can proceed as follows: 1) build the symbolic net defined in section 3; this enables us to obtain the safe co-sets for each event; 2) build an extended net by adding an event to the unfolding using safe co-sets instead of simple co-sets. On the example of Fig. 1 this gives the unfolding of Fig. 2: 1. start with places 0, A, U and event ⊥; 2. to add an event labelled t 0 use a safe co-set: we choose (0, U) and add event e 1 with a read arc to U ; 3. add e 2 and e 3 ; 4. now a new safe co-set has appeared: (0, B); we can add an event e 1 labelled by t 0 with a read arc from place B.

This construction can be formally defined (see [START_REF] Cassez | Symbolic Unfoldings for Networks of Timed Automata[END_REF]). The result is a finite extended symbolic complete prefix EPREF((A 1 | . . . |A n ) I ) that satisfies property (P ). Formally, we define symbolic configurations. Assume EPREF((A 1 | . . . |A n ) I ) = (E, P, γ).

Definition 7. (K, Ψ

) is a symbolic configuration of (E, P, γ) if: 1) K is a configuration of (E, P ), and 2) Ψ = Ψ 1 (K) ∧ Ψ 2 (K) where Φ i (M ), 1 ≤ i ≤ 2 are defined by:

Ψ 1 (K) = e∈ K γ(e) (5) and Ψ 2 (K) = e∈K ∧ p∈ • e∪ • e δ p = δ e (6)
Notice that Ψ uses only information in the past of K and is uniquely determined thus we can write it On the example of Fig. 1(a),{(⊥,0), (e 1 , δ e1 ), (e 2 , δ e2 )} is a timed configuration iff δ e1δ e2 ≤ 2 and δ e2 ≤ 3.

Ψ K . Let ν : K → R ≥0 . (K, ν) is a timed configuration if ν ∈ [[Ψ K ]]. Theorem 5. If (K , Ψ ) is a symbolic configuration of EPREF((A 1 | . . . |A n ) I ) and Θ ∈ [[Ψ ]] then: there exists a symbolic configuration (K, Ψ ) with K ⊇ K and Θ ∈ [[Ψ ]] s.t. 1) GS(CUT(K), Θ) = (l, v) for some (l, v) reachable in (A 1 | . . . |A n ) I , and 2) if (K ∪ {e}, Ψ ) is a symbolic configuration and [[Ψ ]] = ∅ then (l, v) λ(e) ---→ (l , v ) and GS(CUT(K ∪ {e}), Θ ) = (l , v ) for some Θ ∈ [[Ψ ]]. 0 x ≤ 3 1 a; x ≤ 3 A y ≤ 2 B b; y ≤ 2 (a) Two Independent Automata ⊥ δ ⊥ = 0 0 A e2 b δe 2 ≤ 2 B e1 a δe 1 ≤ 3 1 (b) The Unfolding

Minimality for Safe Co-sets.

The purpose of unfoldings is to keep explicit the concurrency of events. In the case of untimed network of automata, • e is sufficient to ensure e can fire. For NTA, we have to use read arcs, but we should be concerned about the number of the new dependencies: for instance, if we use ENABLE(e) as the set of safe representatives for each e, we require that the global state of the network is known each time we want to fire e. This means we do not keep explicit any concurrency in the unfolding. It is thus important to try and reduce the number of read arcs from each event.

To this extent we define a notion of minimality for safe representatives.

We can define a partial order on co-sets i.e. sets of places using the cardinality of the sets:

C 1 C 2 iff |C 1 | ≤ |C 2 |.
For each C ∈ ENABLE(e) we can take one minimal element in the set of safe representatives of C. Given e ∈ E, SAFE(e) denotes a set of minimal safe representatives, one for each C ∈ ENABLE(e). In the example for N 1 we can take the sets: SAFE(e 1 ) = {(0, U), (0, B)}, SAFE(e 2 ) = {(A, U )}, SAFE(e 3 ) = {(0, B)}. For the independent automata of Fig. 3(a), we obtain that 0 is a safe representative of e 1 (in Fig. 3(b)): indeed 0 is a safe representative of (0, A) and a safe representative of (0, B) which belongs to ENABLE(e 1 ). For the NTA given by Fig. 3(a) we obtain the unfolding of Fig. 3(b).

The minimality criterion we have defined does not give a unique set of safe representatives. A consequence is that there is no smallest complete finite prefix for a NTA but rather a set of set of minimal complete finite prefixes. Moreover as we take at least one safe representative for each pair (e, C) the branching process we build is still complete.

Checking Validity of Timed Configuration.

To complete the construction and provide a solution to the problem of checking whether a timed configuration is valid, we can define the constraint Γ (e) associated with an event e by: Γ (e) = Ψ ( e ) | e ∩E . This constraint gathers the constraints of all the past events. The branching process obtained this way is a reduced branching process with only constraints on events. For the network of timed automata of Fig. 1 enables us to decide whether a closed set of events K is a prefix of an extended symbolic branching process.

Conclusion

In this paper we have defined a model, extended symbolic branching process, to define the concurrent semantics of timed systems. We have also proved that each NTA admits a finite complete prefix which is a symbolic extended branching process, and we have given an algorithm to compute such a prefix. Other interesting results are: 1) there is no unique complete finite prefix for a NTA but rather a set of complete finite prefixes; 2) building a small (optimal) complete finite prefix is very expensive as it requires the computation of information spread across the network; and 3) we have pointed out the difficulties arising in the construction of such a prefix, namely the need for safe co-sets. Our future work will consist in: a) define heuristics to determine when an event can be added to a prefix of an unfolding; this means having an efficient way of computing safe representatives, which are no more guaranteed to be minimal; b) when step 1 is developed, we can define algorithms to check properties of the NTA using the unfolding and assess the efficiency of these algorithms.

  This last example is interesting because it shows that the set of dates s.t. a token is in (0, B, V ) depends on the time at which e 2 occurred. Finally we let Θ(e) = {Φ δ C | C ∈ ENABLE(e)} and in the previous example, we obtain:Θ(e 1 ) = {Φ δ (0,A,U) , Φ δ (0,B,V ) }, Θ(e 2 ) = {Φ δ (0,A,U) , Φ δ (1,A,U) }, Θ(e 3 ) = {Φ δ (0,B,V ) } Θ(e)represents the set of different constraints that can be generated by all the enabling cuts of event e. Definition 6. A set of places S is a safe representative of a pair (e, C) where e ∈ E and C ∈ ENABLE(e) if 1) • e ⊆ S ⊆ C and 2) for all ν : δ

Fig. 3 .

 3 Fig. 3. A Network of two Independent Timed Automata

Fig. 4 .

 4 Fig. 4. Reduced Extended symbolic unfolding for the example of Fig. 1(a)

  By definition of E and P a SBP is completely determined by E ans P as • () and ()• are implicitly defined. Let x, y be two nodes (place or transitions). If x ∈ • y or y ∈ x • there is an arc from x to y and we write x → y. This enables us to refer to the directed graph of a net which is simply the graph (E ∪ P, →). The reflexive and transitive closure of → is denoted . x, y are causally related if either x y or y x.x is in the (strict) causal past of y if x y and x = y, i.e. x ≺ y. x, y are in conflict, noted x#y, if there is a place p ∈ P such that p → w x and p → u y with u = w. x and y are concurrent if x and y are neither causally related nor in conflict. If J is a set of events then

• ⊥ = ∅, and if e = (S, t), • e = S; and e • = {s | (e, s) ∈ P}; -for P: • (e, s) = e and (e, s) • = {e | • e ∩ s = ∅}.

invariants and guards can be independent and a transition is not bound to fire before its deadline given by the guard.

The automata synchronize on common labels. Labels of the events and places represent the corresponding location and transition in the network of automata. The constraints appearing near each node are explained later and can be ignored at this stage.

Actually we should write "it is a labeling" of a configuration of the unfolding.

In our definition runs are labeled by transitions.

Any timed automaton can be transformed into an equivalent (behaviours) bounded automaton[START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF].

As equation (4) already imposes δ p = δp for p, p ∈ C we can add δ = δp for any p in C.

program of the French government.