Éric Joulin

INTERTWINING AND COMMUTATION RELATIONS FOR BIRTH-DEATH PROCESSES DJALIL CHAFA Ï AND ALD

Keywords: Preprint Mathematics Subject Classification. 60J80, 39C05 Birth-death process, Feynman-Kac semigroup, discrete gradients, intertwining relation, functional inequalities. 1

Given a birth-death process on N with semigroup (P t ) t≥0 and a discrete gradient ∂ u depending on a positive weight u, we establish intertwining relations of the form ∂ u P t = Q t ∂ u , where (Q t ) t≥0 is the Feynman-Kac semigroup with potential V u of another birth-death process. We provide applications when V u is non-negative and uniformly bounded from below, including Lipschitz contraction and Wasserstein curvature, various functional inequalities, and stochastic orderings. Our analysis is naturally connected to the previous works of Caputo-Dai Pra-Posta and of Chen on birth-death processes. The proofs are remarkably simple and rely on interpolation, commutation, and convexity.

Introduction

Commutation relations and convexity are useful tools for the fine analysis of Markov diffusion semigroups [B-E, B, L]. The situation is more delicate on discrete spaces, due to the lack of a chain rule formula [B-L, A, Che1, J-P, B-T, Cha2, C-DP-P, Che3]. In this work, we obtain new intertwining and sub-commutation relations for a class of birthdeath processes involving a discrete gradient and an auxiliary Feynman-Kac semigroup. We also provide various applications of these relations. Our analysis is naturally related to the curvature condition of Caputo-Dai Pra-Posta [C-DP-P] and to the Chen exponent of Chen [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF][START_REF] Chen | Speed of stability for birth-death processes[END_REF]. More precisely, let us consider a birth-death process (X t ) t≥0 on the state space N := {0, 1, 2, . . .}, i.e. a Markov process with transition probabilities given by

P x t (y) = P x (X t = y) =        λ x t + o(t) if y = x + 1, ν x t + o(t) if y = x -1, 1 -(λ x + ν x )t + o(t) if y = x,
where lim t→0 t -1 o(t) = 0. The transition rates λ and ν are respectively called the birth and death rates of the process (X t ) t≥0 . The process is irreducible, positive recurrent (or ergodic), and non-explosive when the rates satisfy to λ > 0 on N and ν > 0 on N * and ν 0 = 0 and

∞ x=1 λ 0 λ 1 • • • λ x-1 ν 1 ν 2 • • • ν x < ∞ and ∞ x=1 1 λ x + ν x λ x λ x-1 + • • • + ν x • • • ν 1 λ x • • • λ 1 λ 0 = ∞,
respectively. In this case the unique stationary distribution µ of the process is reversible and is given by

µ(x) = µ(0) x y=1 λ y-1 ν y , x ∈ N with µ(0) := 1 + ∞ x=1 λ 0 λ 1 • • • λ x-1 ν 1 ν 2 • • • ν x -1
.

(1.1)

Let us denote by F (respectively F + and F d ) the space of real-valued (respectively positive and non-negative non-decreasing) functions f on N. The associated semigroup (P t ) t≥0 is defined for any bounded or non-negative function f as

P t f (x) = E x [f (X t )] = ∞ y=0 f (y)P x t (y), x ∈ N.
This family of operators is positivity preserving and contractive on L p (µ), p ∈ [1, ∞].

Moreover, the semigroup is also symmetric in L 2 (µ) since λ x µ(x) = ν 1+x µ(1 + x) for any x ∈ N (detailed balance equation). The generator L of the process is given for any f ∈ F and x ∈ N by

Lf (x) = λ x (f (x + 1) -f (x)) + ν x (f (x -1) -f (x)) = λ x ∂f (x) + ν x ∂ * f (x),
where ∂ and ∂ * are respectively the forward and backward discrete gradients on N:

∂f (x) := f (x + 1) -f (x) and ∂ * f (x) := f (x -1) -f (x).

Our approach is inspired from the remarkable properties of two special birth-death processes: the M/M/1 and the M/M/∞ queues. The M/M/∞ queue has rates λ x = λ and ν x = νx for positive constants λ and ν. It is positive recurrent and its stationary distribution is the Poisson measure µ ρ with mean ρ = λ/µ. If B x,p stands for the binomial distribution of size x ∈ N and parameter p ∈ [0, 1], the M/M/∞ process satisfies for every x ∈ N and t ≥ 0 to the Mehler type formula

L (X t |X 0 = x) = B
x,e -νt * µ ρ(1-e -νt ) .

(1.

2)

The M/M/1 queening process has rates λ x = λ and ν x = ν1 N\{0} where 0 < λ < ν are constants. It is a positive recurrent random walk on N reflected at 0. Its stationary distribution µ is the geometric measure with parameter ρ := λ/ν given by µ(x) = (1-ρ)ρ x for all x ∈ N. A remarkable common property shared by the M/M/1 and M/M/∞ processes is the intertwining relation

∂L = L V ∂ (1.3)
where L V = L -V is the discrete Schrödinger operator with potential V given by • V (x) := ν in the case of the M/M/∞ queue • V (x) := ν1 {0} (x) for the M/M/1 queue. Since V ≥ 0 in these two cases, the operator L V is the generator of a birth-death process with killing rate V and the associated Feynman-Kac semigroup (P V t ) t≥0 is given by

P V t f (x) = E x f (X t ) exp - t 0 V (X s )ds .
The intertwining relation (1.3) is the infinitesimal version at time t = 0 of the semigroup intertwining

∂P t f (x) = P V t ∂f (x) = E x ∂f (X t ) exp - t 0 V (X s ) ds . (1.4)
Conversely, one may deduce (1.4) from (1.3) by using a semigroup interpolation. Namely, if we consider s ∈ [0, t] → J(s) := P V s ∂P t-s f with V as above, then (1.4) rewrites as J(0) = J(t) and (1.4) follows from (1.3) since

J ′ (s) = P V s L V ∂P t-s f -∂LP t-s f = 0.
In section 2, we obtain by using semigroup interpolation an intertwining relation similar to (1.4) for more general birth-death processes. By using convexity as an additional ingredient, we also obtain sub-commutation relations. These results are new and have several applications explored in section 3, including Lipschitz contraction and Wasserstein curvature (section 3.1), functional inequalities including Poincaré, entropic, isoperimetric and transportation-information inequalities (section 3.2), hitting time of the origin for the M/M/1 queue (section 3.3), convex domination and stochastic orderings (section 3.4).

Intertwining relations and sub-commutations

Let us fix some u ∈ F + . The u-modification of the original process (X t ) t≥0 is a birthdeath process (X u,t ) t≥0 with semigroup (P u,t ) t≥0 and generator L u given by

L u f (x) = λ u x ∂f (x) + ν u x ∂ * f (x)
, where the birth and death rates are respectively given by λ u

x :=

u x+1 u x λ x+1 and ν u x := u x-1 u x ν x .
One can check that the measure λu 2 µ is symmetric for (X u,t ) t≥0 . As consequence, the process (X u,t ) t≥0 is positive recurrent if and only if λu 2 is µ-integrable. From now on, we restrict to the minimal solution corresponding to the forward and backward Kolmogorov equations given as follows: for any function f ∈ F with finite support and t ≥ 0, [START_REF] Chen | From Markov chains to non-equilibrium particle systems[END_REF]th. 2.21]. In order to justify in all circumstances the computations present in these notes, we need to extend these identities to bounded functions f . Although it is not restrictive for the backward equation, the forward equation is more subtle and requires an additional integrability assumption. From now on, we always assume that the transition rates λ u and ν u and also the potential V u are P u,t integrable. We define the discrete gradient ∂ u and the potential V u by

