Kim Guldstrand Larsen

Axel Legay
email: axel.legay@irisa.fr

Louis-Marie Traonouez

Andrzej Wasowski
email: wasowski@itu.dk

Andrzej W Ąsowski

Robust Specification of Real Time Components

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

For long, software engineers have practiced component-oriented software construction, building systems from modules that only depend on each other in well specified ways. Foundational research follows up by developing trustworthy rigorous methods for component-oriented design. In concurrency theory this includes compositional design (specification theories, stepwise-refinement) and compositional model checking. Akin to algebraic specifications, specification theories provide a language for specifying component interfaces together with operators for combining them, such as parallel (structural) composition and conjunction (logical composition).

Specification theories integrate prior results to provide a uniform design method. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we have proposed the first complete specification theory for timed systems. We build on an input/output extension of the classical timed automata model-inputs are used to represent behaviors of the environment and outputs represent the behavior of the component. The theory is equipped with a game-based semantic, which is used to define all the good operations for such specification theory, including satisfaction (can a specification be implemented), refinement (how to compare specifications), logical composition (computing the intersection of two sets of implementations), structural composition (building large components from smaller ones), and quotient (synthesizing a component in a large design).

The theory in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] is equipped with a consistency check that allows to decide whether a specification can indeed be implemented. Unfortunately, this check does not take imprecision of the physical world into account, that is consistency can be used to synthesize an implementation that may be not robust with respect to variations of the environment. In practice, one would want to guarantee that a perturbation of the implementation still matches the requirements of the specification. Providing a solution to this problem in the setting of timed I/O specifications is our objective in this paper.

Our contributions include:

-We propose a notion of implementation of a specification that is robust with respect to a given perturbation in the delay before an action. Such perturbation is fixed in advance, which is a reasonable assumption as sensitivity with respect to perturbation of the environment is generally given in the description of the component that is provided by the manufacturer. The concept of robust implementation is lifted to a robust satisfaction operation that takes variations of timed behaviors into account when checking whether the implementation matches the requirement of the specification. -We propose a consistency check for robust satisfaction. This new check relies on an extension of the classical timed I/O game to the robust setting. In [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], Chatterjee et al.

showed that problems on robust timed games can be reduced to classical problems on an extended timed game. We modify the original construction of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] to take the duality of inputs and outputs into account. Then, we show how our new game can be used to decide consistency in a robust setting as well as to synthesize a robust implementation from a given specification. -Finally, classical compositional design operators are lifted to the robust setting.

One of the nice features of our approach is that this does not require to modify the definitions of the operators themselves and that all the good properties of a specification theory (including independent implementability) are maintained.

To the best of our knowledge, this paper presents the first complete theory for robust timed specification. While the presentation is restricted to the theory of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we believe that the approach works for any timed specifications. Our experience with industrial projects shows that such realistic design theories are of clear interest [START_REF]The COMBEST Consortium: Combest[END_REF][START_REF]The SPEEDS Consortium: Speeds[END_REF][START_REF] Badouel | Contract theories for embedded systems : A white paper[END_REF].

State of The Art. None of the existing specification theories for timed systems allows for the treatment of robustness.

Various works have considered robustness for timed automata using logical formulas as specifications (and neglecting compositional design operators). The robust semantics for timed automata with clock drifts has been introduced by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF]. The problem has been linked to the implementation problem in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF], which introduced the first semantics that modeled the hardware on which the automaton is executed. In this work, the authors proposed a robust semantics of Timed Automata called AASAP semantics (for "Almost As Soon As Possible"), that enlarges the guards of an automaton by a delay ∆. This work has been extended in [START_REF] Wulf | Robust safety of timed automata[END_REF] that proposes another robust semantics with both clock drifts and guard enlargement. Extending [START_REF] Puri | Dynamical properties of timed automata[END_REF] they solve the robust safety problem, defined as the existence of a non-null value for the delays. They show that in terms of robust safety the semantics with clock drifts is just as expressive as the semantics with delay perturbation. We extend the work of [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF][START_REF] Wulf | Robust safety of timed automata[END_REF] by considering compositional design operators, stepwise-refinement, and reasoning about open systems (only closed system composition were considered so far).

We solve games for consistency and compatibility using a robust controller synthesis approach largely inspired by Chatterjee et al. [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], who provide synthesis techniques for robust strategies in games with parity objectives. Driven by the fact that consistency and compatibility are safety games, we restrict ourselves to safety objectives, but we extend [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] by allowing negative perturbation of delays.

We proceed by introducing the background on Timed Specifications (Section 2). In Section 3 we introduce methods for solving robust time games that arise in our specification theory. These methods are used in Sections 4-5 to reason about consistency, conjunction, parallel composition and synthesis of specifications and robust implementations of real time components.

Background on Timed I/O Specifications

We now recall the definition of Timed I/O specifications [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. We use Z (respectively N) for the set of all integer numbers (resp. non-negative integers), R for the set of all real numbers, and R ≥0 (resp. R >0 ) for the non-negative (resp. strictly positive) subset of R. Rational numbers are denoted by Q, and their subsets are denoted analogously. For x ∈ R ≥0 , let x denote the integer part of x and x denote its fractional part.

In the framework of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], specifications and their implementations are semantically represented by Timed I/O Transition Systems (TIOTS) that are nothing more than timed transition systems with input and output modalities on transitions. Later we shall see that input represents the behaviors of the environment in which a specification is used, while output represents behaviours of the component itself. In what follows, we assume that any TIOTS satisfies the following conditions:

time determinism: whenever s A run ρ of a TIOTS S from its state s 1 is a sequence

s 1 a1 -→ S s 2 a2 -→ S . . . an --→ S s n+1 such that for all 1 ≤ i ≤ n s i ai -→ S s i+1 .
We write Runs(s 1 , S) for the set of runs of S starting in s 1 and Runs(S) for Runs(s 0 , S). We write States(ρ) for the set of states reached in ρ, and if ρ is finite last(ρ) is the last state occurring in ρ.

A TIOTS S is deterministic iff ∀a ∈ Σ S ∪ R ≥0 , whenever s a -→ S s and s a -→ S s , then s = s . It is input-enabled iff each of its states s ∈ St S is input-enabled: ∀i? ∈ Σ S i . ∃s ∈ St S . s i? -→ S s . We say that S is output urgent iff ∀s, s , s ∈ St S if s o! -→ S s and s d -→ S s then d = 0. Finally, S verifies the independent progress condition iff either (∀d ≥ 0.s d -→ S ) or (∃d ∈ R ≥0 .∃o! ∈ Σ S o .s d -→ S s and s o! -→ S )
. TIOTS are syntactically represented by Timed I/O Automata (TIOA). Let X be a finite set of clocks. A clock valuation over X is a mapping X → R ≥0 (thus R X ≥0 ). Given a valuation u and d ∈ R ≥0 , we write u+d for the valuation in which for each clock x ∈ X we have (u+d)(x) = u(x)+d. For Y ⊆ X, we write u[Y → 0] for a valuation agreeing with u on clocks in X \ Y , and giving 0 for clocks in Y . Let C(X) denote all clock constraints ϕ generated by the grammar ψ ::

= x ≺ k | x -y ≺ k | ψ ∧ ψ, where k ∈ Q, x, y ∈ X and ≺ ∈ {<, ≤, >, ≥}. For ϕ ∈ C(X) and u ∈ R X ≥0 , we write u |= ϕ if u satisfies ϕ. Let ϕ denote the set of valuations {u ∈ R X ≥0 | u |= ϕ}. A subset Z ⊆ R X ≥0 is a zone if Z = ϕ for some ϕ ∈ C(X). Definition 2. A Timed I/O Automaton is a tuple A = (Loc, q 0 , Clk, E, Act, Inv), where Loc is a finite set of locations, q 0 ∈ Loc is the initial location, Clk is a finite set of clocks, E ⊆ Loc × Act × C(Clk) × 2 Clk × Loc is a set of edges, Act = Act i ⊕ Act o is a finite set of actions, partitioned into inputs (Act i ) and outputs (Act o ), Inv : Loc → C(Clk) is a set of location invariants.
Without loss of generality we assume that invariants of a location are always included in the guards of the edges that are incident with the location. We also assume that guards are satisfiable (for any guard ϕ the set ϕ is non-empty).

A universal location, denoted l u , in a TIOA accepts every input and can produce every output at any time. Location l u models an unpredictable behavior of a component.

The semantics of a TIOA A = (Loc, q 0 , Clk, E, Act, Inv) is a TIOTS A sem = (Loc × R Clk ≥0 , (q 0 , 0), Act, →), where 0 is a constant function mapping all clocks to zero, and → is the largest transition relation generated by the following rules:

-Each edge (q, a, ϕ, λ, q ) ∈ E gives rise to (q, u) a -→(q , u ) for each clock valuation u ∈ R Clk ≥0 such that u |= ϕ and u = u[λ → 0] and u |= Inv(q ). -Each location q ∈ Loc with a valuation u ∈ R Clk ≥0 gives rise to a transition (q, u)

d -→(q, u + d) for each delay d ∈ R ≥0 such that u + d |= Inv(q).
Since TIOTSs are infinite size they cannot be directly manipulated by computations. Usually symbolic representations, such as region graphs [START_REF] Alur | A theory of timed automata[END_REF] or zone graphs, are used as data structures that finitely represent semantics of TIOAs. Let M be the greatest (in absolute value) integer constant that appears in the guards of a TIOA 4 . A clock region is an equivalence class of the relation ∼ on clock valuations such that u ∼ v iff the following conditions hold:

-∀x ∈ Clk, either u(x) = v(x) , or u(x) > M and v(x) > M , -∀x, y ∈ Clk, ∀c ∈ [-M, M ], u(x) -u(y) ≤ c iff v(x) -v(y) ≤ c, -∀x ∈ Clk if u(x) ≤ M then u(x) = 0 iff v(x) = 0,
We write r for the direct time successor of the region r, if such exists. The region graph of a TIOA

A is G = (R A , - → G ), where R A = {(q, r) | ∃(q, u) ∈ St A sem . u ∈ r} is the set of regions, and - → G ⊆ R A × (Act ∪ {τ }) × R A , such that (q, r) τ -→ G (q, r ) iff r |= Inv(q),
and (q, r) a -→ G (q , r ) iff (q, u) a -→(q , u ) for some u ∈ r and u ∈ r . Basics of the Timed Specification Theory. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], timed specifications and implementations are both represented by TIOAs satisfying additional conditions: Definition 3. A specification S is a TIOA whose semantics S sem is deterministic and input-enabled. An implementation I is a specification whose semantics I sem additionally verifies the output urgency and the independent progress conditions.

