Camille Coquand

Yannick Pencolé
email: yannick.pencole@laas.fr

Audine Subias

Diagnosabilization of Time Petri net for timed fault

Keywords: Discrete event system, Time Petri nets, diagnosabilization, critical pair

come

INTRODUCTION

Fault diagnosis of a partially observable dynamic discrete event system is the problem of determining the occurrence in the system of unobservable faulty events based on the sequence of observations emitted by the system [START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]). In this paper, the complete behaviour of the system is modeled as a Time Petri Net [START_REF] Berthomieu | An enumerative approach for analyzing time Petri nets[END_REF]) and a fault is defined as the occurrence of a single faulty event in a bounded time interval. In other words, a fault is characterized by the occurrence of single event that is considered to be abnormal as soon as it occurs within a fixed set of time bounds: such a timed fault can model, for instance, time shifts of critical events, delays... This paper deals with the ∆-diagnosability of such timed faults. If the system is ∆-diagnosable, it means that the occurrence of the timed fault is always determined with certainty after ∆ time units [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF]; [START_REF] Basile | Diagnosability analysis of labeled time Petri net systems[END_REF]; [START_REF] Pencolé | Diagnosability of event patterns in safe labeled time Petri nets: A model-checking approach[END_REF]). Here, we suppose that the system is not yet ∆-diagnosable and we aim at providing a set of adjustments in the system to ensure that the system becomes ∆-diagnosable. In this paper, we firstly propose a formal definition of this problem that we call diagnosabilization. More precisely, the type of modifications that we propose is to restrict some static time intervals associated with some transitions of the Time Petri nets. This paper then proposes a first and original method that is based on a diagnosability analysis detailed in [START_REF] Coquand | Critical pairs based diagnosability analysis of timed fault in time petri nets[END_REF] and that characterizes a set of solutions as constraints over interval bounds in static intervals that ensures, if it exists, that the system can be ∆-diagnosable by just applying time restrictions complying with this set of constraints.

The problem of synthesizing requirements to design a discrete event system so that it is diagnosable has not yet received a lot of attention in the literature. Recently, [START_REF] He | Using Delay Blocks to Make Non-Diagnosable Discrete Event Systems Diagnosable[END_REF] proposes to use a Sat Modulo Theory method to add delay blocks into an untimed automaton to disambiguate observable events and ensure the overall diagnosability of the system. As far as timed discrete event systems are concerned, closest contributions are not directly focussing on fixing diagnosability but more on repairing the model wrt to the real process via processing mining techniques [START_REF] Fahland | Repairing process models to reflect reality[END_REF]). [START_REF] Basile | Model repair of time petri nets with temporal anomalies[END_REF] proposes to repair Time Petri Nets by adjusting the static intervals, using Mixed-Integer Linear Programming techniques.

The paper is organized as follows. Section 2 recalls the necessary formal background and introduces the diagnosabilization problem. Then Section 3 presents a diagnosability analysis based on the enumeration of critical pairs. Using this enumeration, Section 4 proposes time constraint synthesis for which if the system satisfies them it will be ∆-diagnosable.

DIAGNOSABILIZATION OF TIME PETRI NETS

After some reminders on Time Petri nets and their semantics, this section formally introduces the problem of diagnosabilization.

Safe Labeled Time Petri Nets

Definition 1. A safe Labeled Time Petri Net (LTPN) is a 6-uple N = P, T, A, Σ, , I s where:

• P is a finite set of places • T is a finite set of transitions (P ∩ T = ∅) • A ⊆ (P × T ) ∪ (T × P ) is a binary relation modeling
the arcs between the transitions and the places • Σ is a finite alphabet of transition labels • : T → Σ is the transition labeling function

• I s : T → I Q+ is a static interval function I s (t),
for which the lower bound, also called the date of earlier firing is denoted ↓ (I s (t)) ∈ Q + , and its upper bound, also called the date of later firing, is denoted

↑ (I s (t)) ∈ Q + ∪ {+∞} A marking M of the net is a function M : P → {0, 1}.
The preset of a transition t is the set of input places pre(t) = {p ∈ P | (p, t) ∈ A}, and similarly the postset of t is the set of output places post(t) = {p ∈ P | (t, p) ∈ A}.

For a safe LTPN, a state is a couple S = M, I where I is the partial firing interval application (I: T → I Q+ ) that maps to any transition a time interval of Q + in which t can be fired as soon as it is enabled. S 0 = M 0 , I 0 is the initial state of the net where M 0 is the initial marking of the net and I 0 is defined as follows: for any transition t enabled by M 0 , I 0 (t) = I s (t), else I 0 (t) = ∅. For a marking M , a transition t is firable at the date θ if and only if:

• t is enabled (i.e. ∀p ∈ pre(t), M (p) = 1) • θ ∈ I(t)
and for all t enabled by M, θ ≤↑ (I(t ))

The firing of a transition t at a date θ is denoted: M, I θt -→ M , I and defined such that

• M is such that ∀p ∈ pre(t) \ post(t), M (p) = 0, ∀p ∈ post(t) \ pre(t), M (p) = 1 else M (p) = M (p) • for any transition t ∈ T (t = t) enabled in M and still enabled in M , I(t ) = [a, b] ⇒ I (t ) = [max(0, a -θ), b -θ]
• for every transition t enabled by M , and for each transition disabled by the firing of t and newly enabled by it (loops),