d dt P u,t f = P u,t L u f = L u P u,t f, cf. [
∂ u := (1/u)∂ and V u (x) := ν x+1 -ν u x + λ x -λ u x .
Let ϕ : R → R be a smooth convex function such that for some constant c > 0, and for all r ∈ R, ϕ ′ (r)r ≥ cϕ(r).

(2.1) In particular, the behavior at infinity is at least polynomial of degree c.

Let us state our first main result about intertwining and sub-commutation relations between the original process (X t ) t≥0 and its u-modification (X u,t ) t≥0 . To the knowledge of the authors, this result was not known. A connection to Chen's results on birth-death processes [START_REF] Chen | From Markov chains to non-equilibrium particle systems[END_REF] is given in section 3 in the sequel.

Theorem 2.1 (Intertwining and sub-commutation). Assume that the process is irreducible, non-explosive and that the potential V u is lower bounded. Let f ∈ F be such that sup y∈N |∂ u f (y)| < ∞, and let x ∈ N and t ≥ 0. Then the following intertwining relation holds:

∂ u P t f (x) = P Vu u,t ∂ u f (x) = E x ∂ u f (X u,t ) exp - t 0 V u (X u,s ) ds . (2.2) Moreover, if V u ≥ 0 then we have the sub-commutation relation ϕ (∂ u P t f ) (x) ≤ E x ϕ(∂ u f )(X u,t ) exp - t 0 cV u (X u,s ) ds . (2.3) Proof.
The key point is the following intertwining relation

∂ u L = L Vu u ∂ u , (2.4)
where L u is the generator of the u-modification process (X u,t ) t≥0 and L Vu u := L u -V u is the discrete Schrödinger operator with potential V u . Note that the relation (2.4) is somewhat similar to (1.3) and follows by simple computations. To prove (2.2) from (2.4), we proceed as we did to obtain (1.4) from (1.3). If we define s ∈ [0, t] → J(s) := P Vu u,s ∂ u P t-s f, then (2.2) rewrites as J(0) = J(t). Hence it suffices to show that J is constant. By [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF] we know that if ∂ u f is bounded then ∂ u P t-s f is also bounded. Hence using the Kolmogorov equations and (2.4), we obtain

J ′ (s) = P Vu u,s L Vu u ∂ u P t-s f -∂ u LP t-s f = 0
, yielding to the intertwining relation (2.2). Now let us prove the sub-commutation relation (2.3) by adapting the previous interpolation method, under the additional assumption V u ≥ 0. Denoting

s ∈ [0, t] → J c (s) := P cVu u,s ϕ(∂ u P t-s f ), then (2.
3) rewrites as J c (0) ≤ J c (t). Hence let us show that J c is a non-decreasing function. Since ϕ(∂ u P t-s f ) is bounded, we have by the Kolmogorov equations:

J ′ c (s) = P cVu u,s (T ) where T = L cVu u ϕ(∂ u P t-s f ) -ϕ ′ (∂ u P t-s f ) ∂ u LP t-s f. Letting g u = ∂ u P t-s f ,
we obtain, by using (2.4),

T = L cVu u ϕ(g u ) -ϕ ′ (g u )L Vu u g u = λ u (∂ϕ(g u ) -ϕ ′ (g u )∂g u ) + ν u (∂ * ϕ(g u ) -ϕ ′ (g u )∂ * g u ) + V u (ϕ ′ (g u )g u -cϕ(g u )) = λ u A ϕ (g u , ∂g u ) + ν u A ϕ (g u , ∂ * g u ) + V u (ϕ ′ (g u )g u -cϕ(g u ))
where A ϕ (r, s) = ϕ(r + s) -ϕ(r) -ϕ ′ (r)s is the so-called A-transform of ϕ studied in [START_REF] Chafaï | Binomial-Poisson entropic inequalities and the M/M/∞ queue[END_REF] also known in convex analysis as the Bregman divergence associated to ϕ [Br]. Note that g u + ∂g u = g u (• + 1) and g u + ∂ * g u = g u (• -1). Now, since ϕ is convex, we have A ϕ ≥ 0. Moreover, using (2.1) and V u ≥ 0 we obtain that T ≥ 0. Finally, we get the desired result since the Feynman-Kac semigroup (P cVu u,t ) t≥0 is positivity preserving. Remark 2.2 (Ergodic condition). The potential V u in theorem 2.1 is assumed to be lower bounded. When it is positive, the so-called Chen exponent inf y∈N V u (y) is related to the exponential ergodicity of the original process (X t ) t≥0 , cf. [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF]. However identity (2.2) does not require such an ergodic assumption. A nice study of the exponential decay of birth-death processes was recently studied by Chen in [START_REF] Chen | Speed of stability for birth-death processes[END_REF], with special emphasis on non-ergodic situations including transient cases.

Remark 2.3 (Case of equality). According to the proof of theorem 2.1, the assumption V u ≥ 0 can be dropped if the convex function ϕ realizes the equality in (2.1). Such an observation was expected since in this case the use of Hölder's inequality in (2.2) entails the desired result.

Remark 2.4 (Propagation of monotonicity). The identity (2.2) provides a new proof of the propagation of monotonicity [S, prop. 4.2.10]: if f ∈ F d then P t f ∈ F d for all t ≥ 0. See section 3.4 for an interpretation in terms of stochastic ordering.

Remark 2.5 (Other gradients). Theorem 2.1 possesses a natural analogue for the discrete backward gradient ∂ * . We ignore if there exists a useful "balanced" intertwining relation involving a combination of both forward and backward gradients.

Remark 2.6 (Higher dimensional spaces). The extension of theorem 2.1 to higher dimensional discrete processes such as queuing networks or interacting particles systems arising in statistical mechanics is a very natural question, but seems to be technically difficult. However a first step has been emphasized by Wu in his study of functional inequalities for Gibbs measures through the Dobrushin uniqueness condition: see step 1 in the proof of proposition 2.5 in [W].

Our second new result below complements the previous one for the case u = 1. Let I be an open interval of R and let ϕ : I → R be a smooth convex function such that ϕ ′′ > 0 and -1/ϕ ′′ is convex on I. Following the notations of [START_REF] Chafaï | Binomial-Poisson entropic inequalities and the M/M/∞ queue[END_REF], we define on the convex subset

A I := {(r, s) ∈ R 2 : (r, r + s) ∈ I × I} the non-negative function B ϕ on A I by B ϕ (r, s) := (ϕ ′ (r + s) -ϕ ′ (r)) s, (r, s) ∈ A I .
By theorem 4.4 in [START_REF] Chafaï | Binomial-Poisson entropic inequalities and the M/M/∞ queue[END_REF], B ϕ is convex on A I . Some interesting examples of such functionals will be given in section 3.2 below.

Theorem 2.7 (Sub-commutation for 1-modification). Assume that the process is irreducible and non-explosive. If the transition rate λ is non-increasing and ν is nondecreasing then for any function f ∈ F such that sup y∈N |∂f (y)| < ∞ and for any t ≥ 0,

B ϕ (P t f, ∂P t f ) ≤ P V 1 1,t B ϕ (f, ∂f ) (2.5)
where the non-negative potential is

V 1 := ∂(ν -λ).
Proof. Under our assumption, the two processes (X t ) t≥0 and (X 1,t ) t≥0 are non-explosive. By using standard approximation procedures, one may assume that f has finite support.

If we define s ∈ [0, t] → J(s) := P V 1 1,s B ϕ (P t-s f, ∂P t-s f ) we see that (2.5) rewrites as J(0) ≤ J(t). Denote F = P t-s f and G = ∂P t-s f = ∂F . Since B ϕ (F, G)
is bounded, the Kolmogorov equations are available and using (2.4) with the constant function u = 1, we have

J ′ (s) = P V 1 1,s (T ) with T = L V 1 1 B ϕ (F, G) - ∂ ∂x B ϕ (F, G) LF - ∂ ∂y B ϕ (F, G) L V 1 1 G = λ 1 ∂B ϕ (F, G) -λ ∂ ∂x B ϕ (F, G) ∂F -λ 1 ∂ ∂y B ϕ (F, G) ∂G + ν 1 ∂ * B ϕ (F, G) -ν ∂ ∂x B ϕ (F, G) ∂ * F -ν 1 ∂ ∂y B ϕ (F, G) ∂ * G + ∂(ν -λ) ∂ ∂y B ϕ (F, G) G -B ϕ (F, G) ≥ ∂ν ∂ ∂y B ϕ (F, G) G -B ϕ (F, G) -∂λ ∂ ∂y B ϕ (F, G) G - ∂ ∂x B ϕ (F, G) G -B ϕ (F, G) ,
and where in the last line we used the convexity of the bivariate function B ϕ . Moreover, since the birth and death rates λ and ν are respectively non-increasing and non-decreasing on the one hand, and using once again convexity on the other hand, we get

∂ ∂y B ϕ (F, G) G ≥    ∂ ∂x B ϕ (F, G) G + B ϕ (F, G) B ϕ (F, G)
from which we deduce that T is non-negative and thus J is non-decreasing.

Remark 2.8 (Diffusion case). Actually, the intertwining relations above have their counterpart in continuous state space, as suggested by the so-called Witten Laplacian method used for the analysis of Langevin-type diffusion processes, see for instance Helffer's book [H]. Let A be the generator of a one-dimensional real-valued diffusion (X t ) t≥0 of the type

Af = σ 2 f ′′ + bf ′ ,
where f and the two functions σ, b are sufficiently smooth. Given a smooth positive function a on R, the gradient of interest is ∇ a f = a f ′ . Denote (P t ) t≥0 the associated diffusion semigroup. Then it is not hard to adapt to the continuous case the argument of theorem 2.1 to show that the following intertwining relation holds:

∇ a P t f (x) = E x ∇ a f (X a,t ) exp - t 0 V a (X a,s ) ds .
Here (X a,t ) t≥0 is a new diffusion process with generator

A a f = σ 2 f ′′ + b a f ′
and drift b a and potential V a given by

b a := 2σσ ′ + b -2σ 2 a ′ a and V a := σ 2 a ′′ a -b ′ + a ′ a b a .
In particular, if the weight a = σ, where σ is assumed to be positive, then the two processes above have the same distribution and by Jensen's inequality, we obtain

|∇ σ P t f (x)| ≤ E x |∇ σ f (X t )| exp - t 0 σσ ′′ -b ′ + b σ ′ σ (X s ) ds .
Hence under the assumption that there exists a constant ρ such that

inf σσ ′′ -b ′ + b σ ′ σ ≥ ρ, then we get |∇ σ P t f | ≤ e -ρt P t |∇ σ f |.
This type of sub-commutation relation is at the heart of the Bakry-Émery calculus [B-E, B, L]. See also [M-T] for a nice study of functional inequalities for the invariant measure under the condition ρ = 0. However, as we will see in remark 3.6 below, such a choice of the weight is not really adapted when studying the optimal constant in the Poincaré inequality.

Applications

This section is devoted to applications of theorems 2.1 and 2.7.

3.1. Lipschitz contraction and Wasserstein curvature. Theorem 2.1 allows to recover a result of Chen [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF] on the contraction property of the semigroup on the space of Lipschitz functions. Indeed, the intertwining (2.2) can be used to derive bounds on the Wasserstein curvature of the birth-death process, without using the coupling technique emphasized by Chen. For a distance d on N, we denote by P d (N) the set of probability measures ξ on N such that x∈N d(x, x 0 )ξ(x) < ∞ for some (or equivalently for all) x 0 ∈ N. We recall that the Wasserstein distance between two probability measures µ 1 , µ 2 ∈ P d (N) is defined by

W d (µ 1 , µ 2 ) = inf γ∈Marg(µ 1 ,µ 2 ) N N d(x, y)γ(dx, dy), (3.1)
where Marg(µ 1 , µ 2 ) is the set of probability measures on N 2 such that the marginal distributions are µ 1 and µ 2 , respectively. The Kantorovich-Rubinstein duality [V, th. 5.10] gives

W d (µ 1 , µ 2 ) = sup g∈Lip 1 (d) N g d(µ 1 -µ 2 ), (3.2)
where Lip(d) is the set of Lipschitz function g with respect to the distance d, i.e.

g Lip(d) := sup

x,y∈N

x =y |g(x) -g(y)| d(x, y) < ∞,
and Lip 1 (d) consists of 1-Lipschitz functions. We assume that the kernel P x t ∈ P d (N) for every x ∈ N and t ≥ 0 so that the semigroup is well-defined on Lip(d). The Wasserstein curvature of (X t ) t≥0 with respect to a given distance d is the optimal (largest) constant σ in the following contraction inequality: Let ρ ∈ F + be an increasing function and define u ∈ F + as u x := ρ(x + 1) -ρ(x). The metric under consideration in the forthcoming analysis is

P t Lip(d)→Lip(d) ≤ e -σt ,
d u (x, y) = |ρ(x) -ρ(y)|.
Hence u remains for the distance between two consecutive points. In particular the space of functions f for which the intertwining relation of theorem 2.1 is available is actually Lip(d u ). Then it is shown in [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF][START_REF] Joulin | A new Poisson-type deviation inequality for Markov jump processes with positive Wasserstein curvature[END_REF] by coupling arguments that the Wasserstein curvature σ u with respect to the distance d u is given by the Chen exponent, i.e.

σ u = inf x∈N ν x+1 -ν x u x-1 u x + λ x -λ x+1 u x+1 u x .
The following corollary of theorem 2.1 allows to recover this result via an intertwining relation.

Corollary 3.1 (Contraction and curvature). Assume that the potential V u is lower bounded. Then with the notations of theorem 2.1, for any t ≥ 0,

P t Lip(du)→Lip(du) = P t ρ Lip(du) = sup x∈N E x exp - t 0 V u (X u,s ) ds . (3.4)
In particular, the contraction inequality (3.3) is satisfied with the optimal constant

σ u = inf y∈N V u (y). (3.5) Proof. Let f ∈ Lip 1 (d u )
be a 1-Lipschitz function with respect to the distance d u . For any y, z ∈ N such that y < z (without loss of generality), we have by the intertwining identity (2.2) of theorem 2.1 and Jensen's inequality,

|P t f (z) -P t f (y)| ≤ z-1 x=y u x |∂ u P t f (x)| ≤ z-1 x=y u x E x |∂ u f (X u,t )| exp - t 0 V u (X u,s ) ds ≤ d u (z, y) sup x∈N E x exp - t 0 V u (X u,s ) ds ,
so that dividing by d u (z, y) and taking suprema entail the inequality:

P t Lip(du)→Lip(du) ≤ sup x∈N E x exp - t 0 V u (X u,s ) ds .
Finally, since by remark 2.4 the semigroup (P t ) t≥0 propagates monotonicity, the righthand-side of the latter inequality is nothing but P t ρ Lip(du) , showing that the supremum over Lip 1 (d u ) is attained for the function ρ. The proof of equation (3.4) is achieved.

To establish (3.5), note that it suffices to get part ≤ since the other inequality follows from (3.4). Applying (2.2) to the function ρ which is trivially in Lip 1 (d u ), we have for all x ∈ N,

σ u ≤ - 1 t log E x exp - t 0 V u (X u,s ) ds , t ≥ 0,
and taking the limit as t → 0 entails the inequality σ u ≤ V u (x), available for all x ∈ N.

The proof of (3.5) is now complete.

sup f ∈Lip 1 (du) |∂g f (x)| = sup f ∈Lip 1 (du) u x ∞ 0 |∂ u P t f (x)| dt = u x ∞ 0 ∂ u P t ρ(x) dt = u x ∞ 0 E x exp - t 0 V u (X u,s ) ds dt ≤ u x σ u .
3.2. Functional inequalities. Theorems 2.1 and 2.7 allow to establish a whole family of discrete functional inequalities. We define the bilinear symmetric form Γ on F by

Γ(f, g) := 1 2 (L(f g) -f Lg -gLf ) = 1 2 (λ ∂f ∂g + ν ∂ * f ∂ * g).
Under the positive recurrence assumption, the associated Dirichlet form acting on its domain

D(E µ ) × D(E µ ) is given by E µ (f, g) := 1 2 N Γ(f, g) dµ = N λ ∂f ∂g dµ
where the second equality comes from the reversibility of the process. Here the domain

D(E µ ) corresponds to the subspace of functions f ∈ L 2 (µ) such that E µ (f, f ) is finite.
The stationary distribution µ is said to satisfy the Poincaré inequality with constant c if for any function

f ∈ D(E µ ), c Var µ (f ) ≤ E µ (f, f ), (3.6) where Var µ (f ) := µ(f 2 ) -µ(f ) 2 and µ(f ) := N f dµ.
The optimal (largest) constant c P is the spectral gap of L, i.e. the first non-trivial eigenvalue of the operator -L. The constant c P governs the L 2 (µ) exponential decay to the equilibrium of the semigroup: for all f ∈ L 2 (µ) and t ≥ 0,

P t f -µ(f ) L 2 (µ) ≤ e -c P t f -µ(f ) L 2 (µ) .
Several years ago, Chen used a coupling method which provides the following formula for the spectral gap:

c P = sup u∈F + σ u
where σ u is the Wasserstein curvature of section 3.1 or, in other words, the Chen exponent. It corresponds to theorem 1.1 in [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF], equation (1.4). The following corollary of theorem 2.1 allows to recover the ≥ part of Chen's formula.

Corollary 3.3 (Spectral gap and Wasserstein curvatures). Assume that there exists some function u ∈ F + such that the associated Wasserstein curvature σ u is positive. Then the Poincaré inequality (3.6) holds with constant sup u∈F + σ u , or in other words

c P ≥ sup u∈F + σ u .
Proof. Since there exists some function u ∈ F + such that the Wasserstein curvature σ u is positive, the process is positive recurrent. By proposition 6.59 in [START_REF] Chen | From Markov chains to non-equilibrium particle systems[END_REF], the subspace of D(E µ ) consisting of functions with finite support is a core of the Dirichlet form and thus we can assume without loss of generality that f has finite support. We have

Var µ (f ) = - N ∞ 0 d dt (P t f ) 2 dt dµ = -2 N ∞ 0 P t f LP t f dt dµ = 2 ∞ 0 N λ u 2 (∂ u P t f ) 2 dµ dt ≤ 2 ∞ 0 e -2σut N λ u 2 P u,t (∂ u f ) 2 dµ dt,
where in the last line we used theorem 2.1 with the convex function ϕ(x) = x 2 . Now the measure λu 2 µ is invariant for the semigroup (P u,t ) t≥0 , so that we have

Var µ (f ) ≤ 2 ∞ 0 e -2σut N λ u 2 (∂ u f ) 2 dµ dt = 1 σ u N λ (∂f ) 2 dµ = 1 σ u E µ (f, f ),
where in the second line we used σ u > 0. The proof of the Poincaré inequality is complete.

Remark 3.4 (M/M/∞ and M/M/1). The spectral gap of the M/M/∞ and M/M/1 processes is well-known [START_REF] Chen | Estimation of spectral gap for Markov chains[END_REF]. Corollary 3.3 allows to recover it easily. Indeed, in the M/M/∞ case, the value c P = ν can be obtained as follows: choose the constant weight u = 1 to get c P ≥ ν, and notice that the equality holds for affine functions. For a positive recurrent M/M/1 process, i.e. λ < ν, we obtain c P ≥ ( √ λ -√ ν) 2 by choosing the weight u x := (ν/λ) x/2 , whereas the equality asymptotically holds in (3.6) as κ → ν/λ for the functions κ x , x ∈ N. We conclude that c P = ( √ λ -√ ν) 2 .

Remark 3.5 (Alternative method for M/M/1). In the M/M/1 case, let us recover the bound c P ≥ ( √ λ -√ ν) 2 by using a different method. Letting ρ(x) := x for x ∈ N and

g = f -f (0) for a given function f ∈ D(E µ ), we have N g 2 dµ = 1 ν -λ N g 2 (-Lρ) dµ = 1 ν -λ E µ (g 2 , ρ) = λ ν -λ N ∂(g 2 ) ∂ρ dµ = λ ν -λ N 2g ∂f + (∂f ) 2 dµ ≤ λ ν -λ 2 N g 2 dµ N (∂f ) 2 dµ + N (∂f ) 2 dµ ,
where in the last inequality we used Cauchy-Schwarz' inequality. Solving this polynomial of degree 2 entails the inequality

N g 2 dµ ≤ λ ( √ λ - √ ν) 2 N (∂f ) 2 dµ.
Finally using the inequality Var µ (f ) ≤ N g 2 dµ, we get the result.

Remark 3.6 (Diffusion case). As mentioned in remark 2.8, the argument above leading to the Poincaré inequality might be extended to the positive recurrent diffusion case. In particular, under the same notation we obtain the following lower bound on the Poincaré constant

c P ≥ sup a inf x∈R V a (x),
where the supremum is taken over all positive C 2 function a on R. Note that up to the transformation a → 1/a, such a formula was already obtained by Chen and Wang in [C-W] through their theorem 3.1, equation (3.4), by using a coupling approach somewhat similar to that emphasized by Chen in the discrete case.

Theorem 2.7 allows to derive functional inequalities more general than the Poincaré inequality. Let I be an open interval of R and for a smooth convex function ϕ : I → R such that ϕ ′′ > 0 and -1/ϕ ′′ is convex on I, we define the ϕ-entropy of a sufficiently integrable function f :

N → I as Ent ϕ µ (f ) = µ (ϕ(f )) -ϕ (µ(f ))
. Following [START_REF] Chafaï | Entropies, convexity, and functional inequalities: on Φ-entropies and Φ-Sobolev inequalities[END_REF], we say that the stationary distribution µ satisfies a ϕ-entropy inequality with constant c > 0 if for any

I-valued function f ∈ D(E µ ) such that ϕ ′ (f ) ∈ D(E µ ), c Ent ϕ µ (f ) ≤ E µ (f, ϕ ′ (f )) . (3.7)
See for instance [START_REF] Chafaï | Binomial-Poisson entropic inequalities and the M/M/∞ queue[END_REF] for an investigation of the properties of ϕ-entropies. The ϕentropy inequality (3.7) is satisfied if and only if the following entropy dissipation of the semigroup holds: for any sufficiently integrable I-valued function f and every t ≥ 0, Ent ϕ µ (P t f ) ≤ e -ct Ent ϕ µ (f ). We have the following corollary of theorem 2.7.

Corollary 3.7 (Entropic inequalities and Wasserstein curvature). If the birth rate λ is non-increasing and the Wasserstein curvature σ 1 (with the constant weight u = 1) is positive, then the ϕ-entropy inequality (3.7) holds with constant σ 1 .

Proof. As in the proof of corollary 3.3 the assertion σ 1 > 0 entails the positive recurrence of the process. Moreover, we assume once again that the I-valued function f has finite support. By reversibility, we have

Ent ϕ µ (f ) = N (ϕ(P 0 f ) -ϕ(µ(f ))) dµ = - N ∞ 0 d dt ϕ(P t f ) dt dµ = - ∞ 0 N ϕ ′ (P t f ) LP t f dµ dt = ∞ 0 N λ ∂P t f ∂ϕ ′ (P t f ) dµ dt = ∞ 0 N λ B ϕ (P t f, ∂P t f ) dµ dt,
where B ϕ is as in theorem 2.7 (the identity ∂g ∂ϕ ′ (g) = B ϕ (g, ∂g) comes from g + ∂g = g(• + 1)). Using now theorem 2.7 together with the of the measure λµ for the 1-modification semigroup (P 1,t ) t≥0 , we obtain

Ent ϕ µ (f ) ≤ ∞ 0 N e -σ 1 t λ P 1,t B ϕ (f, ∂f ) dµ dt = ∞ 0 N e -σ 1 t λ B ϕ (f, ∂f ) dµ dt = 1 σ 1 N λ B ϕ (f, ∂f ) dµ = 1 σ 1 E µ (f, ϕ ′ (f )) .
f ∈ D(E µ ) such that log f ∈ D(E µ ), σ 1 Ent ϕ µ (f ) ≤ E µ (f, log f ). (3.8)
Note that beyond this entropic inequality, it is proved in [C-DP-P] that the entropy is convex along the semigroup (a careful reading of the proof in [C-DP-P] suggests that it simply boils down to commutation and convexity of A transforms!). For the M/M/∞ process, the estimate of corollary 3.7 is sharp since σ 1 = ν and the equality in (3.8) holds as α → ∞ for the function x ∈ N → e αx . Note that the M/M/1 process and its invariant distribution, which is geometric, do not satisfy a modified log-Sobolev inequality. Another ϕ-entropy inequality of interest is that obtained when considering the convex function

φ(r) := r p , p ∈ (1, 2], with I = (0, ∞): for any positive function f ∈ D(E µ ) such that f p-1 ∈ D(E µ ), µ(f p ) -µ(f ) p ≤ p σ 1 E µ (f, f p-1 ).
(3.9)

Such an inequality has been studied in [B-T] in the case of Markov processes on a finite state space and also in [START_REF] Chafaï | Binomial-Poisson entropic inequalities and the M/M/∞ queue[END_REF] for the M/M/∞ queuing process. In particular, it can be seen as an interpolation between Poincaré and modified log-Sobolev inequalities.

Under the positive recurrence assumption, theorem 2.1 implies also other type of functional inequalities such as discrete isoperimetry and transportation-information inequalities. Given a positive function u, we focus on the distance d u constructed in section 3.1, where we assume moreover that ρ ∈ D(E µ ), i.e. λu 2 is µ-integrable or, in other words, the u-modification process (X u,t ) t≥0 is positive recurrent. The invariant measure µ is said to satisfy a weighted isoperimetric inequality with weight u and constant h u > 0 if for any absolutely continuous probability measure π with density f ∈ D(E µ ) with respect to µ, (3.10) where the Wasserstein distance W du is defined in (3.1) with respect to the distance d u .

h u W du (π, µ) ≤ N λ u |∂f | dµ,
The terminology of isoperimetry is employed here because it is a generalization of the classical isoperimetry, which states that the centered L 1 -norm is dominated by an energy of L 1 -type. Indeed, if the weight u is identically 1, then the distance d 1 between two different points is at least 1, so that (3.10) entails

2h 1 N |f -1| dµ = h 1 W d (π, µ) ≤ h 1 W d 1 (π, µ) ≤ N λ |∂f | dµ,
where d is the trivial distance 0 or 1. Note that the L 1 -energy emphasized above differs from the discrete version of the diffusion case, since our discrete gradient does not derive from Γ.

On the other hand, let us introduce the transportation-information inequalities emphasized in [G-L-W-Y]. Let α be a continuous positive and increasing function on [0, ∞) vanishing at 0. The invariant measure µ satisfies a transportation-information inequality with deviation function α if for any absolutely continuous probability measure π with density f with respect to µ, we have

α (W du (π, µ)) ≤ I(π, µ), (3.11)
where the so-called Fisher-Donsker-Varadhan information of π with respect to µ is defined as

I(π, µ) := E µ ( √ f , √ f ) if √ f ∈ D(E µ ); ∞
otherwise. Note that I(•, µ) is nothing but the rate function governing the large deviation principle in large time of the empirical measure L t := t -1 t 0 δ Xs ds, where δ x is the Dirac mass at point x. In other words, the Fisher-Donsker-Varadhan information rewrites as the variational identity [START_REF] Chen | From Markov chains to non-equilibrium particle systems[END_REF]th. 8.8]:

