Alain Finkel
email: alain.finkel@ens-paris-saclay.fr

Serge Haddad
email: serge.haddad@ens-paris-saclay.fr

Lina Ye
email: lina.ye@ens-paris-saclay.fr

Introducing Divergence for Infinite Probabilistic Models

Keywords: Reachability probability, Infinite state probabilistic models, Divergence

Computing the reachability probability in infinite state probabilistic models has been the topic of numerous works. Here we introduce a new property called divergence that when satisfied allows to compute reachability probabilities up to an arbitrary precision. One of the main interest of divergence is that our algorithm does not require the reachability problem to be decidable. Then we study the decidability of divergence for probabilistic versions of pushdown automata and Petri nets where the weights associated with transitions may also depend on the current state. This should be contrasted with most of the existing works that assume weights independent of the state. Such an extended framework is motivated by the modeling of real case studies. Moreover, we exhibit some divergent subclasses of channel systems and pushdown automata, particularly suited for specifying open distributed systems and networks prone to performance collapsing in order to compute the probabilities related to service requirements.

Introduction

Probabilistic Models. In the 1980's, finite-state Markov chains have been considered for the modeling and analysis of probabilistic concurrent finite-state programs [START_REF] Vardi | Automatic verification of probabilistic concurrent finite-state programs[END_REF]. Since the 2000's, many works have been done to verify the infinitestate Markov chains obtained from probabilistic versions of automata extended with unbounded data (like stacks, channels, counters and clocks) 1 . The (qualitative and quantitative) model checking of probabilistic pushdown automata (pPDA) is studied in many papers, for example in [START_REF] Brázdil | Analysis and prediction of the long-run behavior of probabilistic sequential programs with recursion[END_REF][START_REF] Esparza | Model checking probabilistic pushdown automata[END_REF][START_REF] Esparza | Quantitative analysis of probabilistic pushdown automata: expectations and variances[END_REF][START_REF] Esparza | Model checking probabilistic pushdown automata[END_REF][START_REF] Kucera | Model checking probabilistic pushdown automata[END_REF] (see [START_REF] Brázdil | Analyzing probabilistic pushdown automata[END_REF] for a survey). In 1997, Iyer and Narasimha [START_REF] Iyer | Probabilistic lossy channel systems[END_REF] started the study of probabilistic lossy channel systems (pLCS) and later both some qualitative and quantitative properties were shown decidable for pLCS [START_REF] Abdulla | Verification of probabilistic systems with faulty communication[END_REF]. Probabilistic counter machines (pCM) have also been studied [START_REF] Brázdil | Efficient analysis of probabilistic programs with an unbounded counter[END_REF][START_REF] Brázdil | Efficient analysis of probabilistic programs with an unbounded counter[END_REF][START_REF] Brázdil | Zero-reachability in probabilistic multi-counter automata[END_REF].

Computing the Reachability Probability. In finite Markov chains, there is a well-known algorithm for computing exactly the reachability probabilities in polynomial time [START_REF] Baier | Principles of Model Checking[END_REF]. Here we focus on the problem of Computing the Reachability Probability up to an arbitrary precision (CRP) in infinite Markov chains. There are (at least) two possible research directions:

The first one is to consider the Markov chains associated with a particular class of probabilistic models (like pPDA or probabilistic Petri nets (pPN)) and some specific target sets and to exploit the properties of these models to design a CRPalgorithm. For instance in [START_REF] Brázdil | Analyzing probabilistic pushdown automata[END_REF], the authors exhibit a PSPACE algorithm for pPDA and PTIME algorithms for single-state pPDA and for one-counter automata.

The second one consists in exhibiting a property of Markov chains that yields a generic algorithm for solving the CRP problem and then looking for models that generate Markov chains that fulfill this property. Decisiveness of Markov chains is such a property. Intuitively, decisiveness w.r.t. s 0 and A means that almost surely the random path σ starting from s 0 will reach A or some state s from which A is unreachable. It has been shown that pPDA are not (in general) decisive but both pLCS and probabilistic Petri nets (pPN) are decisive (for pPN: when the target set is upward-closed [START_REF] Abdulla | Decisive Markov chains[END_REF]).

Two Limits of the Previous Approaches. The generic approach based on the decisiveness property has numerous applications but suffers the restriction that the reachability problem must be decidable in the corresponding non deterministic model. To the best of our knowledge, all generic approaches rely on a decidable reachability problem.

In most of the works, the probabilistic models associate a constant weight for transitions and get transition probabilities by normalizing these weights among the enabled transitions in the current state. This forbids to model phenomena like congestion in networks (resp. performance collapsing in distributed systems) when the number of messages (resp. processes) exceeds some threshold leading to an increasing probability of message arrivals (resp. process creations) before message departures (resp. process terminations).

Our Contributions

-In order to handle realistic phenomena (like congestion in networks), we consider dynamic weights i.e., weights depending on the current state. -We introduce the new divergence property of Markov chains w.r.t. s 0 and A:

given some precision θ, one can discard a set of states with either a small probability to be reached from s 0 or a small probability to reach A such that the remaining subset of states is finite and thus allows for an approximate computation of the reachability probability up to θ. For divergent Markov chains, we provide a generic algorithm for the CRP-problem that does not require the decidability of the reachability problem. While decisiveness and divergence are not exclusive (both hold for finite Markov chains), they are complementary. In fact, divergence is somehow related to transience of Markov chains while decisiveness is somehow related to recurrence [START_REF] Finkel | About decisiveness of dynamic probabilistic models[END_REF]. -In order to check divergence, we provide several simpler sufficient conditions based on existing and new results of martingale theory. -We study for different models the decidability of divergence. Our first undecidability result implies that whatever the infinite models, one must restrict the kind of dynamics weights. Here we limit to polynomial weights, i.e. where a weight is defined by a polynomial whose variables are characteristics of the current state (e.g. the marking of a place in a Petri net). -We prove, by a case study analysis, that divergence is decidable for a subclass of polynomial pPDA (i.e. pPDA with polynomial weights). We show that divergence is undecidable for polynomial pPNs w.r.

= {∆ : S → R ≥0 | s∈S ∆(s) = 1}
is the set of distributions over S. Let ∆ ∈ Dist(S), then the support of ∆ is defined by Supp(∆) = ∆ -1 (R >0 ). Let T ⊆ S, then S \ T will also be denoted T .

Definition 1 (Effective Markov chain).

A Markov chain M = (S, p) is a tuple where:

-S is a countable set of states, p is the transition function from S to Dist(S); When for all s ∈ S, Supp(p(s)) is finite and computable and the function p is computable, one says that M is effective.

Notations. The function p may be viewed as a S×S matrix defined by p(s, s ) = p(s)(s ). Let p (d) denote the d th power of the transition matrix p. When S is countably infinite, we say that M is infinite and we sometimes identify S with N. We also denote p(s, s ) > 0 by s p(s,s ) ----→ s . A Markov chain is also viewed as a transition system whose transition relation → is defined by s → s if p(s, s ) > 0. Let A ⊆ S, one denotes P ost * M (A), the set of states that can be reached from some state of A and P re * M (A), the set of states that can reach A. As usual, we denote → * , the transitive closure of → and we say that s is reachable from s if s → * s . We say that a subset A ⊆ S is reachable from s if some s ∈ A is reachable from s. Note that every finite path of M can be extended into (at least) one infinite path.

Example 1. Let M 1 be the Markov chain of Fig. 1. In any state i > 0, the probability for going to the "right", p(i, i + 1), is equal to 0 < p i < 1 and for going to the "left" p(i, i -1) is equal to 1p i . In state 0, one goes to 1 with probability 1. M 1 is effective if the function n → p n is computable.

