Wei Zheng

Wojciech Wideł
email: wwidel@irisa.fr

Ligong Wang

On implicit heavy subgraphs and hamiltonicity of 2-connected graphs

Keywords: Implicit degree, Implicit o-heavy, Implicit f-heavy, Implicit c-heavy, Hamilton cycle. 2010 Mathematics Subject Classification: 05C45, 05C38, 05C07

A graph G of order n is implicit claw-heavy if in every induced copy of K 1,3 in G there are two non-adjacent vertices with sum of their implicit degrees at least n. We study various implicit degree conditions (including, but not limiting to, Ore-and Fan-type conditions) imposing of which on specific induced subgraphs of a 2-connected implicit claw-heavy graph ensures its hamiltonicity. In particular, we improve a recent result of [X. Huang, Implicit degree condition for hamiltonicity of 2-heavy graphs, Discrete Appl. Math. 219 (2017) 126-131] and complete the characterizations of pairs of o-heavy and f-heavy subgraphs for hamiltonicity of 2-connected graphs.

Introduction

We use [START_REF] Bondy | Graph Theory with Applications[END_REF] for terminology and notation not defined here. In the paper only finite, simple and undirected graphs are considered.

Let G be a graph and H be a subgraph of G. For a vertex u ∈ V (G), the neighbourhood of u in H is denoted by N H (u) = {v ∈ V (H) : uv ∈ E(G)} and the degree of u in H is denoted by d H (u) = |N H (u)|. For two vertices u, v ∈ V (H), the distance between u and v in H, denoted by d H (u, v), is Fig. 1: Graphs B (bull), H (hourglass), N (net), D (deer), W (wounded) and Z i .

the length of a shortest (u, v)-path in H (if there are no (u, v)-paths in H, then d H (u, v) := +∞). When there is no danger of ambiguity, we can use N (u), d(u) and d(u, v) in place of N G (u), d G (u) and d G (u, v), respectively. We use N 2 (u) to denote the set of vertices which are at distance two from u, i.e., N 2 (u) = {v ∈ V (G) : d(u, v) = 2}. Let S be a graph. If there are no induced copies of S in G, then G is said to be S-free. Similarly, for a family S of graphs, G is S-free if it is S-free for every S ∈ S. If one demands G being S-free, then the family S is forbidden in G. A cycle in a graph G is called its Hamilton cycle (or hamiltonian cycle), if it contains all vertices of G, and G is called hamiltonian if it contains a Hamilton cycle. Forbidden subgraph conditions and degree conditions are two important types of sufficient conditions for the existence of Hamilton cycles in graphs.

The only connected graph of order at least three forbidding of which in a 2-connected graph G implies hamiltonicity of G, is the path P 3 (we use P i for a path with i vertices). When disconnected subgraphs are also considered, forbidding of 3K 1 also ensures hamiltonicity. The former fact can be deduced from [START_REF] Faudree | Characterizing forbidden pairs for hamiltonian properties[END_REF] and the latter from Chvátal-Erdős theorem [START_REF] Chvátal | A note on hamiltonian circuits[END_REF]. Actually, the graphs P 3 and 3K 1 are the only graphs of order at least three having this property. In [START_REF] Li | Forbidden pairs of disconnected graphs implying hamiltonicity[END_REF], Li and Vrána proved the necessity part of the following theorem.

Theorem 1 (Li and Vrána [26]). Let G be a 2-connected graph and S be a graph of order at least three. Then G being S-free implies that G is hamiltonian if and only if S is P 3 or 3K 1 .

The case with pairs of forbidden subgraphs other than P 3 and 3K 1 is much more interesting. The complete characterization of forbidden pairs of connected subgraphs for hamiltonicity, based partially on results from [START_REF] Broersma | Contemporary Methods in Graph Theory[END_REF], [START_REF] Duffus | Forbidden subgraphs and the Hamiltonian theme[END_REF], [START_REF] Goodman | Sufficient conditions for a graph to be hamiltonian[END_REF] and [START_REF] Gould | Forbidden subgraphs and hamiltonian properties of graphs[END_REF], was obtained by Bedrossian in [START_REF] Bedrossian | Forbidden subgraph and minimum degree conditions for Hamiltonicity[END_REF]. The 'only if' part of the following theorem is due to Faudree and Gould.

Theorem 2 (Bedrossian [1]; Faudree and Gould [START_REF] Faudree | Characterizing forbidden pairs for hamiltonian properties[END_REF]). Let R and S be connected graphs with R, S = P 3 and let G be a 2-connected graph. Then G being {R, S}-free implies G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S = P 4 , P 5 , P 6 , C 3 , Z 1 , Z 2 , B, N or W (see Fig. 1).

In [START_REF] Li | Forbidden pairs of disconnected graphs implying hamiltonicity[END_REF], Li and Vrána considered pairs of forbidden subgraphs that are not necessarily connected.

Theorem 3 (Li and Vrána [26]). Let R and S be graphs of order at least three other than P 3 and 3K 1 and let G be a 2-connected graph. Then G being {R, S}-free implies G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S is an induced subgraph of P 6 , W, N or K 2 ∪ P 4 .

A widely studied way of relaxing the forbidden subgraph conditions for hamiltonicity is allowing the subgraphs in the graph, but with some requirements regarding degrees of their vertices imposed on them. Some of these extensions exploit the concept of implicit degree, introduced by Zhu et al. in [START_REF] Zhu | Implicit degrees and circumferences[END_REF].

Definition 1 (Zhu,Li and Deng [32]). Let v be a vertex of a graph G and

d(v) = l + 1. Set M 2 = max{d(u) : u ∈ N 2 (v)}. If N 2 (v) = ∅ and d(v) ≥ 2, then let d 1 ≤ d 2 ≤ d 3 ≤ ... ≤ d l ≤ d l+1 ≤ ... be the degree sequence of vertices of N (v) ∪ N 2 (v). Define d * (v) = d l+1 , if d l+1 > M 2 , d l , otherwise.
Then the implicit degree of v in G is defined as

id(v) = max{d(v), d * (v)}. If N 2 (v) = ∅ or d(v) ≤ 1, then define id(v) = d(v).
Observe that, by the above definition, for every v ∈ V (G) the inequality id(v) ≥ d(v) holds. Some of the (implicit) degree conditions suitable for relaxing the forbidden subgraph conditions originate from the following classical results.

Theorem 4 (Fan [15]). Let G be a 2-connected graph of order n ≥ 3. If

d(u, v) = 2 ⇒ max{d(u), d(v)} ≥ n/2
for every pair of vertices u and v in G, then G is hamiltonian.

Theorem 5 (Ore [31]). Let G be a graph of order n. If for every pair of its non-adjacent vertices the sum of their degrees is not less than n, then G is hamiltonian.

The authors of [START_REF] Zhu | Implicit degrees and circumferences[END_REF] prove a counterpart of Ore's Theorem 5, where the degree sum condition is replaced with the implicit degree sum condition. Similar extension of Thereom 4 can be found in [START_REF] Chen | Longest cycles in 2-connected graphs[END_REF]. Theorems 4 and 5, and their extensions, gave rise to notions of f-heavy [START_REF] Ning | Ore-and Fan-type heavy subgraphs for Hamiltonicity of 2-connected graphs[END_REF], o-heavy [START_REF] Čada | Degree conditions on induced claws[END_REF], [START_REF] Ning | Ore-and Fan-type heavy subgraphs for Hamiltonicity of 2-connected graphs[END_REF], implicit f-heavy [START_REF] Cai | Fan-type implicit-heavy subgraphs for hamiltonicity of implicit claw-heavy graphs[END_REF] and implicit o-heavy graphs. Here, we cite the definitions of o-heavy and f-heavy from [START_REF] Ning | Ore-and Fan-type heavy subgraphs for Hamiltonicity of 2-connected graphs[END_REF] which are given as follows. Let G be a graph of order n.

A vertex v of G is called heavy (or implicit heavy) if d(v) ≥ n/2 (or id(v) ≥ n/2
). If v is not heavy (or not implicit heavy), we call it light (implicit light, respectively). For a given graph H we say that G is H-o-heavy (or implicit H-o-heavy) if in every induced subgraph of G isomorphic to H there are two non-adjacent vertices with the sum of their degrees (implicit degrees, respectively) in G at least n. And G is said to be H-f-heavy (or implicit H-f-heavy), if for every subgraph S of G isomorphic to H, and every two vertices u, v ∈ V (S) holds

d S (u, v) = 2 ⇒ max{d(u), d(v)} ≥ n/2 (max{id(u), id(v)} ≥ n/2, respectively).
For a family of graphs H, G is said to be (implicit)

H-o-heavy, if G is (implicit) H-o-heavy for every H ∈ H.
Classes of H-f-heavy and implicit H-f-heavy graphs are defined similarly. We note that the above definitions about H-f-heavy, H-o-heavy, and H-f-heavy are also all from [START_REF] Ning | Ore-and Fan-type heavy subgraphs for Hamiltonicity of 2-connected graphs[END_REF]. When a graph is implicit K 1,3 -o-heavy we will call it implicit claw-heavy.

Observe that every H-free graph is trivially H-o-heavy and H-f-heavy. Furthermore, every H-o-heavy (or H-f-heavy) graph is implicit H-o-heavy (implicit H-f-heavy, respectively). Replacing forbidden subgraph conditions with conditions expressed in terms of heavy subgraphs yielded the following extensions of Theorem 2.