I(π, µ) = sup V ∈F + N - LV V dπ.
The interest of the transportation-information inequality resides in the equivalence with the following tail estimate of the empirical measure [G-L-W-Y, th. 2.4]: for any absolutely continuous probability measure π with density f ∈ L 2 (µ) with respect to µ, and any g ∈ Lip 1 (d u ), r) , r > 0, t > 0.

P π (L t (g) -µ(g) > r) ≤ f L 2 (µ) e -α(
We have the following corollary of theorem 2.1.

Corollary 3.9 (Weighted isoperimetry and transportation-information inequality). With the notations of theorem 2.1, assume that the process is positive recurrent and that the following quantity is well-defined:

κ u := ∞ 0 sup x∈N E x exp - t 0 V u (X u,s ) ds dt < ∞.
Then the weighted isoperimetric inequality (3.10) is satisfied with constant h u = 1/κ u .

If moreover there exists two constants ε > 0 and θ > 1 such that

(1 + ε)λ x u 2 x + (1 + 1/ε)ν x u 2 x-1 ≤ -a (λ x (θ -1) + ν x (1/θ -1)) + b, x ∈ N, (3.12)
where a := a ε,θ ≥ 0 and b := b ε,θ > 0 are two other constants depending on both ε and θ, then the transportation-information inequality (3.11) is satisfied with deviation function

α(r) := sup ε>0,θ>1 b 2 + 2a(r/κ u ) 2 -b 2a .
Remark 3.10 (The case of positive Wasserstein curvature). In particular if the Wasserstein curvature σ u with respect to the distance d u is positive, then the process is positive recurrent and we have

σ u W du (π, µ) ≤ N λ u |∂f | dµ and α (W du (π, µ)) ≤ I(π, µ),
with the deviation function

α(r) := sup ε>0,θ>1 b 2 + 2a(rσ u ) 2 -b 2a .
Proof. For every f, g ∈ D(E µ ) we have, by reversibility,

Cov µ (f, g) := N g - N g dµ f dµ = N - ∞ 0 LP t g dt f dµ = ∞ 0 - N P t g Lf dµ dt = ∞ 0 E µ (P t g, f ) dt. (3.13)
Now, for every probability measure π ≪ µ with dπ = f dµ, f ∈ D(E µ ), we get, using (3.13),

W du (π, µ) = sup g∈Lip 1 (du) Cov µ (f, g) = sup g∈Lip 1 (du) ∞ 0 E µ (P t g, f ) dt = sup g∈Lip 1 (du) ∞ 0 N λ u ∂f ∂ u P t g dµ dt = ∞ 0 N λ u |∂f | ∂ u P t ρ dµ dt ≤ ∞ 0 sup x∈N E x exp - t 0 V u (X u,s ) ds dt N λ u |∂f | dµ,
where in the last inequality we used theorem 2.1. This concludes the proof of the weighted isoperimetric inequality. Using now Cauchy-Schwarz inequality, reversibility and then (3.12) with

V θ (x) := θ x , x ∈ N, W du (π, µ) ≤ κ u I(π, µ) N λ u 2 f (• + 1) + f 2 dµ ≤ κ u I(π, µ) N ((1 + ε)λu 2 + (1 + 1/ε)νu 2 •-1 ) f dµ ≤ κ u I(π, µ) N -a LV θ V θ + b f dµ ≤ κ u I(π, µ) aI(π, µ) + b,
from which the desired transportation-information inequality holds.

Remark 3.11 (M/M/∞ and M/M/1 revisited). Corollary 3.9 exhibits optimal functional inequalities, at least in the M/M/∞ case and its stationary distribution, the Poisson measure of mean λ/ν. Choosing the weight u = 1, we obtain the optimal constant 1 = ν in the isoperimetric inequality. Indeed, corollary 3.9 entails 1 ≥ ν, whereas the other inequality is obtained by choosing π a Poisson measure of different parameter. For the transportation-information inequality, we recover theorem 2.1 in [M-W-W] since the choice of a := θ(1 + 1/ε)/(θ -1) and b := λ(1 + ε + (1 + 1/ε)θ) allows us to obtain the deviation function α(r) := λ( 1 + νr/λ -1) 2 , r > 0. Note that it is optimal in view of example 4.5 in [G-G-W]: for any absolutely continuous probability measure π with square-integrable density with respect to µ,

lim t→∞ 1 t log P π 1 t t 0 X s ds - λ ν > r = -λ 1 + νr λ -1 2 , r > 0.
For the M/M/1 process, we have the following inequalities for the optimal isoperimetric constant u , with u x = (ν/λ) x/2 (a quantity that will appear again in section 3.3):

( √ λ - √ ν) 2 ≤ u ≤ ( √ ν - √ λ) √ ν.
To get the second inequality, we choose the density f = (ν/λ)(1-1 {0} ) and the 1-Lipschitz test function g = ρ. In particular as the ratio λ/ν is small, we obtain u ≈ ν. However, we ignore if such a process satisfies a transportation-information inequality.

3.3.

Hitting time of the origin by the M/M/1 process. Recall that we consider the ergodic M/M/1 process (λ < ν) for which the stationary distribution is geometric of parameter λ/ν. Since the process behaves as a random walk outside 0, the ergodic property relies essentially on its behavior at point 0. Using the notation of theorem 2.1, the intertwining relation (2.2) applied with a positive function u entails the identity

∂ u P t f (x) = E x ∂ u f (X t ) exp - t 0 V u (X u,s ) ds
where the potential is given for every x ∈ N by

V u (x) := ν - u x-1 u x ν1 {x =0} + λ - u x+1 u x λ.
Following Robert [R], the process (X y t ) t≥0 is the solution of the stochastic differential equation (3.14) where (N (λ) t ) t≥0 and (N (ν) t ) t≥0 are two independent Poisson processes with parameter λ and ν, respectively. Since the process is assumed to be positive recurrent, the hitting time of 0, T y 0 := inf{t > 0 : X y t = 0} is finite almost surely. We have the following corollary of theorem 2.1. Corollary 3.12 (Hitting time of the origin for the ergodic M/M/1 process). Given x ∈ N, consider a positive recurrent M/M/1 process (X x+1 t ) t≥0 starting at point x + 1, and denote (X x u,t ) t≥0 its u-modification process starting at point x, where

X y 0 = y and dX y t = dN (λ) t -1 {X y t->0} dN (ν) t , t > 0,
u x := ν λ x 2 ≥ 1.
Then we have the following tail estimate: for any t ≥ 0,

P(T x+1 0 > t) = u x e -t ( √ λ- √ ν) 2 E 1 u(X x u,t ) exp - √ λν t 0 1 {0} (X x u,s ) ds ≤ u x e -t ( √ λ- √ ν) 2 .
Proof. Let us use a coupling argument. Let (X x t ) t≥0 be a copy of (X x+1 t ) t≥0 , starting at point x. We assume that it constructed with respect to the same driving Poisson processes (N , the processes are identically the same, so that the following identity holds:

X x+1 t = X x t + 1 {T x+1 0 >t} , t ≥ 0.
Since the original process is assumed to be positive recurrent, the coupling is successful, i.e. the coupling time is finite almost surely. Therefore we have for any function f ∈ Lip(d 1 ), where d 1 is the distance

d 1 (x, y) = |x -y|, ∂P t f (x) = P t f (x + 1) -P t f (x) = E f (X x+1 t ) -f (X x t ) = E ∂f (X x t ) 1 {T x+1 0 >t}
so that if we denote the function ρ(x) = x, we obtain

P(T x+1 0 > t) = ∂P t ρ(x) = u x ∂ u P t ρ(x).
Using now (2.2) with the function u, we get

P(T x+1 0 > t) = u x E 1 u(X x u,t ) exp - t 0 V u (X x u,s ) ds ,
where

V u := ( √ λ - √ ν) 2 + √ λν 1 {0} .
Remark 3.13 (Sharpness). Using a completely different approach, Van Doorn established in [VD], through his theorem 4.2 together with his example 5, the following asymptotics

lim t→∞ 1 t log P(T x+1 0 > t) = -( √ λ - √ ν) 2 , x ∈ N.
Hence one deduces that the exponential decay in the result of corollary 3.12 is sharp. On the other hand, proposition 5.4 in [R] states that T x+1 0 has exponential moment bounded as follows:

E e ( √ λ- √ ν) 2 T x+1 0 ≤ ν λ (x+1)/2
, so that Chebyshev's inequality yields a tail estimate somewhat similar to ours -although with a worst constant depending on the initial point x + 1.

Remark 3.14 (Other approach). The proof of corollary 3.12 suggests also a martingale approach. First, note that we have the identity

-ν 1 {0} = - Lu u -V u
which entails as in the previous proof and since u ≥ 1, the following computations:

P(T x+1 0 > t) = ∂P t ρ(x) = E exp - t 0 ν 1 {0} (X x s ) ds ≤ E u(X x t ) exp - t 0 Lu u + V u (X x s ) ds ≤ u x e -t ( √ λ- √ ν) 2 ,
since the process (M u t ) t≥0 given by

M u t := u(X x t ) exp - t 0 Lu u (X x s ) ds , t ≥ 0,
is a supermartingale. Indeed, denoting

Z u t := exp - t 0 Lu u (X x s ) ds ,
we have by Ito's formula:

dM u t = Z u t du(X x t ) + u(X x t ) dZ u t = Z u t (dM t + Lu(X x t )dt) -u(X x t ) Lu u (X x t ) Z u t dt = Z u t dM t
, where (M t ) t≥0 is a local martingale. Therefore, the process (M u t ) t≥0 is a positive local martingale and thus a supermartingale.

3.4. Convex domination of birth-death processes. Let (X x t ) t≥0 be the M/M/∞ process starting from x ∈ N. The Mehler-type formula (1.2) states that the random variable X x t has the same distribution as the independent sum of the variable X 0 t , which follows the Poisson distribution of parameter (λ/ν)(1 -e -νt ), and a binomial random variable B (x) t of parameters (x, e -νt ). By convention, B (0) t is assumed to be 0. Hence we have for any non-negative function f and any

x ∈ N, E [f (X x t )] = E[f (X 0 t + B (x) t )], t ≥ 0. (3.15)
Such an identity can be provided by using the commutation relation (1.4). Indeed we have

E f (X x+1 t ) = (1 -e -νt ) E [f (X x t )] + e -νt E[f (X x t + 1)
], so that a recursive argument on the initial state provides the required result. An interesting consequence of (3.15) appears in terms of concentration properties. For instance a straightforward computation entails that for any θ ≥ 0, we get the following inequality on the Laplace transforms

E e θX x t ≤ E e θN x t ,
where N x t is a Poisson random variable with the same mean as X x t . Therefore, using the exponential Chebyshev inequality entails an upper bound on the tail of the centered random variable X x t -E[X x t ], which is sharp as t → ∞ (recall that the stationary distribution is Poisson with parameter λ/ν). Actually, one may ask if for a more general birth-death process, the intertwining relation of type (2.2) may imply a relation similar to (3.15). This leads to the notion of stochastic ordering.

Following the presentation enlighten by Stoyan in [S], let us start with the classical notion of stochastic ordering for integer-valued random variables. We say that X is stochastically smaller than Y , and we note X

≤ d Y , if for any function f ∈ F d , E[f (X)] ≤ E[f (Y )].
Such a relation, as the convex domination introduced below, is a partial ordering on the set of distribution functions. The interesting feature of this stochastic ordering resides in its characterization in terms of coupling: we have X ≤ d Y if and only if there exist random variables X 1 and Y 1 , both defined on the same probability space and with the same distribution as X and Y respectively, such that P(X 1 ≤ X 2 ) = 1. Moreover, it is equivalent to the following comparison between tails: we have X ≤ d Y if and only P(X ≥ x) ≤ P(Y ≥ x) for any x ∈ R. In other words, the random variable X takes small values with a higher probability than Y does.

Another stochastic ordering of interest is the convex ordering, or convex domination. Denote F c the subset of F d consisting of non-negative non-decreasing convex functions, where in our discrete setting the convexity of a function f : N → R is understood as ∂ 2 f ≥ 0. We say that X is convex dominated by Y , and we note

X ≤ c Y , if for any function f ∈ F c , E[f (X)] ≤ E[f (Y )]. It is known to be equivalent to the inequality E (X -x) + ≤ E (Y -x) + , x ∈ R,
where a + := max{a, 0}. Typically, one may deduce from the convex domination concentration properties like a comparison of moments or Laplace transforms as in the M/M/∞ case above. Moreover, this refined ordering might appear for instance when using dela-Vallée-Poussin's lemma about uniform integrability of a family of random variables. However, in contrast to the ≤ d ordering, the authors ignore if there exists a genuine interpretation of the convex domination in terms of coupling.

Coming back to our birth-death framework, we observe that if we want to use the intertwining relation (2.2) of theorem 2.1 in order to obtain stochastic domination, then a first difficulty arises. Indeed, another birth-death process appears in the right-handside of (2.2), namely the u-modification of the original process. Therefore, let us provide first a lemma which allows us to compare two birth-death processes with respect to the ≤ d ordering. Although the result below is somewhat obvious from the point of view of coupling, we give an alternative proof based on the interpolation method emphasized in the proof of theorem 2.1. See also [S, prop. 4.2.10].

Lemma 3.15 (Stochastic comparison of birth-death processes). Let (X x t ) t≥0 and ( Xx t ) t≥0 be two birth-death processes both starting from x ∈ N. Denoting respectively λ, ν and λ, ν the transition rates of the associated generators L and L, we assume that they satisfy the following assumption:

λ ≤ λ and ν ≥ ν

Then for every t ≥ 0, the random variable Xx t is stochastically smaller than X x t . In other words, we have Xx t ≤ d X x t . Proof. Let g ∈ F d and define the function s ∈ [0, t] → J(s) := Ps P t-s g where (P t ) t≥0 and ( Pt ) t≥0 are the semigroups of (X x t ) t≥0 and ( Xx t ) t≥0 respectively. By differentiation, we have J ′ (s) = Ps LP t-s g -LP t-s g = Ps ( λ -λ) ∂P t-s g + (ν -ν) ∂ * P t-s g , which is non-positive since the semigroup (P t ) t≥0 satisfies the propagation of monotonicity, cf. remark 2.4. Hence the function J is non-increasing and the desired result holds. Now we are able to state the following corollary of theorem 2.1, which states a new convex domination involving decoupled random variables in the right-hand-side. However, despite some particular cases like the M/M/1 case for which the convenient coupling appearing in the proof of corollary 3.12 allows us to extend the next result to the ≤ d ordering, we ignore if it can be done in full generality.

Corollary 3.16 (Convex domination). Denote (X y t ) t≥0 a birth-death process starting at some point y ∈ N. We assume that the birth rate λ is non-increasing and that there exists κ ≥ 0 such that ∂(ν -λ) ≥ κ. Then for any t ≥ 0 and any x ∈ N, the random variable

X
E f (X x+1 t ) ≤ E[f (X x t )] + e -κt E ∂f (X x 1,t ) ≤ E[f (X x t )] + e -κt E[∂f (X x t )] = (1 -e -κt ) E[f (X x t )] + e -κt E[f (X x t + 1)] = E[f (X x t + Y t )],
where to obtain the second inequality we used lemma 3.15 with the 1-modification process (X x 1,t ) t≥0 playing the role of ( Xx t ) t≥0 since ∂f is non-decreasing (recall that f ∈ F c ). Remark 3.17 (More on convex domination). By an easy recursive argument one obtains from the latter result the following convex domination:

X x t ≤ c X 0 t + B (x)
t , where B (x) t is a binomial random variable of parameters (x, e -κt ), independent from X 0 t , as in the case of the M/M/∞ queuing process.

Remark 3. 2 (

 2 Pointwise gradient estimates for the Poisson equation). The argument used in the proof of corollary 3.1 allows also to obtain pointwise gradient estimates for the solution of the Poisson equation at the heart of Chen-Stein methods [B-H-J, Br-X, B-X, Sch]. More precisely, let us assume that d u is such that ρ ∈ L 1 (µ). For any centered function f ∈ Lip 1 (d u ), let us consider the Poisson equation -Lg = f , where the unknown is g. Then under the assumption σ u > 0, there exists a unique centered solution g f ∈ Lip(d u ) to this equation given by the formula g f = ∞ 0 P t f dt. We have for any x ∈ N the following estimate (compare with [L-M, th. 2.1]):

Remark 3. 8 (

 8 Examples of entropic inequalities).The constant in the ϕ-entropy inequality provided by corollary 3.7 is not optimal in general (compare for instance with the Poincaré inequality of corollary 3.3 when ϕ(r) = r 2 with I = R). The choice ϕ(r) = r log r with I = (0, ∞) allows us to recover the modified log-Sobolev inequality of th. 3.1]: for any positive function

  t ) t≥0 as the process (X x+1 t ) t≥0 . Hence the stochastic differential equation (3.14) satisfied by the two coupling processes entails that the difference between (X x+1 t ) t≥0 and (X x t ) t≥0 remains constant, equal to 1, until time T x+1 0 , the first hitting time of the origin by (X x+1 t ) t≥0 . After time T x+1 0

  Lip(d)→Lip(d) denotes the supremum of P t f Lip(d) when f runs over Lip 1 (d). It is actually equivalent to the property thatW d (P x t , P y t ) ≤ e -σt d(x, y), x, y ∈ N, t ≥ 0.If the optimal constant is positive, then the process is positive recurrent and the semigroup converges exponentially fast in Wasserstein distance W d to the stationary distribution µ[START_REF] Chen | From Markov chains to non-equilibrium particle systems[END_REF] th. 5.23].

	t ≥ 0.	(3.3)
	Here P t

  x+1 t is convex dominated by the independent sum of X x t and a Bernoulli random variable Y t of parameter e -κt ∈ (0, 1]. In other words, we have X x+1 t ≤ c X x t + Y t . Proof. We have to show that for any function f ∈ F c , Using the intertwining relation (2.2) of theorem 2.1, we have since f is non-decreasing:

	E f (X x+1 t	) ≤ E[f (X x t + Y t )].	(3.16)