I (t ) = I s (t ) A state S is reachable in a marked LTPN if there exists a run r = θ 1 t 1 . . . θ n t n , n ∈ N * such that S 0 θ1t1 --→ S 1 θ2t2 --→ S 2 . . . θntn ---→ S. The set of reachable states of a LTPN N is denoted R(N, S 0 ). A run r = θ 1 t 1 . . . θ n t n of a LTPN N is said to be admissible if there exists {S 1 , . . . S n } ∈ R(N, S 0 ) n such that S 0 θ1t1 --→ S 1 θ2t2 --→ S 2 . . . θntn ---→ S n .
A timed sequence over an alphabet Σ is a sequence of pairs (d, e) ∈ R + × Σ where d corresponds to the relative date of firing of the label e. A run produces a unique timed sequence. Definition 2. The language L(N ) of a LTPN N is the set composed of every timed sequence ρ such that there exists an admissible run for N r = θ 1 t 1 . . . θ n t n with ρ = θ 1 (t 1 ) . . . θ n (t n ).

System and fault modelings

A system is modeled as a partially observable safe LTPN. The set of observable (resp. unobservable) events is denoted Σ o (resp. Σ u ). The following assumptions are considered:

A0 each static firing interval I s (t) is bounded (∀t ∈ T , ↑ (I s (t)) < +∞); A1 the system is ultimately observable, that is at any time, from any reachable state, every run will eventually lead to the fire of an observable transition in bounded time; A2 the system has no zeno run (a zeno run is an infinite sequence of transitions that can occur in a finite amount of time). Example 1. Figure 1 shows an example of a system. The observable alphabet of the system is Σ o Θ = {o1, o2, o3}. The unobservable one is Σ u Θ0 = {f, uo, l}. The blue (resp. the red) transitions are labeled by observable (resp. unobservable) events. r = 3t 0 .7t 1 .1t 2 .3t 3 .1t 4 .5t 6 .3t 0 is a run of Θ. Its associated timed sequence is ρ = 3o1.7f.1o2.3f.1o2.5o3.3o1.

In untimed DES, a fault is modeled as a single event that may occur in the system. One way to refine this modeling is to add a time constraint on the occurrence of the event, as the event may only become troublesome after a certain time in the system's life. A timed fault is modeled here as an unobservable event that may occur in the system in a finite time window. Definition 3. A timed fault Ω f over a system Θ is an unobservable event f ∈ Σ u associated with a bounded rational interval

I Ω f ∈ Q 2 + . The bounds are denoted a Ω f and b Ω f . The language associated with Ω f is L(Ω f ) = {d i f |d i ∈ I Ω f }.
As most of the systems are maintained on a regular basis, dealing with a fault occurring in a finite time window is a reasonable hypothesis.

The occurrence of the fault in the system is formulated as a fault matching problem [START_REF] Coquand | Signature of timed patterns in time Petri nets: a formal characterization[END_REF]). It can be seen as a synchronization between the system and the fault.

Definition 4. A timed sequence ρ ∈ L(Θ) matches a timed fault Ω f (denoted ρ Ω f ) if there exists a sub-word ρ of ρ (i.e ρ is an ordered set of events extracted from ρ) such that ρ ∈ L(Ω f ).
A run matches a fault if its timed sequence matches the fault. If a run matches many times a timed fault, only the first matching is considered. Example 2. Figure 2 shows an example of a timed fault on Θ. The timed sequence ρ of Example 1 matches Ω f (ρ Ω f ) as ρ = 10f is a sub-word of ρ, and ρ ∈ L(Ω f ). As the first occurrence of f in ρ matches Ω f , no other matching is considered.

The projection of a timed sequence onto the observable alphabet of the system (also called observable timed trace) is defined as follows:

• P ΣΘ→Σ o Θ (θ 1 e 1 .θ 2 e 2 . . . θ n e n ) = θ 1 e 1 .P ΣΘ→Σ o Θ (θ 2 e 2 . . . θ n e n ) if e 1 ∈ Σ o Θ • P ΣΘ→Σ o Θ (θ 1 e 1 .θ 2 e 2 . . . θ n e n ) = P ΣΘ→Σ o Θ ((θ 1 + θ 2 )e 2 . . . θ n e n ) otherwise
In this work a method is proposed to guarantee the diagnosis of a timed fault on a time system. A guaranteed diagnosis is a diagnosis for which there is no ambiguity whether the fault has occurred or not. In the diagnosis community this notion is called diagnosability. Diagnosability is the property of a system that guarantees that there is enough observations to decide that a fault has definitively occurred a bounded amount of time after its occurrence. In timed systems it can be reformulated in terms of timed elapsed since the occurrence of the fault. Based on the definition of [START_REF] Pencolé | Diagnosability of event patterns in safe labeled time Petri nets: A model-checking approach[END_REF], diagnosability for timed fault can be defined as:

Definition 5. Θ is said to be Ω f -diagnosable if ∃τ ∈ R + s.t. ∀(ρ 1 , ρ 2 ) ∈ L(Θ) 2 , ρ 1 = ρ 1 .ρ 1 , time(ρ 1 ) ≥ τ , ρ 1 Ω f ∧ P Σ→Σ o Θ (ρ 2 ) = P Σ→Σ o Θ (ρ 1 ) ⇒ ρ 2 Ω f . p 1 p 0 p 9 t 1 f [3, 7] p 2 t 2 o2 [1, 2] p 3 t 3 f [2, 4] p 4 t 4 o2 [1, 2] p 5 t 6 o3 ]4, 5] t 5 l [2, 3] t 0 o1 [2, 6] t 7 o1 [2, 6] p 6 t 8 o2 [4, 9] p 7 t 9 uo [2, 4] p 8 t 10 o2 [1, 2] t 11 o3 ]4, 5[ Fig. 1. System Θ p f 0 t Ω f f [9, 13] p f 1 Fig. 2.
Fault Ω f on Θ: event f between dates 9 and 13 after the start of the system

Where time is the function that associates with each timed sequence its duration. There also exists a restricted version of the diagnosability definition where the time bound τ is fixed (τ = ∆) which is a property that ensures the timed fault will be diagnosed with certainty ∆ time units after its occurrence in any case: this property is the ∆diagnosability.

Definition 6. Let be ∆ ∈ R + . Θ is said to be ∆-Ω f - diagnosable if ∀(ρ 1 , ρ 2 ) ∈ L(Θ) 2 , ρ 1 = ρ 1 .ρ 1 , time(ρ 1 ) ≥ ∆, ρ 1 Ω f ∧ P Σ→Σ o Θ (ρ 2 ) = P Σ→Σ o Θ (ρ 1 ) ⇒ ρ 2 Ω f .

Problem statement

If a system Θ is not diagnosable, the diagnosis of a timed fault Ω f cannot be guaranteed. Therefore guaranteeing the diagnosis of Ω f requires changes in the model of Θ.

As it can be expensive to add sensors on the system, we propose to focus on the development of methods that only modify the scheduling of the system, i.e. modifying the static time intervals of the system. To do so, we suppose in the following that there exists a subset of transitions in the system whose static time intervals can be adjusted: in other words, the bounds of these intervals are now considered as parameters. This set of parameterized transitions is denoted T p ⊆ T . The label of a transition of T p can either be observable or not, as there are cases in which the date of some observable transitions may not be modified and some unobservable transitions may be controllable before the start of the system. The proposed adjustments will be only restrictions of time intervals so that we ensure the causality of the system is preserved. In the following, such a solution will be called a diagnosabilisation by time restrictions (TR-diagnosabilisation for short). Definition 7. A timed system is (∆-)TR-diagnosabilisable for a timed fault Ω f and a set of parameterized transitions T p if there exists at least a valuation set

V d = {I d s (t), t ∈ T p , I d s (t) ⊆ I s (t)} such that, by replacing I s (t) with I d s (t) for every transition t ∈ T p in Θ, Θ becomes (∆-)Ω f - diagnosable. Such a solution S d is also called a (∆-)TR- diagnosabilisation of Θ.
Through the rest of this paper, we now propose a method that provides a solution that ensures that ∆-Ω fdiagnosability holds in the system Θ. For the sake of simplicity in the following, we will omit ∆-and only expressions like TR-diagnosabilisation, TR-diagnosabilisable. . .

∆-DIAGNOSABILITY ANALYSIS: CRITICAL PAIR BASED ANALYSIS

Consider ∆ ∈ R + , the proposed method aims at guaranteeing that ∆-Ω f -diagnosability holds in the system. This TR-diagnosabilization method is based on the enumeration of so-called critical pairs [START_REF] Pecheur | Formal verification of diagnosability via symbolic model checking[END_REF]). In the context of ∆-diagnosability, a critical pair is a couple of runs, one faulty and one safe, that shares the same observable trace. Definition 8. A critical pair is a couple (r, r ) of runs such that:

• let ρ (resp. ρ ) be the timed sequence produced by r (resp. r ),

• ρ = ρ 0 ρ 1 , ρ 0 Ω f , no prefix ρ 0 of ρ 0 matches Ω f , time(ρ 1 ) ≥ ∆ • ρ Ω f • time(ρ) = time(ρ ) • P ΣΘ→Σ o Θ (ρ) = P ΣΘ→Σ o Θ (ρ )
The existence of a critical pair characterizes an ambiguity in the system's behaviour so that it is sometimes impossible to decide whether the timed fault has occurred or not after ∆ time units, based on the system's observations. Proposition 1. A system Θ is ∆-Ω f -diagnosable iff there is no critical pair in Θ.

The enumeration of critical pairs in the system relies on a finite abstraction of the system behaviours inspired by [START_REF] Coquand | Critical pairs based diagnosability analysis of timed fault in time petri nets[END_REF]. This abstraction is a set of 3uples (π, Π, Π o ) called path in the following, where π is a sequence of firable transitions from the system also called a transition support, Π is the set of constraints representing the earliest and latest dates of firing of the transitions of π and Π o is the observable projection of Π, i.e. the set of time constraints representing the earliest and latest firing dates of every observable transition in π relatively to the firing date of the previous observable transition. Section 3.1 briefly presents and illustrates the computation of this abstraction.

The proposed TR-diagnosabilization method is a two step process. First, critical pairs involving one path only are identified (see Section 3.2) and a first TRdiagnosabilization is obtained as detailed in Section 4.1. Then critical pairs involving two paths are identified (see Section 3.3) and a final TR-diagnosabilization is obtained as detailed in Section 4.2.

Abstraction of system behaviours: paths

The objective of a path is to represent a possibly infinite set of runs that share the same transition support π and that might be involved in a critical pair. The computation of the constraint set representing the earliest and latest firing dates of each transition is detailed in [START_REF] Coquand | Critical pairs based diagnosability analysis of timed fault in time petri nets[END_REF]. A support π = t 0 . . . . t n . . . . .t n+l . . . . .t n+k of a given path has the following characteristics:

(1) t n , t n+l , t n+k are transitions labeled with observable events (0 ≤ l ≤ k), no transition t n+m , (l < m < k) is observable.

(2) the earliest firing date of t n is greater than b Ω f , so that after t n there cannot be any transition in the path involved in the matching of the timed fault;

(3) if k = 0, the earliest firing date of t n+l is lower than ∆ + b Ω f ; (4) the earliest firing date of t n+k is greater or equal to ∆ + b Ω f .