Theorem 6 (B. Li, Ryjáček, Wang and S. Zhang [START_REF] Li | Pairs of heavy subgraphs for hamiltonicity of 2-connected graphs[END_REF]). Let R and S be connected graphs with R = P 3 , S = P 3 and let G be a 2-connected graph. Then G being {R, S}-o-heavy implies G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S = C 3 , P 4 , P 5 , Z 1 , Z 2 , B, N or W . Theorem 7. Let R and S be connected graphs with R = P 3 , S = P 3 and let G be a 2-connected graph. Then G being {R, S}-f-heavy implies that G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S is one of the following: -P 4 , P 5 , P 6 (Chen, Wei and X. Zhang [START_REF] Chen | Degree-light-free graphs and hamiltonian cycles[END_REF]), -Z 1 (Bedrossian, Chen and Schelp [START_REF] Bedrossian | A generalization of Fan's condition for Hamiltonicity, pancyclicity and Hamiltonian connectedness[END_REF]), -B (G. Li, Wei and Gao [START_REF] Li | A structural method for hamiltonian graphs[END_REF]), -N (Chen, Wei and X. Zhang [START_REF] Chen | Forbidden graphs and hamiltonian cycles[END_REF]), -Z 2 , W (Ning and S. Zhang [START_REF] Ning | Ore-and Fan-type heavy subgraphs for Hamiltonicity of 2-connected graphs[END_REF]).

Recently, motivated by the main result of [START_REF] Hu | A generalization of Fan's condition and forbidden subgraph conditions for hamiltonicity[END_REF], Li and Ning [START_REF] Li | Heavy subgraphs, stability and hamiltonicity[END_REF] introduced another type of heavy subgraphs. We say that an induced subgraph

H of G is c-heavy in G, if for every maximal clique C of H every non-trivial component of H -C contains a vertex that is heavy in G. Graph G is said to be H-c-heavy if every induced subgraph of G isomorphic to H is c-heavy. For a family H of graphs, G is called H-c-heavy if G is H-c-heavy for every H ∈ H.
Observe that every graph is trivially {K 1,3 , C 3 , P 3 }-c-heavy, since removal of a maximal clique from any of the three subgraphs results in a graph consisting of trivial components (or an empty graph). With that remark in mind, the authors of [START_REF] Li | Heavy subgraphs, stability and hamiltonicity[END_REF] extended Theorem 2 in the following way.

Theorem 8 (B. Li, Ning [START_REF] Li | Heavy subgraphs, stability and hamiltonicity[END_REF]). Let S be a connected graph of order at least three and let G be a 2-connected claw-o-heavy graph. Then G being S-cheavy implies that G is hamiltonian if and only if S = P 4 , P 5 , P 6 , Z 1 , Z 2 , B, N or W .

Similarly to implicit o-heavy and implicit f-heavy graphs, we can define implicit H-c-heavy and implicit H-c-heavy graphs by replacing the degree condition in the definition of c-heavy graphs with implicit degree condition. In the light of the results presented so far, and noting that every implicit claw-f-heavy graph is implicit claw-heavy, it seems worthwhile to tackle the following problems. Problem 1. Characterize all graphs S such that every 2-connected implicit claw-heavy and implicit S-o-heavy graph is hamiltonian. Problem 2. Characterize all graphs S such that every 2-connected implicit claw-heavy and implicit S-f-heavy graph is hamiltonian. Problem 3. Characterize all graphs S such that every 2-connected implicit claw-heavy and implicit S-c-heavy graph is hamiltonian.

As byproducts of the proof of our main result, we obtained the following partial answers to Problems 1-3.

Theorem 9. Let G be a 2-connected implicit claw-heavy graph. If G is implicit S-o-heavy for S being a subgraph of K 2 ∪P 4 , then G is hamiltonian. Theorem 10. Let G be a 2-connected implicit claw-heavy graph. If G is implicit S-f-heavy, with S being one of the graphs K 1 ∪P 3 , K 2 ∪P 3 , K 1 ∪P 4 , K 2 ∪ P 4 , P 4 , Z 1 and Z 2 , then G is hamiltonian. Theorem 11. Let G be a 2-connected implicit claw-heavy graph. If G is implicit S-c-heavy, with S being one of the graphs K 1 ∪ K 2 , 2K 1 ∪ K 2 , K 1 ∪ 2K 2 , K 2 ∪ K 2 , K 1 ∪ P 3 , K 2 ∪ P 3 , K 1 ∪ P 4 , K 2 ∪ P 4 , P 4 , P 5 and P 6 then G is hamiltonian.
Clearly, for S being any of the graphs

K 1 ∪ K 2 , 2K 1 ∪ K 2 , K 2 ∪ K 2 and K 1 ∪2K 2 ,
every graph is S-f-heavy. Observe also that each of the remaining subgraphs of K 2 ∪ P 4 appear in each of Theorems 9-11. Hence, as corollaries from these theorems and Theorems 6-8, we get the following complete characterizations of heavy pairs of (not necessarily connected) subgraphs for hamiltonicity.

Corollary 1. Let R and S be graphs other than P 3 and 3K

, P 6 , Z 1 , Z 2 , B, N , W , K 1 ∪ K 2 , 2K 1 ∪ K 2 , K 1 ∪ 2K 2 , K 2 ∪ K 2 , K 1 ∪ P 3 , K 2 ∪ P 3 , K 1 ∪ P 4 and K 2 ∪ P 4 .
We note that the assumption of the graph S being of order at least three in Corollary 3 is necessary, since every graph is trivially {K 1 , 2K 1 , K 2 }-cheavy.

For triples of forbidden subgraphs there are also many results. The following are two well-known results of this type (graphs D and H, called deer and hourglass, respectively, are represented on Fig. 1).

Theorem 12 (Broersma and Veldman [5]; Brousek [START_REF] Brousek | Forbidden triples for hamiltonicity[END_REF]). Let G be a 2connected graph. If G is {K 1,3 , P 7 , D}-free, then G is hamiltonian.

Theorem 13 (Faudree, Ryjáček and Schiermeyer [START_REF] Faudree | Forbidden subgraphs and cycle extendability[END_REF]; Brousek [START_REF] Brousek | Forbidden triples for hamiltonicity[END_REF]). Let G be a 2-connected graph. If G is {K 1,3 , P 7 , H}-free, then G is hamiltonian.

Note that the pair {K 1,3 , P 6 } that is present in Theorem 2 is missing in Theorem 6. A construction of a 2-connected, claw-free and P 6 -o-heavy graph that is not hamiltonian can be found in [START_REF] Li | Pairs of heavy subgraphs for hamiltonicity of 2-connected graphs[END_REF] 1 . Since every P 6 -o-heavy graph is also implicit {P 7 , D}-o-heavy, it is clear that Theorems 12 and 13 can not be improved by imposing the condition of implicit o-heaviness on all of their forbidden subgraphs. However, a slightly stronger implicit degree sum conditions are sufficient to ensure hamiltonicity. Our main result is the following.

Theorem 14. Let G be a 2-connected, implicit claw-heavy graph of order n such that in every path v 1 v 2 v 3 v 4 v 5 v 6 v 7 induced in G at least one of the following conditions is satisfied:

(1) id(v 4 ) ≥ n/2, or (2) id(v i ) + id(v j ) ≥ n for some i ∈ {1, 2}, j ∈ {6, 7}.
If [START_REF] Bedrossian | Forbidden subgraph and minimum degree conditions for Hamiltonicity[END_REF] Note that the conditions imposed on paths of order seven in Theorem 14 are satisfied in particular by implicit P 7 -f-heavy and implicit P 7 -c-heavy graphs. Similarly, the conditions imposed on induced deers are satisfied by implicit D-f-heavy graphs and implicit D-c-heavy graphs, and the conditions imposed on hourglasses are satisfied by implicit H-c-heavy graphs, implicit H-f-heavy graphs and implicit H-o-heavy graphs. Hence, Theorem 14 implies the following new results. Some previously known results, including recent extensions of Theorem 12 and Theorem 13, can also be deduced from Theorem 14.

Corollary 5 (Huang [21]). Let G be a 2-connected, implicit claw-heavy graph. If G is P 6 -free, then G is hamiltonian. Corollary 6 (Broersma,Ryjáček and Schiermeyer [4]). Let G be a 2connected, claw-f-heavy graph. If G is {P 7 , D}-free or {P 7 , H}-free, then G is hamiltonian.

Corollary 7 (Cai and H. Li [START_REF] Cai | Hamilton cycles in implicit 2-heavy graphs[END_REF]). Let G be a 2-connected, implicit claw-fheavy graph. If G is {P 7 , D}-free or {P 7 , H}-free, then G is hamiltonian.

Corollary 8 (Ning [29]). Let G be a 2-connected, claw-f-heavy graph. If G is {P 7 , D}-f-heavy or {P 7 , H}-f-heavy, then G is hamiltonian.

Corollary 9 (Huang [22]). Let G be a 2-connected, claw-f-heavy graph. If G is implicit {P 7 , D}-f-heavy or implicit {P 7 , H}-f-heavy, then G is hamiltonian.

Corollary 10 (Cai and Zhang [START_REF] Cai | Fan-type implicit-heavy subgraphs for hamiltonicity of implicit claw-heavy graphs[END_REF]). Let G be a 2-connected, implicit clawheavy graph. If G is implicit {P 7 , D}-f-heavy or implicit {P 7 , H}-f-heavy, then G is hamiltonian.

The rest of the paper is organized as follows. In Section 2 we define some auxiliary notions and present lemmas used throughout the proof. The proof of Theorems 9, 10, 11 and 14 is presented in Section 3.

Preliminaries

In this section we present three lemmas that will be used throughout the proofs of our main results. They make use of the notion of an implicit heavy cycle, which is a cycle that contains all implicit heavy vertices of a graph. For a vertex v ∈ V (G) lying on a cycle C with a given orientation, we denote by v + its successor on C and by v -its predecessor. For a set A ⊂ V (C) the sets A + and A -are defined analogously, i.e., A + = {v + : v ∈ A} and A -= {v -: v ∈ A}. We write xCy for the path from x ∈ V (C) to y ∈ V (C) following the orientation of C, and xCy denotes the path from x to y opposite to the direction of C. Similar notation is used for paths.

The next lemma is implicit in [28].

Lemma 1 (Li, Ning and Cai [28]). Every 2-connected graph contains an implicit heavy cycle.

A cycle C is called nonextendable if there is no cycle longer than C in G containing all vertices of C.

We use E * (G) to denote the set {xy : xy ∈ E(G) or id(x) + id(y) ≥ n}.

Lemma 2 (Huang [21]). Let G be a 2-connected graph on n ≥ 3 vertices and C be a nonextendable cycle of G of length at most n -1. If P is an xy-path in G such that V (C) ⊂ V (P ), then xy / ∈ E * (G).

Corollary 4 .

 4 Let G be a 2-connected, implicit claw-heavy graph. If G is -implicit {P 7 , D}-c-heavy or implicit {P 7 , H}-c-heavy, or -implicit P 7 -f-heavy and implicit D-c-heavy, or -implicit P 7 -f-heavy and implicit H-c-heavy, or -implicit P 7 -f-heavy and implicit H-o-heavy, or -implicit P 7 -c-heavy and implicit H-o-heavy, or -implicit P 7 -c-heavy and implicit H-f-heavy, then G is hamiltonian.

  1 , and let G be a 2-connected graph. Then G being {R, S}-o-heavy implies G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S is an induced subgraph of P 5 , W, N or K 2 ∪ P 4 . Let R and S be graphs other than P 3 and 3K 1 , and let G be a 2-connected graph. Then G being {R, S}-f-heavy implies G is hamiltonian if and only if (up to symmetry) R = K 1, 3 and S is one of P 4 , P 5 , P 6 , Z 1 , Z 2 , B, N, W , K 1 ∪ P 3 , K 2 ∪ P 3 , K 1 ∪ P 4 and K 2 ∪ P 4 . Let S be a graph of order at least three other than P 3 and 3K 1 , and let G be a 2-connected graph, claw-o-heavy graph. Then G being S-c-heavy implies G is hamiltonian if and only if S is one of P 4 , P 5

	Corollary 2. Corollary 3.

  in every induced D of G with the set of vertices {u 1 , u 2 , u 3 , u 4 , u 5 , u 6 , u 7 } and the set of edges {u 1 u 2 , u 2 u 3 , u 3 u 4 , u 3 u 5 , u 4 u 5 , u 5 u 6 , u 6 u 7 } at least one of the following conditions is satisfied: (a) id(u 4 ) ≥ n/2, or (b) id(u i ) + id(u j ) ≥ n for some i ∈ {1, 2, 4}, j ∈ {6, 7}, or[START_REF] Bedrossian | A generalization of Fan's condition for Hamiltonicity, pancyclicity and Hamiltonian connectedness[END_REF] in every induced H of G with the set of vertices {u 1 , u 2 , u 3 , u 4 , u 5 } and the set of edges {u 1 u 2 , u 2 u 3 , u 1 u 3 , u 3 u 4 , u 3 u 5 , u 4 u 5 } at least one of the following conditions is satisfied: (a) both u 1 and u 2 are implicit heavy, or (b) id(u i ) + id(u j ) ≥ n for some i ∈ {1, 2}, j ∈ {4, 5},

then G is hamiltonian.

Nevertheless, the condition of P6-o-heaviness can be replaced with other degree conditions on paths P6 to ensure hamiltonicity

of 2-connected claw-o-heavy graphs. We refer an interested reader to[START_REF] Li | Degree conditions restricted to induced paths for hamiltonicity of claw-heavy graphs[END_REF] for details.

Acknowledgements

The work of Wei Zheng and Ligong Wang was supported by the National Natural Science Foundation of China (No. 11671320) and the Natural Science Basic Research Plan in Shaanxi Province of China (No. 2018JM1032).

Proofs of Theorems 9-11 and 14

For a proof by contradiction suppose that a graph G satisfying the assumptions of any of the Theorems 9, 10, 11 or 14 is not hamiltonian. Then G is a 2-connected implicit claw-heavy graph. By Lemma 1, there is an implicit heavy cycle in G. Let C be a longest implicit heavy cycle in G and give C an orientation. From the assumption of 2-connectivity of G it follows that there is a path P connecting two vertices x 1 , x 2 ∈ V (C) internally disjoint with C such that |V (P )| ≥ 3. Let P = x 1 u 1 u 2 ...u r x 2 be such a path of minimum length. Note that this implies that P is induced unless x 1 x 2 ∈ E(G). The following four claims, as readers can see, also appeared in [START_REF] Cai | Fan-type implicit-heavy subgraphs for hamiltonicity of implicit claw-heavy graphs[END_REF][START_REF] Huang | Hamilton cycles in implicit claw-heavy graphs[END_REF][START_REF] Huang | Implicit degree condition for hamiltonicity of 2-heavy graphs[END_REF] since they are basic properties of a longest implicit heavy cycle. We also use them to start our proof.

By Claim 1, we have id(u 1 ) + id(x - 1 ) < n and id(u 1 ) + id(x + 1 ) < n. Since G is implicit claw-heavy, this implies that id(x - 1 ) + id(x + 1 ) ≥ n. Thus,

Proof. Observe that the paths

are paths such that V (C) ⊂ V (P 1 ) and V (C) ⊂ V (P 2 ). Thus, the Claim follows from Lemma 2.

Proof. Suppose to the contrary that x -

By Claim 4, without loss of generality, we assume that x - 1 x + 1 ∈ E(G). The following two claims were proved in [START_REF] Cai | Fan-type implicit-heavy subgraphs for hamiltonicity of implicit claw-heavy graphs[END_REF], here we omit their proofs.

Claim 5 (Cai and Zhang [9]).

By Claim 5, there is a vertex in x + i Cx - 3-i not adjacent to x i in G for i = 1, 2. Let y i be the first vertex in x + i Cx - 3-i not adjacent to x i in G for i = 1, 2. Let u be any vertex of P other than x 1 and x 2 and let z i be an arbitrary vertex in x + i Cy i for i = 1, 2. Claim 6 (Cai and Zhang [9]).

The proof splits now into subcases, depending on the conditions satisfied by G.

Since none of the vertices u 1 and u r belongs to C, both these vertices are implicit light. This implies that both y - 2 and y - 1 are implicit heavy, contradicting Claim 6. This contradiction proves the part of Theorem 10 regarding implicit K 2 ∪ P 4 -fheavy graphs. By taking induced subgraphs from {y -

, K 1 ∪ P 3 and K 2 ∪ P 3 , we get the same contradiction which can also prove the part of Theorem 10 regarding implicit K 1 ∪ P 4 -f-heavy graphs, implicit P 4 -f-heavy graphs, implicit K 1 ∪ P 3 -f-heavy graphs and implicit K 2 ∪ P 3 -f-heavy graphs, respectively.

Consider now the case when G is implicit K 2 ∪ P 4 -o-heavy. Then there is a pair of nonadjacent vertices in both {y - 1 , y 1 , u r , x 2 , y - 2 , y 2 } and {y - 2 , y 2 , u 1 , x 1 , y - 1 , y 1 } which have implicit degree sum not less than n. Let us focus on the set {y - 1 , y 1 , u r , x 2 , y - 2 , y 2 }. Since uz 1 , z 1 x 2 , z 1 z 2 / ∈ E * (G) by Claim 6, it follows that the pair of nonadjacent vertices with implicit degree sum at least n belongs to the set {u r , x 2 , y - 2 , y 2 }. Since uz 2 / ∈ E * (G) by Claim 6, we have id(x 2 ) + id(y 2 ) ≥ n. Now by id(x 1 ) + id(y 1 ) + id(x 2 ) + id(y 2 ) ≥ 2n, we have id(x 1 ) + id(y 2 ) ≥ n or id(x 2 ) + id(y 1 ) ≥ n, which contradicts Claim 6. This contradiction proves the part of Theorem 9 regarding implicit K 2 ∪ P 4 -o-heavy graphs, and the left part regarding implicit S-oheavy graphs for any proper subgraph S of K 2 ∪P 4 is implied by the validity of theorem for K 2 ∪ P 4 . Thus, the proof of Theorem 9 is completed.

Case 2. G is implicit S-f-heavy for S being one of Z 1 and Z 2 . Suppose first that G is implicit Z 1 -f-heavy. Then, since the vertex u 1 is implicit light by the choice of C and the set {x - 1 , x By Claim 3, there is a vertex in

Proof. Suppose that uw - 1 ∈ E(G). By Claim 1, we have that w

From Claim 1 and Claim 9 we have that {u, Proof. Suppose that x 1 x 2 / ∈ E(G). By the choice of P , Claim 1 and Claim 6 we have that P = y 1 y - 1 x 1 u 1 u 2 . . . u r x 2 y - 2 y 2 is an induced P r+6 , where r ≥ 1. Let y 1 y - 1 x 1 u 1 v 5 v 6 v 7 be the path induced by the first seven vertices of P . Since u 1 is implicit light, it follows from the assumptions of Theorem 14 that for some a ∈ {y 1 , y - 1 } and b ∈ {v 6 , v 7 } the inequality id(a) + id(b) ≥ n holds. Since b ∈ V (P ) ∪ {x 2 , y - 2 , y 2 } , this contradicts Claim 6.

We complete the proof by considering two cases, depending on the value of r. When r ≥ 2, we can use the method of the proof of Case 2 in [START_REF] Cai | Fan-type implicit-heavy subgraphs for hamiltonicity of implicit claw-heavy graphs[END_REF] completely, because the proof does not involve any heavy subgraphs other than the claw. Here we omit the proof and consider the case when r = 1.

Suppose that r = 1. Then the set {y 1 , y - 1 , x 1 , u 1 , x 2 , y - 2 , y 2 } induces a D. Since the vertex u 1 is implicit light, Claim 6 implies that G does not satisfy the conditions imposed on induced deers in Theorem 14. Hence, it satisfies the conditions imposed on H.

Observe that {x - 1 , x + 1 , x 1 , u 1 , x 2 } induces an H. Now it follows from Claim 5 and Claim 6 that both vertices x - 1 and x + 1 are implicit heavy. Similarly as in Case 2, this implies that both x - 2 and x + 2 are implicit light and x - 2 x + 2 ∈ E(G). But now the set {u 1 , x 1 , x 2 , x - 2 , x + 2 } induces an H. By Claim 5 and Claim 6, this contradicts the assumptions of Theorem 14. This final contradiction completes the proof of Theorem 14.

Observe that every 2-connected implicit-claw-heavy graph that is implicit S-c-heavy for S being one of K 1 ∪ K 2 , 2K 1 ∪ K 2 , K 1 ∪ 2K 2 , K 2 ∪ K 2 , K 2 ∪ P 3 , K 1 ∪ P 4 , K 2 ∪ P 4 , P 4 , P 5 and P 6 satisfies the assumptions of Theorem 14. Hence, together with Case 3, Case 4 completes also the proof of Theorem 11.


Mahieddine Dellabani
email: mahieddine.dellabani@imag.fr

Jacques Combaz
email: jacques.combaz@imag.fr

Marius Bozga
email: marius.bozga@imag.fr

Saddek Bensalem
email: saddek.bensalem@imag.fr

Local Planning of Multiparty Interactions with Bounded Horizon

Keywords: Distributed Real-Time Systems, Timed Automata, Knowledge

Dynamic scheduling of distributed real-time systems with multiparty interactions is acknowledged to be a very hard task. For such systems, multiple schedulers are used to coordinate the parallel activities of remotely running components. In order to ensure global consistency and timing constraints satisfaction, these schedulers must cope with significant communication delays while moreover, use only point-to-point message passing as communication primitive on the platform. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and we propose a distributed implementation method aiming to overcome the communication delays problem through planning ahead interactions. Moreover, we identify static conditions allowing to make the planning decisions local to different schedulers, and thus to decrease the overall coordination overhead. The method has been implemented and we report preliminary results on benchmarks.

Introduction

Over the past few decades, real-time systems have undergone a shift from the use of single processor based hardware platforms, to large sets of interconnected and distributed computing nodes. Such evolution stems from an increase in complexity of real-time software embedded on such platforms (e.g. electronic control in avionics and automotive domains [START_REF] Charette | This car runs on code[END_REF]), and the need to integrate formerly isolated systems [START_REF] Kopetz | An integrated architecture for dependable embedded systems[END_REF] so that they can cooperate as well as share resources, improving functionality and reducing costs.

The design and the implementation of distributed systems is acknowledged to be a very difficult task. A central question is how to efficiently coordinate parallel activities in a distributed system by means of primary communication primitives offered by the platform, such as point-to-point messages or broadcast. Considering real-time constraints brings additional complexity since any scheduling or control decision may not only impact system performance, but may also affect the satisfaction of timing constraints. To deal with such complexity, the community of safety critical systems often restricts its scope to predictable systems, which are represented with domain specific models (e.g. periodic tasks, synchronous systems, time-deterministic systems) for which the range of possible executions is small enough to be easily analyzed, allowing the precomputation of optimal control strategies. For non-critical systems, the standard practice is not to rely on models for precomputing scenarios but rather to design systems dynamically adapting at runtime to the actual context of execution. Such approaches do not offer any formal guarantee of timeliness. The lack of a priori knowledge on system behavior leaves also little room for static optimization.

In our framework, systems consist of components represented as timed automata that may synchronize on particular actions to coordinate their activities. Timed automata are strictly more expressive [START_REF] Abdellatif | Model-based implementation of real-time applications[END_REF] than time-deterministic systems considered in time-triggered approaches [START_REF] Kopetz | Time-triggered real-time computing[END_REF], [START_REF] Chabrol | Deterministic distributed safety-critical real-time systems within the oasis approach[END_REF], [START_REF] Ghosal | Event-driven programming with logical execution times[END_REF], [START_REF] Henzinger | Composable code generation for distributed giotto[END_REF]. Our framework also differs from the one proposed in [START_REF] Behrmann | UPPAAL 4.0[END_REF] and [START_REF] Zhao | A programming model for time-synchronized distributed real-time systems[END_REF] by considering not only binary, but also multiparty (n-ary) synchronizations, a.k.a. interactions, expressing the fact that a subset of components may jointly (and atomically) switch their states if given preconditions are fulfilled. Such high level coordination means are rarely part of the built-in primitives offered by distributed platforms, and thus need to be implemented using simpler ones, e.g. exchange of messages. This has been extensively studied in the untimed context [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF], [START_REF] Bagrodia | A distributed algorithm to implement n-party rendevouz[END_REF], [START_REF] Chandy | Parallel Program Design: A Foundation[END_REF], [START_REF] Chandy | The drinking philosopher's problem[END_REF], [START_REF] Pérez | An order-based, distributed algorithm for implementing multiparty interactions[END_REF], [START_REF] Parrow | Multiway synchronizaton verified with coupled simulation[END_REF], [START_REF] Bensalem | Methods for Knowledge Based Controlling of Distributed Systems[END_REF], [START_REF] Bensalem | Knowledge-based Distributed Conflict Resolution for Multiparty Interactions and Priorities[END_REF] but to the best of our knowledge, it has been solved for timed systems only under the assumption of non-decreasing deadlines in [START_REF] Bensalem | Rigorous system design flow for autonomous systems[END_REF], [START_REF] Triki | Distributed Implementation of Timed Component-based Systems[END_REF].

We contribute to this research field by proposing methods for scheduling interactions with bounded horizons, which aims to reduce the impact of communication delays on systems execution. In particular, (i) we define a semantics for planning interactions with bounded horizons, (ii) we provide sufficient conditions for this semantics to be correct, and (iii) we present an operational method to check those conditions using system knowledge.

The rest of the paper is organized as follows. In Section 2 we provide a formal definition of composition of timed automata with respect to multiparty interactions. We also present a semantics for planning interactions with bounded horizons. In Section 3, we study sufficient conditions for a safe planning of interactions. Thereafter, we use global knowledge of the system to refine the latest conditions for more precise results and in order to avoid unnecessary verification (Section 4). Finally, the application of previous results on various examples is presented in Section 5. Note that all the proofs can be found in the technical report [START_REF] Mahieddine Dellabani | Local planning of multiparty interactions with bounded horizon[END_REF].

Timed Systems and Properties

Global State Semantics

In the framework of the present paper, components are timed automata and systems are compositions of timed automata with respect to multiparty inter-actions. The timed automata we use are essentially the ones from [START_REF] Alur | A theory of timed automata[END_REF], however, slightly adapted to embrace a uniform notation throughout the paper.

Definition 1 (Component).

A component is a tuple (L, 0 , A, T, X , tpc) where L is a finite set of locations, 0 ∈ L is an initial location, A a finite set of actions, X is a finite set of clocks, T ⊆ L × (A × C × 2 X ) × L is a set of transitions labeled with an action, a guard, and a set of clocks to be reset, and tpc : L → C assigns a time progress condition, tpc , to each location, where C is the set of clock constraints defined by the following grammar:

C := true | x ∼ ct | x -y ∼ ct | C ∧ C | false,
with x, y ∈ X , ∼ ∈ {<, ≤, =, ≥, >} and ct ∈ R ≥0 . Time progress conditions are restricted to conjunctions of constraints of the form x ≤ ct.

Throughout the paper, we consider that components are deterministic timed automata, that is, at a given location and for a given action a, there is at most one outgoing transition from labeled by a. Given a timed automaton (L, 0 , A, T, X , tpc), we write a,g,r ---→ if there exists a transition τ = , (a, g, r), ∈ T . We also write:

guard (a, ) = g, if ∃τ = , (a, g, r), ∈ T false, otherwise Let V be the set of all clock valuation functions v : X → R ≥0 . For a clock constraint C, C(v) is a boolean value corresponding to the evaluation of C on v. For a valuation v ∈ V, v + δ is the valuation satisfying (v + δ)(x) = v(x) + δ,
while for a subset of clocks r, v[r] is the valuation obtained from v by resetting clocks of r, i.e. v[r](x) = 0 for x ∈ r, v[r](x) = v(x) otherwise. We also denote by C + δ the clock constraint C shifted by δ, i.e. such that C(v + δ) iff C(v).

Definition 2 (Semantics).

A component B = (L, 0 , A, T, X , tpc) defines the labeled transition system (LTS) (Q, A ∪ R >0 , →) where Q ⊆ L × V(X ) denotes the states of B and →⊆ Q × (A ∪ R >0 ) × Q denotes the set of transitions between states according to the rules:

-( , v) a -→ ( , v[r]) if a,g,r ---→ , and g(v) is true (action step). -( , v) δ -→ ( , v + δ) if tpc (v + δ) (time progress).
We define the predicate urg(tpc ) characterizing the urgency of a time progress condition tpc = m i=1

x i ≤ ct i at a state ( , v) as follows:

urg(tpc ) = m i=1 (x i = ct i ),
An execution sequence of B from a state ( , v) is a path in the LTS starting at ( , v) and that alternates action steps and time steps (time progress), that is:

( 1 , v 1 ) σ1 -→ . . . σi -→ ( n , v n ), n ∈ Z ≥0 , σ ∈ A ∪ R >0
In this paper, we always assume components with well formed guards meaning that transitions a,g,r ---→ satisfy g(v) ⇒ tpc (v) ∧ tpc (v[r]) for any v ∈ V. We say that a state ( , v) is reachable if there is an execution sequence from the initial configuration ( 0 , v 0 ) leading to ( , v), where v 0 assigns 0 to all clocks. Notice that the set of reachable states is in general infinite, but it can be partitioned into a finite number of symbolic states [START_REF] Tripakis | The analysis of timed systems in practice[END_REF][START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF][START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF]. A symbolic state is defined by a pair ( , ζ) where, is a location of B, and ζ is a zone, i.e. a set of clock valuations defined by a clock constraint (as defined in Definition 1). Efficient algorithms for computing symbolic states and operations on zones are fully described in [START_REF] Bengtsson | On clock difference constraints and termination in reachability analysis of timed automata[END_REF]. Given symbolic states {( j , ζ j )} j∈J of B, the predicate Reach(B) characterizing the reachable states can be formulated as:

Reach(B) = j∈J at( j ) ∧ ζ j ,
where at( j ) is true on states whose location is j , and clock constraint ζ j is straightforwardly applied to clock valuation functions of states.

We also define the predicate Enabled (a) characterizing states ( , v) at which an action a is enabled, i.e. such that ( , v) a -→ ( , v ). It can be written:

Enabled (a) = ( ,a,g,r, )∈T at( ) ∧ guard (a, )
Definition 3 (Deadlock). We say that a state ( , v) of a component B deadlocks, if neither action steps nor time steps can be done from this state. The following equation characterizes those states: ∀a ∈ A. ¬Enabled (a) ∧ urg(tpc )

In our framework, components communicate by means of multiparty interactions. A multiparty interaction is a rendez-vous synchronization between actions of a fixed subset of components. It takes place only if all the participants agree to execute the corresponding actions. Given n components B i , i = 1, . . . , n, with disjoint sets of actions A i , an interaction is a subset of actions α ⊆ ∪ 1≤i≤n A i containing at most one action per component, i.e. α ∩ A i is either empty or a singleton {a i }. That is, an interaction α can be put in the form {a i } i∈I with I ⊆ {1, . . . , n} and a i ∈ A i for all i ∈ I.

Definition 4 (Composition). For n components

B i = (L i , i 0 , A i , T i , X i , tpc i ), with L j ∩ L j = ∅, A i ∩ A j = ∅,
and X i ∩ X j = ∅ for any i = j, the composition γ(B 1 , . . . , B n ) w.r.t. a set of interactions γ is defined by a timed automaton S = (L, 0 , γ, T γ , X , tpc) where

0 = ( 1 0 , . . . , n 0 ), X = X 1 ∪. . .∪X n , L = L 1 ×. . .×L n , tpc = tpc 1 ∧ . . . ∧ tpc n for = ( 1 , . . . , n ), and T γ is such that α,g,r ---→ for α = {a i } i∈I , = ( 1 , .
. . , n ), and = ( 1 , . . . , n ), if for i ∈ I we have i = i , and for i ∈ I we have i ai,gi,ri -----→ i , and g α = i∈I g i and r = i∈I r i .

In practice we do not explicitly build compositions of components as presented in Definition 4. We rather interpret their semantics at runtime by evaluating enabled interactions based on current states of components. In a composition of n components B i∈{1,••• ,n} , denoted by γ(B 1 , . . . , B n ), an action a i can execute only as part of an interaction α such that a i ∈ α, that is, along with the execution of all other actions a j ∈ α, which corresponds to the usual notion of multiparty interaction.

Property 1 (Semantics of a Composition). Given a set of components {B 1 , • • • , B n } and an interaction set γ. The semantics of the composite component S = (L, 0 , γ, T γ , X , tpc) w.r.t the set of interaction γ, is the LTS (Q g , γ ∪ R >0 , → γ ) where:

-Q g = L × V(X ) is the set of global states, where L = L 1 × • • • × L n and X = n i=1 X i . We write a state q = ( , v) where = ( 1 , • • • , n ) ∈ L is a global location and v = (v 1 , • • • , v n ) ∈ V(X ) is a global clocks valuations.
γ is the set of interactions -→ γ is the set of labeled transitions defined by the rules:

• Action steps:

α = {a i } i∈I ∈ γ, ∀i ∈ I.( i , v i ) ai -→ ( i , v i ), ∀i / ∈ I.( i , v i ) = ( i , v i ) ( , v) α -→ γ ( , v )
• Time steps:

δ ∈ R >0 ∀i ∈ {1, • • • , n} tpc i (v i + δ) ( , v) δ -→ γ ( , v + δ)
In what follows, we consider only deadlock-free systems w.r.t the presented semantics. By abuse of notation, predicates at( i ) of individual components B i are interpreted on states of S, being true for ( , v)

iff B i is at location i in , i.e. iff ∈ L 1 × . . . × L i-1 × { i } × L i+1 × . . . × L n .
Similarly, clock constraints of components B i are applied to clock valuation functions v of the composition S = (L, 0 , γ, T γ , X , tpc) by restricting v to clocks X i of B i . Given an interaction α ∈ γ, these notations allow us to write Enabled (α) as:

Enabled (α) = =( 1,••• , n )∈Lα at( ) ∧ guard (α, ), = ( 1,••• , n )∈Lα at( ) ∧ ai∈α guard (a i , i ), = ( 1,••• , n )∈Lα n i=1 at( i ) ∧ ai∈α guard (a i , i ), = ai∈α Enabled (a i ),
where Let us consider as a running example the composition of four components C, T 1 , T 2 , and R of Figure 1. Component C represents a controller that initializes, releases, and ends tasks T 1 and T 2 . Tasks use the shared resource R during their execution. To implement such behavior, we consider the following interactions between C, R, and T 1 : α 1 = {init 0 , init 1 }, α 3 = {run, start 1 }, α 5 = {take, process 1 }, α 7 = {end 0 , f ree, end 1 }, and similar interactions α 2 , α 4 , α 6 , α 8 for task T 2 , as shown by connections on Figure 1. The controller is responsible for firing the execution of each task. First, it nondeterministically initializes one of the two tasks, i.e. executes α 1 or α 2 , and then releases it through interaction α 3 or α 4 . Tasks perform their processing independently of the controller, after being granted an access to the shared resource (α 5 or α 6 ). When ended by the controller, a task releases the resource (interactions α 7 or α 8 ) and go back to its initial location. An example of execution sequence of the system of Figure 1 is given below, in which valuations v of clocks x, y, and z are represented as a tuples (v(x), v(y), v(z)):

L α = { ∈ L| α,g,r ---→ }. 1 0 1 1 C end0 init0 z > 4 end0 run z := 0 2 0 2 1 2 2 x ≤ 3 T1 2 3 init1 start1 x := 0 process1 1 ≤ x ≤ 3 end1 3 1 3 0 3 2 y ≤ 3 T2 3 3 init2 start2 y := 0 process2 1 ≤ y ≤ 3
(( 1 0 , 2 0 , 3 0 , 4 0 ), (0, 0, 0)) 5 -→γ (( 1 0 , 2 0 , 3 0 , 4 0 ), (5, 5, 5)) α 1 --→γ (( 1 1 , 2 1 , 3 0 , 4 0 ), (5, 5, 5)) α 3 --→γ (( 1 0 , 2 2 , 3 0 , 4 0 ), (0, 5, 0)) 2 -→γ (( 1 0 , 2 2 , 3 0 , 4 0 ), (2, 7, 2)) α 5 --→γ (( 1 0 , 2 3 , 3 0 , 4 1 ), (2, 7, 2)) 3 -→γ (( 1 0 , 2 3 , 3 0 , 4 1
), (5, 10, 5))

α 2 --→γ (( 1 1 , 2 3 , 3 1 , 4
1 ), (5, 10, 5))

Weak Planning Semantics

The presented semantics is based on a global state operational semantics, that is, the operational semantics rules and the computation of possible interactions between timed components is achieved through global states. Considering a distributed context, components are intrinsically concurrent and their execution is asynchronous. This means that even if states of components participating in an interaction α are known, α cannot be executed in the global state semantics until the states of all components are known, which breaks the principle of distribution. Usually, components are mapped at different areas on the distributed platform in a way that better suits their interactions. In other terms, components that synchronize their actions are more likely to be next to each others. However, there are cases where several components participate in the same interaction but are mapped far from each other, which adds on communication delays to the interaction corresponding to the exchange of messages.

In order to reach an efficient scheduling, able of taking decisions ahead and using only partial (local) information, we define a different semantics based on a local planning of interactions. It aims to alleviate the problem of communication delays through an early decision making mechanism while preserving deadlock freedom property of the system. This is achieved by planning each interaction ahead, which means to choose an execution time within a certain horizon for each interaction, based only on the states of components involved in that interaction. Consequently, components are notified ahead through communication primitive, and will wait until the chosen execution time to perform their corresponding actions. Our approach is to define for each interaction its earliest planning date, which correspond to the maximum horizon value that ensure a safe planning of the considered interaction.

Preliminaries

We define the predicate Enabled δ (α) characterizing all states from which α is enabled if time progresses by δ units of time, that is:

Enabled δ (α) = ∈Lα at( ) ∧ ai∈α (guard (a i , i ) + δ) , (1)
Property 2. Let ( , v) be a state of the composition S. For any interaction

β ∈ γ such that, part(α) ∩ part(β) = ∅ and ( , v) β -→ γ ( , v
), where part(α) (resp. part(β)) represents components participating in interaction α (resp. β), if Enabled δ (α) holds at state ( , v) then it still holds at state ( , v ).

This property derives from the fact that executing interactions with disjoint set of components than α does not change the states of components participating in α, that is, for a i ∈ α we have i = i and v i = v i .

Property 3. Let ( , v) and ( , v + δ ), with δ ∈ R >0 be two states of the composition S.

If Enabled δ (α) is true at state ( , v) then Enabled δ-δ (α) is true at state ( , v + δ ) for δ ≤ δ.
This property can be found directly by writing Equation 1 on state ( , v + δ ). Let δ max be a partial function δ max : γ → R ≥0 that defines for each interaction a maximum horizon to be planned with. We define the predicate Enabled [0,δmax(α)] (α) characterizing all states from which α can be planned with a δ max (α)-horizon as follows:

Enabled [0,δmax(α)] (α) = ∈Lα (at( )∧ δmax(α) ( ai∈α guard (a i , i ))),
with δmax(α) represents an adaptation of the backward operators [START_REF] Tripakis | The analysis of timed systems in practice[END_REF] that satisfies: δmax(α) g(x) ⇔ ∃δ ≤ δ max (α).g(x + δ), Property 4. If the predicate Enabled δ (α) is true at a state ( , v), then the predicate Enabled [0,δmax(α)] (α) is also true for δ ≤ δ max (α).

Definition 5 (Plan). We say that two interactions α and β, α = β, conflicts if part(α) ∩ part(β) = ∅, and we write α#β. A plan π is a partial function π : γ → R ≥0 defining relative times for executing a subset of non conflicting interactions, i.e.:

α = α , π(α) =⊥, π(α ) =⊥ =⇒ ¬(α#α ).
We also denote by conf (π) the set of interactions conflicting with the plan π, i.e. conf (π) = {α | ∃β#α . π(β) = ⊥}, and part(π) the set of components involved in interactions planned by π, i.e. part(π

) = {B i | ∃α . π(α) = ⊥∧B i ∈ part(α)}.
We denote by min π the closest relative execution time of interactions in the plan π, i.e. min π = min {π(α) | α ∈ γ ∧ π(α) = ⊥} ∪ {+∞}. Notice that since π stores relative times, whenever time progresses by δ the value π(α) assigned by π to an interaction α should be decreased by δ, until it reaches 0 which means that α have to execute. We write π -δ describing the progress of time over the plan, that is, (π -δ)(α) = π(α) -δ for interactions α such that π(α) = ⊥.

We also write π -α to denote the removal of interaction α from the plan π, i.e. (π -α)(β) = π(β) for any interaction β = α, (π -α)(α) = ⊥. Similarly, π ∪ {α → δ} assigns relative time δ to α, α / ∈ conf (π), into existing plan π, i.e. (π ∪ {α → δ})(β) = δ for β = α, (π ∪ {α → δ})(β) = π(α) otherwise. Finally, the plan π such that π(α) = ⊥ for all interactions α ∈ γ is denoted by ∅.

We define below the semantics for planning each interaction α ∈ γ with δ max (α)-horizon.

Definition 6 (Weak Planning Semantics). Given a set of components {B 1 , • • • , B n } and an interaction set γ, we define the weak planning semantics of the composite component S = (L, 0 , γ, T γ , X , tpc), as the labeled transition system S p = (Q π , γ ∪ R >0 ∪ {plan}, ∼∼∼>) where:

-Q π = L × V(X ) × Π,
where L is the set of global location, V(X ) is the set of global clocks valuations, and Π is the set of plans.

-plan defines the action of planning interactions -∼∼∼> is the set of labeled transitions defined by the rules:

• Plan:

δ ≤ δ max (α), α ∈ γ, part(α) ∩ part(π) = ∅ Enabled δ (α) ( , v, π) ∼∼∼∼> plan(α,δ) ( , v, π ∪ {α → δ}).
• Exec:

π(α) = 0 ( , v, π) ∼∼∼> α ( , v , π -α)} • Time Progress: δ ∈ R >0 δ ≤ min π ∧ tpc i (v i + δ) i∈{1,••• ,n} ( , v, π) ∼∼∼> δ ( , v + δ, π -δ)
Example 2. Let us consider the following execution sequence for the example of Figure 1 under the weak planning semantics rules and for a value δ max = 5 for all interactions except α 5 and α 6 that will be assigned a δ max = 3:

(( 1 0 , 2 0 , 3 0 , 4 0 ), (0, 0, 0), ∅) ∼∼∼∼∼∼> plan(α 1 ,5)

(( 1 0 , 2 0 , 3 0 , 4 0 ), (0, 0, 0), {α1 → 5})∼∼∼>

5

(( 1 0 , 2 0 , 3 0 , 4 0 ), (5, 5, 5), {α1 → 0}) ∼∼∼> α 1 ((

(( 1 0 , 2 3 , 3 2 , 4 1 ), (5, 0, 0), {α7 → 4})∼∼∼> 3 (( 1 0 , 2 3 , 3 2 , 4 1 ), (8, 3, 3), {α7 → 1})
This execution sequence represents a path that alternates plan actions, time steps and execution of some interactions. We can see that for interaction α 7 which is planned 4 units of time ahead, the system cannot reach the state from which it can be executed since there is a time progress expiration in component T 2 after 3 time units from planning this interaction. This means that local planning of interactions doesn't always allow the progress of time and may thus, introduce deadlocks even if the system under the global semantics rules is deadlock-free.

Relation between Global and Weak Planning Semantics

We use weak simulation to compare the model under the global semantics rules and the one under the weak planning semantics rules by considering plantransitions unobservable. As explained in Example 2, the weak planning semantics does not preserve the deadlock property of our system. Nevertheless, the following proves weak simulation relations between the two semantics.

Theorem 1. For all the reachable states ( , v, π) of the weak planning semantics, and ∀α ∈ π, the predicate Enabled π(α) (α) is true.

Let S g = (Q g , γ ∪ R >0 , - → γ ) (resp. S p = (Q p , γ ∪ R >0 ∪ {plan}, ∼∼∼>)
) the labeled transition system characterizing the global (resp. weak planning) semantics.

Proposition 1. Relation 1 ∀δ ∈ R >0 .( , v, π) ∼∼∼> δ ( , v , π ) ⇒ ( , v) δ -→ γ ( , v ) Relation 2 ∀α ∈ γ.( , v, π) ∼∼∼> α ( , v , π ) ⇒ ( , v) α -→ γ ( , v )
It is straightforward that Relation 1 is a consequence of the definition of time progress in the weak planning semantics. For Relation Relation 2, using Definition 6, we can deduce that:

( , v, π) ∼∼∼> α ( , v , π ) ⇒ π(α) = 0,
By Theorem 1, this implies that Enabled 0 (α) is true at state ( , v, π), meaning that Enabled (α) is also true, which allows to infer Relation 2.

Corollary 1. If a state ( , v, π) ∈ Reach(S p ), then ( , v) ∈ Reach(S g ).

Definition 7 (Weak Simulation). A weak simulation over

A = (Q A , ∪{β}, → A ) and B = (Q B , ∪{β}, → B ) is a relation R ⊆ Q A × Q B such that we have: ∀(q, r) ∈ R, a ∈ .q a -→ A q =⇒ ∃r : (q , r ) ∈ R ∧ r β * aβ * ----→ B r and ∀(q, r) ∈ R : q β -→ A q =⇒ ∃r : (q , r ) ∈ R ∧ r β * -→ r . B simulates A, denoted by A R B, means that B can do everything A does.
The definition of weak simulation is based on the unobservability of β-transitions. In our case, β-transitions corresponds to plan-transitions.

Corollary 2. S p R1 S g with R 1 = {(q, π); q) ∈ Q p × Q g }.
Corollary 2 corresponds to a notion of correctness of the weak planning semantics: any execution in weak planning semantics corresponds to an execution in the global state semantics.

Theorem 2. S g R2 S p with R 2 = {(q; (q, π)) ∈ Q g × Q p |π = ∅}.
Theorem 2 states that the weak planning semantics preserves all execution sequences of the global state semantics. They are obtained using immediate planning, i.e. plans π such that π(α) = 0 or π(α) = ⊥. The weak planning semantics aims to reduces the impact of communication delays in the system through planning interactions execution ahead, and by considering only the state of components involved in the planned interaction, which is more suitable for distributed real-time systems than the global state semantics. It does not restrict the behavior of the global state semantics (see Theorem 2), and it executes ony sequences allowed by the global state semantics (see Corollary 2). However, it may introduce deadlocks as shown by the scenario presented in Example 2.

In the following, we present sufficient conditions for deadlock-free planning of interactions.

Deadlock-free Planning

As explained in Example 2, local planning of interactions can introduce deadlocks in the system since it does not consider time progress conditions of components not participating in the planned interactions. Effectively, the weak planning semantics ensures that time can progress until the chosen execution date only w.r.t timing constraints of participating components, but such progress may be disallowed by the rest of the system leading to deadlock states. In this section, we provide sufficient conditions for having deadlock-free planning.

Planning an interaction α implies not only blocking components participating in α until α executes, but also preventing the system from planning interactions involving these components, that is, interactions of conf (α). Consequently, the subset of interactions γ ⊆ γ that can be planned at a given state ( , v, π) depends on the content of the plan π. It satisfies γ = {γ \ π ∪ conf (π)}.

By Corollary 1, a (reachable) deadlock state ( , v, π) of the weak planning semantics S p is such that ( , v) is a reachable state of the global state semantics S g . Since we assume that S g is deadlock-free, ( , v) is not a deadlock in S g . A deadlock state ( , v, π) of S p is caused by the plan π which is restricting the execution in S p w.r.t. S g : interactions α of π cannot execute before π(α) time units, and interactions α ∈ conf (π) are blocked for (at least) max {π(β) | β#α}. Notice that due to well-formed guards, in a deadlock state ( , v, π) we have necessarily at( i ) ∧ urg(tpc i ) for a location i of a component B i / ∈ part(π).

Theorem 3. If a state ( , v, π) ∈ Reach(S p ) deadlocks, the following equation is satisfied:

α∈π Enabled π(α) (α) A ∧ Bi∈S\part(π) i∈Li at( i ) ∧ urg(tpc i ) B ∧ α∈π π(α) = 0 ∧ α∈π (Enabled (α) ∨ α∈conf (π) Enabled (α) C (2)
From Theorem 1, Term A of Equation 2 represents an invariant of the system. On the other hand, terms B and C characterize the deadlock: Term B expresses the urgency of time progress condition in components not involved in the planned interactions, whereas, term C specifies the origin of the deadlock: it characterizes states ( , v, π) of S p for which π restricts the execution of an interaction α whereas it can be executed at ( , v) in S g . As explained above, such an interaction satisfies π(α) > 0 or α ∈ conf (π).

It is clear that Equation 2 depends on the reachable states of the planning semantics since it explicitly depends on plans π. The following gives weaker conditions for deadlocks which are independent of the plan. Theorem 4. Let Φ(α) be the following predicate:

Enabled [0,δmax(α)] (α) ∧ Bi∈S\part(α) i∈Li at( i )∧urg(tpc i )∧ β∈α∪conf (α) Enabled (β) (3)
where Enabled [0,δmax(α)] (α) is the result of transforming all the timing con-

straints of the form x ≤ ct by x < ct in δmax(α) ( ai∈α guard (a i , i )) of Enabled [0,δmax(α)] (α).
If a reachable state of the system ( , v, π) deadlocks then the following is satisfied:

∃α ∈ γ, Φ(α) ∧ δ max (α) = 0 (4)
Let schedule(α, δ max (α)) be the following predicate:

schedule(α, δ max (α)) = ¬Φ(α) ∨ (δ max (α) = 0)
Using Theorem 4 and Corollary 1, we can conclude that for all interactions α ∈ γ and for all reachable states of the global state semantics S g , if the predicate schedule(α, δ max (α)) is satisfied, then the weak planning semantics is deadlock-free. Notice that given an interaction α ∈ γ the satisfaction of schedule(α, δ max (α)) on Reach(S g ) depends only on δ max (α). Moreover, it is monotonic, that is, if it holds for δ max (α) then it holds for any δ max (α) < δ max (α). This provides means for building implementations that plan interactions as soon as possible by taking for δ max (α) the maximal value of δ such that schedule(α, δ) holds on Reach(S g ).

Using Knowledge to Enhance Deadlock-free Planning

In Section 3, we presented sufficient conditions that ensure a deadlock-free planning of interactions. Effectively, we use an SMT solver to check the satisfiability of those conditions on the reachable states of the planning semantics. As explained in Section 3 to prove deadlock-freedom of weak planning semantics it is sufficient to prove that for all interactions α ∈ γ the following formula:

Reach(S g ) ∧ ¬schedule(α, δ max (α))
is unsatisfiable. In practice, we do not calculate Reach(S g ) to avoid the combinatorial explosion problem inherent to composition of timed automata. Instead, we use over-approximations of the latter which enable us to build stronger conditions of deadlock freedom. As explained in more detail below, these overapproximations take the form of invariants I (i.e. such that Reach(S g ) ⇒ I) that are used to establish deadlock freedom by checking the unsatisfiability of:

I ∧ ¬schedule(α, δ max (α))

Timed Invariants

Our approach consists in leveraging global knowledge of the system in the form of invariants that will be used to approximate Reach(S g ). Locations reachable in a composition S = γ(B 1 , . . . , B n ) are necessary combinations of reachable locations of individual components B i , i.e, Reach(S g ) ⇒ n i=1 Reach(B i ). However, in general not all combinations are reachable since components are not fully independent as they synchronize through interaction set γ. Moreover, individual reachable states of components do not express the fact that time progresses the same way in all components.

For example, a global location may be not reachable because component locations having disjoint time progress conditions, or an interaction may be not enabled from a state because of an empty timing constraint. Such properties require additional relationships relating clocks of different components that are not available in Reach(B i ) as it is is restricted to clocks of a single component.

We follow the approach of [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF], [START_REF] Rayana | Compositional verification for timed systems based on automatic invariant generation[END_REF], [START_REF] Saddek Bensalem | Compositional invariant generation for timed systems[END_REF] for reinforcing individual reachable states of components with global invariants on clocks. They are induced by simultaneity of transitions execution when executing an interaction and the synchrony of time progress. To compute such invariants, additional history clocks are first introduced in components. History clocks are associated to actions of components and to interactions, and reset upon their execution. They do not modify the behavior since they are not involved in timing constraints. They only reveal local timing of components, relevant to the interaction layer, which allows to infer further properties referred as history clocks inequalities in [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF], expressing the fact that the history clock of an interaction is necessary equal to history clocks of its actions after its execution and until the execution of another interaction involving these actions. By combining history clocks inequalities E(S) and symbolic states of components, we have:

Reach(S g ) ⇒ n i=1 Reach(B i ) ∧ E(S g ) (5)
Notice that for such systems with multiparty interactions, other types of invariants could be used, like those of [START_REF] Bensalem | Incremental generation of linear invariants for component-based systems[END_REF] that corresponds to the notion of Sinvariants in the Petri net community [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]. Even if they are time abstracted, it is proved that they are appropriate for verifying non coverage of subsets of individual locations.

Example 3. We illustrate the application of (5) for a safe planning of interactions by considering again example of Figure 1. It can be shown that locations configuration including location 3 2 (resp. 2 2 ) does not satisfy the predicate schedule(α, δ max (α)) for interaction α 5 (resp. α 6 ). In the following, we prove how such configurations can be excluded using history clocks inequalities. Since action run of C is synchronized with either start 1 of T 1 or start 2 of T 2 , and since history clocks h a of an action a is reset whenever a is executed, by [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF] the history clock inequalities for run are:

(h run = h start1 < h start2 -4) ∨ (h run = h start2 < h start1 -4). (6)
Equation ( 6) states that h run is equal to the history clock corresponding to the last synchronization, i.e. either h start1 or h start2 , and is lower than history clocks of previous synchronizations. Value 4 in ( 6) is obtained considering separation constraints computed from symbolic states of components [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF]: two occurrences of run are separated by at least 4 time units because of timing constraints of C, and so do occurrences of start 1 or start 2 which can only execute jointly with run. To relate history clocks with components clocks, we simply include history clocks when computing symbolic states of components (i.e. Reach(B i ) for components), which is used to establish here that x = h start1 and y = h start2 . That is, combined with (6) we obtain x < y -4 or y < x -4. By definition of Enabled we have Enabled (

α 6 ) = at( 2 2 ) ∧ (1 ≤ x ≤ 3). Similarly, Enabled (α 6 ) = at( 3 2 ) ∧ (1 ≤ y ≤ 3
). This proves that components T 1 and T 2 can never be at locations 3 2 and 2 2 at the same time. Thus, while checking for interaction α 5 (resp. α 6 ) that n i=1 Reach(B i )∧E(S g )∧¬schedule(α, δ max (α)) is unsatisfiable, this case will be excluded using history clock inequalities.

Implementation and Experiments

The presented method has been implemented as a middleend filter of the BIP compiler. BIP [START_REF] Basu | Modeling heterogeneous real-time components in bip[END_REF] is a highly expressive, component-based framework with rigorous semantics that allows the construction of complex, hierarchically structured models from single components characterized by their behavior. The method input consists of real-time BIP model and a file containing an approximation of the reachable states of components combined with history clock inequalities as explained in Section 4. The latter is generated using the RTD-Finder tool, a verification tool for real-time component based systems modeled in the RT-BIP language. Our filter generates for each interaction of the input model a Yices [START_REF] Dutertre | The yices smt solver[END_REF] file containing system invariants together with the condition for planning the considered interaction, that is, ¬schedule(α, δ max (α)). Thereafter, Yices checks the satisfiability of n i=1 Reach(B i )∧ E(S g ) ∧ ¬schedule(α, δ max (α)). We also define δ max (α) as free variable. If this condition is unsatisfiable, then planning interactions α is safe and unbounded that is, δ max = +∞. Otherwise, Yices generates a counter-example. Due to the monotony of the condition, this counter-example can be used to find the maximal value of δ max (α) satisfying the above condition using a binary search algorithm. Together, the determined values of the bounds δ max for each interaction will affect the dynamic of the hole system: for an interaction α the greater δ max (α) is, the more flexible the scheduling of α will be.

We ran our experiments on three other models besides of the model presented in Figure 1: Pacemaker [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF], Fischer [START_REF] Lamport | A fast mutual exclusion algorithm[END_REF], and Gear controller [START_REF] Lindahl | Formal Design and Analysis of a Gearbox Controller[END_REF]. We developed an implementation of these models in RT-BIP. The following tables show the result of our experiments. Table 1 gives a detailed result of the experiments ran on the Task Manager model 1. It summarizes, for each interaction, its conflicting interactions and the potential locations for which a time progress condition may expire while planning it (column tpc). The last column, δ max (α), details the maximum horizon for planning interaction α. Notice that the symmetry of the model allows to perform the verification on interactions α 1 , α 3 , α 5 , and α 7 and deduce the results for the other interactions. Table 2 depicts the results of our experiments on different models. For each model, it summarizes the number of interactions that can be safely planned with an unbounded horizon (δ max = ∞). It also gives the number of interactions that cannot be planned in advance, and thus need to be executed immediately after being planned(δ max = 0).

Conclusion and Future Work

We presented a method for scheduling real-time systems in a distributed context considering models including multiparty interactions. The proposed approach defines sufficient conditions ensuring a deadlock-free local planning of interactions with certain horizons. Moreover, it is proved that those conditions are interaction dependent, in other terms, this means that changing the planning horizon of an interaction does not affect the planning of other interactions. A key innovative idea is the use of global knowledge in addition to local components informations to enhance the local scheduling of interactions. The computed knowledge captures not only the way components synchronize through interactions, but it also consider the history clock inequalities between those interactions and express explicitly the synchrony of time progress.

There are many open problems to be investigated such as: (i) considering more conditions when planning an interaction based on the state of components involved in this interaction, and (ii) defining a lower bound for planning interaction. The latter represents an important point meaning that, if planning interactions can be ensured for a lower bound, that effectively represents the communication delays of the target platform, then all the problems induced by those delays, such as global consistency and performance dropping will be solved.

Fig. 1 :

 1 Fig. 1: Task Manager

Table 1 :

 1 Detailed Results of the Task Manager Experiments

	Interaction Conflicting Interactions tpc δmax(α)
	α1	α2, α4, α8	3 2	∞
	α3	α2, α4, α8	3 2	∞
	α5	α6, α8	3 2	∞
	α7	α2, α4	3 2	0

Table 2 :

 2 Results of Experiments

	Model	Number of Interactions δmax = 0 δmax = ∞ total
	Task Manager	2	6	8
	Pacemaker	0	6	6
	Gear	0	17	17
	Fischer	0	10	10


Irifune

C Sanloup

B Cochain

C De Grouchy

K Glazyrin

Z Konôpkova

H-P Liermann

I Kantor

Torchio

O Mathon

T Irifune

Behaviour of niobium during early Earth's differentiation: insights from its local structure and oxidation state in silicate melts at high pressure

Keywords: numbers Niobium valence, niobium coordination number, magmas, high pressure, X-ray absorption spectroscopy

Behaviour of niobium during early Earth's differentiation: insights from its local structure and oxidation state in silicate melts at high pressure

Introduction

Niobium (Nb) is a high field strength element (HFSE) due to its small size and high charge. Nb can occur as Nb 2+ , Nb 4+ , and Nb 5+ oxides under ambient conditions, while Nb 5+ is the only oxidation state present in geological minerals. It is of geochemical interest due to what is termed the 'missing niobium' or 'niobium paradox'. The ratio of Nb to Ta and La for the crust, depleted mantle, and ocean island basalts is less than expected for a chondritic Earth [START_REF] Munker | Evolution of planetary cores and the Earth-Moon system from Nb/Ta systematics[END_REF]. This has been used to infer the presence of a hidden Nb-rich, or super-chondritic, reservoir. Potential reservoirs have been proposed such as subducted eclogite (e.g. [START_REF] Rudnick | Rutile-bearing refractory eclogites: Missing link between continents and depleted mantle[END_REF]), an early enriched crustal reservoir derived from a Hadean magma ocean and subducted to the D" layer [START_REF] Nebel | Deep mantle storage of the Earths missing niobium in late-stage residual melts from a magma ocean[END_REF], and the Earth's core [START_REF] Wade | The Earths missing niobium may be in the core[END_REF]. Preferential sequestration of Nb over Ta in the core could indeed be a consequence of Nb valence change in silicate melts during core formation upon decreasing fO 2 conditions as inferred from metal/silicate partitioning experiments [START_REF] Wood | Core formation and the oxidation state of the Earth: Additional constraints from Nb, V and Cr partitioning[END_REF][START_REF] Cartier | Redox control of the fractionation of niobium and tantalum during planetary accretion and core formation[END_REF]. This latter hypothesis is supported by recent analysis of silicate meteorites from various asteroidal parent bodies, with the most reduced ones having lower Nb/Ta ratios [START_REF] Munker | Silicate Earth's missing niobium may have been sequestered into asteroidal cores[END_REF]. The accretion of such bodies on the growing Earth's would explain its subchondritic Nb/Ta signature, assuming that full core/mantle re-equilibration was not attained. The former hypothesis of Nb sequestration in an early enriched crustal reservoir might be tested by exploring the effect of pressure on the local structure of Nb in melts. Indeed, structural changes in silicate melts affect their physical properties, but they may also affect their chemical properties and the way elements partition between the melt and crystals upon partial melting of a source mantle rock. Links between melt structure and crystal/melt element partitioning have been explored theoretically at ambient pressure for some trace elements (e.g. [START_REF] Wagner | Trace element partitioning between silicate melts -a molecular dynamics approach[END_REF] and references therein). At high pressure, lutetium (Lu) was shown experimentally to undergo a change of coordination number circa 4-5 GPa in basaltic melts, a change that underpins the evolution of Lu mineral/melt partitioning at high pressure [START_REF] De Grouchy | Lutetium incorporation in magmas at depth: changes in melt local environment and the influence on partitioning behaviour[END_REF], and consequently the evolution of the Lu/Hf ratio in terrestrial rocks depending on the melting depth. In the case of Nb, previous XAS studies in silicate glasses at ambient conditions were initially focused on continental crust analogues (sodium disilicate NS2, sodium trisilicate NS3, and haplogranitic glasses), and found that Nb is present as NbO 6 moiety with a +5 valence [START_REF] Piilonen | Structural environment of Nb 5+ in dry and fluid-rich (H 2 O, F) silicate glasses: A combined XANES and EXAFS study[END_REF]. The range of compositions and fO 2 conditions was later extended to Fe-free mafic glasses between iron-wüstite (IW)-4.3 to IW+6.7, but no valence change was observed [START_REF] Burnham | The oxidation states of niobium and tantalum in mantle melts[END_REF]. Only at IW-7.9 was Nb found in +2 valence in a silicate glass that had been previously equilibrated with molten Fe-alloy at 5 GPa [START_REF] Cartier | Evidence for Nb 2+ and Ta 3+ in silicate melts under highly reducing conditions: A XANES study[END_REF]. Quench effects might however occur, and the only in situ XAS study on Nb environment in a granitic melt, using a hydrothermal diamond-anvil cell at 0.7 GPa-983 K, also shows a coordination number of 6 in both glass and melt, while no information is given on Nb oxidation state [START_REF] Mayanovic | Synchrotron x-ray spectroscopy of Eu/HNO 3 aqueous solutions at high temperatures and pressures and Nb-bearing silicate melt phases coexisting with hydrothermal fluids using a modified hydrothermal diamond anvil cell and rail assembly[END_REF]. Here we use X-ray Absorption Near Edge Structure (XANES) and Extended X-Ray Absorption Fine Structure (EXAFS) spectroscopies with resistive heating diamond anvil cells (RH-DAC) to determine the oxidation states of Nb and its coordination and oxygen distance in silicate melts at high pressure and temperature.

Samples and high pressure XAS data acquisition

The haplogranite (HPG) composition was chosen as a simplified analogue of the continental crust. The HPG glass was synthesized by mixing together the appropriate amounts of chemical grades (SiO 2 , Al 2 O 3 , K 2 CO 3 , Na 2 CO 3 ) from Alfa Aesar with purity >99.99% (Table 1). The mixed powders were ground and decarbonated for 12 hours at 1273 K, then fused at 1873 K in a platinum crucible for 1 hour. The molten glass was quenched by immediately placing the crucible into cold water. The glass was then ground and remelted twice to ensure chemical homogeneity and finally checked for lack of crystals and bubbles. The composition of the glass (Table 1) was determined by taking an average over 10 analyses made with a CAMECA SX100 electron microprobe at the EMMAC centre (The Edinburgh Materials and Micro-Analysis Centre), University of Edinburgh. The microprobe analyses were performed under soft operating conditions, in order to avoid any loss of Na, with a 15 kV accelerating voltage, a defocused beam of 10 µm and a current of 15 nA. Nb was added in the form of high purity Nb 2 O 5 to the ground glass to match a 0.5 at% Nb content (3.75 wt% Nb). Approximately 10 wt% water was added to the sample through high pressure addition in a pistoncylinder press at 2 GPa and 1670 K in order to lower the melting temperature to temperatures achievable in a resistively heated diamond anvil cell. The samples were crushed to a fine homogeneous powder before being loaded. XAS measurements at ambient and high pressure-high temperature (high P -T ) conditions were performed in transmission mode across the Nb-K edge (18.97 keV) on the BM23 beamline at the European Synchrotron Radiation Facility (ESRF -Grenoble, France). Details of the beamline layout are reported elsewhere [START_REF] Mathon | The time-resolved and extreme conditions XAS (TEXAS) facility at the European Synchrotron Radiation Facility: the general-purpose EXAFS bending-magnet beamline BM23[END_REF]. The storage ring was operating in the 16bunch mode with an average current of 200 mA. X-rays were generated using a bending magnet, and monochromatized with a double-crystal, fixed exit Si(111) monochromator. The beamsize was 0.1×0.3 mm 2 . The energy of the EXAFS spectra was calibrated using a Nb metallic foil and no significant drift of the energy was observed for the duration of the measurements. EXAFS spectra of the Nb-bearing reference compounds (Nb 2 O 5 and NbO 2 ), the Nb-doped HPG glass and the in situ EXAFS spectra measurements were recorded in transmission from 18800 eV to 19846 eV with a total scan time of about 20 minutes. EXAFS spectra of the melt were measured under high P -T conditions of up to 9.3 GPa and 1350 K using resistive heating diamond-anvil cell under vacuum conditions [START_REF] Shen | Distinct thermal behavior of GeO 2 glass in tetrahedral, intermediate, and octahedral forms[END_REF]. We used nano-polycrystalline diamond anvils of 400 µm culets synthesized at the Geodynamics Research Center (Ehime University, Japan) instead of single crystal diamond anvils in order to eliminate the serious interference of the diamond Bragg peaks in the EXAFS spectra [START_REF] Ishimatsu | Applications of nano-polycrystalline diamond anvils to X-ray absorption spectroscopy under high pressure[END_REF]. High T was achieved by resistive heating through a graphite heater. Temperature was recorded by two R-type thermocouples (thermally insulated from the diamond anvils) placed on both sides of the gasket indent as close to the sample chamber as possible. Finely ground Nb-HPG sample powder was loaded into the 250 µm electro-eroded hole of the rhenium gasket, along with a ruby sphere and a Pt foil inserted on the side of the sample chamber for P calibration. The powder was packed into the hole thoroughly to avoid collapse of the sample chamber. Experiments were conducted by cold compression of the sample to a given pressure, followed by gradual heating to the desired temperature between 1200 K and 1350 K. Diffraction on the Pt calibrant was collected for 300 s at each pressure point before and during heating using a MAR165 CCD detector. P was determined before and during the experiment by monitoring ruby fluorescence and the cell volume of Pt [START_REF] Fei | A critical evaluation of pressure scales at high temperatures by in situ x-ray diffraction measurements[END_REF]. Estimated error bars are ±0.5 GPa on P , and ±50 K on T . Before recording the EXAFS spectra, the molten state of the sample was assessed by the disappearance of crystalline Bragg peaks in the diffraction patterns and concomitant appearance of diffused scattered signal by the melt. All melt spectra were collected between 1270 K and 1350 K. X-ray diffraction spectra of the sample were systematically recorded before and after collection of EXAFS data to check for the lack of crystallization.

EXAFS data analysis

The extended X-ray absorption fine structure (EXAFS) signal (χ) was extracted using the DEMETER package based on the IFEFFIT program [START_REF] Ravel | HEPHAESTUS: data analysis for X-ray absorption spectroscopy using IFEFFIT[END_REF]. Briefly, an average of 4 to 6 EXAFS spectra was normalized to the absorption edge height using the background algorithm from the DEMETER package with the minimum atom-atom contact distance, R bkg , chosen as 1.3 Å. The edge E 0 was calculated as the first maximum of the first derivative of the absorption spectra. EXAFS interference functions k 2 χ(k) were exported into ARTEMIS, Fourier transformed and fit to the EXAFS equation [START_REF] Newville | EXAFS analysis using FEFF and FEFFIT[END_REF] over k-range of 2.25-12 Å-1 for the crystalline references, and 2.5-8.5 Å-1 for the glasses at ambient conditions and the melts at high P -T conditions. For all compositions, the fit parameters included the number of oxygen neighboring atoms, CN , average distance, d, to the central Nb atom, the Debye-Waller factor, σ 2 , characterizing the degree of disorder present in the signal, the amplitude reduction factor S 2 0 and the energy offset 2). The amplitude reduction factor S 2 0 was fit for the reference NbO 2 EXAFS spectrum, and set to the best fit value found, i.e. 0.73 ± 0.09, for the other spectra to minimize errors and correlation between the derived structural parameters. The fitted values of ∆E 0 never exceed 4 eV confirming the validity of the fitting procedure. Finally, the third order anharmonic cumulant-expansion fitting parameter, σ 3 , which measures the asymmetry in the signal disorder, was included in the fitting of the melts EXAFS spectra in order to partially compensate for the structural disorder due to the high P -T conditions but did not improve the fitting results and is therefore not presented here. The goodness of the fits is expressed by the R-factor which is a sum-of-squares of the fractional misfit between model and EXAFS data [START_REF] Newville | Analysis of multiplescattering XAFS data using theoretical standards[END_REF].

Results and discussion

Nb K-edge XANES spectra of the starting glass at high pressure and room temperature (R), in the melt at high pressure (M) and the resulting quench at high pressure (Q), and of the Nb 2 O 5 and NbO 2 references are shown in Fig. 1.

The XANES spectra of the references show a clear difference in the edge position with the inflexion point E 0 of the Nb 5+ reference Nb 2 O 5 being at 19004.05 eV while the one of the Nb 4+ reference NbO 2 lies almost 3 eV below at 19001.35 eV, highlighted in Fig. 2. Overall, the sample spectra bear close resemblance to those of the alkali niobosilicate crystals (vuonnemite and labuntsovite) and glasses presented in [START_REF] Piilonen | Structural environment of Nb 5+ in dry and fluid-rich (H 2 O, F) silicate glasses: A combined XANES and EXAFS study[END_REF], for which Nb is pentavalent and coordinated to 6 oxygen atoms. All glasses show a doublet in the main edge (Fig. 1), similar to those for the silicate glasses [START_REF] Piilonen | Structural environment of Nb 5+ in dry and fluid-rich (H 2 O, F) silicate glasses: A combined XANES and EXAFS study[END_REF] and for 6-coordinated Zr in synthetic glasses [START_REF] Farges | Structural environments of incompatible elements in silicate glass/melt systems: I. Zirconium at trace levels[END_REF][START_REF] Farges | Water in Zr-bearing synthetic and natural glasses[END_REF]. These features tend to disappear in the melt in agreement with a disordered local structure at high temperature as observed by [START_REF] Mayanovic | Synchrotron x-ray spectroscopy of Eu/HNO 3 aqueous solutions at high temperatures and pressures and Nb-bearing silicate melt phases coexisting with hydrothermal fluids using a modified hydrothermal diamond anvil cell and rail assembly[END_REF] at 0.7 GPa for Nb. The pre-edge resolution and white line components exhibit small but clear differences between the melts and glasses, either before or after heating as shown in Figs. 1 and2a, and at the exception of the pre-edge features at 9.3 GPa where no change is observed. The first derivative of the XANES spectra, from which is determined the position of the inflexion point of the white line in-situ XANES data are shown in Fig. 2. The inflexion point of the glasses located at 19003.3 ± 0.2 eV shows that Nb is in 5+ state, and is not affected by the increase in pressure. The inflexion point of the white line of the melt XANES spectra are found to be systematically at a lower position by 0.8 eV to 1.2 eV than for the glasses (Fig. 2b). Temperature-induced modifications are not expected to induce such a shift, as only 0.15 eV difference was observed between melt and glass at the Ni K-edge [START_REF] Farges | Transition elements in water-bearing silicate glasses/melts. Part I. a high-resolution and anharmonic analysis of Ni coordination environments in crystals, glasses, and melts[END_REF]. Instead, the shift of the edge indicates that Nb is found in a lower redox state in the melt closer to +4 compared to the glass. As for the changes affecting the pre-edge peak, its intensity is lower and its position shifted to higher energies in the glass compared to the melt, as previously reported for Fe, Ti and Ni (see [START_REF] Wilke | Fe in magma -an overview[END_REF] and references therein), and consistently with the increased oxidation state in the glass. These changes may also be enhanced by temperature, as theoretically understood through increased radial distortions and deviations from central symmetry of the local environment [START_REF] Manuel | Experimental evidence of thermal fluctuations on the x-ray absorption near-edge structure at the aluminum K edge[END_REF]. Only at the highest P point (i.e. 9.3 GPa) have the room T glass and melt comparable pre-edge features. This could be due to the opposite effects of increased CN [START_REF] Farges | Does Zr-F 'complexation' occur in magmas?[END_REF] and decreased oxidation state that could cancel each other out.Finally, subtle differences in pre-edge features between room T and quenched glasses might be attributed to structural relaxation effects that occurred during melting, although this can be treated with caution as we only have 2 P points for which both room T and quenched glasses data were collected (at 3.0 GPa and 4.3 GPa).

The best model for each EXAFS spectrum is presented on Fig. 3a. The normalized k 2 -weighted spectra and their Fourier Transform for the samples at 4.3 GPa and for the NbO 2 reference are shown in Fig. 3, and the corresponding fit parameters are listed in Table 2. Small differences are observed between the in-situ samples and the oxide model compounds, notably at high k. One main contribution is detected around the Nb atom (Fig. 3b).

Up to 4.3 GPa, this Nb-O shell has 5.8 to 6.3 nearest neighbors (Fig. 4a) and an average bond-length of 2.00 Å, 1.95 Å and 1.95 Å respectively for the starting glasses, the melts and the high pressure quenched glasses at the pressure investigated (Fig. 4b). Our results for these low P glasses and melts agree with ambient P data on similar glasses [START_REF] Piilonen | Structural environment of Nb 5+ in dry and fluid-rich (H 2 O, F) silicate glasses: A combined XANES and EXAFS study[END_REF]. For the two highest P points, i.e. 7.5 GPa and 9.3 GPa, the number of nearest oxygen neighbors increases up to 7.1±0.4. No concomitant increase of the Nb-O distance is observed (Fig. 4b), but that could be due to the larger error bars (±0.7 Å) of the fit at high pressures.

Implications

Early silicate Earth's differentiation events, i.e. mantle melting, are likely to have occurred at pressures lower than 7 GPa where structural changes of Nb in haplogranitic melts are negligible. If these results were to apply to basaltic melts as well, this would rule out the hypothesis of Nb/Ta fractionation through the formation of enriched silicate reservoirs at depth. Nb local structure and oxidation state remain to be investigated in basaltic melts at high pressures, as Lu local environment was shown by in situ X-ray diffraction to be not affected by P in continental crustal melts, but to drastically change coordination number from 6 to 8 in basaltic melts circa 4-5 GPa [START_REF] De Grouchy | Lutetium incorporation in magmas at depth: changes in melt local environment and the influence on partitioning behaviour[END_REF]. The relevant experiments are nonetheless challenging due to the high melting point of basalts especially at high P , combined with the weakening of EXAFS oscillations at high T . Rutile-melt Nb partitioning data with silica-rich melts analogous to the one studied here have only been collected up to 3.5 GPa [START_REF] Xiong | Partitioning of Nb and Ta between rutile and felsic melt and the fractionation of Nb/Ta during partial melting of hydrous metabasalt[END_REF]. They did not show any P -effect on Nb partitioning, which is consistent with the absence of changes in the local environment of Nb, includ-ing coordination number and oxidation state, in silica-rich melts over this P -range as reported here. The P -range investigated for partitioning experiments might have been too small to evidence any clear P dependence. Rutile-basaltic melt partitioning data collected up to 10 GPa [START_REF] Bromiley | The role of tio 2 phases during melting of subduction-modified crust: Implications for deep mantle melting[END_REF] have evidenced a marked decrease of the rutile-melt partition coefficient for Nb, D rutile/melt , with increased P , which was interpreted as resulting from structural changes in the melt as the rutile-TiO 2 (II) phase transition only occurs circa 7 GPa. Structural changes in the melt might however concern either a change of the local environment around Nb atoms, as reported here for silica-rich melts with the observed increase of Nb-O coordination number at the highest P points, and/or a change in the melt bulk properties such as the compressibility. The latter, for instance, has been invoked to explain the change in REE partitioning between olivine and silicate melt at high pressure [START_REF] Imai | Element partitioning between olivine and melt up to 10 GPa: Implications for the effect of pressure[END_REF].

2012.

Figure 1 .

 1 Figure1. Normalized XAS spectra for the references and for the pressurized glasses before heating (blue), high pressure melts collected at T ranging between 1270 K and 1350 K (red), and corresponding quenched glasses (black) at all P points investigated.

Figure 2 .

 2 Figure 2. (a) XANES derivative spectra for the references and for the starting glass, high pressure melt, and high pressure quenched glass at 4.3 GPa. (b) Position of the Nb-edge as measured by the inflexion point (blue circles: glass before heating, red squares: melt, black diamonds: quenched glass after heating). 'IV' represents the E 0 value of NbO 2 (+4 valence), 'V' the E 0 value of Nb 2 O 5 (+5 valence).

Figure 3 .

 3 Figure 3. (a) Normalized, k 2 -weighted, EXAFS spectra for the references and sample at 4.3 GPa (colors: same as for other figures; full lines: data, dashed lines: fit). (b) Fourier Transform of the corresponding normalized, k 2 -weighted, EXAFS spectra.

Figure 4 .

 4 Figure 4. (a) Fitted Nb-O interatomic distance. (b) Fitted Nb-O coordination number.

Table 1 .

 1 Compositions from electron microprobe analysis of the starting HPG glass given in wt% oxide. Analyses are based on an average of 10 sample spots, standard deviations are shown in brackets.

	Oxide Sample
	SiO 2	78.7 (3)
	Al 2 O 3 11.9 (2)
	Na 2 O 3.3 (3)
	K 2 O	3.7 (1)
	Total 99.4 (5)

Table 2 .

 2 EXAFS-derived structural parameters for the crystalline reference NbO 2 and for the parent glass at room temperature (R), the melts (M) and the quenched glasses (Q).

		P (GPa) Nb-O CN d ( Å) R-factor	σ 2	∆E 0
	NbO 2 Ambiant 6.01(30) 2.09(8)	0.07	0.010(2) 1.24(37)
	R	1.0	6.4(1)	2.00(2)	0.08	0.010(2) -0.18(24)
	M	1.0	6.1(2)	1.96(3)	0.12	0.010(2) -0.75(45)
	R	3.0	6.3(1)	1.99(1)	0.07	0.010(2) 1.22(75)
	M	3.0	6.4(2)	1.98(2)	0.26	0.120(2) 1.05(43)
	Q	3.0	6.1(2)	1.97(3)	0.09	0.010(2) 1.64(38)
	R	4.3	6.2(3)	1.98(2)	0.06	0.010(2) 1.24(32)
	M	4.3	6.3(3)	1.93(6)	0.09	0.040(2) 1.66(93)
	Q	4.3	5.8(1)	1.95(5)	0.07	0.010(2) 1.47(37)
	R	7.5	6.4(2)	2.00(4)	0.08	0.010(2) 1.80(95)
	M	7.5	6.8(2)	1.93(7)	0.13	0.080(2) 1.31(1.01)
	R	9.3	6.4(3)	1.99(4)	0.07	0.010(2) 2.07(65)
	M	9.3	7.1(4)	1.93(4)	0.09	0.050(2) 1.87(87)
	∆E 0 (Table

Acknowledgements

The chamber used to hold the hot RH-DAC in vacuum was designed by the group of A. Ehnes (Extreme Conditions Science infrastructure, Petra-III, DESY). We thank C. Hayward for his help with electron microprobe analyses. This work was supported by the European Research Council under the European Community's Seventh Framework Programme (FP7/20072013 Grant Agreement No. 259649 to C.S.).