Acknowledgments. The authors are grateful to Arnaud Guillin and Laurent Miclo for their remarks during the ANR EVOL meeting held in Hammamet (2010). They also thank the anonymous referees for their helpful suggestions and comments. This work was partially supported by the French ANR Project EVOL.


Andres Toom

Arnaud Dieumegard

Marc Pantel

Specification and Validation of Model Transformations for Certified Systems' Development

Certifying critical systems requires very precise specifications and ability to verify each development step. However, proofreading and test based verification are usually not exhaustive and as systems get more complex, their coverage is less and less adequate. Use of models allows early verification, validation and automated building of "correct by construction" systems. Our work targets formal specification and verification of model transformations. Such techniques provide significantly higher confidence of correctness and can even reach exhaustiveness. In this paper, we rely on common model driven engineering techniques to allow common engineers to write these specifications and to conduct verification. We propose to use a simple transformation model for specifying the expected relation between the source and target models after the transformation. The source and target metamodels are extended with a traceability model that defines a set of links that must exist after the transformation and whose correctness is specified as OCL constraints.

Introduction

Software is playing an increasing role in all domains, including safety critical domains such as avionics, railway, nuclear energy or medicine, besides more traditional domains. It is well known that all these systems are becoming more and more complex. Model Driven Engineering (MDE) is one of the techniques that has been applied quite successfully for designing complex software systems. Splitting a system into layers and abstracting different system properties into respective models makes large systems manageable. In an iterative or V-like development process high-level system requirements and initial coarse models are refined until the requirements and models are precise enough to be implemented. In many cases, software code can be largely or fully automatically generated from low-level models. On the other hand, modelling languages have often (but not always) clearly defined syntax and semantics. This makes a model a formal specification analysable by formal mathematically based methods. Besides complexity, in critical embedded systems there is also a related strong concern regarding safety for the end-users and the environment. A critical software system cannot be released and embedded without complying fully with the certification of its corresponding domain, for example DO-178C in the avionics, ISO26262 in the automotive and ECSS for space systems. Most of these are process-oriented, requiring that every stage of the software development needs to be verified and verifiable. The exact means for achieving these goals are usually left open and are up to the party seeking certification or qualification. An important aspect in these normative guidelines is the need for clear separation between specification, implementation and verification. Splitting these concerns to separate tasks that can be allocated to independent parties (a requirement for highly critical systems) helps to eliminate both specification and implementation flaws. Most commonly the final implementation is verified against the low level requirements via extensive testing. If the low-level requirements are in a form of human language, then the respective testsuites must be first manually created and their conformance and coverage of the requirements must be separately shown. If however, the requirements are in a formal language, then automatic verification or test generation can be applied. Ideally, the implementation can be even automatically generated from the requirement specification, as for example in the COMPCERT compiler project from Leroy [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] that is currently being experimented for flight control software by one of the authors [START_REF] França | Towards formally verified optimizing compilation in flight control software[END_REF]. This approach was experimented in the GeneAuto project where this experiment also takes place by one of the authors [START_REF] Izerrouken | Machine-checked sequencer for critical embedded code generator[END_REF]. However, the proof assistant technologies it relies on is costly and requires expert users that are currently not available in the software engineering industry that implements development tools for safety critical systems.