Example 1. Figure 1a presents a specification of a researcher. It accepts either coffee (coff) or tea in order to produce publications (pub). If tea is served after a too long period the researcher falls into an error state represented by a universal state l u . An individual researcher is an implementation of this specification. One example is presented in Figure 1b.

In specification theories, a refinement relation plays a central role. It allows to compare specifications, and to relate implementations to specifications. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], as well as in [START_REF] De Alfaro | Interface automata[END_REF][START_REF] De Alfaro | Interface-based design[END_REF][START_REF] Bulychev | Efficient on-the-fly algorithm for checking alternating timed simulation[END_REF], refinement is defined in the style of alternating (timed) simulation: Definition 4 (Refinement). An alternating timed simulation between TIOTS S = (St S , s 0 , Σ S , → S ) and

T = (St T , t 0 , Σ T , → T ) is a relation R ⊆ St S × St T such that (s 0 , t 0 ) ∈ R and for every (s, t) ∈ R -If t i? -→ T t for some t ∈ St T , then s i? -→ S s and (s , t ) ∈ R for some s ∈ St S -If s o! -→ S s for some s ∈ St S , then t o! -→ T t and (s , t ) ∈ R for some t ∈ St T -If s d -→ S s for d ∈ R ≥0 , then t d -→ T t and (s , t ) ∈ R for some t ∈ St T
We write S ≤ T if there exists an alternating simulation between S and T . For two TIOAs S and T , we say that S refines T , written S ≤ T , iff S sem ≤ T sem .

Definition 5 (Satisfaction). An implementation I satisfies a specification S, denoted I sat S, iff I sem ≤ S sem . We write S mod for the set of all implementations of S, so S mod = {I | I sat S and I is an implementation}.

The reader might find it surprising that in a robust specification theory we refrain from adjusting the refinement to account for imprecision of implementations when comparing specifications. Our basic assumption is that specifications are precise mathematical objects that are not susceptible to imprecision of execution. In contrary, implementations can behave imprecisely when executed, so in Section 3 we will introduce an extension of Def. 5 that takes this into account. It is a fortunate property of Def. 4 that we do not need to modify it in order to reason about robust implementations (Property 3 in Sect. 3).

In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], we have reduced refinement checking to finding winning strategies in timed games. In the reminder of this section, we recall the definition of such games and show how they can be used to check consistency. Timed games also underly other operations such as conjunction, composition, and quotient [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], which will be illustrated in Sect. 4-5.

Timed Games for Timed I/O Specifications. TIOAs are interpreted as two-player real-time games between the output player (the component) and the input player (the environment). The input plays with actions in Act i and the output plays with actions in Act o . A strategy for a player is a function that defines her move at a certain time (either delaying or playing a controllable action). A strategy is called memoryless if the next move depends solely on the current state. We only consider memoryless strategies, as these suffice for safety games. For simplicity, we only define winning strategies for the output player (i.e. output is the verifier). Definitions for the input player are obtained symmetrically. Definition 6. A memoryless strategy f for the output player on the TIOA A is a function

St A sem → Act o ∪ {delay}, such that whenever f (s) ∈ Act o then s f (s)
--→s for some s , and whenever f (s) = delay then s d -→s for some d > 0 and state s .

The restricted behavior of the TIOA when one player applies a specific strategy is defined as the outcome of the strategy.

Definition 7.

Let A be a TIOA, f a strategy over A for the output player, and s a state of A sem . The outcome Outcome o (s, f ) of f from s is the subset of Runs(s, A sem ) defined inductively by:

-s ∈ Outcome o (s, f ), -if ρ ∈ Outcome o (s, f ) then ρ = ρ a -→s ∈ Outcome o (s, f ) if ρ ∈ Runs(s, A sem )
and one the following conditions hold:

1. a ∈ Act i , 2. a ∈ Act o and f (last(ρ)) = a, 3. a ∈ R ≥0 and ∀d ∈ [0, a[.∃s .last(ρ) d -→s and f (s ) = delay. -ρ ∈ Outcome o (s, f ) if ρ infinite
and all its finite prefixes are in Outcome o (s, f ).

A winning condition for a player in the TIOA A is a subset of Runs( A sem ). In safety games the winning condition is to avoid a set Bad of "bad" states (without lost of generality we assume these "bad" states correspond to a set of entirely "bad" locations). Formally, the winning condition is

WS o (Bad) = {ρ ∈ Runs( A sem ) | States(ρ)∩Bad = ∅}. A strategy f for output is winning from state s if Outcome o (s, f ) ⊆ WS o (Bad).
A state s is winning if there exists a winning strategy from s. The game (A, WS o (Bad)) is winning if the initial state is winning. Solving this game is decidable [START_REF] Maler | On the synthesis of discrete controllers for timed systems (an extended abstract)[END_REF][START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF][START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF].

Strategies can also be defined symbolically, using the region graph introduced in the previous section. For a region (q, r), if f (q, r) = delay then (q, r)

τ -→ G (q, r ), and if f (q, r) ∈ Act o then ∃(q , r ).(q, r) a -→ G (q , r ). An outcome of f is then a run in the region graph, such that if ρ ∈ Outcome o ((q, r), f ) then ρ = ρ a -→(q , r ) ∈ Outcome o ((q, r), f ) if last(ρ) a -→ G (q , r
), and either a ∈ Act i , or a ∈ Act o and f (last(ρ)) = a, or a = τ and f (last(ρ)) = delay.

Maximum Strategies in Timed Games as Operators on Timed Specifications. We sketch how timed games can be used to establish consistency of a timed specifications.

An immediate error occurs in a state of a specification if the specification disallows progress of time and output transitions in a given state-such a specification will break if the environment does not send an input. For a specification S we define the set of immediate error states err S ⊆ St S sem as:

err S = s (∃d. s d -→) and ∀d ∀o! ∀s . s d -→s implies s o! -→
It follows that no immediate error states can occur in implementations, since they verify independent progress. In [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] we show that S is consistent iff there exists a winning strategy for output in the safety game (S, WS o (err S )). Moreover, the maximum consistent part of S corresponds to the maximum wining strategy for output in this game.

Conjunction of two specifications is found as a maximal strategy for output in a safety game on the product state space to avoid immediate errors. Similarly, optimistic parallel composition of two specifications is computed as a maximum strategy for input in a safety game over the product state space; and a quotient of two specifications is found as a maximum strategy for output in another safety game. Optimistic composition means that two specifications are compatible if there exists at least one environment, in which they can avoid error states. Details can be found in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF].

Robust Timed I/O Specifications

We now define a robust extension of our specification theory. An essential requirement for an implementation is to be realizable on a physical hardware, but this requires admitting small imprecisions characteristic for physical components (computer hardware, sensors and actuators). The requirement of realizability has already been linked to the robustness problem in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] in the context of model checking. In specification theories the small deficiencies of hardware can be reflected in a strengthened satisfaction relation, which introduces small perturbations to the timing of implementation actions, before they are checked against the requirements of a specification-ensuring that the implementation satisfies the specification even if its behavior is perturbed.

We first formalize the concept of perturbation. Let ϕ ∈ C(X) be a guard over the set of clocks X. The enlarged guard ϕ ∆ is constructed according to the following rules:

-Any term x i ≺ n i of ϕ with ≺ ∈ {<, ≤} is replaced by x i ≺ n i +∆ -Any term x i n i of ϕ with ∈ {>, ≥} is replaced by x i n i -∆
Similarly, the restricted guard ϕ ∆ is using the two following rules:

-Any term x i ≺ n i of ϕ with ≺ ∈ {<, ≤} is replaced by x i ≺ n i -∆ -Any term x i n i of ϕ with ∈ {>, ≥} is replaced by x i n i +∆.
Notice that for a for a clock valuation u and a guard ϕ, we have that u |= ϕ implies u |= ϕ ∆ , and u |= ϕ ∆ implies u |= ϕ, and ϕ ∆ ∆ = ϕ ∆ ∆ = ϕ. Perturbed Implementation and Robust Timed I/O Specifications. We lift the perturbation to implementation TIOAs. Given a jitter ∆, the perturbation means a ∆-enlargement of invariants and of output edge guards. Guards on the input edges are restricted by ∆:

Definition 8. For an implementation I = (Loc, q 0 , Clk, E, Act, Inv) and ∆ ∈ Q >0 , the ∆-perturbation of I is the TIOA I ∆ = (Loc ∪ {l u }, q 0 , Clk, E , Act, Inv ), such that:

-Every edge (q, o!, ϕ, λ, q ) ∈ E is replaced by (q, o!, ϕ ∆ , λ, q ) ∈ E , -Every edge (q, i?, ϕ, λ, q ) ∈ E is replaced by (q, i?, ϕ ∆ , λ, q ) ∈ E , -Every invariant Inv(q) is replaced by Inv (q) = Inv(q) ∆ , -∀q ∈ Loc. ∀i? ∈ Act i . (q, i?, ϕ u , ∅, l u ) ∈ E with ϕ u = ¬ (q,i?,ϕ,λ,q )∈E ϕ ∆ .

I ∆ is not necessarily action deterministic, as output guards are enlarged. However it is input-enabled, since by construction (the last case above), any input not accepted after restricting input guards is redirected to the universal location l u . Also I 0 equals I.

In essence, we weaken the constraints on output edges, and strengthen the constraints on input edges. This is consistent with the game semantics of specifications: perturbation makes the game harder to win for the verifier. Since the gaps created by strengthening input guards are closed by edges to the universal location, the implementation becomes less predictable. If an input arrives close to the deadline, the environment cannot be certain if it will be handled precisely as specified. Enlargement of output guards has a similar effect. The environment of the specification has to be ready that outputs will arrive slightly after the deadlines.