0 1 2 3 • • • 1 1 -p1 p1 1 -p2 p2 1 -p3 p3 1 -p4 Fig. 1. A random walk M1
Given an initial state s 0 , the sampling of a Markov chain M is an infinite random sequence of states (i.e., a path) σ = s 0 s 1 . . . such that for all i ≥ 0, s i → s i+1 . As usual, the corresponding σ-algebra whose items are called events is generated by the finite prefixes of infinite paths and the probability of an event Ev given an initial state s 0 is denoted Pr M,s0 (Ev). In case of a finite path s 0 . . . s n , Pr M,s0 (s 0 . . . s n ) = 0≤i<n p(s i , s i+1 ).

Notations. From now on, G (resp. F, X) denotes the always (resp. eventual, next) operator of LTL.

Let A ⊆ S. We say that σ reaches A if ∃i ∈ N s i ∈ A and that σ visits A if ∃i > 0 s i ∈ A. The probability that starting from s 0 , the path σ reaches (resp. visits) A will be denoted by Pr M,s0 (FA) (resp. Pr M,s0 (XFA)).

We now state qualitative and quantitative properties of a Markov chain.

Definition 2 (Irreducibility, recurrence, transience). Let M = (S, p) be a Markov chain and s ∈ S.

Then M is irreducible if for all s, s ∈ S, s → * s . s is recurrent if Pr M,s (XF{s}) = 1 otherwise s is transient.
In an irreducible Markov chain, all states are in the same category, either recurrent or transient [START_REF] Kemeny | Denumerable Markov Chains[END_REF]. Thus an irreducible Markov chain will be said transient or recurrent depending on the category of its states. In the remainder of this section, we will relate this category with techniques for computing reachability probabilities.

Example 2. Clearly M 1 is irreducible. Moreover (see [START_REF] Finkel | Introducing divergence for infinite probabilistic models[END_REF]), M 1 is recurrent if and only if n∈N 1≤m<n ρ m = ∞ with ρ m = 1-pm pm , and when transient, the probability that starting from i the random path visits 0 is equal to i≤n 1≤m<n ρm n∈N 1≤m<n ρm . One of our goals is to approximately compute reachability probabilities in infinite Markov chains. Let us formalize it. Given a finite representation of a subset A ⊆ S, one says that this representation is effective if one can decide the membership problem for A. With a slight abuse of language, we identify A with any effective representation of A. The Computing of Reachability Probability (CRP) problem is defined by: -Input: an effective Markov chain M, an (initial) state s 0 , an effective subset of states A, and a rational number θ > 0. -Output: an interval [low, up] such that uplow ≤ θ and Pr M,s0 (FA) ∈

[low, up].

Divergent Markov Chains

Let us first discuss two examples before introducing the notion of divergent Markov chains.

Example 3. Consider again the Markov chain M 1 of Fig. 1 with for all n > 0,

p n = p > 1 2 .
In this case, for m ≥ 0, Pr M1,m (F{0}) = ρ m with ρ = 1-p p . Thus here the key point is that not only this reachability probability is less than 1 but it goes to 0 when m goes to ∞. This means that given some precision θ, one could "prune" states n ≥ n 0 and compute the reachability probabilities of A in a finite Markov chain. Consider the Markov chain of Fig. 2, where Pr M,0 (F{m, m+1, . . .}) = n<m p n goes to 0 when m goes to ∞. As in the precedent example, computing the reachability probabilities of A can be also done in a finite Markov chain after pruning states n ≥ n 0 , given some precision θ.

0 1 2 3 • • • A finite Markov chain containing A n∈N pn = 0 p0 1 -p0 1 -p1 p1 1 -p2 p2 1 -p3 p3 Fig. 2. An infinite (divergent) Markov chain
Intuitively, a divergent Markov chain w.r.t. s 0 and A generalizes these examples: given some precision θ, one can discard a set of states with either a small probability to be reached from s 0 (f -1 0 ([0, θ]) in the next definition) or a small probability to reach A (from any state of the set f -1

1 ([0, θ]) in the next definition), such that the remaining subset of states is finite and thus allows for an approximate computation of the reachability probability up to θ. Definition 3 (divergent Markov chain). Let M be a Markov chain, s 0 ∈ S and A ⊆ S. We say that M is divergent w.r.t. s 0 and A if there exist two computable functions f 0 and f 1 from S to R ≥0 such that:

-For all 0 < θ < 1, Pr M,s0 (Ff -1 0 ([0, θ])) ≤ θ; -For all s ∈ S, Pr M,s (FA) ≤ f 1 (s); -For all 0 < θ < 1, {s | f 0 (s) ≥ θ ∧ f 1 (s) ≥ θ} ∩ P ost * M ({s 0 }) is finite.
Observation and Illustration. Let us remark that there may not exist, for general Markov chains, an algorithm to decide the existence of such functions f 0 , f 1 and if there exist, to find them. Indeed as for decisiveness, divergence is a semantical property. But there exist some simpler sufficient conditions for divergence.

A finite Markov chain is divergent (letting f 0 = f 1 = 1) w.r.t. any s 0 and any A. In the first Markov chain of Example 3, f 0 = 1 and f 1 (m) = ρ m and in the second Markov chain, f 1 = 1, f 0 (m) = 0≤n<m p n and f 0 (s) = 1 for all s in the finite Markov chain containing A. Generalizing these two examples, the next proposition introduces a sufficient condition for divergence. Its proof is immediate by choosing (f = f 0 and f 1 = 1) or (f = f 1 and f 0 = 1). Proposition 1. Let M be a Markov chain, s 0 ∈ S, A ⊆ S, and a computable function f from S to R ≥0 such that:

-For all 0 < θ < 1, Pr M,s0 (Ff -1 ([0, θ])) ≤ θ or for all s ∈ S, Pr M,s (FA) ≤ f (s); -For all 0 < θ < 1, {s | f (s) ≥ θ} ∩ P ost * M ({s 0 }) is finite. Then M is divergent w.r.t. s 0 and A.

An Algorithm for Divergent Markov Chains

We now design an algorithm for accurately framing the reachability probability for a divergent (effective) Markov chain w.r.t. s 0 and an effective A.

Let us describe this algorithm. It performs an exploration of reachable states from s 0 maintaining S , the set of visited states, and stopping an exploration when the current state s fulfills: either (1) for some i ∈ {0, 1}, f i (s) ≤ θ 2 in which case s is inserted in the AlmostLoose i set (initially empty), or (2) s ∈ A in which case s is inserted in A (initially empty). When the exploration is ended, if A is empty, the algorithm returns the interval [0, θ]. Otherwise it builds M = (S , p ) a finite Markov chain over S whose transition probabilities are the ones of M except for the states of AlmostLoose 0 ∪ AlmostLoose 1 ∪ A , which are made absorbing. Finally it computes the vector of reachability probabilities starting from s 0 in M (function CompFinProb) and returns the interval [preach(A ), preach(A ) + preach(AlmostLoose 0 ) + θ 2 • preach(AlmostLoose 1 )]. The next proposition establishes the correctness of the algorithm. Proposition 2. Let M be a divergent Markov chain with s 0 ∈ S, A ⊆ S and θ > 0. Then Algorithm 1 solves the CRP problem.

Algorithm 1: Framing the reachability probability