The use cases of transforming computer data differ largely in size and complexity ranging, for example, from transforming a configuration table to another configuration table upto translating a general purpose programming language to assembly code. While verifying the compilation of traditional programming languages to lower level languages has been studied a lot and there exist many good techniques, the studies of Domain Specific Language (DSL) transformation, model transformation and code generation is much less established. This is largely due to the fact that each case is somewhat unique -developed according to a particular need, the languages are likely to change over time and moreover, there might not be a clear formal specification of the respective languages and a suitable semantics must be chosen during the specification of the transformation. Often the semantic gap between the source and target languages of such transformations is also larger than in traditional program compilation. The approach we present here is a lightweight syntactic-structural way to specify the transformations in the Model Driven Engineering (MDE) fashion as model transformations and specify the details of the transformation relations using Object Constraint Language (OCL) constraints. Our approach has several similarities with the ones in [START_REF] Narayanan | Verifying model transformations by structural correspondence[END_REF] and [START_REF] Cariou | Ocl contracts for the verification of model transformations[END_REF], but has an important methodological difference -we are making the links between the source and target models explicit and part of the transformation specification. Our approach is a gray-box approach, which has several advantages when dealing with complex transformations.

The paper proceeds as follows. We will first present a model transformation case study that is based on the GeneAuto embedded code generator in Section 2. We will then give a high-level overview of the proposed transformation specification and verification scheme in Sections 3 and 4. In Section 5 we will formalise the specification of the transformation used in the case study and in Section 6 we describe an experimental setup that implements the whole approach. In Section 7 we explain how some routine part of the specification can be automated and in Section 8 comment some possible extensions of the approach.