Such considerations are out of place in classical robustness theories for model checking, but are crucial when moving to models, where input and output transitions are distinguished. For example, in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] the authors propose a robust semantics for timed automata. Their maximal progress assumption is equivalent to the output urgency condition of our implementations. However, in [START_REF] Wulf | Almost ASAP semantics: from timed models to timed implementations[END_REF] both input and output guards are increased, which is suitable for the one-player setting, but incompatible with the contravariant nature of two-player games. Such enlargement would not be monotonic with respect to the alternating refinement (Def. 4), while the perturbation of Def. 8 is monotonic.

We are now ready to define our notion of robust satisfaction: Definition 9. An implementation I robustly satisfies a specification S given a delay ∆ ∈ Q ≥0 , denoted I sat ∆ S, iff I ∆ ≤ S. We write S ∆ mod for the set of all ∆-robust implementations of S, such that S ∆ mod = {I | I sat ∆ S ∧ I is an implementation}.

Property 1. Let I be an implementation and 0 ≤ ∆ 1 < ∆ 2 . Then I ≤ I ∆1 ≤ I ∆2 .

In addition, we obtain the following by transitivity of the refinement:

Property 2.
Let S be a specification and

∆ 1 ≤ ∆ 2 , then S ∆2 mod ⊆ S ∆1 mod ⊆ S mod .
Property 3. Let S and T be specifications and 0 ≤ ∆, then S ≤ T =⇒ S ∆ mod ⊆ T ∆ mod .

We now turn to the problem of deciding whether a specification is robustly consistent:

Definition 10. Let S be a specification and ∆ ∈ Q >0 , then S is ∆-robust consistent if there exists an implementation I such that I sat ∆ S.

Like in the non-robust case, deciding consistency and performing operations on specifications are reducible to solving games. But now, we will need to make the games aware of the robustness conditions. In the rest of this section, we propose a definition for such games. Then, in Sections 4 and 5, we show how they can be used to perform classical operations on specifications.

Example 2. Figure 2 presents the ∆-perturbation of the researcher implementation presented in Fig. 1b. One can check that this implementation robustly satisfies the specification of Fig. 1a for any ∆ ∈ ]0, 1].

Robust Timed Games for Timed I/O Specifications. We first define robust strategies that guarantee winning even if subject to bounded timing perturbations. We then propose a technique for finding such strategies. We start with the construction of syntactic outcome that represents game outcomes as TIOAs. We rely on the region graph construction in the definition of syntactic outcome, but any stable partitioning of the state-space could serve this purpose, and would be more efficient in practice. Definition 11. Let A = (Loc, q 0 , Clk, E, Act, Inv) be a TIOA and f a strategy over A for output. The TIOA A f = (R A , (q 0 , r 0 ), Clk ∪ {z}, E, Act ∪ {τ }, Inv) is built by decorating the region graph G = (R A , -→ G ) of A, using the original clocks of A and an additional clock z to impose output urgency. For each region (q, r), the incident edges and the invariant are defined as follows:

-Inv(q, r) = Inv(q) ∧ (r ∨ r ); -If (q, r) τ -→ G (q, r ) then ((q, r), τ, r , {z}, (q, r )) ∈ E; -For each edge (q, i?, ϕ, λ, q ) ∈ E, if (q, r) i?

-→ G (q , r ) then ((q, r), i?, ϕ, λ ∪ {z}, (q , r )) ∈ E; -If f (q, r) = o!, then Inv(q, r) = r ∧ {z = 0}, and for each edge (q, o!, ϕ, λ, q

) ∈ E, if (q, r) o! -→ G (q , r ), then ((q, r), o!, ϕ, λ ∪ {z}, (q , r )) ∈ E.
This construction captures the semantic outcome of the game in the following sense:

Proposition 1. Let (A, W ) be a timed safety game and f be a strategy for output. Then a run ρ in the region graph G of A is in Outcome o ((q, r), f ) iff ρ is an untimed run of A f starting from region (q, r).

In a robust timed game we seek strategies that remain winning after perturbation by a delay ∆. The perturbation is defined on the syntactic outcome of the strategy, by enlarging the guards for the actions of the verifier. We write A o ∆ (resp. A i ∆ ) for the TIOA where the guards of the output (resp. input) player and the invariants have been enlarged by ∆.

Definition 12. For a timed game (A, W ), a strategy f for output is ∆-robust winning if it is winning when the moves of output are perturbed, i.e. Runs(

A f o ∆ sem ) ⊆ W . 5
As proposed in [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], robust timed games for a bounded delay can be reduced to classical timed games by a syntactic transformation of the game automaton. Here, we propose a modified version of the construction that respects the duality between inputs and outputs: Definition 13. Let A = (Loc, q 0 , Clk, E, Act, Inv) be TIOA and a ∆ ∈ Q >0 , the robust game automaton A ∆ rob = ( Loc, q 0 , Clk ∪ {y}, E, Act, Inv) uses an additional clock y and is constructed according to the following rules:

-Loc ⊆ Loc, and for each location q ∈ Loc and each edge e = (q, o!, ϕ, λ, q ) ∈ E, two locations q α e and q β e are added in Loc. The invariant of q is unchanged; the invariants of q α e and q β e are y ≤ ∆. -For each action o! ∈ Act o , an additional action o? is added in Act i .

-Each edge e = (q, i?, ϕ, λ, q ) ∈ E gives rise to the following edges in E:

(q, i?, ϕ, λ ∪ {y}, q ), (q α e , i?, ϕ, λ ∪ {y}, q ) and (q β e , i?, ϕ, λ ∪ {y}, q ). -Each edge e = (q, o!, ϕ, λ, q ) ∈ E gives rise to the following edges in E:

(q, o!, ϕ 2∆ , {y}, q α e ), (q α e , o!, {y = ∆}, {y}, q β e ), (q α e , o?, {y ≤ ∆}, λ ∪ {y}, q ) and (q β e , o?, {y ≤ ∆}, λ ∪ {y}, q ), where ϕ 2∆ is constructed from ϕ by restricting upper bound constraints by 2∆.

The construction is demonstrated in Fig 3 . The output player can propose a move in the time interval ϕ ∆ (which is done in two steps: first playing o! in the time interval ϕ 2∆ and then a second firing after ∆ time units), but the input player can perturb this move by choosing a smaller or greater delay to perform the action.

The construction shall serve as a tool for deciding robust consistency, synthesizing a robust implementation, and other operations of the specification theory with robustness.

Theorem 1. For a timed safety game (A, W ), if f is a winning strategy for output in the robust game (A ∆ rob , W ), then the following strategy f is a ∆-robust winning strategy for output in the game (A, W ):

∀(q, r) ∈ R A , f (q, r) = o! if ∃e.f (q α e , r) = o!, where r is a region of R A ∆
rob , and r its projection on R A 6 , otherwise f (q, r) = delay.

5 Technically, we assume that runs in Runs( A f o ∆ sem ) abstract τ transitions 6 To this end the region graph of A must be computed with ∆ as the lowest constant. Our method and our notion of robust strategy guarantees non-zenoness for the synthesized strategies. Indeed by allowing the opponent to perturb the verifier by ∆ or -∆ we impose that the verifier only performs non-null delay actions. Later, in the context of timed specifications, this ensures realizability of implementations. Also non-Zeno environements are used as witnesses of compatibility in optimistic composition, which could have happened in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], which ignored Zeno-problems altogether.

Robust Consistency and Conjunction

We now provide a method to decide the ∆-robust consistency of a specification and synthesize robust implementations by solving a robust timed safety game, in which the output player must avoid a set of immediate error states. From there, the computation of a robust strategy gives a method to synthesize a robust implementation of the specification.

Intuitively a specification is ∆-robust with respect to input i?, if between enabling of any two i? edges at least 2∆ time passes, during which the reaction to i? is unspecified. So, if the two transitions triggers ∆-too-late and ∆-too-early (respectively), there is no risk that the reaction is resolved non-deterministically in the specification.

In our input-enabled setup, lack of reaction is modeled using transitions to the universal (unpredictable) state. Formally, we say that ∆-robust specifications should admit ∆-latency of inputs. A state (q, u) verifies the ∆-latency condition for inputs, iff for each edge e = (q, i?, ϕ, c, q ), where q = l u and e is enabled in (q, u) we have: ∀d ∈ [0, 2∆]. ∀e = (q, i?, ϕ, c, q ). if e = e and (q, u) d -→(q, u + d) and e is enabled in (q, u + d) then q = l u For a specification S, the safety objective for the robust consistency game is to avoid the set of states of error states err S ∆ such that (q, u) ∈ err S ∆ iff (q, u) violates independent progress or ∆-latency for inputs, so:

-Violates independent progress: (∃d ∈ R ≥0 .(q, u) d ) and (∀d∀o!.(q, u)

d -→(q, u + d) ⇒ (q, u + d) o! ),
-Violates ∆-latency of inputs: ∃e = (q, i?, ϕ, c, q ), q = l u , enabled in (q, u), such that ∃d ∈ [0, 2∆].(q, u) d -→(q, u+d) and ∃e = (q, i?, ϕ, c, q ) enabled in (q, u+d), with e = e and q = l u .

Observe that err S ⊆ err S ∆ , because the error condition with robustness is weaker than in the classical case (cf. page 7).

The robust safety game (S, WS o (err S ∆ )) can be solved with the method presented in the previous section, and a winning strategy f for the game can be synthesized. Let S f be the syntactic outcome of f in S. We build from a robust implementation I f by applying the following transformation to S f :

-When we apply a ∆-perturbation on I f , a state ((q, r), u) can be reached even if u ∈ r ∨ r . However due to the region partitioning, the inputs available in S f might not be firable from r ∨ r . Then, in order to check the robust satisfaction relation between (I f ) ∆ and S, we add additional input edges to I f : for each location (q, r) in S f , for each edge e = ((q, r), i?, ϕ, λ ∪ {z}, (q * , r * )) (with q * = l u ), and for each location (q , r ) linked to (q, r) by a sequence of τ transitions, we add an edge e = ((q , r ), i?, ϕ, λ ∪ {z}, (q * , r * )). -To support restriction of input guards in (I f ) ∆ , we replaced in I f all guards ϕ of edges e = ((q, r), i?, ϕ, λ ∪ {z}, (q , r )) with q = l u by their elargement ϕ ∆ . Guards on edges to the l u location are adjusted in order to maintain action determinism and input-enableness.

Note that this construction adds many input edges to the implementation, out of which many are never enabled. This simplifies the construction and the proof of correctness.