CompProb(M, s0, A, θ) AlmostLoose0 ← ∅; AlmostLoose1 ← ∅; S ← ∅ A ← ∅; Front ← ∅; Insert(Front, s0) while Front = ∅ do s ← Extract(Front); S ← S ∪ {s} if f0(s) ≤ θ 2 then AlmostLoose0 ← AlmostLoose0 ∪ {s} else if f1(s) ≤ θ 2 then AlmostLoose1 ← AlmostLoose1 ∪ {s} else if s ∈ A then A ← A ∪ {s} else for s → s ∧ s / ∈ S do Insert(Front, s ) end if A = ∅ then return (0, θ) Abs ← AlmostLoose0 ∪ AlmostLoose1 ∪ A for s ∈ Abs do p (s, s) ← 1 for s ∈ S \ Abs ∧ s ∈ S do p (s, s ) ← p(s, s ) preach ← CompFinProb(M , s0) // M = (S , p ): a finite Markov chain return (preach(A ), preach(A ) + preach(AlmostLoose0) + θ 2 • preach(AlmostLoose1))
We also provide an algorithm for models with a decidable reachability problem that returns [0, 0] when A is unreachable and [ , u] with > 0 otherwise. This algorithm and the proof of its correctness are both presented in [START_REF] Finkel | Introducing divergence for infinite probabilistic models[END_REF].

(Un)Decidability Results

We now study probabilistic versions of well-known models like Pushdown Automaton (PDA) and Petri nets (PN), for which we analyse the decidability of the divergence property.

Probabilistic Pushdown Automata

Let Γ be a finite alphabet. Γ ≤k is the set of words over Γ with length at most k. Let w ∈ Γ * , then |w| denotes its length. ε denotes the empty word.

Definition 4 (pPDA). A (dynamic-)probabilistic pushdown automaton (pPDA) is a tuple

A = (Q, Γ, ∆, W ) where: -Q is a finite set of control states; -Γ is a finite stack alphabet with Q ∩ Γ = ∅; -∆ is a subset of Q × Γ ≤1 × Q × Γ ≤2 such that for all (q, ε, q , w) ∈ ∆, |w| ≤ 1; -W is a computable function from ∆ × Σ * to Q >0 .
In the version of pPDA presented in [START_REF] Esparza | Model checking probabilistic pushdown automata[END_REF], the weight function W goes from ∆ to Q >0 . In order to emphasize this restriction here and later we say that, in this case, the weight function is static and the corresponding models will be called static pPDA. In what follows, pPDA denotes the dynamic version.

An item (q, a, q , w) of ∆ is also denoted q ?a!w ---→ q and ?a!ε is also simply denoted by ?a. A configuration of A is a pair (q, w) ∈ Q × Γ * . We use the letters a, b, c, x, y for elements in Γ and w for a word in Γ * . Definition 5. Let A be a pPDA. Then the Markov chain M A = (S A , p A ) is defined by:

-S A = Q × Γ * is the set of configurations; -For all (q, ε) ∈ S A s.t. {t = q ?ε!wt ---→ q } t∈∆ = ∅, p A ((q, ε), (q, ε)) = 1; -For all (q, ε) ∈ S A s.t. {t = q ?ε!wt ---→ q } t∈∆ = ∅, let W (q, ε) = t=q ?ε!w t ---→q W (t, ε).
Then: for all t = q ?ε!w t ---→ q ∈ ∆, pA((q, ε), (q , wt)) = W (t,ε)

W (q,ε)
-For all (q, wa) ∈ S A s.t. {t = q ?a!wt ---→ q } t∈∆ = ∅, p A ((q, wa), (q, wa)) = 1; -For all (q, wa) ∈ S A s.t. {t = q ?a!wt ---→ q } t∈∆ = ∅, let W (q, wa) = t=q ?a!w t ---→q W (t, wa). Then: for all t = q ?a!w t ---→ q ∈ ∆, pA((q, wa), (q , wwt)) = W (t,wa) W (q,wa)

We now show that even for pPDA with a single state and with a stack alphabet reduced to a singleton, divergence is undecidable.

Theorem 1. The divergence problem for pPDA is undecidable even with a single state and stack alphabet {a}.

Due to this negative result on such a basic model, it is clear that one must restrict the possible weight functions. A pPDA A is said polynomial if for all t ∈ ∆, W (t, w) is a positive integer polynomial (i.e. whose coefficients are non negative and the constant one is positive) whose single variable is |w|.

Theorem 2. The divergence problem w.r.t. s 0 and finite A for polynomial pPDA with a single state and stack alphabet {a} is decidable (in linear time).

Probabilistic Petri Nets

A probabilistic Petri net (resp. a probabilistic VASS) is a Petri net (resp. a VASS) with a computable weight function W . In previous works [START_REF] Abdulla | Decisive Markov chains[END_REF][START_REF] Brázdil | Efficient algorithms for asymptotic bounds on termination time in VASS[END_REF], the weight function W is a static one: i.e., a function from T , the finite set of transitions of the Petri net, to N >0 . As above, we call these models static probabilistic Petri nets. We introduce here a more powerful function where the weight of a transition depends on the current marking. Definition 6. A (dynamic-)probabilistic Petri net (pPN) N = (P, T, Pre, Post, W, m 0 ) is defined by: -P , a finite set of places; -T , a finite set of transitions; -Pre, Post ∈ N P ×T , resp. the pre and post condition matrices; -W , a computable function from T × N P to Q >0 the weight function; m 0 ∈ N P , the initial marking.

When for all t ∈ T , W (t, -) is a positive polynomial whose variables are the place markings, we say that N is a polynomial pPN.

A marking m is an item of N P . Let t be a transition. Then t is enabled in m if for all p ∈ P , m(p) ≥ Pre(p, t). When enabled, the firing of t leads to marking m defined for all p ∈ P by m (p) = m(p) + Post(p, t) -Pre(p, t) which is denoted by m t -→ m . Let σ = t 1 . . . t n be a sequence of transitions. We define the enabling and the firing of σ by induction. The empty sequence is always enabled in m and its firing leads to m. When n > 0, σ is enabled if m t1 -→ m 1 and t 2 . . . t n is enabled in m 1 . The firing of σ leads to the marking reached by t 2 . . . t n from m 1 . A marking m is reachable from m 0 if there is a firing sequence σ that reaches m from m 0 . Definition 7. Let N be a pPN. Then the Markov chain M N = (S N , p N ) associated with N is defined by: -S N is the set of reachable markings from m 0 ; -Let m ∈ S N and T m be the set of transitions enabled in m.

If T m = ∅ then p N (m, m) = 1. Otherwise let W (m) = m t -→mt W (t, m). Then for all m t -→ m t , p N (m, m t ) = W (t,m) W (m)
. Contrary to the previous result, restricting the weight functions to be polynomials does not yield decidability for pPNs. Theorem 3. The divergence problem of polynomial pPNs w.r.t. an upward closed set is undecidable.

Illustration of Divergence

Due to the undecidability results, we propose syntactical restrictions for standard models like pushdown automata and channel systems that ensure divergence. Observing that function f 1 of Definition 3 is somewhat related to transience of Markov chains, we first establish a sufficient condition of transience from which we derive a sufficient condition of divergence for infinite Markov chains used for our two illustrations. Theorem 4. Let M be a Markov chain and f be a function from S to R with

B = {s | f (s) ≤ 0} fulfilling ∅ B S, ε, K ∈ R >0 and d ∈ N * such that: for all s ∈ S \ B s ∈S p (d) (s, s )f (s ) ≥ f (s) + ε and |f (s )-f (s)|≤K p(s, s ) = 1
(1) Then for all s ∈ S such that f (s) > dK,

Pr M,s (FB) ≤ c 1 e -c2(f (s)-dK)
where c 1 = n≥1 e -ε 2 n 2(ε+K) 2 and c 2 = ε (ε+K) 2 , which implies transience of M when it is irreducible. Proposition 3. Let M be a Markov chain and f be a computable function from S to R with B = {s | f (s) ≤ 0} fulfilling ∅ B S, and for some ε, K ∈ R >0 and d ∈ N * , Equation [START_REF] Abdulla | Verification of probabilistic systems with faulty communication[END_REF]. Assume in addition that for all n ∈ N, {s | f (s) ≤ n} is finite. Then M is divergent w.r.t. any s 0 and any finite A.

Probabilistic Channel Systems