Case study: Verifying transformations in the GeneAuto code generator

GeneAuto 3 is an open code generator project for transforming a set of high-level graphical modelling languages to selected common textual programming languages (see [START_REF] Toom | Gene-auto -an automatic code generator for a safe subset of simulink-stateflow and scicos[END_REF][START_REF] Izerrouken | Certifying an automated code generator using formal tools : Preliminary experiments in the geneauto project[END_REF][START_REF] Toom | Towards reliable code generation with an open tool: Evolutions of the gene-auto toolset[END_REF][START_REF] Bordin | Compilation of heterogeneous models: Motivations and challenges[END_REF] that describe the evolution of the toolset in the last 6 years). It currently supports subsets of Simulink, Stateflow and Scicos as input and C and Ada language as output. It is intended to be used and certified for critical embedded systems. That's why its design follows a clear modular MDE approach allowing to independently verify different transformation phases. After the initial importing step transformations are carried out as a sequence of refinements of intermediate models, as displayed on Figure 1. Altogether there are about 50-60 transformation passes in the tool depending on the configuration. Some of them are rather small and simple structure preserving transformations, but others are rather complex or change significantly the model structure. For practical purposes collections of transformations are combined into independent executables called elementary tools. An elementary tool reads its input model from a file and writes the output model to another file. The low-level tool requirements or transformation specification is written with respect to these observable intermediate models. However, often these are a result of several successive transformations and verifying the structural correspondence between the input and output models is non-trivial. Here, explicit transformation links provided by the transformation tool can be very helpful, as shown by the next example. Currently, the specification for most of the elementary tools in GeneAuto have been specified in the English language, with a notable exception of the Block Sequencer tool that has been specified and implemented in the Coq proof assistant [START_REF] Izerrouken | Machine-checked sequencer for critical embedded code generator[END_REF]. The natural language requirements are of course incomplete, ambiguous and not directly verifiable. In our case study we have formalised some of these requirements in such a way that the specification can be directly used for transformation verification according to the scheme described in Section 3. We will look at some transformations done by a tool called Functional Model Pre-Processor (FMPreProcessor), which handles normalising and refinement of Simulink and Scicos block diagrams. The tool is executed right after importing a user model (a diagram). At this point there is only rather basic information known about the model. Figure 2 shows a section of the simplified GASystemModel metamodel with the relevant concepts. The FMPreProcessor tool performs several quite simple transformations. Some of these are:

Simulink

-Replaces subsystems (hierarchical blocks) that have corresponding library equivalents by library blocks -Flattens virtual subsystems -Matches and replaces primitive blocks with library blocks -Removes Goto-From block pairs -Determines the execution priorities of concurrent blocks based on their graphical position As a concrete example we will look at removing Goto-From block pairs. Goto-From blocks (see Figure 3) are a way in a Simulink diagram to avoid visual clutter and split signals to sections. The GeneAuto tool removes such block pairs during the model preprocessing. A matching Goto-From pair is deleted, the endpoint of the first signal is moved to the endpoint of the second signal and the second signal is also deleted.

Verifying the correctness of this transformation is easy, provided that this is the only transformation. However, if transformations add up, even repetitive applications of the same transformation, like on figure 3, where the endpoint of the signal from From1 to Goto2 is also removed, then it will be much harder to verify the transformation's correctness. Such analysis would have to determine in the source model the whole flow path from the block In1 to the first block that will not be removed. It would have to know a lot more about the model and transformation semantics. On the other hand, if the transformation tool maintains a link relating each port to a port in a target model, then a property like the correctness of a Goto-From removal can be specified and verified with a few simple OCL rules. What all the transformation tools has to do to allow it, is to store that after the first transformation: 1. Goto1, From1 and s2 were replaced by s1 2. The port corresponding to the input port of Goto1 is now the input port of Goto2 And after the second transformation:

Out1 1 In1 1 Out1 1 Goto 2 [B] Goto 1 [A] From2 [B]
1. Goto1, From1 and s2 were replaced by s1 2. The port corresponding to the input port of Goto1 is now the input port of Out1 3. Goto2, From2 and s3 were replaced by s1 4. The port corresponding to the input port of Goto2 is now the input port of Out1.