In practice, to efficiently synthesize implementations, coarser abstractions like zones should be used, that do not include τ transitions and thus avoid multiplying input edges.

Theorem 2. For a specification S and a robust winning strategy f in the ∆-robust consistency game, we have that I f is a ∆-robust implementation of S, i.e. I f sat ∆ S.

Conjunction. A conjunction of two specifications captures the intersection of their implementation sets. The following conjunction operator has been proposed in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]: Definition 14. Let S = (Loc S , q S 0 , Clk S , E S , Act, Inv S ) and T = (Loc T , q T 0 , Clk T , E T , Act, Inv T ) be specifications that share the same alphabet of actions Act. We define their conjunction, denoted S ∧T , as the TIOA (Loc, q 0 , Clk, E,Act, Inv) where Loc = Loc S ×Loc T , q 0 = (q S 0 , q T 0 ), Clk = Clk S Clk T , Inv((q s , q t )) = Inv(q s )∧Inv(q t ), and the set of edges is defined by the following rule: if (q s , a, ϕ s , c s , q s ) ∈ E S and (q t , a, ϕ t , c t , q t ) ∈ E T then ((q s , q t ), a, ϕ s ∧ϕ t , c s ∪ c t , (q s , q t )) ∈ E.

It turns out that this operator is robust, in the sense of precisely characterizing also the intersection of the sets of robust implementations. So not only conjunction is the greatest lower bound with respect to implementation semantics, but also with respect to the robust implementation semantics. More precisely:

Theorem 3. For specifications S, T and ∆ ∈ Q >0 : S ∧T ∆ mod = S ∆ mod ∩ T ∆ mod
The theorem is a direct extension for robust implemenations of Theorem 6 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. We remark that due to the monotonicity of the refinement (Property 1), we can use two different delays ∆ 1 and ∆ 2 , such that S ∆1 mod ∩ T ∆2 mod ⊇ S ∧T max(∆1,∆2) mod

. So requirements with different precision can be conjoined, by considering the smaller jitter.

Robustness of the operator in Def. 14 is very fortunate. Thanks to this large parts of implementation of theory of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] can be reused. We have experimented on small examples asking simple robust consistency questions by applying constructions manually and using non-robust version of ECDAR [START_REF] David | ECDAR: An environment for compositional design and analysis of real time systems[END_REF], obtaining promising results.

Robust Compatibility, Composition and Quotient

We lift the composition and quotient operators [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] to the robust setting. Composition is used to build systems from smaller units, while quotient is used to synthesize specifications of missing components in a larger design, for example for controller synthesis.

Parallel Composition. Two specifications S, T can be composed only iff Act

S o ∩ Act T o = ∅.
Parallel composition is obtained by a product, where the inputs of one specification synchronize with the outputs of the other: Definition 15 (Parallel Composition). Let S = (Loc S , q S 0 , Clk S , E S , Act S , Inv S ) and T = (Loc T , q T 0 , Clk T , E T , Act T , Inv T ) be two composable specifications. We define their parallel product, denoted S T , as the TIOA (Loc, q 0 , Clk, E, Act, Inv) where Loc = Loc S × Loc T , q 0 = (q S 0 , q T 0 ), Clk = Clk S Clk T , Inv(q s , q t ) = Inv(q s ) ∧ Inv(q t ), and the set of edges is defined by the three following rules:

if (q s , a, ϕ s , c s , q s ) ∈ E S with a ∈ Act S \Act T then each q t ∈ Loc T gives rise to an edge ((q s , q t ), a, ϕ s , c s , (q s , q t )) ∈ E; if (q t , a, ϕ t , c t , q t ) ∈ E T with a ∈ Act T \Act S then each q s ∈ Loc S gives rise to an edge ((q s , q t ), a, ϕ t , c t , (q s , q t )) ∈ E; if (q s , a, ϕ s , c s , q s ) ∈ E S and (q t , a, ϕ t , c t , q t ) ∈ E T with a ∈ Act S ∩ Act T then this gives rise to an edge ((q s , q t ), a, ϕ s ∧ ϕ t , c s ∪ c t , (q s , q t )) ∈ E.

Robustness distributes over parallel composition in the following fashion:

Lemma 1. For any implementations I, J and a delay ∆ ∈ Q >0 :

(I J ) ∆ ≤ I ∆ J ∆
We model incompatibility by introducing a predicate describing undesirable states denoted by the set und. For example, a communication failure in the input-enabled setting can be modeled, by redirecting an input edge to an undesirable location. In general any reachability objective, for example given by a temporal logics property, can serve as the set of undesirable behaviors und. It is important that such behaviors are avoided during the composition. For doing so, we propose to follow the optimistic approach to composition introduced in [START_REF] De Alfaro | Interface automata[END_REF] that is two specifications can be composed if there exists at least one environment in which they can work together. In the robustness setting we consider imprecise environments by applying a ∆-perturbation to their outputs. Then, in what follows, we say that a specification is ∆-robust useful if there exists an imprecise environment E that avoids the undesirable states, whatever the specification does. Definition 16. A specification S is ∆-robust useful if there exists an environment E such that no undesirable states are reached in E o ∆ S sem .

To check robust usefulness we solve the robust game (S, WS i (und)), and determine if the input player has a robust strategy f that avoids the undesirable states. Let S f be the syntactic outcome of f in S. We build from S f a robust environment E f by permuting the input and output players, such that each input in S f becomes an output, and conversely. Theorem 4. If there exists a robust winning strategy f in the ∆-robust usefulness game for a specification S, then S is ∆-robust useful in the environment E f . Finally, two specifications are compatible if their composition is useful. Definition 17. Two composable specifications S and T are ∆-robust compatible iff S T is ∆-robust useful.

It is important that the robust theory does not modify the definition of the operations themself. This means that all the important properties of composition introduced in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] remain valid. This is illustrated with the independent implementability property in Theorem 5, which follows from Lemma 1 and Thm. 10 in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF].

Theorem 5. Let S and T be composable specifications and let I and J be ∆-robust implementations of S and T (resp.), i.e. I sat ∆ S and J sat ∆ S, then I J sat ∆ S T . Moreover if S and T are ∆-compatible then I and J are also ∆-compatible.

Due to the monotonicity of perturbations with respect to the refinement, two different delays can be used to implement specifications S and T . For two implementations I sat ∆1 S and J sat ∆2 T of the parallel components, their composition satisfies the composition of specifications with the smaller of the two precisions: I J sat min(∆1,∆2) S T .

Quotient. Quotient is a dual operator to composition, such that for a large specification T and a small one S, T S is the specification of the components that composed with S will refine T . In other words, T S specifies the component that still needs to be implemented after having an implementation of S, in order to build an implementation of T . One possible application is when T is a system specification, and S is the plant, then a robust controller for a safety objective can be achieved by finding a ∆-consistent implementation of the quotient T S.

To apply quotienting, we require that Act S ⊆ Act T and Act S o ⊆ Act T o . The construction of a quotient requires the use of a universal location l u , as well as an inconsistent location l ∅ that forbids any outputs and forbids elapsing of time.

Definition 18 (Quotient). Let T = (Loc T , q T 0 , Clk T , E T , Act T , Inv T ) and S = (Loc S , q S 0 , Clk S , E S , Act S , Inv S ) with Act S ⊆ Act T and Act S o ⊆ Act T o . Their quotient, denoted T S, is the TIOA (Loc, q 0 , Clk, E, Act, Inv) where Loc = Loc T × Loc S ∪ {l u , l ∅ },

q 0 = (q T 0 , q S 0 ), Clk = Clk T Clk S {x new }, Act = Act i Act o with Act i = Act T i ∪ Act S
o ∪{i new } and Act T o \Act S o , Inv(q t , q s ) = Inv(l u ) = true and Inv(l ∅ ) = {x new ≤ 0}, and the set E of edges is defined by the following rules:

-∀q t ∈ Loc T .∀q s ∈ Loc S .∀a ∈ Act.∃((q t , q s ), a, ¬Inv S (q s ), {x new }, l u ) ∈ E, -∀q t ∈ Loc T .∀q s ∈ Loc S .∃((q t , q s ), i new , ¬Inv(q t ) ∧ Inv(q s ), {x new }, l ∅ ) ∈ E, if (q t , a, ϕ t , c t , q t ) ∈ E T and (q s , a, ϕ s , c s , q s ) ∈ E S , then ∃((q t , q s ), a, ϕ T ∧ ϕ S , c t ∪ c s , (q t , q s )) ∈ E, -∀(q s , a, ϕ s , c s , q s ) ∈ E S with a ∈ Act S o , ∃((q t , q s ), a, ϕ S ∧ ¬G T , {x new }, l ∅ ) ∈ E, where G T = {ϕ t | (q t , a, ϕ t , c t , q t )}, -∀(q t , a, ϕ t , c t , q t ) ∈ E T with a ∈ Act S , ∃((q t , q s ), a, ϕ T , c t , (q t , q s )) ∈ E, -∀(q t , a, ϕ t , c t , q t ) ∈ E T with a ∈ Act S o , ∃((q t , q s ), a, ¬G T , {}, l u ) ∈ E, where

G T = {ϕ s | (q s , a, ϕ s , c s , q s )}, -∀a ∈ Act i .∃(l ∅ , a, x new = 0, ∅, l ∅ ) ∈ E, -∀a ∈ Act.∃(l u , a, true, ∅, l u ) ∈ E.
As stated in Thm. 12 of [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF], the quotient gives a maximal (the weakest) specification for a missing component. This theorem can be generalized to specifications that are locally consistent (see [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]), and used to argue for completeness of the quotient construction in the robust case. It turns out that this very operator is also maximal for the specification of a robust missing component, in the following sense: Theorem 6. Let S and T be two specifications such that the quotient T S is defined and let J be an implementation, then

S J ∆ ≤ T iff J sat ∆ T S

Concluding Remarks

We have presented a compositional framework for reasoning about robustness of timed I/O specifications. Our theory builds on the results presented in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF] combined together with a new robust timed game for robust specification theories. We extend the construction of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] to the setting of specification theories, to solve robust games by reducing them to problems on classical timed games. This construction can easily be implemented in tools such as ECDAR. Our approach can be used to synthesize an implementation that is robust with respect to a given specification, and to combine or compare specifications in a robust manner. Our approach can potentially be applied to lift any game-based timed specification theory to a robust setting.