Now we introduce a probabilistic variant of channel systems particularly appropriate for the modelling of open queuing networks. Here a special input channel c in (that works as a counter) only receives the arrivals of anonymous clients all denoted by $ (item 1 of the next definition). Then the service of a client corresponds to a message circulating between the other channels with possibly change of message identity until the message disappears (items 2 and 3).

Definition 8.

A probabilistic open channel system (pOCS) S = (Q, Ch, Σ, ∆, W ) is defined by: -a finite set Q of states; -a finite set Ch of channels, including c in ; -a finite alphabet Σ including $; -a transition relation

∆ ⊆ Q × Ch × Σ ε × Ch × Σ ε × Q that fulfills:
1. For all q ∈ Q, (q, c in , ε, c in , $, q) ∈ ∆; 2. For all (q, c, a, c , a , q

) ∈ ∆, a = ε ⇒ a = $ ∧ c = c = c in ; 3. For all (q, c, a, c , a , q ) ∈ ∆, c = c in ⇒ c = c in ; -W is a function from ∆ × (Σ * ) Ch to Q >0 .
Illustration. We consider three types of transitions between configurations: sending messages to the input channel (i.e., (q, c in , ε, c in , $, q)) representing client arrivals; transferring messages between different channels (i.e., (q, c, a, c , a , q ) with ε ∈ {a, a } and c = c in ) describing client services; and terminating message processing (i.e., (q, c, a, c , ε, q ) with a = ε) meaning client departures. All messages entering c in are anonymous (i.e., denoted by $). The left part of Fig. 3 is a schematic view of such systems. The left channel is c in . All dashed lines represent message arrivals (to c in ) or departures. The solid lines model message transferrings.

The next definitions formalize the semantics of pOCS.

Definition 9. Let S be a pOCS, (q, ν) ∈ Q × (Σ * ) Ch be a configuration and t = (q, c, a, c , a , q ) ∈ ∆. Then t is enabled in (q, ν) if ν(c) = aw for some w.

The firing of t in (q, ν) leads to (q , ν ) defined by:

- As usual one denotes the firing by (q, ν) t -→ (q , ν ). Observe that from any configuration at least one transition (a client arrival) is enabled. -

S S = Q × (Σ * ) Ch is the set of configurations; -For all (q, ν) ∈ S S let W (q, ν) = (q,ν) t -→(q ,ν )
W (t, ν). Then: for all (q, ν) t -→ (q , ν ), pS ((q, ν), (q , ν )) = W (t,ν) W (q,ν) . The restrictions on pOCS w.r.t. standard CS do not change the status of the reachability problem. As discussed in the introduction, when the number of clients exceeds some threshold, the performances of the system drastically decrease and thus the ratio of arrivals w.r.t. the achievement of a task increase. We formalize it by introducing uncontrolled pOCS where the weights of transitions are constant except the ones of client arrivals which are specified by positive non constant polynomials. Let ν ∈ (Σ * ) Ch . Then |ν| denotes c∈Ch |ν(c)|. Definition 11. Let S be a pOCS. Then S is uncontrolled if:

-For all t = (q, c, a, c , a , q ) ∈ ∆ with a = ε, W (t, ν) only depends on t and will be denoted W (t); -For all t = (q, c in , ε, c in , $, q), W (t, ν) is a positive non constant polynomial, whose single variable is |ν|, and will be denoted W in (q, |ν|).

The next proposition establishes that an uncontrolled pOCS generates a divergent Markov chain. This model illustrates the interest of divergence: while reachability of a pOCS is undecidable, we can apply Algorithm 1.

Proposition 5. Let S be a uncontrolled pOCS. Then M S is divergent.

Probabilistic Pushdown Automata

Increasing pPDA. We introduce the subset of increasing pairs, denoted as Inc(A), which is a subset of Q × Γ that contains pairs (q, a) such that from state (q, wa), the height of the stack can increase without decreasing before. When some conditions on Inc(A) are satisfied, we obtain a syntactic sufficient condition for M A to be divergent. This set Inc(A) can be easily computed in polynomial time by a saturation algorithm. Definition 12. Let (q, a), (q , a ) ∈ Q × Γ . Then (q , a ) is reachable from (q, a) if either (q, a) = (q , a ) or there is a sequence of transitions of ∆, (t i ) 0≤i<d such that: t i = q i ?ai!ai+1 -----→ q i+1 , (q 0 , a 0 )=(q, a), (q d , a d )=(q , a ) and for all i, a i = ε. The set of increasing pairs Inc(A) ⊆ Q × Γ is the set of pairs (q, a) that can reach a pair (q , a ) with some q ?a !bc ---→ q ∈ ∆. Definition 13. A pPDA A is increasing if:

-

Inc(A) = Q × Γ ;
-for all t = q ?a!w ---→ q ∈ ∆ such that |w| ≤ 1, W (t, -) is an integer constant denoted W t ; -for all t = q ?a!bc ---→ q ∈ ∆, W (t, -) is a non constant integer polynomial where its single variable is the height of the stack denoted W t ; -for all q ?a -→ q ∈ ∆, there exists q ?a!bc ---→ q ∈ ∆.

Illustration. The right part of Fig. 3 is an abstract view of a pPDA modelling of a server simultaneously handling multiple requests. The requests may occur at any time and are stored in the stack. The loop labelled by ?x!xy is a symbolic representation of several loops: one per triple (q, x, y) with q ∈ Q, x ∈ Γ and y ∈ Γ . Due to the symbolic loop, the set of increasing pairs of the pP DA server is equal to Q × Γ and there is always a transition increasing the height of the stack outgoing from any (q, a). Assume now that for any other transition, its weight does not depend on the size of the stack and that a transition t = q ?a!ab ---→ q has weight W t (n) = c t × n. Then A is increasing. The dependance on n means that due to congestion, the time to execute tasks of the server increases with the number of requests in the system and thus increase the probability of a new request that occurs at a constant rate. One is interested in computing the probability to reach (q f , ε) from (q 0 , ε) representing the probability that the server reaches an idle state having served all the incoming requests.

We establish that an increasing pPDA generates a divergent Markov chain. Proposition 6. Let A be an increasing pPDA. Then the Markov chain M A is divergent w.r.t. any s 0 and finite A.

Conclusion and Perspectives

We have introduced the divergence property of Markov chains and designed two generic CRP-algorithms depending on the status of the reachability problem. Then we have studied the decidability of divergence for pPDA and for pPN for different kinds of weights and target sets. Finally, we have provided two useful classes of divergent models within pCS and pPDA.

In the future, we plan to study the model checking of polynomial pPDA (as a possible extension of [START_REF] Esparza | Model checking probabilistic pushdown automata[END_REF]) and some heuristics to find functions f 0 and f 1 .

  if c = c then ν (c) = wa and for all c = c, ν (c ) = ν(c ); -if c = c then ν (c) = w, ν (c ) = ν(c )aand for all c / ∈ {c, c }, ν (c ) = ν(c ).

Fig. 3 .

 3 Fig. 3. A schematic view of pOCS (left) and a pPDA (right)

Proposition 4 .

 4 The reachability problem of pOCS is undecidable.

This work has been supported by ANR project BRAVAS (ANR-17-CE40-0028) with Alain Finkel and ANR project MAVeriQ (ANR-20-CE25-0012) with Serge Haddad. field of research at the time.


domain: phys spi

text:
Cyril Nicard
email: cyril.nicard@univ-lille.fr

Maxime Farin

Emmanuel Moulin

David Balloy

Ingrid Proriol Serre

Ingrid Proriol
email: ingrid.proriol-serre@univ-lille.fr

Monitoring of generalised corrosion: Ultrasonic Coda Wave Interferometry technique applied to Steel Corrosion in aqueous NaCl solutions

Keywords:

Generalised steel corrosion in salted

Introduction