The support π can be seen as a path in the State Class Graph of the system (SCG) defined in [START_REF] Berthomieu | An enumerative approach for analyzing time Petri nets[END_REF]. There are a finite number of supports to extract as a consequence of Assumptions A0-A1-A2 and b Ω f < +∞ and any run r of the system such that time(r) ≤ ∆ + b Ω f is represented by exactly one of these supports, especially every run r with time(r) ≤ ∆ + b Ω f such that r Ω f . Finally, as Ω f is a timed fault whose occurrence date is bounded by b Ω f , any faulty run with time(r) > ∆ + b Ω f has, as a prefix, a run r such that time(r ) ≤ ∆ + b Ω f . Example 3. Considering the system of Figure 1 and ∆ = 1, π 0 = t 0 .t 1 .t 2 .t 3 .t 4 .t 6 .t 0 is a possible support. The firing dates of the second occurrence of t 0 relatively to the start of the system are necessarily greater than 15 (the execution of a loop in the system to fire t 0 is greater than the sum of the lower bounds of the static time intervals of the transitions) so it is greater than b Ω f , moreover t 0 is observable. Note also here that as ∆ = 1, the earliest date of t 0 is also greater than ∆ + b Ω f = 14 (special case where k = 0 so this occurrence of t 0 corresponds to transition t n = t n+l = t n+k as defined in the characteristics of the support hereabove). The constraints representing the earliest and latest firing dates of π 0 are in the set Π