Metamodel based transformation specification with explicit relation links

A posteriori transformation verification

To prove that an implementation of a program or model transformation (a transformation tool) matches its specification there are broadly two approaches. First, one could verify once and for all, that the implementation is correct for any possible input, as for example in [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. This approach is naturally preferable, when possible. However, in some cases an alternative approach of verifying the correctness of the transformation a posteriori on a transformation instance level can be more feasible. This idea is not new. The approach and a term Translation Validation was proposed by A.

Pnueli in [START_REF] Pnueli | Translation validation[END_REF]. The approach suggests that a program transformation phase should be followed by a verification phase, which independently from the transformation tool, verifies that the semantics of the source and target programs are the same. It further suggests that the transformation tool could provide hints to the verifier tool to help build the relation between the source and target programs more efficiently, but these should not affect the logical outcome of the verification phase. This approach generally has the obvious drawback of having to perform the verification after each transformation instance, when compared to the approach of a verified transformation tool. However, its main advantage is a simpler specification of the properties of interest and a simpler verification tool. Hence, the approach can be of advantage, when the requirements for the transformation tool are complex and evolving, as is often the case for realistic compilers or domain specific program transformers. Also, verifying the correctness of the verifier itself can be simpler in this case.

Metamodel based transformation specification

In the context of MDE the manipulated artefacts are models. The type of models is usually referred to as a metamodel: a model that defines the concepts of an instance model. This relation is purely syntactical. The Meta-Object Facility (MOF) 4 OMG standard defines a formal four-layered (M0..M3) metamodelling architecture. For example, the metamodel of the widely used Unified Modeling Language (UML) is a M2 MOF model. Similarly, all domain specific languages can also be expressed as MOF models. The core of MOF allows only expressing simple structural properties, like associations between elements, containment, cardinality etc. The Object Constraints Language (OCL) 5 is a standard declarative first order constraint and query language, which can be used to refine MOF models. For instance, one can specify structural invariants, definitions and pre-post contracts of abstract MOF operations in the OCL language. Model transformations can also be specified as models and transformation constraints as correctness properties of the transformation model. Figure 4 presents the high-level view of our approach. Both, the transformation input and output models are expected to conform to their respective metamodels. These metamodels consist of a basic structural specification with possibly additional OCL constraints. The input and output metamodels can be the same or different. The first kind of transformation is also known as a refinement or endogenous transformation and the second one as exogenous. The transformation metamodel contains three essential parts: source, target and a transformation relation. The transformation relation is a set of explicit links between elements in the source and target model. These explicit links play a key role in our approach. These links must be explicitly given along with the transformation instance to allow feasible verification of the correctness of the transformation. In our approach these links are part of the specification and it is the responsibility of the transformation performer, be it a tool or even human, to provide these links. Such an approach is also called a gray-box approach: we require some information from the transformation performer, but we don't need to know all the details of the implementation. The number and kinds of links that must be specified is transformation specific and somewhat open. The relation metamodel defines the structure of the links and the properties they must satisfy and the transformation metamodel defines, which links must exist.

Checking the correctness of the transformation

In this setting, the correctness of the transformation instance can be simply verified by checking first, that the target model conforms to the target metamodel and its constraints (conformance of the source model to its metamodel and constraints can be assumed and is likely to be at least partly verified during the transformation phase), that the transformation model structurally conforms to the transformation metamodel, that all the required translation links exist and finally that all links satisfy the respective constraints. These checks can be carried out using any standard metamodelling framework and an OCL checker. Figure 5 displays a high-level view of such a workflow. Structural correspondence verification of a transformation requires relating and element-wise comparing of elements in source and target models. The main difficulty relies in matching the corresponding elements. If the transformation is simple and structure preserving, then establishing the structural correspondence relation is straightforward and can be even automated [START_REF] Cariou | Ocl for the specification of model transformation contracts[END_REF][START_REF] Cariou | Ocl contracts for the verification of model transformations[END_REF][START_REF] Narayanan | Verifying model transformations by structural correspondence[END_REF][START_REF] Narayanan | Towards verifying model transformations[END_REF]. However, if transformations are more complex or combined, then this correspondence is much harder to establish, resulting in complex and computationally expensive verification criteria. An example is given in Section 2. Explicit transformation links, on the other hand, make it trivial to identify the related elements. It is also not necessary for all elements of source and target models to be explicitly linked. Generally, it is only required that the explicit relation is given for elements, where the location of the translated elements in the target model doesn't follow directly from the relative location of the source elements in the source model. This is also shown in Section 2.

Such an implementation can be used for early testing of the requirements and be replaced with a different one when needed. An important additional property of our approach is that: the transformation specification does not need to be complete to be usable. It can initially only address the parts whose verification is of primary concern and other parts can be specified as needed.

About executable specification

It must be noted that technologically this approach has some common points with an "executable specification" approach. In its MDE version, the source and target specifications are also given by metamodels. The transformation specification too follows a certain metamodel : the metamodel of the transformation language (for example, QVT6 , ATL 7 ). But differently from ours, the transformation model is the transformation specification and is executed with respect to a given source model to produce the target model. This approach might be good for some transformations. Especially, when the transformation can be specified declaratively. However, complex transformations are hard to represent purely declaratively. Secondly, such a transformation scheme might not satisfy the performance or other non-functional requirements that can be met in a custom transformation implementation. Thirdly, verifying the correctness of a generic model transformation engine is generally more complex than verifying an OCL checker. Finally, this approach alone does not answer the required separation of concerns and independence between specification, implementation and verification described in Section 1.

But on the other hand, since our approach presented above makes no assumptions of the transformation implementation technology, the "executable specification" can be treated as a realisation of the basic transformation specification and it can benefit from the source and target metamodel specifications. The only additional requirement is that besides the output model it must also produce the required explicit transformation links.

Interpretation of the verification result

The transformation implementation might not be perfect. If the verification passes for a specific transformation run, the output is known to satisfy the specified properties. If the verification fails, one has either the option to fix the transformation tool or the output. For large and complex applications fixing a bug might be a lengthy process and/or not under the control of the user of the tool. In some cases it might be possible to correct the output instead. If the verification then succeeds, the user has a verified output with similar guarantees as in the first case. Finally, a failure in the verification phase islikely to give messages that are understandable to the user. This is because the verification checks only structural properties of the source and target model and is able to immediately point the user to a violated rule in the OCL language and particular source and target elements. The OCL language is understandable by common engineers and there is no reference to intermediate data that has been built by the verification tools, only to the source and target models.

Transformation Metamodel

To perform model-based specification and verification of the transformation, we express the transformation of interest also as a model. Figure 6 shows our metamodel of the transformation model. This model has three main parts: references to source and target models and the relation links. The links refer to some elements in the source and target models and we expect the transformation tool to provide them. For convenient specification and verification of completness properties we also use backlinks from model elements to links. However, these backlinks can be built automatically during the verification phase. To simplify the model transformation constraints, we have introduced an attribute inSrcModel and an inverse derived attribute inTgtModel to the GenerciModelElement class. A valid transformation model needs to comply with the transformation metamodel and a set of additional OCL constraints. Some of these constraints just specify the basic consistency of a transformation model. For example, to ensure the correctness of the relation links, we define the following OCL constraints (represented partially, the OCL keyword inv defines an invariant and the keyword context specifies, for which class the constraint applies to). context GenericModelElement inv s r c h a s o n l y s r c l i n k s : inSrcModel implies t g t L i n k s ->isEmpty ( ) inv t g t h a s o n l y t g t l i n k s : inTgtModel implies s r c L i n k s ->isEmpty ( ) inv s r c l i n k s s t a r t f r o m s r c : . . . inv t g t l i n k s e n d i n t g t : . . . context G e n e r i c L i n k inv s r c e l e m s a l l d e f i n e d : . . . inv t g t e l e m s a l l d e f i n e d : . . .

Other constraints are transformation specific and are specified in either the context of the respective model elements or the relation links. We use a following general pattern: for source and target metamodel elements we specify as class invariants which links they must have and for links we specify as class invariants the respective transformation's correctness properties. This will be illustrated by an example in Section 5.

Correctness of the Goto-From elimination transformation

To specify the correctness of the Goto-From elimination described in Section 2 we define a specific link class GotoFrom2SignalLink. In the transformation specifiction we also refer to another link class Port2PortLink, which keeps track of the transformation of the port. This ability to refer and navigate through links in the transformation specification makes writing precise and directly verifyable specifications very convenient -we can refer to the image of any transformed element in the target model by following the link. This allows to specify a complex transformation compositionally and verify multiple transformations with one pass.

The main OCL rules that check the correctness of a Goto-From pair elimination are given below. Notice the getTgtPort operation used in the gotoTagCheck that navigates from a port of a source model block to a corresponding port in the target model. The target port, as explained in Section 2, might not be in the same relative location as the original. Our experimental verification framework has been written in Java using standard components from the Eclipse Modeling Framework (EMF 8 ) for model handling and OCL checking. However, the approach is general and only requires capabilities to read MOF compliant models and execute OCL queries. The transformation tool that we use in our case study, FMPreProcessor, has also been implemented in Java, however, this is again not a restriction, since it is only required from the transformation tool to input and output MOF compliant models and output also the required link information relation as a MOF compliant model. The transformation workflow using the GeneAuto toolset starts by either the SimulinkImporter or ScicosImporter tool that transforms a user model to an intermediate model SM 1 in the GeneAuto System Model Language (GASystemModel). This model is read by the FMPreProcessor tool, which transforms it to SM 2 and outputs also the required links. The SM 2 model is in turn read by the next tool in the transformation chain.

The verification workflow begins with a small tool called TransformationBuilder that reads the input and output models and links, and converts them to a Transformation Model. This tool also builds the backlinks described in Section 4. Alternatively, the Transformation Model could be also built by the transformation tool, but then one must additionally verify that the source part of the Transformation Model exactly corresponds to the original source model of the transformation (SM 1 , in our example), as the Transformation Model was built by the tool we are verifying and we should not trust it. The Transformation Model is then fed to an OCLChecker tool along with a set of OCL files. The OCLChecker processes the OCL files one-by-one and checks the constraints in it with respect to the relevant elements in its input model (the Transformation Model). It produces as output either the result "Success" or an Error Model containing information about the failed constraints and references to concrete model elements that violated them.

Preferably, the formal specification exists before a transformation is implemented. However, it is possible also to refine the specification and apply the presented approach at a later phase. In our case study the FMPreProcessor tool already existed, when carrying out the study. We made small non-intrusive modifications in the tool to record and output the relation links. If the requirement to maintain the transformation links had existed beforehand, it would have cost no additional effort at this stage. Additionally, we have implemented an interface between the presented verification toolchain and the existing GeneAuto testsuite enabling to run the verification automatically on a large number of models. We plan to extend this study to specify and verify a larger part of GeneAuto in this style. The material related to the experiment can be found at http://toom. perso.enseeiht.fr/verification.

Automating specification of refinement transformations

In refinement transformations the source and target metamodels (languages) are the same. Such transformations have significant practical importance. For instance, in the GeneAuto embedded code generator that we use in our case study there are about 50-60 model transformation phases, but there are only two intermediate languages and the majority of the transformations are endogenous.

Endogenous transformations change only a part of the model and one also needs to specify that the "other parts" do not change. This can be a rather tedious task to do manually for large metamodels. However, it can be partly automated. It is relatively easy to generate the specification of an identity transformation. Then the specification can be manually refined to take into account the required changes in the model. For instance, ATL can be used to generate a part of the relation metamodel and the respective OCL constraints based on the source metamodel. We have partly used this in our case study.

Perspectives

As we target this work to be used in the modeling community and in an industrial context, we plan to extend it on other transformations in order to test for the scalability of the approach both in size and practical complexity. For the moment it's difficult to measure the difficulty to write the full specification of a code generator like Geneauto without proceeding to further investigations. The practical complexity must also be addressed by describing a taxonomy of transformations constraints adapted to model transformations specification.

We also plan to address the verification of the specification itself by developing a methodology for combining the syntactic transformation specification with additional semantics-based analysis to show the soundness and completeness of the transformation specification with respect to the semantics of the source and target languages. By verifying the conservation of the semantic properties by the application of the transformation we may be able to prove the soundness of the whole transformation independently of the implementation language.

Related works

Many authors target the verification of model transformations or code generation with various purposes and technologies (see [START_REF] Dave | Compiler verification: a bibliography[END_REF] for a compiler verification bibliography). We restricted this comparison to the closest ones: the use of model driven engineering technologies for the specification and verification of model transformation using the translation validation method. The main specific aspects of our proposal are that: a) we target qualification with respect to certification standards; b) thus we must consider the global process including independent specification, implementation and verification activities; c) we rely on OMG standards for the specification and do not enforce any technology on the implementation; d) we target only structural properties and propose to handle semantic aspects using more appropriate technologies for the specification validation in a separate phase done by different people than the one that implement the transformation; and e) we must be able to handle industrial size models.