As corrosion of metallic structures can reduce their lifetime and lead to mechanical failure, it has to be considered in their design to prevent financial or safety issues [START_REF] Melchers | Early corrosion of mild steel in seawater[END_REF][START_REF] Jeffrey | Corrosion of vertical mild steel strips in seawater[END_REF][START_REF] Roberge | Corrosion Engineering: Principles and Practice[END_REF][START_REF] Revie | Uhlig's Corrosion Handbook[END_REF]. Efficient measurement and corrosion detection are crucial to plan structural maintenance before it is too late. Despite the large number of existing corrosion sensors [START_REF] Wright | Corrosion sensors for structural health monitoring of oil and natural gas infrastructure: A Review[END_REF][START_REF] Agarwala | Corrosion detection and monitoring -A Review[END_REF][START_REF] Perkins | Technique for Monitoring Corrosion and related Parameters in Field Applications[END_REF][START_REF] Zou | Electrochemical techniques for determining corrosion rate of rusted steel in seawater[END_REF], Coda Wave Interferometry (CWI) technique [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF] is an interesting choice that could be used to create new ones that will have the advantage of being a direct, non-destructive, continuous and very sensitive method to measure precisely the thickness loss of corroding metal. This publication has been done in complement with the work done in collaboration with Farin et al. [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF] to help develop a CWI-based sensor. This study has been carried out in the frame of the European Socorro II project, which aims to provide industries with computer tools to help them to take preventive actions on their corroding structures. To create this tool, a machine learning algorithm will be fed with corrosion data (direct and indirect techniques) from around the "Two-Seas" area to create a corrosion model. The more data are gathered and fed to the algorithm, the better it is expected to perform. The CWI technology is promising to provide a cheap, small-sized, continuous and direct technique to measure thickness loss on chosen steel grade that could be made into an autonomous system and easily installed in various locations around the North Sea area to gather corrosion data for this project.

The most straightforward and most broadly used technique to test and follow the corrosion evolution of a given material is to put coupons in natural or "accelerated" corrosion conditions and analyse it after a certain amount of time. Generally, the analysis consists of a thickness loss measurement [START_REF] Wright | Corrosion sensors for structural health monitoring of oil and natural gas infrastructure: A Review[END_REF]: corrosion products are removed from the surface and the coupons are weighted and compared to its initial weight to measure the mass loss induced by corrosion. Knowing the coupons size, an average thickness loss can then be calculated from the measured mass loss. The main issue with this technique is that coupons can only be used once per measurement and need to be handled each time manually, making this technique time and material-consuming. CWI technique is a Non-Destructive Testing that has been considered to automatically and continuously measure the thickness loss of a corroding metallic plate.

Coda Wave Interferometry (CWI), which has initially been developed for seismic wave analysis [START_REF] Snieder | Coda wave interferometry for estimating nonlinear sehavior in seismic velocity[END_REF][START_REF] Gret | Time-lapse monitoring of rock properties with coda wave interferometry[END_REF], has also been used to create Non-Destructive Testing (NDT) methods to follow biofilm growth on the metallic surface for agronomical applications [START_REF] Chen | Monitoring cleaning cycles of fouled ducts using ultrasonic coda wave interferometry[END_REF][START_REF] Chen | Detection of biofilm formation by ultrasonic coda wave interferometry[END_REF]. This same technique has been recently adapted to corrosion monitoring [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF]. CWI is an ultrasonic technique that relies on the same basic principle as the pulse echo technique. The idea is to generate an ultrasonic pulse within the material, then record and analyse the material response as the emitted ultrasonic waves are reflected at interfaces and defects. The main difference between CWI and pulse-echo is that instead of just analysing the response time of the first wave packet arrivals to measure the thickness and detect a defect, the coda part (multiple echoes and reflections) is considered. Indeed, coda wave is theoretically more sensitive to any small perturbation occurring in the medium, such as temperature, velocity change, etc. To generate an ultrasonic impulse and record the response of the material, a piezoelectric transducer placed on the opposite side of the sample is a common choice, and it has the advantage of allowing post-experiment surface analysis if needed.