0 ={2 ≤ θ 0 ≤ 6, 3 ≤ θ 1 ≤ 7, 1 ≤ θ 2 ≤ 2, 2 ≤ θ 3 ≤ 4, 1 ≤ θ 4 ≤ 2, 4 < θ 5 ≤ 5, 2 ≤ θ 6 ≤ 6}. (Here θ i (resp.
= {2 ≤ θ o 0 ≤ 6, 4 ≤ θ o 1 ≤ 9, 3 ≤ θ o 2 ≤ 6, 4 < θ o 3 ≤ 5, 2 ≤ θ o 4 ≤ 6}. 1
1 As the running example in this paper is simple for the sake of readability, there is actually no parallelism so the computation of the constraints is straightforward. However, in the general case, Π 0 and

Critical pair extracted from one path only

Let us consider a path (π, Π, Π o ) such that there is a run of this path that matches Ω f . This means that there is at least one transition label by the faulty event and whose firing fits the constraint of Ω f . Such a transition occurrence is called a faulty transition candidate in the following of this paper. For example, let us consider again the support π 0 , occurrences of t 1 and t 3 in π 0 are faulty transition candidates. Given the same path π it is also possible that it abstracts another run such that it does not match Ω f , which means that the path itself characterizes some critical pairs. Example 4. Back to Figure 2, run r 1 = 5t 0 .4t 1 .1t 2 matches the fault Ω f while run r 1 = 5t 0 .3t 1 .2t 2 does not match Ω f . Both runs share their observable projection P ΣΘ→Σ o Θ (r 1 ) = P ΣΘ→Σ o Θ (r 1 ) = 5o 1 .5o 2 . Now, it can be noticed that there exists a common continuation r 2 of r 1 and r 1 , that is r 2 = 2t 3 .1t 4 .5t 6 .2t 0 so that run r (= r 1 r 2 ) and run r (= r 1 r 2 ) are both represented in the path (π 0 , Π 0 , Π o 0 ) and (r, r ) is a critical pair. after the fire of t f relatively to the start of the system is such that t obs o = t f + t o . A straight blue line in Figure 3 then represents the set of couples of firing dates (t f , t o ) that are possible for a given value θ obs of the observed date t obs o . Obviously, if θ obs is associated with a blue line that only intersects the red (resp. green) area then the firing date of t f ensures the run is faulty (resp. safe). On the contrary, if θ obs is associated with a blue line that intersects both the red and the green areas, it means Π o 0 also contain parallelism constraints that require more complex computations, see [START_REF] Coquand | Signature of timed patterns in time Petri nets: a formal characterization[END_REF] for details. = θ obs leads to an ambiguity as the firing date of t f may be faulty or not. From this analysis, it follows that it is possible to characterize polyhedra by a set of constraints over θ obs , a Ω f , b Ω f , a o , b o that assert for any couple (t f , t o ) whether the situation is safe, certainly faulty or ambiguous (see Figure 4). The polyhedra are defined as follows: safe (Π s,L and Π s,R ):

θ obs o < a Ω f + a o (1a) b Ω f + b o < θ obs o (1b) certain (Π c ): a Ω f + b o ≤ θ obs o ≤ b Ω f + a o (1c)
ambiguous (Π a,L and Π a,R ):

a o + a Ω f ≤ θ obs o < a Ω f + b o (1d)
a o + b Ω f < θ obs o ≤ b Ω f + b o (1e)
Note that some areas may be empty regarding the different values of Based on Proposition 2, we can apply the first step of the TR-diagnosabilization to ensure that S(Π o a ) = ∅, this step is described in Section 4.1.

a f b f , a Ω f , b Ω f ,

Critical pair extracted from two different paths

We assume that a first TR-diagnosabilization has been successfully performed based on Section 4.1 to get a new set of parameters S d such that S(Π o a ) = ∅. By using again Equations 1a,1b and 1c, it is then possible to update Π c , Π o c and Π s , Π o s for each path to take into account this set of parameters S d . But, still, this first TRdiagnosabilization is not sufficient as there may be some critical pairs involving a faulty run from a path and a safe run from another path. The faulty (resp. faultless) polyhedron for a path (π, Π, Π o ) can be written as (π, Π o c ) (resp. (π, Π o s )). [START_REF] Coquand | Critical pairs based diagnosability analysis of timed fault in time petri nets[END_REF] shows that the search for critical pairs between two different paths is then equivalent to checking for the intersection between their safe and certain polyhedron:

Proposition 3. If there exists ((π, Π, Π o ), (π , Π , Π o )) such that ∃(r, r ) ∈ (π, Π o s ) × (π , Π o c
), P Σ→Σo (r) = P Σ→Σo (r ), then the system is not ∆-Ω f -diagnosable. Example 5. The observable timed sequence ρ o = 2o 1 .9o 2 . 3o 2 .4, 5o 3 .4o 1 .5o 2 .5o 2 .4, 2o 3 is produced by a faulty run of π 0 and by a non-faulty run of π 1 = t 7 .t 8 .t 9 .t 10 .t 11 .t 7 . It belongs to the intersection between the certain polyhedron of π 0 and the safe polyhedron of π 1 .

Based on Proposition 3, the second and final step of the TR-diagnosabilization is finally described in Section 4.2.

DISAMBIGUATION OF CRITICAL PAIR

Section 3 shows that the sources of critical pair, i.e. the reasons of undiagnosability of a system can be divided in two classes: the first is the ambiguities inherent to a path (S(Π o a ) = ∅), the second is the ambiguities coming from the intersection of the safe and certain polyheron abstracting two different paths. As the number of paths and the number of faulty candidate transitions are bounded, there are a bounded number of sources of critical pairs. After enumerating the different sources of critical pairs using the results of the previous section, the proposed method synthetises new time constraints the system must satisfy to delete ambiguities, i.e. to make the system ∆-diagnosable.

∃t f ∈ F π , a Ω f ≤ a t f ≤ b t f ≤ b Ω f
where a t f and b t f are respectively the earliest and latest dates of firing of t f relatively to the start of the system. Solution S1 can be seen as forcing the system to be faulty if its behaviour follows a particuliar support. As for S0, its implementation depends on the transitions involved in the time constraints and their belonging to T p .

For a path (π, Π, Π o ), the constraint set that characterizes the disambiguation from Π a can be written Π ∧ (S0∨S1). Considering that a system contains k ambiguous path (k sequences of transition for which there are inherent ambiguities), the constraints set providing a non-ambiguous solution can be written k-1 j=0.

(Π j ∧ (S0 j ∨ S1 j ).

Example 6. Let's consider T p = {t 0 , t 4 , t 5 , t 7 , t 11 }. For the path π 0 , solution S1 can be implemented as the following constraints: a Ω f ≤ a t0 + a t1 and b t0 + b t1 ≤ b Ω f . As t 0 is parameterized, there is a solution for these constraints: a t0 = b t0 = 6.

Ambiguities from two different paths

Considering two paths (π, Π, Π o ) and (π , Π , Π o ) such that (π, Π o s ) ∩ (π , Π o c ) = ∅, Proposition 3 states that there is a source of critical pairs. This source of critical pairs comes from the fact that for each observable transition of the two paths there is at least one common observable date. In order to delete such an ambiguity, one need:

CONCLUSION

This paper introduces the problem of TR-diagnosabilisation of a system modeled as a safe LTPN and proposes a first resolution method that ensures ∆-diagnosability. Based on a ∆-diagnosability analysis that enumerates the sources of critical pairs, time constraints that delete critical pairs are synthetized. Those constraints are added to the time constraints relative to the structure of the system, and if there is a solution to this constraints set, this solution is a solution for TR-diagnosabilisation.

The proposed method relies on a sufficient condition for TR-diagnosabilisation. Future works will focus on the determination of a necessary and sufficient condition for TRdiagnosabilization and the extension to Ω f -diagnosability.

  θ

  o i ) corresponds to the date of firing of the i-th transition of the sequence (resp. of the observable sequence)). The observable constraint set associated with Π 0 finally is Π o 0

Fig. 3 .

 3 Fig. 3. Faulty and safe areas for a timed fault occurring between a Ω f and b Ω f t.u.A faulty transition candidate can be source of an ambiguity, i.e. it is involved in critical pairs that can be extracted from the same support π. Figure 3 represents this situation. Transition t f is a faulty transition candidate and t o is the first observable transition that is fired after t f in the considered path. a f (resp. b f ) is the earliest (resp. latest) firing date of t f relatively to the start of the system, and a o (resp. b o ) is the earliest (resp. latest) firing date of t o relatively to the firing of t f . The red and green polyhedra correspond to admissible firing of t f and t o in the considered path. The red area corresponds to faulty firing of t f and the green ones correspond to faultless firings. The observation of the system that captures the firing of t f corresponds to the firing of t o , i.e. the first observed date t obs o

Fig. 4 .

 4 Fig. 4. Ambiguous and non-ambiguous polyhedra for the timed fault of Figure 3 that observing t obs o

  a o and b o . Such constraints, if added to the observable projection Π o of the path, lead to the definition of a set of polyhedra representing three different types of run in a path • Π o a = Π o ∪ ambiguous: the set of observable timed sequences leading to an ambiguity • Π o s = Π o ∪ safe the set of observable timed sequences involving safe runs only • Π o c = Π o ∪ certain the set of observable timed sequences involving faulty runs only The existence of critical pairs inherent to one path only is then determined by the following result. Proposition 2. Considering a path (π, Π, Π o ), S(Π o a ) = ∅ iff • there exists a faulty transition candidate t f such that a Ω f ≤ a f ≤ b f ≤ b Ω f , or • for each faulty transition candidate t f , the earliest and latest firing dates of t o are equal (a o = b o ).

4. 1

 1 Ambiguities inherent to a path (S(Π o a ) = ∅)

  ∨ a t0 > b t7 . Using a t0 = b t0 = 6 and b t7 = 4, Θ is 1-diagnosable, so for the set of parametrised transitions T p , the valuation setV d = {I s (t 0 ) = [6, 6], I s (t 4 ) = [1, 2], I s (t 5 ) = [2, 3], I s (t 7 ) = [2, 4], I s (t 11 ) =]4, 5[} is a solution of TR-diagnosabilisation.

  Considering a support π = t 0 . . . t f1 . . . t o f 1 . . . t f2 . . . t fn . . . t m , its faulty transition candidates {t f1 , . . . , t fn }, and suppose that there is at least one faulty transition candidate that induces that S(Π o a ) = ∅. For each t fi , the first observable transition following it in π is denoted t o f i . S0: trivialization of the firing date of t o f i relatively to the firing of t fi for each t fi that is source of an ambiguity S1: enforcement of the ambiguous transition to become always faulty (by adjusting the set of its firing dates to always match the fault behaviour for this particuliar sequence) Lemma 1. Let's consider t fi , t o f i and t uo0 , . . . t uo k the unobservable transitions between t fi and t o f i in π. S0 can be formalized as the set of constraints: Solution S0 can be seen as a determinisation of the time elapsed since the firing of the faulty transition candidate, for each faulty transition candidate. This solution, however, cannot be applied as soon as one of the transitions t o f i , t uo0 , . . . t uo k is not in T p (a transition cannot be parameterized). Consider now solution S1. Lemma 2. Let F π = {t f1 , . . . , t fn } be the set of faulty transition candidates of π. S1 can be formalized as:

	Proposition 2 defines the conditions of emptiness of S(Π o a ).
	As a consequence, the type of adjustments by time restric-
	tion to empty S(Π o a ) are the following ones:

∀j ∈ [0, k], ↓ (t uoj ) =↑ (t uoj ), ↓ (t o f i ) =↑ (t o f i )

  S2: modification for one of the observable transition of π of its earliest observable date such that it becomes greater than the latest observable date of the corresponding transition in π . Lemma 3. Considering two polyhedra (π, Π o c ) and (π , Π o s ) sharing their untimed observable trace, S2 can be formalized as follows. Let (t n+l , t n+l ) be a couple of observable transitions with same label and common firing dates from π and π :To disambiguate pair (π, π ) such that (π, Π s ) ∩ (π , Π c ) = ∅, constraint S2 must be added to the previous constraints. Example 7. Considering the paths π 0 and π 1 = t 7 .t 8 .t 9 .t 10 .t 11 .t 7 , there is an ambiguity as π 0 can be faulty and π 1 is safe. Solution S2 can be implemented as a t7 > b t0

	S2 =	(a t n+l > b t
		set of (t n+l ,t n+l )

n+l ) ∨ (a t n+l > b t n+l ).


domain: spi phys

text:
Mohamed Abdi
email: abdi.mohamed1@live.fr

Meryem Ould-Rouiss

Abdelkader Noureddine

LES of Turbulent Forced Convection of a Non-Newtonian Fluid in a Stationary Pipe: The Mean Quantities

A fully developed forced convection heat transfer of a thermally independent shear thinning (n=0.75) and Newtonian fluids flowing inside a uniform heated axially pipe has been carried out numerically by means of the large eddy simulation (LES) with an extended Smagorinsky model at a simulation's Reynolds and Prandtl numbers equal to Res=4000 and Prs=1 respectively. The present investigation aims to ascertain the accuracy and reliability of the LES laboratory code predicted results and evaluate the effectiveness of the extended Smagorinsky model to resolve and describe the evolution of the main mean flow quantities and thermal statistics in the present computational domain especially at the wall vicinity. The Computations are based on a finite difference scheme, second order accurate in space and in time, the numeric resolution is 65 3 grid points in r, θ and z direction respectively, with length of the domain of 20R. The predicted results show an excellent agreement with the DNS results, the main findings show that the present LES laboratory code can be considered as a powerful tool for predicting the mean thermal quantities of the Non-Newtonian fluid. The reduction in the fluid flow index (n) results in enhancement in the mean axial velocity and a pronounced attenuation in the mean temperature over the radial direction, where leads also to noticeable drop in the average Nusselt number.

Introduction

The turbulent forced convection heat transfer of the Non-Newtonian fluids is of practical importance in many industrial applications for example in paper making, drilling of petroleum products, slurry transportation and processing of food and polymer solutions. a considerable amount of literature has been carried out on the flow of the Newtonian fluid in a straight pipe, where is contains a number of well-documented, either experimentally or numerically by [START_REF] Reich | Fluid flow and heat transfer in an axially rotating pipe-I. Effect of rotation on turbulent pipe flow[END_REF] [2] [3] [4] [START_REF] Ould-Rouiss | Numerical predictions of turbulent heat transfer for air flow in rotating pipe[END_REF].

On the other hand, the turbulent Non-Newtonian fluid in axially pipe has been largely investigated experimentally and numerically over the recent decades, among them [START_REF] Metzner | Flow of nonnewtonian fluids-correlation of the laminar, transition, and turbulent-flow regions[END_REF] [START_REF] Metzner | Non-Newtonian Fluid Flow. Relationships between Recent Pressure-Drop Correlations[END_REF] [8] [START_REF] Pinho | Flow of nonnewtonian fluids in a pipe[END_REF] [10] [START_REF] Gnambode | Large-Eddy simulation of turbulent pipe flow of power-law fluids[END_REF] [START_REF] Singh | The influence of shear-dependent rheology on turbulent pipe flow[END_REF] [START_REF] Singh | The effect of yield stress on pipe flow turbulence for generalised newtonian fluids[END_REF].

Despite the particular importance of the heat transfer of the Non-Newtonian fluids in the above-mentioned engineering application, there is a paucity of scientific literature focusing specifically on the forced convection heat transfer of Non-Newtonian fluids in such issue. Toward this end, the present study seeks to ascertain the accuracy and reliability of the LES laboratory code predicted results and evaluate the accuracy of the employed extended Smagorinsky model to predict the effect of shear thinning flow index on the main thermal statistics, in addition to shed further light on shear thinning rheological and thermal behaviour in the turbulent flow. Toward this end, a LES with an extended Smagorinsky model has been applied to investigate numerically the fully developed turbulent forced convection heat transfer of a shear thinning (n=0.75) and Newtonian fluids in a uniform heated axially stationary pipe at a simulation's Reynolds and Prandtl numbers of Res=4000 and Prs=1 respectively, with an adequate grid resolution of 65 3 grid points in r, θ and z direction respectively and a domain length of 20R . The present paper is organized as: governing equations and numerical procedure are presented in section 2. the mean flow and thermal quantities are presented in section 3 and finally section 4 summarizes the results of this work and draws conclusions.

Governing equations and numerical procedure 2.1 Governing equations

The present study deals with a fully developed turbulent forced convection of a thermally independent shear thinning (n=0.75) and Newtonian (n=1) fluids across a heated pipe with a uniform constant heat flux qw imposed at the pipe wall, by mean of the LES approach with an extended Smagorinsky (Fig. 1), with domain length of 20R at the at a simulation's Reynolds and Prandtl numbers of Res=4000 and Prs=1 respectively.

The filtered equations can be expressed as follows:

0 i i u x ∂ = ∂ (1) 1 1 Re j i j j ij n i i j s i i j i u u u u u dP t x x x x x x τ γ -     ∂ ∂ ∂ ∂ ∂ ∂ + = - + + +       ∂ ∂ ∂ ∂ ∂ ∂ ∂       & (2) ( ) 2 1 Re Pr j j z w j s s k k d u T u T t x dz x x Θ ∂Θ ∂ ∂ Θ + Θ - - = ∂ ∂ ∂ ∂ (3)
The overbar symbol (¯) denotes the filtering operation, Re s , s Pr are the Reynolds number and Prandtl number of the simulation and are defined respectively by:

Re s CL U R ρ µ = , s CL Pr R U µ αρ = .
The dimensionless temperature is defined as:

( ) ( ) ( )
, , ,

w ref T z T r z t T θ Θ = - (4)
Tref presents the reference temperature and in defined as

ref w p CL T q C U ρ =
, where Tw is the pipe wall temperature and is an average in time and periodic directions.

Figure 1 computational domain

Numerical procedure

The governing equations were discretized on a staggered mesh in cylindrical coordinates with a computational length in the axial direction 20R. The numerical integration was performed by using a finite difference scheme, second-order accurate in space and in time. the time-advancement employs a fractionalstep method. a third-order Runge-Kutta explicit scheme and a Crank-Nicholson implicit scheme were used to evaluate the convective and diffusive terms, respectively. The above mathematical model was implemented in a finite difference laboratory code. The grid 65 3 grid points in axial, radial and circumferential directions respectively, was found to provide an accurate prediction of the turbulence statistics, in agreement with the available data of the literature, and to give a good compromise between the required CPUtime and accuracy.

A periodic boundary condition has been applied to the axial and circumferential directions, and a usual noslip boundary condition on the pipe wall, in additional to a uniform heat flux was imposed on the pipe wall as a thermal boundary condition. As for the grid resolution of the present mesh, uniform computational grid was applied to the axial and circumferential directions, in the radial direction, non-uniform meshes specified by a hyperbolic tangent function, the various parameter settings for mesh and LES simulations are summarized in Tab.1.

Results and discussion

A large eddy simulation with an extended Smagorinsky model has been applied to a fully developed turbulent forced convection heat transfer of a shear thinning (n=0.75) and Newtonian (n=1) fluids at simulation's Reynolds number and Prandtl number of 4000 and 1 respectively. In the present section we will briefly analyse and discuss the LES obtained to ascertain the accuracy and reliability of the laboratory code predicted results, in addition to know to what extent the LES with the extended Smagorinsky model be able to predict the effect of shear thinning flow index on the main flow and thermal quantities, especially the mean axial velocity and mean temperature. For the validation purpose, the predicted LES results are compared reasonably with the available results of literature: experimental and numerical data of Rudman et al. [START_REF] Rudman | Turbulent pipe flow of shearthinning fluids[END_REF] of a shear thinning fluid (n=0.75) in a turbulent pipe flow.

The Fig. 2 compares the predicted mean axial velocity profile with the experimental data obtained at generalised Reynolds number of Reg=7027 and DNS data at Metzner-Reed Reynolds number of ReMR=3935. As shown in the Fig. 2, the predicted profile is in an excellent agreement with the other profiles over the entire pipe radius, where the predicted profile almost coincides with the experimental and DNS profiles in each of the viscous sublayer, buffer and logarithmic layer. It should be noted here that the little marked discrepancy may be the difference in the Reynolds number value and the numerical solution procedure. In the viscous sublayer (0≤Y + ≤5), the velocity profile coincides and agrees with the universal linear law U + =Y + , the mean axial velocity remains constant denoting a linear velocity distribution in this region as (Fig. 3). Beyond the buffer region the mean axial velocity enhances progressively further away from the wall towards the core region, where the inertia force dominants pronouncedly compared to the viscous one out of the viscous sublayer.

On the other hand, it can be seen also that the velocity profile of the shear thinning fluid coincides completely with that of the Newtonian one in the vicinity of the pipe wall, it can be said that the velocity profile are nearly independent of the rheological model, where the flow index influence is limited near the pipe wall up to approximately (Y + ~30). At the larger wall distance Y + >30, the mean axial velocity profile of the Newtonian fluid in accordance with the universal logarithmic law U + =2.5lnY + +5.5 in the logarithmic region (30≤Y + ≤200), while the shear thinning profile lies above the universal law in this region. Beyond Y+~30 the predicted profiles deviate significantly from each other with the distance from the wall away from the wall towards the pipe centre. As shown in Fig. 3 the shear thinning fluid profile is somewhat larger than that corresponding of the Newtonian one where this trend is more pronounced as closes to the core region, it is evident that this deviation in the velocity profiles is due to the difference in the fluid apparent viscosity.

Figure 3 Mean axial velocity

In turn, the Fig. 4 presents the streamwise velocity profiles along the pipe radius of the shear thinning and Newtonian fluids, in addition to the analytical velocity profile in the laminar regime for the both fluids scaled by the analytical laminar centreline velocity (UCL=(3n+1)Ub/(n+1)), against the distance from the wall, normalized by the pipe radius (R). It can be seen from Fig. 4 that the velocity profiles are characterised by a parabolic shape along the pipe regions, as mentioned above the velocity of the shear thinning (n=0.75) is more significant than the Newtonian one especially in the logarithmic and core region, where this is due to the difference in the fluid apparent viscosity.

Figure 4 Mean axial velocity

Temperature profile

In order to examine the fluid flow index on the mean thermal quantities, and describe the heat transfer between the heated pipe wall and the fluids, the following paraphrases analyse and discuss the mean temperature revolution (Fig. 5) and (Fig. 6) in a heated pipe under a with a constant uniform heat flux qw imposed at the pipe wall as thermal boundary condition, where the Prandtl number of the working fluid was assumed to be Prs=1.

The Fig. 5 presents the shear thinning (n=0.75) and Newtonian (n=1) fluids temperature (Θ) profiles along the pipe radius (R) scaled by the reference temperature (Tref), against the distance from the wall in wall units Y + at Res=4000, where the dash lines represent the universal temperature distributions in the conductive sublayer and in the logarithmic layer. Whereas the Fig. 6 illustrates the temperature profiles scaled by the bulk temperature (Θb) versus the radial coordinates (r) scaled by the pipe radius (R).

It can be seen from Fig. 5 that the mean temperature (Θ) is enhanced gradually further away from the wall towards the core region with the wall distance Y + , along the pipe radius over the different flow regions. In other words, the fluid temperature (T) attenuates progressively far away from the pipe wall, the predicted mean temperature exhibits its maximum and minimum values at the pipe wall and the pipe centreline respectively.

It can be seen also that the shear thinning and Newtonian fluids have the same trend of temperature distribution along the pipe radius, the both profiles agree and coincide with the universal linear law Θ + =PrY + in the vicinity of the wall (0≤Y + ≤1). Beyond (Y + ~2) the shear thinning profile deviates significantly from the universal linear law and the profile of the Newtonian fluid, where the Newtonian profile is somewhat larger than that of the shear thinning one in the conductive sublayer (0≤Y + ≤5) and in the logarithmic layer (30≤Y + ≤200), this trend is more apparent as the distance from the wall is increased.

It is worth noting that the flow index affects considerably on the heat transfer between the pipe wall and the fluid flowing inside the heated pipe along the pipe radius especially out of the conductive sublayer towards the pipe centre as shown in Fig. 6, where this influence is attributed to the fluid apparent viscosity.

Conclusion

The present study reports on numerical investigation of a fully developed turbulent forced convection heat transfer of a thermally independent shear thinning (n=0.75) fluid flowing inside a uniform heated pipe under an uniform heat flux, by applying a large eddy simulation with extended Smagorinsky model, at simulation Reynolds and Prandtl numbers of 4000 and 1 respectively, In order to ascertain the accuracy and reliability of the LES laboratory code predicted results and evaluate the reliability of the extended Smagorinsky model to predict the main mean flow quantities and thermal statistics such as the mean streamwise velocity, mean temperature and the Nusselt number. The major conclusions of this research will be summarized:

The accuracy and reliability of the laboratory code predicted results and numerical solution procedure have been ascertained by comparing the main predicted results with those available in the literature, these findings clearly indicate that the present code can be considered as a powerful tool, where the present LES with the extended Smagorinsky model shows a great promise in predicting the thermal turbulent statistics of the turbulent forced convection heat transfer of the power law fluids in the present configuration.

On the other hand, the reduction in the fluid flow index resulted in a pronounced enhancement in the mean streamwise velocity profile along the radial coordinates especially in the logarithmic region, this deviation was raised because the difference in the fluid apparent viscosity. In turn, this reduction in the fluid index indices a marked attenuation in the mean temperature along the pipe radius in addition to a noticeable drop in the average Nusselt number, leading to attenuate the energy transfer between the fluid and the pipe wall.

ERMA' 19 Figure 2

 192 Figure 2 Validation

Figure 5 Figure 6 Figure 7

 567 Figure 5 Mean Temperature Profile

Table 1 .

 1 parameters of present LES simulations Res=4000

	Parameters	n=0.75	n=1
	z + ∆		69.89	49.75
	r θ + ∆	21.95	15.63
	∆	r +	min	0.0506	0.0360

cl U U τ .