Many proposals rely on the use of formal methods and targets both structural and semantics issues. Based on the feedbacks from the industrial partners in the GeneAuto project, we have chosen to focus on structural properties in order to ease the use of our proposal by classical software engineering team in the industry and its acceptation by certification authorities. Semantics issues will be handled at the specification validation phase by specialists. On the structural properties side, declarative languages based on rewriting rules have been the subject of many proposals based on model checking technologies (see Varro et al. [START_REF] Rensink | Model checking graph transformations: A comparison of two approaches[END_REF]) or rewriting technologies like concluence or termination checking (see Taentzer et al. [START_REF] Heckel | Confluence of typed attributed graph transformation systems[END_REF][START_REF] De Lara | Automated model transformation and its validation using atom 3 and agg[END_REF][START_REF] Ehrig | Termination criteria for model transformation[END_REF]). However, these technologies do not scale well to industrial size models.

Cariou et al. have proposed in [START_REF] Cariou | Ocl for the specification of model transformation contracts[END_REF] to specify model transformation using pre and post conditions on the source and target metamodel expressed using OCL constraints. This work was improved in [START_REF] Cariou | Ocl contracts for the verification of model transformations[END_REF] and experimented on another use case in [START_REF] Cariou | Contracts for model execution verification[END_REF]. The key difference is that they propose to build the transformation model automatically based on the available information in the source and target models. The implementation can thus be a black-box one. However, if the metamodels do not contain the appropriate information, it might not be possible to build the mandatory links, or it might be very costly for industrial size models. The use of explicit traceability links through the transformation model allows to alleviate that risk at the cost of enforcing the transformation to build the links. However, this kind of links are already mandatory for the development of certified systems. Thus, they do not increase the costs.

Narayanan et al. first proposed in [START_REF] Narayanan | Towards verifying model transformations[END_REF] to use translation validation for verifying the correctness of model transformation. They focus on the verification method and rely on the cross-links created as part of the the transformation in the GReAT9 language much in the same manner as the traceability links from the transformation model in our proposal. Their proposal could be applied to most of the declarative transformation languages that enforce the use of explicit or implicit links between source and targets in order to execute the transformations, e.g. the QVT/Relational standard, Atlas Transformation Language (ATL10 ) or Triple Graph Grammar [START_REF] Schürr | 15 years of triple graph grammars[END_REF] based tools like Fujaba11 or Moflon12 , . . . . However, these links are most of the time implementation links that appear each time a transformation rule is applied. Thus, either the rules are written in order to ease the implementation and you usually get much more links than needed, or you introduce constraints on the way you can implement the transformation in order to produce exactly the links needed for the verification. This last case is sometime not possible as the links are also needed for the internal management of the transformation. This work also focus on semantics verification that is significantly more complex and cannot usually be handled by common software engineers.

Büttner et al. have proposed recently in [START_REF] Büttner | On Validation of ATL Transformation Rules By Transformation Models[END_REF] to rely on the links inside the transformation model in order to ease the verification of transformation. They propose to extract the links from declarative transformation languages taking ATL as use case and then implement verification activities as OCL constraints on the extracted model. The verification approach is very close to our proposal. However, as the links are derived from the transformation implementation, the drawbacks stated in the previous paragraph still apply.

Narayanan et al. have also proposed something very similar to our proposal in [START_REF] Narayanan | Verifying model transformations by structural correspondence[END_REF]. They advocate to focus on structural properties, to specify the transformation as relations between the source and target metamodels and then to extract these links from the cross-links used for the implementation of the transformation with the GReaT language. There is a potential drawback if the structures of the source and target metamodels are very different. It might be required to build the transformation using several intermediate models as it is usually the case with declarative languages. Then it might get complicated to retrieve the specification link that is a composition of many implementation links. The transitive closure of a transformation rule is already a complex case: should it be translated to a single specification link, to all the intermediate links, to only the implementation links ? We enforce the implementation to build exactly the right links that must be precisely described in the specification. This introduces a cost on the implementation side but it also relieves the implementation team from the constraint of using a declarative transformation language. Morevover, as in our approach it is possible to reference the links in the transforma-tion specification, complex and composed transformations can be specified and implemented more flexibly.

Conclusion

We have described a pragmatic approach for specifying and verifying model transformations using standard modelling techniques, explicit specification of a subset of the transformation relation and OCL for specifying the transformation's correctness properties. Such an approach is well suited to the development process of complex and critical software. It promotes early formalization of the system's requirements and supports a separation of concerns between the domain specialist, who specifies the initial requirements, implementor of the transformation and a verifier. Verification of the implementation with respect to the specification is performed automatically using an OCL checker. However, the specification itself can be further verified by a verification specialist, who can independently verify the soundness and consistency of the specification by formal techniques, e.g. theorem proving. The last step is facilitated by the fact that the requirements have already been specified in a formal language (MOF with OCL). On the other hand, the transformation specification does not need to be complete to be usable, thus allowing to verify some properties of a transformation specification and implementation already at a very early stage.

On a high-level, the proposed approach is similar to the Translation Validation technique [START_REF] Pnueli | Translation validation[END_REF]. This has, on one hand, the obvious drawback of having to perform verification after each transformation instance. However, it has also advantages, when the transformation specification is complex and subject to evolvement, as in many realistic tools. The fact that in our case the specification is expressed strucutrally and using standard modelling techniques, makes the approach applicable also in an industrial context by industrial engineers. In a certified/qualified context it is also very important to be able to feasibly vertify the verification toolchain itself. This is facilitated by the fact that our approach makes use of a rather lightweight toolchain and standard components.

We have developed an experimental verification framework for testing our approach using Java and components from the EMF framework. We have formalised the transformation specification of some of the transformations from the GeneAuto embedded code generator and verified their correctness using the scheme proposed here. This experiment has been integrated in the GeneAuto nightly built testing framework. We plan to extend this work to other transformations in order to test the scalability of the approach both in size and practical complexity. We plan also to develop a methodology for combining the syntactic transformation specification with additional semanticsbased analysis to show the soundness and completeness of the transformation specification with respect to the semantics of the source and target languages.

Fig. 1 .

 1 Fig. 1. Model transformation chain in the GeneAuto code generator.

Fig. 2 .

 2 Fig. 2. A fragment of the simplified GASystemModel metamodel

From1 1 Fig. 3 .

 13 Fig. 3. Simulink diagram with chained Goto-From blocks before the normalizing transformation (above) and after it (below)

Fig. 4 .

 4 Fig. 4. High level view of the model transformation specification

Fig. 5 .

 5 Fig. 5. High-level view of model transformation and verification

Fig. 6 .

 6 Fig. 6. Transformation Metamodel

  context Block inv Goto block has GotoFromLink : type = ' Goto ' implies s r c L i n k s ->one ( o c l I s K i n d O f ( GotoFrom2SignalLink ) ) inv From block has GotoFromLink : type = ' From ' implies s r c L i n k s ->one ( o c l I s K i n d O f ( GotoFrom2SignalLink ) ) inv G o t o b l o c k i n S r c M o d e l o n l y : type = ' Goto ' implies inSrcModel inv F r o m b l o c k i n S r c M o d e l o n l y : type = ' From '

This work has been partly funded by the ITEA2 project OPEES, by ERDF through the Estonian Center of Excellence in Computer Science (EXCS) and by the French and Estonian Science Foundations throught the Parrot program.

www.geneauto.org

http://www.omg.org/mof

http://www.omg.org/spec/OCL/2.2

http://www.omg.org/spec/QVT/1.0

http://eclipse.org/atl

http://repo.isis.vanderbilt.edu/tools/get_tool?GReAT

http://eclipse.org/atl

http://www.fujaba.de

http://www.moflon.org