Nowadays, Electrical Resistance sensors (ER) and Linear Polarisation Probes (LPP) are the mainly used solutions to remotely follow corrosion evolution in natural exposition sites. ER sensors and LPP give quantitative corrosion rates but they only works with a specific material that must be designed and shaped to fit the sensors. ER is more robust and works in immersed and atmospheric conditions but the corrosion rates obtained by corrosion depth derivative, whereas LPP only works in immersed configuration and is less robust in the maritime environment when it tends to deteriorate quickly but gives instantaneous corrosion rates [ [START_REF] Bhargava Reddy | Sensors in advancing the capabilities of corrosion detection: A review[END_REF].

In this work, which complements the previous technical developments [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF], controlled electrochemical experiments are performed in parallel with ultrasonic sensor measurements to investigate the efficiency of ultrasonic CWI to monitor the corrosion of construction steels in aqueous 3 wt.% NaCl.

The CWI technique used in this work is described in more detail in the previous publication [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF]. In the present study, we will compare a CWI-based sensor to an existing solutions and focus on the precision of this technique, the conditions and the precautions required to obtain reliable and precise measurements of corrosion rates.

Material and experiments

To evaluate the accuracy of the CWI technique for steel corrosion monitoring, a thermoregulated electrochemical cell has been coupled with a CWI measurement set-up. For this study, the S355 grade steel, provided by Thissenkrupp Steel Europe has been used. The chemical composition of this carbon steel is given in Table 1.

The corroding samples (Figure 1) are 5 by 5 cm, 3 mm thick square plates of S355 grade steel. Those plates were preliminarily polished with SiC grinding paper up to a 1200 grade and cleaned with ethanol to prevent premature corrosion. A piezoelectric transducer, both emitter and receiver (Figure 1.a) with a diameter of 2.6 cm, is glued with superglue on the face of the steel plate samples that will not be in contact with the electrolyte. Some samples were completely or partially varnished on the corroding side with a Flexible Silicon Coating (Electrolube). The varnishing details are given in the results section as they vary from one experiment to another.

The electrochemical cell (Figure 2) dimensions are 15-by-15-by-15 cm, and the volume of electrolyte put inside for all the experiments is 2.5 L. The Working Electrode (WE) is the steel sample, the Reference Electrode (RE) is a Saturated Calomel Electrode (SCE), and the Counter Electrode (CE) is a platinum plate electrode 8-by-8 mm. The CE and the RE are directly immersed from the top of the tank, whereas the steel sample (WE) is pressed with an adaptor against a hole on the side of the cell with an O-ring joint to maintain water-tightness. The adaptor was 3D printed so the sample could be pressed against the cell side without putting mechanical stress on the glued piezo-transducer and the welded wires on the samples back. The electrodes are connected to a potentiostat (model: Origaflex 500 mA by Origalys) in an inverted configuration so that the groundmass is connected to the sample to prevent "current leakage" during the imposed current phases of the electrochemical sequences.

Electrochemical sequences details are given alongside results as the sequence change depending on the experiment. Electrochemical cell temperature is controlled with a heat exchanger made of a glass tube that weaves in the cell. In this glass tube runs water whose temperature is regulated with a cryothermostat (model: Lauda RA8). The temperature in the electrochemical cell is continuously measured with a varnished thermocouple positioned as close as possible to the sample inside the cell.

Corrosion of S355 steel in water can be globaly described as the reaction of iron, oxygen and water to form rust:

4𝐹𝑒 + 3𝑂 2 + 2𝐻 2 𝑂 → 2𝐹𝑒 2 𝑂 3 𝐻 2 𝑂 (1)
This will result in the consumption of the iron atos at the surface of the steel surface and thus a reduction of the thickness of the plate. If the corrosion products are not adherent or not dense inough, this corrosion depth can be measured by ultrasonic technics.

The CWI measurements setup (Figure 3) is composed of a function generator (Metrix GX 1050) connected to the emission part of the piezoelectric transducer and an acquisition board (14-bit, PicoScope 5444D, Pico Technology, 125MS/s) connected to the reception part of the piezoelectric transducer to record the sample response to the excitation with a 125 MHz sampling frequency.

The CWI technique is the same that the one used and detailed in the previous publication [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF]. This technique consists of periodically sending the same ultrasonic excitation signal (a frequencymodulated chirp with frequencies varying from 5 MHz to 15 MHz) and measuring the sample response to this excitation. The sample response is then convolved with the time-reversed chirp function to obtain the impulse response of the sample. The coda part of this response, which is composed of the multiple reflections of the emitted waves off the sample opposite faces, is compared with a reference coda signal 𝑠 0 measured at the beginning of the experiment (Figure 3). Since the multiple wave reflections are probing the sample many times, the coda is very sensitive to any change in the sample boundary conditions and material. To compare the measured coda signal 𝑠 𝑥 with its reference 𝑠 0 in a defined time window [ta; tb] with ta>tb it is classical to use the decorrelation. The decorrelation (D) is very useful for investigating the global physical modification/evolution of a system. However, it cannot be used to obtain a quantitative corrosion depth value as it is influenced by all the physical modifications of the sample (like pressure-induced constraint, temperature etc …).

Corrosion of S355 grade steel in NaCl 3wt.% distilled water can be assimilated to near homogeneous corrosion resulting in a thickness loss. This loss will result in a shorter travel time of the incident wave through the sample thickness. This time gain will accumulate as the ultrasonic wave goes back and forth multiple times in the sample (multiple reflections off the sample opposite faces), resulting in the fact that the later the time window is situated in the coda, the more this effect will be visible. This effect will make the reference coda signal look stretched compared with the coda signal measured for a smaller thickness. As shown in precedent work [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF], this stretching of the response signal can be computed. The coda stretching factor is mathematically determined by introducing an α factor varying between -0.5% and 0.5% as follows in the reference response signal s0:

𝑠 0 (𝑡) → 𝑠 0 (𝑡 * (1 + 𝑎)) (2)
The coda stretching factor 𝛼 at a given time tx is determined for the value of a, which gives the best correlation D between the stretched reference coda signal 𝑠 0 (𝑡 * (1 + 𝛼)) and the coda signal measured at this instant 𝑠 𝑥 (𝑡).

As temperature also modifies the ultrasonic wave propagation velocity in the material, it also influences the travel time and thus the coda stretching factor. As shown in [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF], this temperature contribution can be corrected if a temperature measurement is close to the sample. Stretching from the temperature can be expressed like this:

𝑠 0 (𝑡 * (1 + 𝛼 𝑟𝑎𝑤 )) = 𝑠 0 (𝑡 * (1 + (α corr + α 𝑡𝑒𝑚𝑝 ))) (3)
Where α corr corresponds to corrosion coefficient, and α 𝑡𝑒𝑚𝑝 for temperature one.

So, the coda stretching factor from corrosion only can be obtained by removing the coda stretching factor of the temperature from the raw stretching factor.

If the temperature is stable or the temperature contribution to the coda stretching factor is mathematically compensated (αcorr = αraw -αtemp) it is possible to convert a stretching factor to a corrosion depth using the following logic. If we consider that the stretching is only influenced by the corrosion thickness loss and if we only consider the time for an emitted ultrasonic wave to travel to the sample opposite face, be reflected and go back to the piezoelectric transducer, we obtain:

For an uncorroded sample:

𝑡 0 = 2𝐿 𝐶 (4)
For a corroded sample:

𝑡 𝑥 = 2(𝐿-𝑙 𝑐𝑜𝑟𝑟 ) 𝐶 (5)
With:

-L: the initial thickness of the sample.

-lcorr: the corrosion thickness loss.

-C: The longitudinal ultrasonic wave speed in the sample.

If the coda stretching factor is only due to thickness loss, in this condition, it will be calculated so that:

𝑡 𝑥 = 𝑡 0 (1 + 𝛼) (6)
(4), ( 5), ( 6)

→ 2(𝐿-𝑙 𝑐𝑜𝑟𝑟 ) 𝐶 = 2𝐿 𝐶 (1 + 𝛼) → 𝑙 𝑐𝑜𝑟𝑟 = -𝐿𝛼 (7)
This equation is coherent with the result obtained for the coda stretching factor in the corrosion depth model developed in [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF] in which for a 2 mm-thick plate, we obtained 𝑙 𝑐𝑜𝑟𝑟 (µ𝑚) ≈ -2004𝛼.

As said before, the stretching factor is also influenced by temperature. If we look at the same equation for a sonic wave going back and forth once (4) we can see that temperature will influence the flight distance due to material dilation and the ultrasonic wave speed 𝐶. [START_REF] Nowacki | The sound velocity in an alloy steel at high-temperature conditions[END_REF]. An increase in temperature will result in an increase in the flight distance and a reduction in the speed of the ultrasonic wave, which will both contribute positively to the stretching factor α.

If we consider only the dilatation of steel due to temperature variation using the dilatation coefficient ( 𝛾=11*10 -6 ) and using the same logic as [START_REF] Perkins | Technique for Monitoring Corrosion and related Parameters in Field Applications[END_REF], but varying D with temperature instead of corrosion, we obtain :

𝛼 = √1 + 𝛾(𝑇 𝑥 -𝑇 0 ) 3 -1 (8)
(with 𝑇 0 the temperature for the reference signal and 𝑇 𝑥 the temperature of the present measurement)

and which corresponds to a modification of the coda stretching factor of 0.0004% per degree Celsius (dilatation coefficient is relatively stable for steel between 0-100°C). For a 2 mm thin plate, it corresponds to a shift of 0.006 µm per degree on corrosion depth. If we now consider the modification of ultrasonic wave speed in the steel taking the data from the publication of [START_REF] Bhargava Reddy | Sensors in advancing the capabilities of corrosion detection: A review[END_REF] we can consider that in the 0-100°C domain, longitudinal ultrasonic wave speed can be defined as 𝐶 (𝑚. 𝑠 -1 ) = 6000 -𝑏 * 𝑇 (with 𝑇 the temperature in degrees Celsius and 𝑏 a factor between 0.5 and 1. Using this equation combined with (4), varying 𝐶 with temperature and keeping 𝐿 constant, we obtain:

𝛼 = 𝑏(𝑇 𝑥 -𝑇 0 ) 6000-𝑏𝑇 1 (9)
Here, if we choose 𝑇 0 = 0 °C and 𝑇 𝑥 = 1 °C it corresponds to a shift of 0,008 % of stretching factor alpha for b = 0.5 and 0.0167 % for b = 1, corresponding to a corrosion depth computation error between 0.16 µm and 0.32 µm per degree. Consequently, the influence of temperature on the ultrasonic wave speed in steel on the coda stretching factor α is more critical than on the dilatation of the material. Those computations match the result obtained in [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF] in which a change in temperature of 1 °C induced a stretching factor (α) shift of -0.0124 %.

Determining the influence of temperature on the coda stretching factor can be difficult because the dilatation coefficient and ultrasonic wave speed vary from material to material. The simplest way to obtain the influence of temperature on the stretching factor is to directly measure it by experimenting with a completely varnished sample which is protected from corrosion and only affected by temperature.

The influence of temperature and temperature correction will be investigated in this paper, but we will work at stable temperature for the first experiments. In order to check the accuracy of our corrosion depth measurement, surfaces were observed with an optical profilometer (Bruker Profilometer:

Contour GT-K Automated) after each experiment. Several measurements were performed at the limit of the corroded area (after varnish removal with ethanol) to measure the corrosion depth (Figure 4)

and compare it with the corrosion depth deduced from the CWI measurement.

Results

Corrosion detection with CWI

In order to estimate the accuracy that can be expected on the corrosion depth from CWI, a first corrosion experiment has been conducted with an S355 steel 3 mm thick plate in NaCl 3 wt.% distilled water. The electrochemical sequence was an open circuit potential for 5 days. The sample was partially varnished to prevent under-joint corrosion, the surface exposed to the electrolyte was a 3.8 cm² circle. As the coda signal is very sensitive to temperature, the temperature of the electrochemical cell is regulated at 29.5±0.5°C for this first experiment (Figure 5).

Polished S355 steel initial free potential in NaCl 3wt.% distilled water is around -0.4 V vs SCE evolving in a few hours to around -0.7 V vs SCE, which is coherent with the corrosion of S355 steel grade in NaCl 3 wt.% [START_REF] Zou | Electrochemical techniques for determining corrosion rate of rusted steel in seawater[END_REF]. The coda stretching factor of the coda signal (Figure 6) increases steadily during the experiment. The coda stretching factor is then converted into a corrosion depth and gives a constant corrosion speed of around 1.0 µm.day -1 .

After 5 days of immersion, the corrosion depth measured with the CWI technique was 5.1 µm (Figure 6). Corrosion products (mainly red rust) were cleaned from the surface with ethanol. Then, an optical profilometer was used to measure the corrosion depth and compare it with the CWI value. Over 5 measurements were performed along the edge of the corroded area and the corrosion depth on average was 4.5±0.5 µm.

The same experiment was performed with a completely varnished sample to investigate the possible contribution of the varnish and more largely the contribution of the experimental setup on the CWI signal stretching factor (Figure 7) and evaluate the baseline of the technique.

For the varnished sample, the coda stretching factor decreases rapidly on the first day of experiment and then more slowly over 5 days. Even if, in this case this stretching factor evolution does not correspond to a real corrosion depth (varnished sample) but rather to a drift of the corrosion depth measurement, it needs to be taken into account because it will influence the final result of the corrosion depth in the case of a non-varnished sample. This corrosion depth drift coming from the experimental set-up could explain the slight decrease observed at the beginning of the open circuit corrosion experiment (Figure 6). When real corrosion happens at the surface, this corrosion depth drift is rapidly small compared to the corrosion depth induced by corrosion, but it can shift it slightly.

Corrosion measurements with temperature correction

As explained in the experimental setup section, temperature variation will induce a stretching (dilatation/compression) on the coda part. In order to verify that the temperature influence on the coda stretching factor (α) can be corrected, the coda stretching factor in the experiment has been reproduced

with the completely varnished sample but with temperature variation between 20 °C and 30 °C (Figure 8).

This experiment allows us to determine that the shift induced by a temperature increase of 1 Celsius degree on the coda stretching factor α is -0.0123 %, which is close to the one from publication [START_REF] Farin | Monitoring saltwater corrosion of steel using ultrasonic coda wave interferometry with Temperature Control[END_REF].

Thank to that we corrected the temperature contribution to the coda stretching factor by removing it from the raw stretching factor as follows:

𝛼 𝑐𝑜𝑟𝑟 = 𝛼 𝑟𝑎𝑤 -𝛼 𝑡𝑒𝑚𝑝 = 𝛼 𝑟𝑎𝑤 -(0.0123 * (𝑇 -𝑇 𝑜 )) [START_REF] Snieder | Coda wave interferometry for estimating nonlinear sehavior in seismic velocity[END_REF] With 𝑇 the temperature at the time of the actual measurement and 𝑇 𝑜 the temperature at the reference measurement. The correction worked well, especially for slow temperature changes (e.g. from t = 25 h to t = 85 h and from t = 100 h to 120 h) (Figure 8.b). The temperature influence is not completely compensated for quicker temperature changes (at t = 20 h and t = 90 h). However, such drastic temperature changes are rarely observed in natural environments. After 5 days, the corrosion depth is around -0.5 µm (Figure 8.c), coherent with the one obtained for the experiment with the varnished sample and fixed temperature.

To complete those results, an experiment with an S355 grade steel sample with an unvarnished surface of 3.8 cm² in NaCl 3 wt.% and controlled temperature variation between 20 and 30°C has been performed (Figure 9).

Again, temperature correction is better for slow than sudden temperature changes (Figure 9.a) (visible at t = 25 h; t = 50 h; t = 120 h). The corrosion depth obtained for S355 grade steel reached 4.5 µm after

5 days at open circuit potential, coherent with the 5±1 µm corrosion depth measured with an optical profilometer and the corrosion depth obtained in the first experiment with stable temperature (Figure 6).

Those experiments demonstrate the efficiency of CWI in detecting corrosion and quantifying the rate of corrosion at the surface of a steel sample. In order to test the accuracy of this technique more quantitatively, more experiments with imposed electrochemical dissolution have been performed.

Quantitative continuous corrosion rate measurement with CWI.

To simplify the quantitative comparison with the final corrosion depth obtained from CWI, the one measured by optical profilometer and the ones extracted from literature, the imposed currents are converted in equivalent dissolution rate (µm.day -1 ) with the hypothesis that all electrons contribute to the stochiometric dissolution of iron following the reaction:

𝐹𝑒 → 𝐹𝑒 2+ + 2𝑒 -(11)
If we take the standard values for iron (close enough to steel) with a weight density of 7.874 g.cm -3 , a molar mass of 55.845 g.mol -1 and the Faraday constant, we obtain a dissolution rate of 1 µm.day -1 corresponding to a current of 31,6 µA.cm -². So, to give an example for our 3.8 cm² sample, a dissolution current of 1µm/day corresponds to an imposed current density of 31.6 µA.cm -², equivalent to an imposed current of 120 µA.

A first experiment was performed on an S355 steel, 3.8 cm² sample in NaCl 3 wt.

%. An open circuit potential phase of a few hours was followed by an imposed current equivalent to a dissolution of 5 µm.day -1 (158 µA.cm -²) (Figure 10). This experiment has been carried out with controlled temperature variations between 20 and 30 °C.

The corrosion rate calculated from the corrosion depth curves (Figure 10.c) gives a steady dissolution of 4.5 µm.day -1 . The corrosion depth expected from the current at the end of the experiment was 30 µm, the corrosion depth deduced from the CWI technique is 24 µm and the corrosion depth observed with the optical profilometer is 35±10 µm. The difference between the corrosion expected from the current and the CWI measurement (lower) came from the fact that not all the electrons sent in the system contribute to the Fe → Fe 2+ dissolution and are lost in other reactions/phenomena. The high corrosion deft measured by the optical profilometer can be due to the fact that the corrosion is not perfectly homogeneous and we only measure the corrosion depth at the edge of the corroded surface.

To complete this study on the possibility of the CWI technique to get a continuous quantitative estimate of the corrosion depth, an experiment with different corrosion rates has been performed on S355 steel in NaCl 3wt % distilled water at a regulated temperature of 29±0.5 °C. The electrochemical sequence was composed of an open circuit potential (OCP) phase of 12 hours and imposed dissolution current phases of 1 hour each, respectively equivalent to the electrochemical dissolution of 1 µm.day -1 (IC1), 5 µm.day -1 (IC5), 10 µm.day -1 (IC10), 20 µm.day -1 (IC20) and 40 µm.day -1 (IC40). There are two free potential phases between the imposed current phases, one between IC10 and IC20 and one between IC20 and IC40. Those free potential phases are there to check if the imposed current is not disturbing the baseline of the experiment. This last experiment was conducted at a regulated 29.5±0.5

°C temperature (Figure 11).

During the imposed current phases, the potential rises from -0.73 V (vs SCE) to -0.56 V (vs SCE), which is close enough to the OCP to support the considered hypothesis that the electrons are mainly contributing to the dissolution of the steel. The final corrosion depth estimated with CWI after the experiment is 4.2 µm, while the value obtained with the optical profilometer is 4.5±0.5 µm, which is in very acceptable agreement. The corrosion rate measured with CWI is compared with the expected corrosion rate calculated from the imposed anodic current (Table 2). Except for the IC1 phase, the corrosion rates deduced from CWI are relatively close to the ones expected from the imposed current.

The incoherence observed at IC1 may come from the imposed current being very close to the natural corrosion and thus difficult to differentiate, especially in just 1h.

Discussion

To test the performance of the CWI technique to measure corrosion depth, an electrochemical cell has been specially designed to make possible an ultrasonic measurement in parallel with an electrochemical corrosion experiment controlled with a potentiostat. CWI was able to monitor corrosion depth over time in OCP and imposed dissolution with an accuracy of a scale of a few micrometres.The chosen parameters make measuring corrosion depth evolution over time possible during all the experiments. The corrosion of S355 steel in NaCl 3wt.% distilled water in our experimental conditions is a homogeneous generalised corrosion (verified with an optical profilometer). CWI depth loss measurement is very efficient for this kind of corrosion as the surface in front of the sensor is homogenously affected by the corrosion and the corrosion depth model is making this assumption. If the corrosion is not homogeneous, the corrosion depth value is an average of the corrosion depth on the sample over the surface facing the sensor. As the system is designed now, it is impossible to differentiate homogeneous corrosion from localised corrosion by just looking at the coda stretching factor.

The corrosion depth model used to convert the coda stretching factor into thickness loss is accurate.

For the experiments (Figure 6, 9 and 11), the values given by CWI method after 5 days is less than 0.5 µm away from the measurement obtained with the optical profilometer, representing a 10% error. Our experimental setup and varnish baseline contribution to the corrosion depth calculated from the coda stretching factor is around 0.5 µm over 5 days (Figure 7), but it is expected to be less and less important over time as this evolution is nonlinear. Considering that for this sample size, a classical mass loss measurement would be impossible without a precise weighting scale and the error would be more than 10%, the used technique could be an interesting alternative. Moreover, the corrosion rates computed with CWI in the last experiment (Figure 11) are less than 10% away from the rates expected with the imposed current. An interesting experiment could be to test dissolution rates of different electrodeposition electrodes or protective cathodes at different imposed currents.

The model tested to remove temperature contribution from the raw coda stretching factor is efficient but performs poorly for significant and quick temperature changes of about ten degrees in less than an hour (Figures 8, 9 and 10). However, this compensation is sufficient to obtain an accurate long-term measurement of the corrosion depth but needs to be considered carefully. As the thermocouple we used was located in the electrochemical cell, close to the sample but a few centimetres from it, this delay in temperature correction could be because the temperature measurement is not done directly on the sample. That will be investigated and corrected in the future. Compared with ER sensors, CWIbased sensor precision is on the same order of magnitude (~ 1µm) and the corrosion rates is calcultated the same way (thickness loss derivative). The CWI-based sensors drawback is that temperature needs to be measured in order to remove its contribution from the measurement but have the advantages that the corroding part of the sensor can be made with any metallic material as long as it's a plate wherase for ER the corrosion material has to be shaped and make specifaclly for the sensor.

Also, in the case of CWI-based sensor, if the plate is not too corroded, it is possible to repolished and reuse the sensor. electrode degradation over time depending on the imposed current could also be investigated.

Conclusion

A sensor based on Coda Wave Interferometry (CWI) was tested in a controlled electrochemical corrosion experiment to continuously measure corrosion depth on S355 grade steel in NaCl 3 wt.%.

CWI technique applied to corrosion consists in periodically recording multiple echoes of an ultrasonic impulse emitted in the material thanks to a piezoelectric transducer, both emitter and receiver and following the evolution of those responses, looking at precise parameters influenced by corrosion.

Corrosion of S355 grade steel in NaCl 3 wt.% corresponds to a homogeneous thickness reduction that mainly compresses the response signal. This compression can be considered as a stretching factor that can be extracted from the response signal to follow corrosion evolution. A model to convert this stretching factor into corrosion depth has been tested and verified experimentally by measuring the final corrosion depth with an optical profilometer. The value obtained this way was compared with the one expected from the imposed electrochemical sequence and the one obtained with the CWI technique. Temperature variations also influence the coda stretching factor so temperature has to be maintained stable or the response signal has to be treated to remove the temperature contribution. A temperature contribution correction method was tested and validated. For this temperature correction to work, a temperature measurement as close to the sample as possible has to be performed. In addition, CWI is very sensitive to every physical change that modifies ultrasonic wave propagation in the material, so the experimental set-up and sensor have to be carefully designed, so their contribution to the response signal is stable and/or negligible during the measurement time. Due to this high sensitivity, CWI is potentially more sensitive than ultrasonic pitch catches sensors. That CWI technique can be used to obtain continuous quantitative measurements on small corroding samples without manipulating them and could give precious information on corrosion rates change as the corrosive environment evolves. Under specific conditions, those sensors could provide an excellent alternative to classical weight loss measurements that are time and material-consuming but also offer another way to remotely measure and follow corrosion evolution in various environments and can be used in parallel with others sensors.

Figure 1 :

 1 Figure 1: (a) back side of S355 steel 5-by-5cm plate with piezo emitter/receiver glued and wired. (b)

Figure 2 :Figure 3 :

 23 Figure 2 : Schematic and picture with corresponding elements of the experiment setup composed of an

Figure 4 :

 4 Figure 4: Topography (a) and corrosion depth profile (b) along orange dotted line measured with an

Figure 5 :

 5 Figure 5 : (a) Open circuit potential, (b) temperature and (c) stretching factor of the coda

Figure 6 :

 6 Figure 6 : Corrosion depth deviation measured by the sensor during 5 days on a

Figure 7 :

 7 Figure 7 : Corrosion depth measurement "drift" measured with CWI during 5 days on a

Figure 8 :

 8 Figure 8 : "Virtual" corrosion depth deviation measured with the CWI technique during 5

Figure 9 :

 9 Figure 9 : Temperature, coda stretching factor and corrected corrosion depth measured

Figure 10 :

 10 Figure 10 : Temperature, coda stretching factor and corrected corrosion depth measured

Figure 11 :

 11 Figure 11 : Temperature (a.), potential(b.) and corrected corrosion depth (c.) (by CWI

  The present work revealed that the CWI technique is accurate enough to compete with mass loss measurement due to homogeneous corrosion and Electrical Resistance sensors. As this technique is less time-consuming and gives a continuous depth measurement, it could be interesting to see if it performs well in other applications where mass loss and ER measurements usually are used. Salt spray tests and alternate immersion tests are planned in future work but the study of electrodeposition

Table 1 :

 1 Elemental composition of steel samples

	Element	Fe	C	Si	Mn P	S	Al	B	Cr	Cu	Mo	Nb	Ni	Ti	V
	%	Bal. 0.177 0.016 1.5	0.015 0.01 0.04 0.0002 0.04 0.02 0.004 0.001 0.025 0.016 0.002

Table 2 :

 2 Imposed dissolution rates and dissolution rates measured with CWI sensor during the experiment corresponding to Figure11.

	IC1	IC5	IC10	IC20	IC40

Acknowledgements

The authors thank Dr Geert Potters, Wikke Witteveen (from Antwerp Maritime Academy, Antwerp, Belgium), Dr Guillaume Delaplace a , Dr Marwan Abdallah a , Dr Pierre Campistronne b , Dr Lynda Chehami b and Dr Farouk Benmeddour b,c for their help and support.

Funding

This study was supported by our institutes and partially by the European Union. This work was a part of the European project Interreg 2 Seas, Seeking Out Corrosion, before it is too late (SOCORRO). This work was supported by Lille University (France) and the French National Center for Scientific Research.