In the future, we will consider the parametric extension of our theory, that is to synthesize the value of the perturbation for which consistency holds. The emptiness problem that decides if there exists a robust delay has already been studied in the case of 1-player games in different works [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Wulf | Robust safety of timed automata[END_REF][START_REF] Bouyer | Robust model-checking of linear-time properties in timed automata[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF]. A quantitative analysis of this problem has only been studied in [START_REF] Jaubert | Quantitative robustness analysis of flat timed automata[END_REF].

A Proofs

Given a function f on a domain D and a subset C of D, we denote by f |C the restriction of f to C. We write [u] for the region containing the clock valuation u.

A.1 Proof of Section 3

Proof (Property 1). First let remark that for any clock valuation u and guard ϕ, if u |= ϕ ∆1 then u |= ϕ ∆2 , and on the contrary if u |= ϕ ∆2 then u |= ϕ ∆1 . We now check the refinement between I ∆1 sem and I ∆2 sem . Let s 1 = (q 1 , u 1 ) ∈ I ∆1 sem and s 2 = (q 2 , u 2 ) ∈ I ∆2 sem , we define the relation R such that s 1 Rs 2 iff q 1 = q 2 and u 1 = u 2 , and we prove by coinduction that R is an alternating timed simulation:

1. if (q, u) d -→ 1 (q, u + d) for some d ∈ R ≥0 , then (q, u) d -→ 2 (q, u + d), since u + d |= Inv(q) ∆1 ⇒ u + d |= Inv(q) ∆2 ; 2. if (q, u) o! -→ 1 (q , u ), then (q, u) o! -→ 2 (q , u ), since u |= ϕ ∆1 ⇒ u |= ϕ ∆2
(where ϕ is the guard of the edge that fires o!) and we assumed the invariant of q is included in the guard; 3. if (q, u)

i? -→ 2 (q , u ) then (q, u) i? -→ 1 (q , u ), since u |= ϕ ∆2 ⇒ u |= ϕ ∆1
(where ϕ is the guard of the edge that fires i?) and we assumed the invariant of q is included in the guard.

Proof (Proposition 1). Let ρ be an untimed run of A f (i.e. a run of A f where delay transitions are hidden). Then, trivially ρ is a run of G since A f is a subgraph of G. Let denote by ρ i be the prefixe of length i of ρ with last(ρ i ) = (q i , r i ). We assume that ρ i is an outcome of f and that (q i , r i ) a -→(q i+1 , r i+1 ). If a ∈ Act o it means by construction that f (q i , r i ) = o!. If a = τ is means also by construction that f (q i , r i ) = delay. Otherwise a ∈ Act i . This proves that ρ i+1 is an outcome of f , and by induction on i also ρ. Now let ρ ∈ Outcome o ((q, r), f ) and let assume that ρ i is an untimed run of A f and ρ i+1 = ρ i a -→ G (q i+1 , r i+1 ). If a ∈ Act i , then since a is firable from (q i , r i ) in the region graph it means that a there is an edge in A f such that a is firable from (q i , r i ). If a ∈ Act o , then f (q i , r i ) = a and thus there is an edge in A f such that a is firable from (q i , r i ). Otherwise a = τ , and thus f (q i , r i ) = delay, and since the delay action τ is possible in G, the action is also possible in A f . By induction we can then prove that ρ is an untimed run of A f . Proof (Theorem 1). We consider the automaton A f . We must prove that any run ρ of A f o ∆ can be mapped to a run ρ of A, and that no Bad locations are reached in ρ. We use an induction on the length of the run. We assume that for a run ρ i of length i in Runs( A f o ∆ sem ), there exists a run ρ i in Runs( A sem ), such that if last( ρ i ) = ((q i , r i ), u i ), then last(ρ i ) = (q i , u i ), where u i = u i|Clk (the projection of u i on the clocks of A such that clock z is removed).

Let ρ i+1 = ρ i a -→((q i+1 , r i+1 ), u i+1 ). We prove the induction at level i+1 depending on the action a:

1. if a ∈ Act i , then there exists an edge e = ((q i , r i ), a, ϕ, λ ∪ {z}, (q i+1 , r i+1 )) in A(f ). By construction, there also exists an edge e = (q i , a, ϕ, λ, q i+1 ) in A. Since e is firable, u i |= ϕ, and consequently u i |= ϕ, which proves that e i is also firable. So ρ i+1 = ρ i a -→(q i+1 , u i+1 ) is a run of A, and u i+1 = u i+1|Clk since the same clocks λ are reset.

2. if a ∈ Act o , then similarly there exists e = ((q i , r i ), a, ϕ, λ ∪ {z}, (q i+1 , r i+1 )) in A f and by construction, e = (q i , a, ϕ, λ, q i+1 ) in A. Additionally, u i |= ϕ ∆ since e is firable, and u i |= r i ∩ {z = 0} ∆ that is the enlarged invariant of (q i , r i ). By construction also f (q i , r i ) = a, which implies that f (q α i , r i ) = a. Since

u i |= r i ∆ , ∃δ ∈ [-∆, ∆].u i + δ |= r i . Let u i = (u i1 , u i2 , .
. . , u in ), then u i + δ = (u i1 +δ, u i2 +δ, . . . , u in +δ), and so u iδ = (u i1 +δ, u i2 +δ, . . . , u in +δ, ∆) ∈ r i . In A ∆ rob now, this implies that u iδ -∆ |= ϕ 2∆ , and consequently it proves that u i |= ϕ. So e is firable and ρ i+1 = ρ i a -→(q i+1 , u i+1 ) is a run of A, and u i+1 = u i+1|Clk .

3. if a ∈ R ≥0 , either in ((q i , r i ), u i ) output has the strategy to wait infinitely, which implies that Inv(q i ) is unbounded, and this is sufficient to prove that ρ i+1 ∈ Runs( A sem ). Or output has a strategy that eventutally performs an action. This implies the following sequence of edges in A f :

(q i , r i ) τ -→(q i , r i1 ) τ -→(q i , r i2 ) . . . (q i , r in ) o!
-→(q i , r i ). We consider that a is the maximum delay firable from ρ i , thus

ρ i+1 = ρ i a1 -→((q i , r i1 ), u i + a 1 ) τ -→((q i , r i2 ), u i + a 1 ) a2 -→((q i , r i2 ), u i + a 1 + a 2 ) τ -→ . . . ((q i , r in ), u i +a) o! -→((q i , r i ), u i ), such that a = n j=1 a j . Then u i +a |= r in ∆
, and as previously we can prove that u i + a |= ϕ, and since we assume that ϕ contains the location invariant, we prove that ρ i+1 ∈ Runs( A sem ).

We prove now that all the states in A f o ∆ are safe, by mapping the runs of A f with the ones of A ∆ rob . We use another induction on the length on the run. Let assume that ρ i ∈ Runs( A f o ∆ sem ) is mapped to a run ρ i ∈ Runs( A ∆ rob sem ), such that if last( ρ i ) = ((q i , r i ), u i ), then last( ρ i ) = (q i , u i ), and u i|Clk = u i|Clk , and (q i , u i ) is a winning state.

Then, either in ((q i , r i ), u i ) the strategy f allows to delay infinitely, and consequently the strategy f allows to delay infinitely in A ∆ rob without reaching an unsafe state. For any delay d ∈ R ≥0 , all the inputs firable from a state ((q i , r i ), u i + d) are also firable in (q i , u i + d) since the guard are the same, and the state (q i+1 , u i+1 ) reached is also winning and is equivalent to ((q i+1 , r i+1 ), u i+1 ), which proves the induction hypothesis Otherwise output has a strategy that eventutally performs an action o! after a delay a. Thus let

ρ i+1 = ρ i a -→((q i , r i ), u i + a) o!
-→((q i+1 , r i+1 ), u i+1 ) (abtracting τ transitions). This implies that the following edges exists in A ∆ rob : (q i , o!, ϕ 2∆ , λ ∪ {y}, q α i ), (q i , o!, {y = ∆}, {y}, q β i ), (q α i , o?, {y ≤ ∆}, {y}, q i+1 ) and (q β i , o?, {y ≤ ∆}, {y}, q i+1 ). Since o! is firable in ((q i , r i ), u i + a), this means that f (q i , r i ) = o! and u i + a ∈ r i ∆ . Then by construction of f , f (q α i , r i ) = o!, and there exists

b ∈ R ≥0 s.t. (q i , u i ) b - →(q i , u i + b) (abstracting transitions o!), and u i + b ∈ r i . Addi- tionally, ∀γ ∈ [-∆, ∆].(q i , u i ) b+γ --→(q i , u i + b + γ) o?
-→. This is in particular the case for b + γ = a since a ∈ r i ∆ . To finish, the previous argument is used to demonstrate that the input transitions firable from ((q i , r i ), u i ) after some delay are also firable from (q i , u i ), and they are winning since (q i , u i ) is winning.

A.2 Proofs of Section 4

Proof (Theorem 2). We first check that by construction I f is an implementation TIOA. It verifies the output urgency condition, since the clock z is reset at each firing, and when an output is fired the invariant of the location is z = 0. It verifies the independent progress condition since I f is the outcome of the strategy f that avoids the inconsistent states in S. Finally, all the states in I f verify the ∆-latency condition, which permits to increase guards on input edges without adding non-determinism in I f .

We check now that I f sat ∆ S with the following relation R = {(((q, r), u), (q, v))

∈ (I f ) ∆ sem × S sem | v = u |Clk }. Note that (I f ) ∆ sem is included into S f o ∆ sem
since in the input-enablened setting the additional inputs only replace inputs to the l u location, and we remind that the runs of S f o ∆ sem are included in the runs of S sem since f is a robust winning strategy. Finally we admit that S can accept τ transitions in any states as output transitions.

Let consider (((q, r), u), (q, v)) ∈ R:

1. If ((q, r), u) d -→ (I f ) ∆ ((q, r), u + d) for some d ∈ R ≥0 , then since the runs of S f o ∆
are included into the one of S, it is also the case that (q, v) d -→ S (q, v + d) and the relation is trivially preserved. 2. If ((q, r), u) o! -→ (I f ) ∆ ((q , r ), u ) for some o! ∈ Act o , then there exists and edge ((q, r), o!, ϕ, λ ∪ {z}, (q , r )) in I f and also in S f . It also means that there exists a similar edge (q, o!, ϕ, λ, q ) in S that is firable in between the two regions r and r . Then since the runs of S f o ∆ are included into the one of S, (q, v) o! -→ S (q , v ), and since the same reset of clocks is applied v = u |Clk . 3. If ((q, r), u) τ -→ (I f ) ∆ ((q, r ), u) then by assumption (q, v) τ -→ S (q, v). 4. If (q, v) i?

-→ S (q , v ) for some i? ∈ Act i , then there exists and edge e = (q, i?, ϕ, λ, q ) such that v |= ϕ. Thus there also exists an edge (q, [v]) i?

-→ G (q , [v ]) in the region graph of S. If u ∈ r then this edge also exists in I f . Otherwise u ∈ r ∨ r ∆ . This means that there exists a sequence of τ transitions in I f between r and [v], and by construction the edge i? is copied in each location along this sequence, including (q, r). Since v |= ϕ it implies that u |= ϕ ∆ ∆ which proves that it is firable. Thus ((q, r), u) i?

-→ I ∆ ((q , [v ]), u ) and v = u |Clk since the same reset of clocks is applied.

A.3 Proofs of Section 5

A definition of the parallel composition for two TIOTS is given in [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]. We recall the following theorem that relates the two definitions of the parallel composition on TIOTS and TIOA: Theorem 7 ( [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]). For two specifications TIOA S and T composable, we have S sem | T sem = S T sem Proof (Lemma 1). In the following, we denote (Loc k , q k 0 , Clk k , E k , Act k , Inv k ), with k ∈ {I, J, I J}, the TIOAs corresponding to I, J , or I J , respectively, and (St k , (q k 0 , 0), Act k , → k ), with k ∈ {I, J, I J}, their semantics, and with k ∈ {I ∆ , J ∆ , [I J] ∆ }, their perturbed semantics. We prove the refinement (I J ) ∆ sem ≤ I ∆ sem | J ∆ sem by witnessing the following relation: R = {(((q i , q j ), u ij ), (( q i , u i ), ( q j , u

j )) ∈ St [I J] ∆ × (St I ∆ × St J ∆ ) | ((q i = q i ∧ u i = u ij|Clk I ) ∨ q i = l u ) ∧ ((q j = q j ∧ u j = u ij|Clk J ) ∨ q j = l u )}
We prove by coinduction that R is a timed alternating relation. Let (((q i , q j ), u ij ), (( q i , u i ), ( q j , u j )) ∈ R.

1. if ((q i , q j ), u ij ) d -→ [I J] ∆ ((q i , q j ), u ij + d) for some d ∈ R ≥0 ,
then by definition u ij |= Inv(q i , q j ) ∆ . By construction of the parallel product Inv(q i , q j ) ∆ = Inv(q i ) ∧ Inv(q j ) ∆ = Inv(q i ) ∆ ∧ Inv(q j ) ∆ . Then, we can deduce that u i + d |= Inv(q i ) ∆ and u j +d |= Inv(q j ) ∆ . This implies that (q i , u i ) d -→ I ∆ (q i , u i +d) and (q j , u j ) d -→ J ∆ (q j , u j + d). Besides, by definition of the universal state, for any valuation u of a TIOA is always true that (l u , u)

d -→(l u , u + d).
Consequently, by definition of the composition I ∆ sem | J ∆ sem , (( q i , u i ), ( q j , u j )) d -→ I ∆ |J ∆ (( q i , u i + d), ( q j , u j + d)), and the relation R is trivially preserved in the next states. 2. if ((q i , q j ), u ij ) o! -→ [I|J] ∆ ((q i , q j ), u ij ), then ∃e ∈ E I J .e = ((q i , q j ), o!, ϕ, c, (q i , q j )) such that u ij |= ϕ ∆ and u ij |= Inv(q i , q j ) ∆ , (a) and if o ∈ Act I o \Act J i (or conversely, if o ∈ Act J o \Act I i ; this case is similar, so we will not consider it), then ∃e i ∈ E I .e i = (q i , o!, ϕ i , c i , q i ), and q j = q j , ϕ = ϕ i , c = c i , and u ij|Clk J = u j . Consequently, u i |= ϕ i ∆ and u i = u ij|Clk I |= Inv(q i ) ∆ , which proves that (q i , u i ) o! -→ I ∆ (q i , u i ). Besides, by definition of the universal state, (l u , u i ) o! -→ I ∆ (l u , u i ). Consequently, by definition of the composition I ∆ sem | J ∆ sem , (( q i , u i ), ( q j , u j )) o! -→ I ∆ |J ∆ (( q i , u i ), ( q j , u j )). Moreover, either q i = q i and then q i = q i , or q i = l u = q i , which proves that the relation R is preserved. (b) If o ∈ Act I o ∩ Act J i (the reverse case o ∈ Act J o ∩ Act I i is similar), then ∃e i ∈ E I .e i = (q i , o?, ϕ i , c i , q i ) and ∃e j ∈ E J .e j = (q j , o!, ϕ j , c j , q j ) and ϕ = ϕ i ∧ ϕ j , c = c i ∪ c j . On the side of I, since u ij |= ϕ ∆ and u ij |= Inv(q i , q j ) ∆ , we get that u i |= ϕ i ∆ and u i = u ij|Clk I |= Inv(q i ) ∆ , which implies that (q i , u i ) o! -→ I ∆ (q i , u i ). On the side of J , we also get that u j |= ϕ j ∆ and u j |= Inv(q j ) ∆ . If moreover u j |= ϕ j ∆ , then as previously it implies that (q j , u j ) o? -→ J ∆ (q j , u j ). Otherwise, a reductio ab absurdum argument allows us to prove that there exists no other edges e j = (q j , o?, ϕ j , c j , q j ) ∈ E J such that u j |= ϕ j ∆ (since u j |= ϕ j ∆ it implies that ∃ε ∈ [-∆, ∆].u j + ε |= ϕ j , but in the same time it would be the case that u j + ε |= ϕ j . This is absurd since J, as an implementation is supposed to be deterministic). By construction of J ∆ sem however, input-enableness is preserved by linking the unexpected input to a universal location l u . So (q j , u j ) o? -→ J ∆ (univ, u j ).

To conclude, we get by definition of I ∆ sem | J ∆ sem that (( q i , u i ), ( q j , u j )) o! -→ I ∆ |J ∆ (( q i , u i ), ( q j , u j )), and as previously, by construction we check that the relation is preserved.

3. finally, if (( q i , u i ), ( q j , u j )) i?

-→ I ∆ |J ∆ (( q i , u i ), ( q j , u j )), for i ∈ Act I i ∩ Act J i (the cases i ∈ Act I i \Act J i or i ∈ Act J i \Act I i can be proved similarly by considering that only one component reacts, while the other stay in the same state), then from the definition of the composition:

-( q i , u i ) i?

-→ I ( q i , u i ), and -( q j , u j ) i? -→ J ( q j , u j ). Besides, due to input-enableness, ((q i , q j ), u ij ) i?

-→ [I J] ∆ ((q i , q j ), u ij + d), which implies that:

-(q i , u i ) i?

-→ I (q i , u i ), with u i = u ij|Clk I , and -(q j , u j ) i? -→ J (q j , u j ), with u j = u ij|Clk J . If q i = l u then q i = l u , and in this case the relation R is always preserved (and similarly for q j ). Otherwise q i = q i and u i = u i (and similarly for q j ). In this latter case, since I ∆ sem is deterministic, it implies that q i = q i and u i = u i , which also proves the induction for relation R.

Proof (Theorem 4). The theorem directly follows from the definition of the robust strategy. S f i ∆ sem ⊆ S sem which implies that E f o ∆ synchronizes with every action of S when computing the composition. Thus, only the states belonging to S f i ∆ sem can be reached in the composition, and by definition they are not undesirable.

Finally, the theorem 5 can be proved with the lemma 1 and the following theorem from [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]: Theorem 8 ( [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF]). Refinement is a pre-congruence with respect to parallel composition; for any specifications TIOTS S 1 ,S 2 and T such that S 1 ≤ S 2 and S 1 composable with T , we have S 2 composable with T and S 1 | T ≤ S 2 | T . Moreover if S 2 compatible with T , then S 1 compatible with T .

Proof (Theorem 5). The first part of the theorem can be directly deduced:

due to lemma 1, (I J ) ∆ sem ≤ I ∆ sem | J ∆ sem ; then due theorem 8, I ∆ sem | J ∆ sem ≤ S sem | T sem ; finally due theorem 7, S sem | T sem = S T sem ; all together this proves (I J ) ∆ sem ≤ S T sem , that is to say I J sat ∆ S T .

We prove now the second part of the theorem. Since S and T are ∆-compatible, there exists an environement E such that E o ∆ (S T ) avoids reaching any undesirable states. From theorems 8 and 7 we get that I J ≤ S T . Again with theorem 8 we get that (I J )

E o ∆ ≤ (S T ) E o ∆ .
Consequently, since no undesirable states are reached in (S T )

E o ∆ this is also the case in (I J ) E o ∆ , which proves that I J is ∆-useful and so I and J are ∆-compatible.

Definition 1 .

 1 A Timed I/O Transition System is a tuple S = (St S , s 0 , Σ S , → S ), where St S is an infinite set of states, s 0 ∈ St S is the initial state, Σ S = Σ S i ⊕ Σ S o is a finite set of actions partitioned into inputs Σ S i and outputs Σ S o , and → S : St S ×(Σ S ∪ R ≥0 )×St S is a transition relation. We write s a -→ S s when (s, a, s ) ∈→ S and use i?, o! and d to range over inputs, outputs and R ≥0 , respectively.

d-→

  S s and s d -→ S s then s = s time reflexivity: s 0 -→ S s for all s ∈ St S time additivity: for all s, s ∈ St S and all d 1 , d 2 ∈ R ≥0 we have s d1+d2 ----→ S s iff s d1 -→ S s and s d2 -→ S s for an s ∈ St S

Fig. 1 :

 1 Fig.1: TIOAs of a specification and an implementation for a researcher.

Fig. 2 :

 2 Fig. 2: ∆-perturbation of the researcher implementation.

Fig. 3 :

 3 Fig. 3: Construction of the robust game automation A ∆ rob from an original automaton A.

The region graph of an automaton with rational constants can be built by multiplying all constants of the automaton to work only with integers.


V Laurain

M Gilson

M Benoît

Data-driven modeling for water resource quality over long term trends

Keywords: data-driven modelling, nitrogen propagation, drinking water quality

Since the 50 last years, the rapid development of modern agriculture in industrialised countries has considerably affected the quality of water resources, up to the point to jeopardise the capacity of rural territories to produce drinking water. Hence, there has been interest within the field of agronomy to study complex nitrogen biogeochemical interactions over a long time period. Nevertheless, if the agronomists are able to produce very accurate models at different scales, they have a limited number of available tools in order to cope with quality measurements in water sources for which very little information about the geological information is available. It prevents the specialists of being affirmative about the prediction of their current actions on the water quality. By opposition, system identification can deliver dynamical models from measured data: they cannot be generalised but offer strong insight without any a priori. This applicative paper introduces a datadriven model software for both modelling the nitrogen propagation in drinking water and offering new decision tools to stakeholders.

INTRODUCTION

Agriculture is challenged by large scale issues, like impacts of land system changes on the preservation of environmental resources, urging agronomy to evolve. Landscape agronomy has been proposed as new perspective to address these issues [START_REF] Benoît | Landscape agronomy: a new field for addressing agricultural landscape dynamics[END_REF]. In European Union, the WFD (Water Framework directive) is built on a strict basis: water policy is a result based policy. Therefore, States and Agencies have to maintain water in a good state, link to chemical norms and dates to obtain these results [START_REF] Ec | Directive 2000/60/EC of the European Parliament and of the council of 23 October, 2000 establishing a framework for community action in the field of water policy[END_REF][ /60/EC, 2000]]. It has hence become compulsory to deal with two main parameters to help decision makers in this domain: the evolution of concentration and the level of chemical contents at precise dates (2015,2021,2025). This work is hence dedicated to water quality depletion or improvement. During the past decades many different models have been proposed in order to analyse the complex biogeochemical behaviour of Nitrogen (N) in agricultural soils. In [START_REF] Manzoni | Soil carbon and nitrogen mineralization: Theory and models across scales[END_REF], 250 different models are classified in terms of mathematical features such as spatial and temporal scale or isotropy approximations. These models take into account different phenomena (denitrification, biomass growth and decay, water flux ...) and therefore require the tuning of a large number of parameters. They also require quite a large number of input such as the type of culture (cereals,vegetables...), the N density at different depths or the soil type [START_REF] Bacsi | Validation: an objective or a tool? results on a winter wheat simulation model application[END_REF][START_REF] De Willigen | Comparison of six simulation models for the nitrogen cycle in the soil[END_REF]. Hence, they are mostly exclusively validated on dedicated experimental parcels [START_REF] Cavero | Modeling nitrogen cycling in tomato-safflower and tomato-wheat rotations[END_REF][START_REF] Bacsi | Validation: an objective or a tool? results on a winter wheat simulation model application[END_REF][START_REF] De Willigen | Comparison of six simulation models for the nitrogen cycle in the soil[END_REF], where each required information is available from measurements. The strength of those models is their deep physical insight and the respect of a modelling protocol allowing their generalisation to other parcels. Nevertheless, their main drawback is their inability to be tuned on parcels where some of the required knowledge is unavailable: in this case, some assumptions are required, which can average favourably at large scales, but that cannot be applied at smaller scales such as catchment or parcels scales [START_REF] Del Grosso | Daycent national-scale simulations of nitrous oxide emissions from cropped soils in the united states[END_REF]. In the presented application, the only available information is the compulsory N concentration measure in drinkable water sources. There is not any knowledge about the depth of these sources, the surface of water they drain, their flow or the soil type. Modelling and understanding the N propagation into the water is a challenging issue in such a situation which actually represents the most realistic scenario in most of drinkable sources.

In opposition to the traditional approaches, a "top-down" approach is proposed in this paper: the model is determined using the measured data and despite some slight vocabulary divergences, these approaches link directly to the field of system identification. The field of system identification uses statistical methods to build mathematical models of dynamical systems from measured data. Their are many environmental fields where system identification was successfully used, and one of the most prosperous field related to the presented application is the rainfall/runoff modelling [START_REF] Laurain | A new data-based modelling method for identifying parsimonious nonlinear rainfall/flow models[END_REF][START_REF] Young | Data-based mechanistic modelling and the rainfall-flow nonlinearity[END_REF].

This paper main contribution is to propose a data-driven model, along with its physical validation process. The obtained model aims at bridging the gap between the modelling possibilities with regards to slow/complex dynamics effects and the stakeholders expectations. It is organised as follows. In Section 2, the issues and dead-end of traditional modelling and nitrogen propagation are detailed. In Section 3, the proposed data-driven model is explained along with some algorithmic aspects. Finally, the results are exposed and validated using physical principles in Section 4.1. Conclusions and some future directions of research are given in Section 5.

PROBLEM FORMULATION

The 2000 European Directive, the Water Framework Directive (WFD), proposed three new articles: preservation of water bodies as a whole (taking into account non-point pollution instead of only point-source pollution), an imposed schedule, and objectives defining quantified results aiming for the ecological restoration of the environment. This text is complex (because it includes several types of regulatory tools), ambitious, and is a cornerstone of the European Union's environmental policy. However, its application is delicate for a number of countries [START_REF] Dworak | Wfd and agriculture linkages at the eu level 2007-2013[END_REF] in which achieving consistency within the law has followed other pathways or which do not know how to achieve this result. France partially conformed to this directive only 6 years later through its Law on Water and Aquatic Environments [START_REF] Dworak | Wfd and agriculture linkages at the eu level 2007-2013[END_REF] where for the first time in French law, the notion of non-point pollution appeared. In 1990, nitrate peaks reaching 70 mgNO3-/L (exceeding the European drinking standard of 50 mgNO3-/l) caused a lively debate on management strategies to deal with this N contamination. The public service delegated for water proposed a strategy to protect all of the sources used for drinking water. With the European directive in mind, a collective action called "Ferti-Mieux" started on the sources of the Haut-Saintois plateau (800 ha= 8 km 2 ), Lorraine, France. A list of agricultural new practices has been proposed to farmers and many of them ( 85 % of cultivated surface) adopted these improvements to protect water resources. The main changes are i) farmyard management through low amount of compost (less than 20 t/ha/y) and ii) mineral fertilisation control taking into account soil mineralization (the global decreasing of input is 60 kg N/ha/y). These improvements are near from other European agricultural improvement operations for water quality protection [START_REF] Kunkel | Forecasting the effects of eu policy measures on the nitrate pollution of groundwater and surface waters[END_REF][START_REF] Lam | The impact of agricultural best management practices on water quality in a north german lowland catchment[END_REF]. Since then, six sources are monitored by measuring the N concentration at a fortnight rhythm during 20 years by technicians of Inra research unit (Lionel Caudy, Gilles Rouyer and Damien Foissy). The samplings have been realised directly in the source catchment, with all the legal security processes. The location of these sources is characterized by an agricultural landscape. The land use is: Forests (12 %), small rural roads (4 %) and agricultural fields (84 %). Hence, the pollution sources are only diffuse pollution one, without any building and houses in the watersheds. In this paper, due to space restrictions, we focus on two of these sources which nitrate ion concentration C N (t) is displayed in Figure 1 in grey. It must be noticed that the same modelling strategy with similar results was applied on all the available data. The goal is to study the link between the practice changes and the water quality. As there is not any available model of water dynamics in this karstic zone, and no N concentration measure in the soil is available, we propose a data-driven modelling strategy.

THE PROPOSED TOOL : DATA-DRIVEN MODEL

The physical-based modelling problem

In practice, long-time trend forecasting and decision help requires a dynamical model able to simulate the concentration in the water with respect to some given scenario. Nevertheless, in the presented problem, no model is available to link the agricultural N mass to the actual N concentra-

(t) andM N 2 (t)
tion measured in the water. Should there be one, it would also not be possible to tune it in order to fit the current measured data : indeed, none of the N input have been measured. Hence, the commonly used modelling technique for this problem is to use a simplistic polynomial fit such as exposed in Figures 1 in red. Unfortunately, such a static model indicates the current trend but is not suitable for future forecasting. Finally and most importantly, despite the similar region, soil and agricultural policy, it appears that the polynomial curves indicate opposite results for these two sources: no conclusion can be drawn from this measured data.

The data-driven modelling problem

The solution proposed in this paper relies on the identification of a model under its transfer function form which offers the ability to interpret a posteriori the data-driven model in physical or ecological terms: this process is the so-called data-driven mechanistic modelling [START_REF] Young | Data-based mechanistic modelling and the rainfall-flow nonlinearity[END_REF].

The main advantages in using such a modelling paradigm are:

• A simplified model is obtained without requiring any physical assumption or model reduction. The obtained model might not even be possibly derived from physical assumptions. Nonetheless, only a physics-based validation and its capacity to predict physical phenomena legitimate its validity.

• If a very simple model is obtained, it also means that a source can be characterised using only a small set of parameters, helping a lot in terms of data compression in big data contexts.

• Finally, even though the obtained model cannot be directly applied to other sources without measures, the data-driven mechanistic process can be applied directly to any kind of relationship (rainfall/runoff...), at any scale as soon as some measures are available.

Regarding the specific nitrogen propagation problem, from a system theory viewpoint, two main issues have to be dealt with and are not detailed here due to space restrictions:

1 The lack of nitrogen input: none of the nitrogen soil concentration is measured. Consequently, a preliminary data-mining phase has been realised. It is based on a simple correlation analysis and the result is a possible correlation between C N (t) and both the raw rainfall R(t)(mm/day) and the temperature T (t) ( o C) (downloaded from the European Climate Assessment website, Source 741, [START_REF] Tank | Daily dataset of 20th-century surface air temperature and precipitation series for the european climate assessment[END_REF].

2 System identification is dedicated to dynamical models: the drift represented by the polynomial approximation M N (t) varies too slowly to be identified from a reduced set of data and needs to be removed. Hence, the considered output is

C N c (t) = C N (t) -M N (t).
The proposed model which is the main contribution of this paper is described by the following so-called Output-Error model:

M C N c (t) = b1 s+a1 Rc(t) + β1 s + α1 Tc(t) + e(t), (1)
where s is the Laplace variable and e(t) is assumed to be a white noise stochastic process.

C N c (t),Rc(t) and Tc(t) are the centred Nitrogen concentration, rainfall and temperature respectively, defined as

C N c (t) = C N (t) -M N (t), Rc(t) = R(t) -mean(R(t))
and Tc(t) = T (t)mean(T (t)). b1, a1, α1, b1 are the parameters to be identified and they fully characterise the presented structure. The same structure was proposed from the data for all the sources analysed in this study (6 in total). Hence, this dynamical model is a simple first order model, with two inputs and one output. Please note that other more complicated models such as nonlinear Hammerstein and Wiener structures along with nonparametric approaches (Support Vector Machines) have been tested. Nevertheless, probably due to the amount of noise and the relatively low number of data points, the results were not significantly better (or worse), lead to an harder interpretation, and therefore, the simplest structure was retained.

This model implies that the temperature and the rainfall should affect consistently the nitrogen concentration in water. This statement can naturally not be derived from any physical logic. Hence, one would think that this type of model does not have any legitimacy. However, should this model be physically validated (temperature could be correlated to an actual N source), it would be very interesting in the sense that temperature and rainfall are widely available measures. Before drawing any conclusion identification must be performed. Nonetheless, identification is not a trivial matter either in such context. While the white noise assumption is fair when measurement noise is the major perturbation source, the problem is more complicated here : noise on the inputs (the rain and the temperature are not measured exactly above the considered parcel), missing inputs, system approximation... Hence, the identification needs to be robust to noise modelling errors. For this application, the so-called simplified refined instrumental variable algorithm (SRIVC) [START_REF] Young | Refined instrumental variable methods of recursive timeseries analysis -part III. extensions[END_REF] has been chosen. It hands out unbiased estimates in case the true noise is zero mean, independently of its distribution and it was successfully used in many other environmental applications [START_REF] Laurain | A new data-based modelling method for identifying parsimonious nonlinear rainfall/flow models[END_REF][START_REF] Young | Data-based mechanistic modelling and the rainfall-flow nonlinearity[END_REF]. Consequently, before presenting the results, here are all the steps necessary for the identification of the proposed N propagation model:

Step 1: Force all the data to the same sampling period : in our application C N (t) was sampled every 15 days, and was linearly interpolated to fit the one day sampling period of the rainfall and temperature.

Step 2: Compute the polynomial curve and subtract it to the original measured data.

Step 3: Split the data into a identification dataset and a validation dataset.

Step 4: Use the identification dataset to identify a linear structure using the SRIVC function (a free Matlab version can be downloaded with the Contsid Toolbox at http://www.cran.uhp-nancy.fr/contsid/) using different model orders.

Step 5: Use the validation dataset in order to choose the most suitable order (for example using Young's Information criterion [START_REF] Young | Refined instrumental variable methods of recursive timeseries analysis -part III. extensions[END_REF] and display the obtained model (resulting here in (1)). The obtained results are provided in the next section.

MODEL VALIDATION

Physical propositions

In this section, the identification results are depicted in the form of physical propositions and data fit. Before detailing the results, it must be emphasised here that no a priori has been used in order to build this model and it has been solely built using commonly measured data. The identification data has been chosen as a period of 4 years between 1997 and 2001 as they contain the most different rainfall scenarii and the rest is used for validation purpose. The coefficients of the identified models for the two presented sources are exposed in table 1. Naturally, the equations are not homogenous and therefore, the absolute value of these parameters are of little interest. Nevertheless, it can be seen that the b1 coefficients are negative for both sources (and actually all other studied sources).

Source

rainfall temperature This indicates a negative static gain on the rainfall transfer function. The exact opposite statement can be concluded for the temperature transfer function.

a 1 b 1 α 1 β 1 S 1 0.
The simulated output of the identified model can be computed. The estimation data, validation data and simulated output are exposed in Figure 2. Two striking facts appear from the simulation results. Even though these two parcels behave differently from the trend perspective, their dynamic is actually quite similar. The identified model outputs are actually nearly identical for both of these sources. Furthermore, the model output fits quite well the original data (at least from in the estimation dataset) considering that the rainfall and temperature are not actual sources of nitrogen. In order to quantify this fit, a local score inspired from the NASH score [START_REF] Nash | River flow forecasting through conceptuel models. part 1-a discussion of principles[END_REF] is used and is defined as:

N ASH(t k ) = 1 - || ĈN c (t k ) -C N c (t k )|| 2 k-N,k+N ĈN c (t k ) -mean(C N c ) 2 k-N,k+N . (2)
where ĈN c (t k ) is the output simulated from the identified model and the notation ||.|| 2 k-N,k+N depicts the ℓ2 norm on the samples between k -N and k + N . Here, N is chosen as 365 days. In other words, the presented score represents the NASH score on a local 2 years long window on each time sample k. It must be noticed that N ASH = 1 means perfect fit, N ASH = 0 means that the simulated output is only as predictive as the output average, while N ASH < 0 means that the simulated output is not predictive. The fitting score quantification is displayed in Figure 3. It quantitatively appears now that both sources (actually all studied sources) evolve from a non-predictive to a predictive zone around 1994. From a system theory viewpoint, it could be argued that the obtained fit is rather poor. Nevertheless, the main unpredicted part is located in the high frequencies which is not surprising considering the relatively high sampling period taken for concentration measurements with respect to rainfall and temperature. Finally, by taking into account that the true model inputs are unknown, this models fits the data really well. To sum it up, the result of the data-driven modelling are the following physical statements: H1: The rainfall acts negatively on the nitrogen concentration. H2: The temperature acts positively on the nitrogen concentration. H3: The dynamic behaviour of S1 and S2 are similar. H4: The sources undergo a major change around the beginning of year 1994, even though this year was not used for identification.

The physical validation

In agronomy, temperature is a good indicator of vegetation growth season. In our temperate zones, the 6 • C is the basis of two main phenomena: vegetation growth, and nitrate mineralization in the soil. Therefore, temperature is used as an indicator of biological activity in the fields, which is strongly involved in soil nitrification which validates H1. For agronomists, rainfall minus evapotranspiration is a pertinent indicator of nitrate movement in the soils and in the aquifer: without rainfall, N are stable in the soils while with high level of rainfall, they are moving through the soils to the aquifers. When the amount of rain is low, the N solubility being high, the concentration of N will raise in the water. On the contrary, if the amount of rain is high, once the N soil nitrification decreases under a critic mass, the N concentration will decrease. This fact strongly validates H2. Consequently, these two variables are in the heart of N leaching model and strongly correlated to N inputs [START_REF] Brisson | Why are wheat yields stagnating in europe? a comprehensive data analysis for france[END_REF].

For our situation, these sources are situated very closely in the same geographic location on this karstic plateau with a similar situation in terms of climate and soil behaviours: they should behave the same (H3). Finally, the only change on these parcels is the farmers' practice changes, from a high level of inputs until 1992, to a strong decreasing in 1993 with the initiation of "Ferti-Mieux" local water resource management operation. For all studied sources, it seems that the simple proposed model is able to emphasise this change clearly in time despite the fact that this a priori knowledge was not used in the modelling process (H4).

Consequently, while this model could not have been possibly derived from physical reasoning, it seems that it is strongly supported by the physical validation. This model takes as an input only natural measurements. Naturally, it means that this model is unable to emphasize agricultural practice changes when most of the nitrogen source take origins from human activity. That could also mean that this model indicates how naturally behaves the source. More data would be needed in order to assess this statement. While some of the dynamics are well predicted by this model, the slow trends and the high frequencies phenomena could though not be captured. Hence, either the trends are caused by earlier data and a slower dynamic integrative effect is present or they are caused by measures taking place in the unmodelled high-frequencies phenomena. In order to study the latter assumption, a high frequency sampled-data would be needed and the current acquisition might not be sufficient to assert the future behaviour of the sources. Nevertheless, should the proposed model represent a natural behaviour, then the closer the N concentration to this model output, the more likely to see the N concentration decrease at some point. However, Further study is needed for this purpose.

CONCLUSIONS

In conclusion, a data-driven model has been proposed for nitrogen propagation in drinking water.It must be well understood that such an approach can be applied only on instrumented lands as the model drives the model definition. Hence, it does not require the same amount of a priori as physical based-model, but it has other limitations. For example, an identified model cannot therefore not be directly extended to other similar parcels as its parameters cannot be directly linked to any actual physical process. Nevertheless, it was shown that most of the yearly dynamics could be predicted by solely using the rainfall and temperature when the human nitrogen source is low, giving a completely different insight on the system as usual. It can be pointed out that this data was not acquired for system identification purposes and therefore, the method can be considered as applicable on commonly available data. Even though the data-driven model does not represent any physical relationship it still can be validated from physical principles. The fact that it is able to detect a change in the agricultural policy from strong nitrogen loads to considerable decreased loads could even support the fact that this model can well represent the natural behaviour of a source. The more the model fits, the more the source is natural. Nevertheless, deeper investigations are required in order to validate this assumption. Hence, the presented model could not estimate yet the long terms trends. Nevertheless, the current trends might be a residual of past effects. Should it be the case, and depending on the time constants (which might be several dozens of years) the trends will never be possibly forecasted. However, should this model represent the naturalness of a source, then it would give the stakeholders a tool to assess the naturalness of their watershed and assert whether the current trends are caused by current policies or not.

Figure 1 .

 1 Figure 1. Measured nitrogen concentration C N 1 (t) and C N 2 (t) in two similar sources S1 and S2 along with a 3 rd order polynomial approximation M N 1 (t) andM N 2 (t)

Figure 2 .

 2 Figure 2. Original centred concentration C N c (t) (estimation data in green and validation data in grey) along with the model output simulated from the rainfall and temperature data, for sources S1 (left) and S2 (right).

Figure 3 :

 3 Figure 3: Local NASH score for S1 and S2

Table 1 .

 1 Identified parametersV. Laurain et al. / Data-driven modelling for water resource quality over long term trends

		016 -0.050 0.021 0.0007
	S 2	0.003 -0.023 0.007 0.0002

ACKNOWLEDGEMENTS

This work is supported by the CNRS PEPS project ContamiNit. The authors would also like to thank Gilles Rouyer (Aster unit) for the water analysis, LTER-ZAM (Zone Atelier du Bassin de la Moselle) and R ésEAu Lor-Lux for their support.