Caterina Urban
email: urban@di.ens.fr

The Abstract Domain of Segmented Ranking Functions

We present a parameterized abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating. The abstract domain is parameterized by a numerical abstract domain for environments and a numerical abstract domain for functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instantiation of this generic domain with intervals and affine functions. We define all abstract operators, including widening to ensure convergence. To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small imperative language, that yielded interesting preliminary results.

Introduction

Static analysis has made great progress since the introduction of Abstract Interpretation [START_REF] Cousot | Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF][START_REF] Cousot | Abstract Interpretation Frameworks[END_REF]. Most results in this area are concerned with the verification of safety properties. The verification of liveness properties (and, in particular, termination) has received considerable attention recently.

The traditional method for proving program termination is based on the synthesis of ranking functions, which map program states to elements of a wellfounded domain. Termination is guaranteed if a ranking function that decreases during computation is found. In [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], Patrick Cousot and Radhia Cousot proposed a unifying point of view on the existing approaches to termination, and introduced the idea of the computation of a ranking function by abstract interpretation. We build our work on their proposed general framework, and we design and implement a suitable parameterized abstract domain for proving termination of imperative programs by abstract interpretation.

The domain automatically synthesizes piecewise-defined ranking functions through backward invariance analysis. The analysis does not rely on assumptions about the structure of the analyzed program: for example, is not limited to simple loops, as in [START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF]. The ranking functions can be used to give upper bounds on the computational complexity of the program in terms of execution steps. Moreover, the domain infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating, while a program execution that does not respect these conditions might not terminate.

We employ segmentations to handle disjunctions arising in static program analysis, as proposed in [START_REF] Cousot | A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis[END_REF] for array content analysis. The analysis automatically partitions the space of values for the program variables by means of abstract environments. A segment is a pair of an abstract environment and an abstract function. During the analysis (similarly to other partitioning approaches in static analysis [START_REF] Jeannet | Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems[END_REF][START_REF] Rival | The Trace Partitioning Abstract Domain[END_REF]), segments are split by tests, modified by assignment and joined when merging control flows. Widening limits the number of segments of a ranking function to a maximum given as a parameter of the analysis.

The segmented ranking functions abstract domain is parameterized by the choice of the abstract environments (e.g. intervals, as in Section 3.1) and the choice of the abstract functions (e.g. affine functions, as in Section 3.2). This parameterization allows a wide range of instantiations of the domain making it possible to easily tune the trade-off between analysis precision and cost.

Motivating Example. To illustrate the potential of segmentations, let us consider the following program annotated with numbered labels to denote control points:

while 1 (x ≥ 0) do 2 x := -2x + 10 od 3
The program terminates if we consider variables with integer values (if we admit non-integer values, for x = 10 3 the program is not terminating). However, it does not have a linear ranking function. As a result, well-known methods to synthesize ranking functions like [START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF][START_REF] Bradley | The Polyranking Principle[END_REF], would not be capable to guarantee its termination.

Figure 1 illustrates the details of our backward invariance analysis. We will map each program control point to a function f ∈ Z → N of the (integer-valued) variable x, representing an upper bound on the number of execution steps before termination. We denote by 2[x ≥ 0] the function obtained from the test x ≥ 0 applied to the function at program point 2. Similarly, 3[x < 0] denotes the function obtained from the test x < 0 applied to the function at program point 3.

The analysis is performed backwards starting with the totally undefined function ⊥ at each program point. The first iteration begins from the total function f (x) = 0 at program point 3. The test x < 0 enforces loop exit: it splits the domain of the function and enforces termination in 1 step. At program point 1, the function 3[x < 0] is unmodified by the join with the yet totally undefined function 2[x ≥ 0]. At program point 2, the assignment x := -2x + 10 propagates the function increasing its value to 2. Then, the test x ≥ 0, since it does not need to split further the function domain, just propagates the function increasing again its value to 3. Finally, a second iteration starts joining once more the functions 3[x < 0] and 2[x ≥ 0] at program point 1. In this particular case, there is no need for convergence acceleration and the analysis is rather precise: at the sixth iteration, a fix-point is reached providing the following ranking function f ∈ Z → N as loop invariant at program point 1:

1st iteration 2nd iteration . . . 5th/6th iteration 3 ⊥ f (x) = 0 f (x) = 0 . . . f (x) = 0 3[x < 0] ⊥ f (x) = 1 x < 0 ⊥ x ≥ 0 f (x) = 1 x < 0 ⊥ x ≥ 0 . . . f (x) = 1 x < 0 ⊥ x ≥ 0 1 ⊥ f (x) = 1 x < 0 ⊥ x ≥ 0 f (x) =      1 x < 0 ⊥ 0 ≤ x ≤ 5 3 x > 5 . . . f (x) =                1 x < 0 5 0 ≤ x ≤ 2 9 x = 3 7 4 ≤ x ≤ 5 3 x > 5 2 ⊥ f (x) = ⊥ x ≤ 5 2 x > 5 f (x) =      4 x ≤ 2 ⊥ 3 ≤ x ≤ 5 2 x > 5 . . . f (x) =          4 x ≤ 2 8 x = 3 6 4 ≤ x ≤ 5 2 x > 5 2[x ≥ 0] ⊥ f (x) = ⊥ x ≤ 5 3 x > 5 f (x) =          ⊥ x < 0 5 0 ≤ x ≤ 2 ⊥ 3 ≤ x ≤ 5 3 x > 5 . . . f (x) =                ⊥ x < 0 5 0 ≤ x ≤ 2 9 x = 3 7 4 ≤ x ≤ 5 3 x > 5
f (x) =                1 x < 0 5 0 ≤ x ≤ 2 9 x = 3 7 4 ≤ x ≤ 5 3 x > 5
Unlike [START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF][START_REF] Bradley | The Polyranking Principle[END_REF], our method is not impaired from the fact that the program does not have a linear ranking function.

Our Contribution. In summary, this paper proposes a new abstract domain for proving termination of imperative programs. We introduce the family of parameterized abstract domains of segmented ranking functions (Section 3). We also describe the design (Section 3.3) and implementation (Section 4) of a particular instance of these generic domains based on affine functions.

Outline of the Paper. Section 2 introduces the syntax and concrete semantics of our language. In Section 3 we define the segmented ranking functions abstract domain. We describe the implementation of our prototype static analyzer, in Section 4. Finally, Section 5 discusses related work and Section 6 concludes and envisions future work.

Concrete Termination Semantics

In the following, we briefly recall some results presented in a language independent way in [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]. Then, we tailor these results for a small imperative language.

Termination Semantics

We consider a programming language with non-deterministic programs. We describe the small-step operational semantics of a program by means of a transition system Σ, τ . Σ is the set of all program states, and τ ⊆ Σ × Σ is the transition relation: a binary relation describing the transitions between a state and its possible successors during program execution. Let β τ denote the set of final states:

β τ {s ∈ Σ | ∀s ′ ∈ Σ : s, s ′ ∈ τ }.
The program trace semantics generated by a transition system Σ, τ is the set of all infinite traces over the states in Σ and all finite traces that end with a final state in β τ .

The traditional method for proving program termination is based on ranking functions, mapping program states to elements of a well-founded domain (e.g., ordinals in O). Termination is guaranteed if a ranking function that decreases during computation is found.

In [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], Patrick Cousot and Radhia Cousot prove the existence of a most precise ranking function that can be expressed in fix-point form by abstract interpretation of the program trace semantics. This function1 v τ ∈ Σ → O associates to each program state definitely leading to a final state in β τ (i.e. a program state such that all traces to which it belongs end up at a final state in β τ ), an ordinal in O representing an upper bound on the number of remaining program execution steps to termination. Otherwise stated, v τ is a partial function which domain dom(v τ ) is the set of states leading to program termination: any trace starting in a state s ∈ dom(v τ ) must terminate in at most v τ (s) execution steps, while a trace starting in a state s ∈ dom(v τ ) might not terminate.

Let us define a computational partial order :

v 1 v 2 dom(v 1 ) ⊆ dom(v 2 ) ∧ ∀x ∈ dom(v 1 ) : v 1 (x) ≤ v 2 (x).
Its related join operator is:

v 1 v 2 λρ.      v 1 (ρ) if ρ ∈ dom(v 1 ) \ dom(v 2 ) sup{v 1 (ρ), v 2 (ρ)} if ρ ∈ dom(v 1 ) ∩ dom(v 2 ) v 2 (ρ) if ρ ∈ dom(v 2 ) \ dom(v 1 )
Then, the ranking function v τ is computed by fix-point iteration2 starting from the totally undefined function ∅:

v τ lfp ∅ φ τ φ τ (v) λs. 0 if s ∈ β τ sup{v(s ′ ) + 1 | s, s ′ ∈ τ } if s ∈ pre(dom(v))
The idea is to extract the well-founded part of the transition relation τ : starting from the states in β τ and, through a backward computation based on the inverse of the transition relation τ , mapping all the states definitely leading to a final state to their ordinal rank. In case of a non-deterministic transition system Σ, τ , using pre ensures that we take into account all the possibly infinite choices made at each execution step, eliminating all traces potentially branching (through local non-determinism) to non-termination.

The next example is taken from [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF].

Example 1. Let us consider the following trace semantics:

The fix-point iterates for the corresponding ranking function are:

0 0 1 0 0 2 1 0 0 2 1 0 0 ⊓ ⊔
Note that the computational order does not coincide (see [START_REF] Cousot | Abstract Interpretation Frameworks[END_REF][START_REF] Cousot | Higher Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis[END_REF] for further discussion) with the approximation order ⊑. The order ⊑ is defined as follows:

v 1 ⊑ v 2 dom(v 1 ) ⊇ dom(v 2 ) ∧ ∀x ∈ dom(v 2 ) : v 1 (x) ≤ v 2 (x).
Its corresponding join operator is:

v 1 ⊔ v 2 λρ ∈ dom(v 1 ) ∩ dom(v 2 ). sup{v 1 (ρ), v 2 (ρ)}.
The partial orders coincide only when the functions have the same domain:

Lemma 1. dom(v 1 ) = dom(v 2 ) ⇒ (v 1 ⊑ v 2 ⇔ v 1 v 2 ). X ∈ X , n, n1, n2 ∈ I A ::= X | n | [n1, n2] | ? | -A | A1 ⋄ A2 ⋄ ∈ {+, -, * , /} B ::= true | false | ? | !B | B1 ∨ B2 | B1 ∧ B2 | A1 ⊲⊳ A2 ⊲⊳∈ {<, ≤, =, =, >, ≥} S ::= X := A | if B then S1 else S2 fi | while B do S od | S1; S2
Fig. 2: Syntax

The termination semantics v τ is sound and complete to prove termination of a program P with initial states in I: Theorem 1. A program P , with trace semantics generated by a transition system Σ, τ , terminates for all traces starting from initial states in

I ∈ ℘(Σ) if and only if there exists v ∈ Σ → O such that v τ ⊑ v ∧ I ⊆ dom(v).
Proof. See [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF].

⊓ ⊔ 2.2 A Small Imperative Language.

In the following, we give a denotational definition of v τ ∈ Σ → O for a simple imperative language. We consider a small sequential non-deterministic programming language with no procedures, no pointers and no recursion. Let X be a finite set of variables and let I be a set of values, where I ∈ {Z, Q, R}. In Figure 2, we define inductively the syntax of programs. An environment ρ ∈ X → I maps each variable in X to a value in I. Let E denote the set of all environments. The semantics of an arithmetic expression A is a function A A ∈ E → ℘(I) mapping an environment to the set of all possible values for the expression in the given environment. Similarly, the semantics of a boolean expression B is a function B B ∈ E → ℘({T, F}) mapping an environment to the set of all possible truth values for the expression in the environment. We need power-sets because we also consider non-deterministic arithmetic and boolean expressions (cf. Figure 2). Non-determinism comes in handy to model program input and to approximate non-linear expressions.

Let L be a finite set of labels. The initial and final labels of a program are denoted by i and e, respectively. A state s ∈ L × E is a pair consisting of a program control point l ∈ L and an environment ρ ∈ E. Let Σ denote the set of all program states. The program initial states belong to

Σ i {s ∈ Σ | ∃ρ ∈ E : s = i, ρ } while Σ e {s ∈ Σ | ∃ρ ∈ E : s = e, ρ }
S X := A v λρ. sup{v(ρ[X → n]) + 1 | ∀n ∈ A A ρ : ρ[X → n] ∈ dom(v)} S if B then S1 else S2 fi v (λρ(ρ ∈ dom(v1) ∧ F ∈ B B ρ). v1(ρ)) (λρ(ρ ∈ dom(v2) ∧ T ∈ B B ρ). v2(ρ)) (v1 ⊔ v2) where v1 λρ(ρ ∈ dom(S S1 v) ∧ T ∈ B B ρ). (S S1 v)(ρ) + 1 v2 λρ(ρ ∈ dom(S S2 v) ∧ F ∈ B B ρ). (S S2 v)(ρ) + 1 S while B do S od v lfp ∅ φ where φ λx. (λρ(ρ ∈ dom(v1) ∧ F ∈ B B ρ). v1(ρ)) (λρ(ρ ∈ dom(v2) ∧ T ∈ B B ρ). v2(ρ)) (v1 ⊔ v2)) v1 λρ(ρ ∈ dom(S S1 x) ∧ T ∈ B B ρ). (S S1 x)(ρ) + 1 v2 λρ(ρ ∈ dom(v) ∧ F ∈ B B ρ). v(ρ) + 1 S S1; S2 v S S1 (S S2 v) Fig. 3: Concrete Semantics v τ ∈ L → (E → O).
In a similar way, we can redefine the statement semantics: . However, such a fix-point is usually not computable.

S S ∈ (E → O) → (E → O) is
In the next section, we will present a decidable abstraction of v τ by means of piecewise-defined functions computed through backward invariance analysis.

An Abstract Domain Functor for Termination

We derive an approximate program semantics by abstract interpretation [START_REF] Cousot | Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF][START_REF] Cousot | Abstract Interpretation Frameworks[END_REF]. We look for v # τ ∈ L → V # mapping each program point l ∈ L to an abstraction of the program ranking function in that specific program point.

In particular, we abstract the ranking functions in E → O by piecewisedefined ranking functions in V # . To this end, we introduce the family of segmented ranking functions abstract domains V(E, P), parameterized by the environments abstract domains E and the functions abstract domains P. Adopting an OCaml terminology, each V is an abstract domain functor: a function mapping the parameter abstract domains E and P into a new abstract domain V(E, P). V can be applied to various implementations of E and P yielding the corresponding implementations of V(E, P), with no need for further programming effort.

In the following, in order we present the family of environments abstract domains E, the family of functions abstract domains P, and the family of pa-rameterized abstract domains of segmented ranking function V(E, P). We also describe the design of particular instances, based on intervals and affine functions, of each one of these abstract domains.

To ensure the soundness of our abstraction, throughout the rest of the paper we will continue to maintain a strict separation between approximation and computational orders (as we already did in Section 2).

Environments Abstract Domain

The environments abstract domain E abstracts sets of concrete environments in ℘(E). The abstract properties ρ # ∈ E # are called abstract environments. The concretization function γ E ∈ E # → ℘(E) maps an abstract property to the set of concrete environments having that abstract property.

In case E is a non-relational domain, ℘(E) = ℘(X → I) is abstracted to X → ℘(I), and we have E # X → B # , where the abstract domain B abstracts properties of values in I with concretization function γ B ∈ B # → ℘(I).

Intervals Abstract Domain. In the literature, numerous environments abstract domains have already been proposed (e.g., the numerical abstract domains of intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF], and convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF]).

In the following, as a simple example of non-relational environments abstract domain, we will consider the intervals abstract domain [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF]. The abstract properties in B # are empty (⊥ B ) or non-empty ([a, b]) intervals with bounds in I ∪ {-∞, +∞}. We denote the abstract partial order by ⊑ B , the join operator by ⊔ B , the meet operator by ⊓ B and the widening operator by ▽ B .

As for the abstract transformers for assignments and tests, we recall that our program concrete semantics is defined backwards (cf. Section 2), and we will see (in Section 3.4) that the program abstract semantics is computed backwards as well. Consequently, we consider backward assignment and test transfer functions, denoted by ASSIGN B and FILTER B , respectively. The primitive ASSIGN B returns an abstraction of a set of environments that can lead to another given abstraction of a set of environments by an assignment X := A. The primitive FILTER B filters out environments that do not verify a boolean expression B.

ρ # ≡ x → [-∞, 2]. The result of FILTER B for x ≥ 0 on ρ # is x → [0, 2].
Let us consider now the assignment x := -2x + 10 applied segment-wise to the ranking function at program point 1 in the last column of the table. In particular, the result of ASSIGN B on the segment represented by the environment x → [START_REF] Bourdoncle | Efficient Chaotic Iteration Strategies with Widenings[END_REF][START_REF] Bradley | The Polyranking Principle[END_REF] is the segment represented by x → [START_REF] Berdine | Variance Analyses from Invariance Analyses[END_REF][START_REF] Berdine | Variance Analyses from Invariance Analyses[END_REF] (recall that we consider the space of values for the variable x to be the set of integers Z).

⊓ ⊔

Functions Abstract Domain

The functions abstract domain P is itself a functor P(E), parameterized by the environment abstract domain E. It abstracts partial functions E → O from environments to ordinals by natural-valued partial functions of the I-valued variables in X . Let n denote |X |. The abstract properties of P belong to E # × F # , where

F # {⊥ F } ∪ {f # | f # ∈ I n → N} ∪ {⊤ F }.
The bottom function ⊥ F denotes the totally undefined function, and the top function ⊤ F , abstracts all functions mapping environments to infinite ordinals.

The concretization function γ P ∈ (E # × F # ) → (E → O) depends on the value of the variables in X according to an abstract environment ρ # ∈ E # :

γ P ( ρ # , ⊥ F ) = ∅ γ P ( ρ # , f # ) = λρ ∈ γ E (ρ # ). f # (ρ(x 1 ), . . . , ρ(x n )) γ P ( ρ # , ⊤ F ) = ∅
We define the abstract approximation preorder ⊑ P , in such a way that

ρ # 1 , f # 1 ⊑ P ρ # 2 , f # 2 ⇔ γ P ( ρ # 1 , f # 1 ) ⊑ γ P ( ρ # 2 , f # 2 ), as follows: ρ # 1 , f # 1 ⊑ P ρ # 2 , f # 2 ρ # 2 ⊑ E ρ # 1 ∧ f # 1 ⊑ F f # 2 where f # 1 ⊑ F f # 2 ∀ρ ∈ γ E (ρ # 1 ⊓ E ρ # 2 ) : f # 1 (ρ(x 1 ), . . . , ρ(x n )) ≤ f # 2 (ρ(x 1 ), . . . , ρ(x n )). Theorem 2. ρ # 1 , f # 1 ⊑ P ρ # 2 , f # 2 ⇔ γ P ( ρ # 1 , f # 1 ) ⊑ γ P ( ρ # 2 , f # 2
). The result proves that γ P is monotonic. We also define a computational partial order P :

ρ # 1 , f # 1 P ρ # 2 , f # 2 ρ # 1 ⊑ E ρ # 2 ∧ f # 1 ⊑ F f # 2 . Lemma 2. (ρ # 1 ⊑ E ρ # 2 ∧ ρ # 2 ⊑ E ρ # 1 ) ⇒ ( ρ # 1 , f # 1 ⊑ ρ # 2 , f # 2 ⇔ ρ # 1 , f # 1 ρ # 2 , f # 2 )
. Finally, in addition to a join operator ⊔ P , P is equipped with backward assignment and test abstract transformers ASSIGN P and FILTER P . In the following, we will define these operators for the affine functions abstract domain.

Affine Functions Abstract Domain. As an example of functions abstract domain, we instantiate the functor P with the intervals environment abstract domain E described above, and as abstract properties f # ∈ F # we choose affine functions of the form:

y = f (x 1 , . . . , x n ) = m 1 x 1 + • • • + m n x n + q
where x 1 , . . . , x n are variables in X , y ∈ X is a special variable not included in X , and m 1 , . . . , m n , q are constants.

The operators of the affine functions abstract domain include the join operator ⊔ P , and the abstract property transformers ASSIGN P for backward assignments and FILTER P for backward tests.

f 1 (x 1 , x 2 ) = -1 2 x 2 +2 (shown in (a)) is joined with f 2 (x 1 , x 2 ) = -1 2 x 1 +2 (shown in (b)), within the environment {x 1 → (-∞, 4], x 2 → (-∞, 4]}. The result is the function f (x 1 , x 2 ) = -1 2 x 1 -1 2 x 2 + 4 (shown in (c)).
Example 5. Let us consider f (x) = 2x + 1 within the environment x → [START_REF] Bourdoncle | Efficient Chaotic Iteration Strategies with Widenings[END_REF][START_REF] Cook | Proving Conditional Termination[END_REF], and the assignment x := x + 1. The result of the assignment is ρ # , f # , where

ρ # ≡ x → [3, 5] and f # ≡ f (x + 1) + 1 = 2(x + 1) + 1 + 1 = 2x + 4. ⊓ ⊔
In case of a non-linear expression A, the limited expressiveness of the domain forces the assignment to be approximated using non-determinism and taking into account all possible outcomes of the resulting non-deterministic assignment.

Note that the assignment abstract transformer ASSIGN P is not sound due to the over-approximation introduced by the environments transformer ASSIGN E . Example 6. Let us consider ρ # ≡ x → [2, 3] and f # ≡ f (x) = x + 1, and the assignment x := x + [START_REF] Albert | Closed-Form Upper Bounds in Static Cost Analysis[END_REF][START_REF] Alias | Multi-Dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs[END_REF]. The result of the assignment is ρ# , f # , where

ρ# ≡ x → [0, 2] and f # ≡ f (x + [1, 2]) ≡ f (x) = x + 4. It is not sound because S x := x + [1, 2] γ P ( ρ # , f # ) ⊑ γ P ( ρ# , f # ): in fact, the domain of γ P ( ρ# , f # ), that is {x → 0, x → 1, x → 2}, is not included in the domain of S x := x + [1, 2] γ P ( ρ # , f # ), that is {x → 1}. ⊓ ⊔
However, in the next section, we will exploit ASSIGN P to define ASSIGN V , for the abstract domain V(E, P), and we will prove the soundness of such transformer, despite the fact that it uses an unsound ASSIGN P .

Tests. The test abstract transformer FILTER P , given ρ # , f # ∈ E # × F # , simply narrows the domain of f # , represented by the environment ρ # , by means of the environments transformer FILTER E .

Segmented Ranking Functions Abstract Domain

The segmented ranking functions abstract domain V(E, P) introduces segmentations into P: it abstracts ranking functions in E → O by piecewise-defined abstract ranking functions belonging to:

V # {(E # × F # ) k | k ≥ 0}. An abstract property v # ∈ V # has the form v # ≡ ρ # 1 , f # 1 . . . ρ # k , f # k
, where ρ # 1 , . . . , ρ # k are non-overlapping abstract environments forming a partition of the space of values for the program variables in X .

Let ⊥ V denote the totally undefined function.

The concretization function

γ V ∈ V # → (E → O) is defined as follows 3 : γ V (v # ) = γ V ( ρ # 1 , f # 1 . . . ρ # k , f # k ) = ˙ i γ P ( ρ # i , f # i )
As in [START_REF] Cousot | A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis[END_REF], the abstract domain V(E, P) relies on a segmentation unification algorithm: given two functions v # 1 and v # 2 , it modifies their segments so that they form a common refined partition of the space of values for each program variable. The abstract order ⊑ V applies such segmentation unification and then compares the abstract ranking functions. First, their domains are compared considering the number of segments ρ # , f # in which each of the functions is defined (i.e. in which

f # = ⊥ F and f # = ⊤ F ). Then, if v #
2 is defined on less segments than v # 1 , the functions are compared piecewise using the functions order

⊑ P . Theorem 4. v # 1 ⊑ V v # 2 ⇔ γ V (v # 1 ) ⊑ γ V (v # 2 )
The result shows that γ V is monotonic. We define as well a computational partial order V that also exploits the segmentation unification algorithm. Then, it compares the domains of the functions v # 1 and v # 2 (as ⊑ V does) and, if v # 1 is defined on less segments than v # 2 , it compares the functions piecewise using the partial order P .

Note that, the approximation order ⊑ V and the computational order V coincide when the functions are defined on the same segments.

Let ⊔ V denote the join operator, ▽ V the widening operator, and let ASSIGN V and FILTER V denote the backward assignment and test transfer functions, respectively. In the following, we will define these operators and prove their soundness for an instance of V(E, P) with intervals and affine functions.

Segmented Affine Ranking Functions Abstract Domain As an example of segmented ranking functions abstract domain, we apply the functor V to the interval environments abstract domain E (described in Section 3.1) and to the affine functions abstract domain P(E) (described in Section 3.2). The abstract properties # ∈ V # are piecewise-defined affine ranking functions.

In this case, since the segments are determined by abstract intervals with constant bounds, the segmentation unification algorithm is rather simple: the unification simply introduces new bounds consequently splitting intervals in both segmentations. An example of segmentation unification is illustrated in Figure 5. Join. As the order ⊑ V , also the join operator ⊔ V depends on the segmentation unification algorithm. After the unification, the abstract ranking functions are joined piecewise by means of the abstract functions join operator ⊔ P . The next result proves the soundness of ⊔ V .

Theorem 5. γ V (v # 1 ) ⊔ γ V (v # 2 ) ⊑ γ V (v # 1 ⊔ V v # 2 )
We now define another join operator V that we will use in the following to join two functions v # 1 and v # 2 , the segmentations of which have different lower and upper bounds. Where both segmentation are defined, V applies the segmentation unification algorithm and then joins the ranking functions piecewise using the join operator ⊔ P . To the resulting segmented function, segments are added, where only one of the functions is defined.

Example 7. Let us consider the abstract piecewise-defined ranking functions

v # 1 ≡ x → [2, 4], y = 2 and v # 2 ≡ x → (-∞, 4
], y = -x + 4 represented in Figure 6a and Figure 6b, respectively. Their join is the piecewise-defined ranking function

v # ≡ x → (-∞, 2), y = -x + 4 x → [2, 4], y = 2 of Figure 6c. ⊓ ⊔
Assignments. The backward assignment abstract transformer ASSIGN V , given a segmented function v # , applies piecewise the transformer ASSIGN P and then joins the resulting segments using the join operator V . In this way, it refines the segmentation of the function so as to avoid overlapping segments.

Example 8. Let us consider v # ≡ x → [-∞, 9], ⊥ F x → [10, +∞], y = 0 and the assignment x := x + [0, 2]. The result of the assignment on v # is x → [-∞, 9], ⊥ F V x → [8, +∞], y = 1 . That is the segmented function x → [-∞, 7], ⊥ F x → [8, 9], ⊥ F x → [10, +∞], y = 1 .
The following result proves the soundness of ASSIGN V .

Theorem 6. S X := A γ V (v # ) ⊑ γ V (ASSIGN V (X := A, v # )). x 2 4 (a)
x 4 (b)

x 2 4 (c)
Fig. 6: Example of join of partial piecewise-defined ranking functions.

v # 1 (shown in (a)) is joined with v # 2 (shown in (b)). The result v # is shown in (c).
We omit the proof due to space limits. Intuitively, as we have seen in the previous section, the transformer ASSIGN P is unsound because it introduces overapproximations. In particular, over-approximations are more likely to appear because of non-determinism (cf. Example 8). However, since the resulting segments are joined by means of V , we recover from the unsoundness of ASSIGN P . In fact, by definition of V , the possible overlaps are handled with the sound join operator ⊔ P and this yields a sound backward assignment transformer ASSIGN V .

Tests. The transformer FILTER V for backward tests simply applies piecewise the transformer FILTER P .

In the following (cf. Figure 8), we will exploit FILTER V and the operator V to define the abstract counterpart of the concrete semantics for the if statement, and the abstract counterpart φ # ∈ V # → V # of φ ∈ (E → O) → (E → O), as defined in Figure 3 for the while statement. The soundness of these operators relies on an argument similar to the one we used to justify ASSIGN V .

Widening. The widening operator ▽ V prevents the number of pieces of an abstract ranking function from growing indefinitely. First, to avoid infinite chains, it performs a segmentation unification that keeps only the bounds occurring in the first segmentation. Then, it widens the functions piecewise (basically reusing4 the widening on polyhedra) and toward the adjacent segments (cf. Example 9). is shrunk by the constraint x < 5 originating from the first segment:

{x < 5, 0 ≤ y ≤ - 2 5
x + 7}.

The resulting widened segmented function is

v # ≡ x → (-∞, 5), y = - 2 5 x + 7 x → [5, 10), y = 3 x → [10, +∞), y = 1
represented in Figure 7c.

⊓ ⊔

Note that this widening does not respect the traditional definition [START_REF] Cousot | Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], since the property γ

V (v # 1 ) ⊔ γ V (v # 2 ) ⊑ γ V (v # 1 ▽ V v # 2 )
does not always hold. However, we are able to prove the following weaker result (that will be decisive for the soundness of the iterations with widening):

Lemma 3. (X ▽ V Y = X) ⇒ Y ⊑ V X Proof. When X ▽ V Y = X, we have Y V X.
Moreover, since the widening force the segmentation of X on Y , having X ▽ V Y = X means that X and Y are defined on the same segments. In this case, as we have already observed, the orders ⊑ V and V coincide, and we have Y ⊑ V X. ⊓ ⊔

Abstract Termination Semantics

We now use the operators of V(E, P) to define the statement abstract semantics S # S ∈ V # → V # by induction on the syntax of programs in Figure 8. The program abstract semantics r # τ ∈ L → V # is computed through backward invariance analysis, starting from the program final control point e ∈ L with the constant function equals to 0. The ranking function is then propagated towards the program initial control point i ∈ L taking assignments and tests

The analysis proceeds by structural induction on the program syntax, iterating loops until an abstract fix-point is reached. In case of nested loops, a fix-point on the inner loop is computed for each iteration of the outer loop, following [START_REF] Bourdoncle | Efficient Chaotic Iteration Strategies with Widenings[END_REF].

To illustrate the expressiveness of our domain, we consider more examples, besides the one shown in Section 1.

Example 10. Let us consider the following program:

while 1 (x 1 ≥ 0 ∧ x 2 ≥ 0) do if 2 (?) then 3 x 1 := x 1 -1 else 4 x 2 := x 2 -1 fi od 5
The presence of the test within the loop does not impair our method. We run our analysis delaying widening of 2 iterations, and we obtained the following loop invariant at program point 1:

f (x 1 , x 2 ) =                              1 x 1 < 0 1 x 2 < 0 3 0 ≤ x 1 < 1 ∧ 0 ≤ x 2 < 1 5 0 ≤ x 1 < 1 ∧ 1 ≤ x 2 < 2 5 1 ≤ x 1 < 2 ∧ 0 ≤ x 2 < 1 2x 1 + 3 2 ≤ x 1 ∧ 0 ≤ x 2 < 1 2x 2 + 3 0 ≤ x 1 < 1 ∧ 2 ≤ x 2 2x 1 + 2x 2 + 3 1 ≤ x 1 ∧ 1 ≤ x 2
Note how the ranking function, since its value represents an upper bound on the number of steps to termination, also provides information on the program computational complexity.

⊓ ⊔ Example 11. Let us consider the following program:

while 1 (x < 10) do 2 x := 2x od 3
Such program always terminates if and only if x > 0.

Our tool, with delayed widening of 2 iterations, is able to provide the following loop invariant:

f (x) = 3 5 ≤ x < 10 1 10 ≤ x
We can see that even when the analysis fails to prove whole program termination, it can still infer useful sufficient conditions for termination. Besides, in this case, if we assume that the variable x takes values in Z, it is sufficient to further delay the widening, to obtain the most precise ranking function:

f (x) =                9 x = 1 7 x = 2 5 3 ≤ x ≤ 4 3 5 ≤ x ≤ 9 1 10 ≤ x ⊓ ⊔

Related Work

Termination analysis has attracted increased interest over the years (cf. [START_REF] Cook | Proving Program Termination. Commun[END_REF]). Proving termination of programs is necessary for ensuring the correct behavior of systems, especially those for which unexpected behavior can be catastrophic.

The first results in this field date back to [START_REF] Turing | Checking a Large Routine[END_REF] and [START_REF] Floyd | Assigning Meanings to Programs[END_REF]. In the recent past, despite the undecidability of termination, termination analysis has benefited from many research advances and powerful termination provers have emerged.

Many results are developed on the basis of the transition invariants method introduced in [START_REF] Podelski | Transition Invariants[END_REF]. In particular, the Terminator prover [START_REF] Cook | Terminator: Beyond Safety[END_REF] is based on an algorithm for the iterative construction of transition invariants. This algorithm search for counterexamples (i.e. single paths of a program) to termination, computes a ranking function for each one of them individually (as in [START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF]), and combines them into a single termination argument. Our approach differs in that it aims to prove termination for all program paths at the same time, without resorting to counterexample-guided analysis. Moreover, it avoids the cost of explicit checking for the well-foundedness of the termination argument. The approach presented in [START_REF] Tsitovich | Loop Summarization and Termination Analysis[END_REF] shares similar motivations, but prefers loop summarization to iterative fix-point computation with widening, as considered in this paper.

Among the methods based on transition invariants, we also recall the strategy, proposed in [START_REF] Berdine | Variance Analyses from Invariance Analyses[END_REF], based on the indirect use of invariants to prove program termination (and liveness properties). On the other hand, our approach infers ranking functions directly as invariants.

In [START_REF] Alias | Multi-Dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs[END_REF], the invariants are pre-computed as in [START_REF] Berdine | Variance Analyses from Invariance Analyses[END_REF], but each program point is assigned with a ranking function (that also provides information on the program computational complexity), as in our technique.

Finally, in the literature, we found only few works that have addressed the problem of automatically finding preconditions to program termination. In [START_REF] Cook | Proving Conditional Termination[END_REF], the authors proposed a method based on preconditions generating valid ranking functions. Our approach somehow goes the other way around, using the computation of ranking functions to infer sufficient condition for termination.

Conclusions and Future Work

In this paper, we presented a family of parameterized abstract domains for proving termination of imperative programs. These domains automatically synthesize piecewise-defined ranking functions through backward invariance analysis.

We also described the design and implementation of a particular instance of these generic abstract domains based on intervals and affine functions. We have seen that the piecewise-definition of the functions allows us to overcome the non-existence of a linear ranking function for a program (cf. Section 1). Our invariance analysis is not limited to simple loop (cf. Example 10) and, even when it fails to prove whole program termination, it can still infer useful information as sufficient conditions for termination (cf. Example 11).

As might be expected, the implemented domain has a limited expressiveness that translates into an imprecision of the analysis especially in the case of nested loops (and, in general, of programs with non-linear complexity). For this reason, we would like to consider the possibility of structuring computations as suggested by [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]. It also remains for future work to design more abstract domains, based on non-linear functions as exponentials [START_REF] Feret | The Arithmetic-Geometric Progression Abstract Domain[END_REF] or polynomials. In addition, we plan to extend our research to proving other liveness properties.

We are interested as well in exploring further the possible potential of our approach in the termination-related field of automatic cost analysis [START_REF] Albert | Closed-Form Upper Bounds in Static Cost Analysis[END_REF].

Finally, another line of research would be proving definite non-termination by abstraction of the potential termination semantics proposed in [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF].

Fig. 1 :

 1 Fig. 1: Motivating Example Analysis. The analysis starts from f (x) = 0 at program point 3. At program point 1, the functions 3[x < 0] (obtained from the test x < 0) and 2[x ≥ 0] (obtained from the test x ≥ 0) are joined.

  is the set of program final states. The semantics of a statement S is a function S S ∈ (Σ → O) → (Σ → O) mapping a partial function from states to ordinals into a partial function from states to ordinals with greater value. The program semantics v τ ∈ Σ → O is computed backwards, starting from the partial function λs(s ∈ Σ e ). 0 and propagating it towards the initial states by means of S S . Note that we can redefine v τ ∈ Σ → O = (L × E) → O in an isomorphic way by point-wise lifting to L of the partial function from environments to ordinals:

  defined by induction on the syntax of programs in Figure 3. In this form, we can consider v τ ∈ L → (E → O) as an invariance semantics: to each program control point l ∈ L, it associates a partial function in E → O representing the program ranking function in that particular program point. Loop semantics requires the computation of a loop invariant as the least fix-point of a monotonic function φ ∈ (E → O) → (E → O)

Example 2 .

 2 Let us consider the ranking function at program point 2 in the second iteration column of Figure 1. The test x ≥ 0 is applied to each segment of the function, yielding the function 2[x ≥ 0]. In particular, we consider one of the segments on which such function is defined: the segment represented by the environment

Fig. 4 :

 4 Fig.4: Example of join of two abstract functions of two variables. The functionf 1 (x 1 , x 2 ) = -1 2 x 2 +2 (shown in (a)) is joined with f 2 (x 1 , x 2 ) = -1 2 x 1 +2 (shown in (b)), within the environment {x 1 → (-∞, 4], x 2 → (-∞, 4]}. The result is the function f (x 1 , x 2 ) = -1 2 x 1 -1 2 x 2 + 4 (shown in (c)).

Fig. 5 :

 5 Fig. 5: Example of segmentation unification. The segmentation shown in (a) is joined with the one shown in (b). The resulting segmentation is depicted in (c).

Example 9 .Fig. 7 :

 97 Fig. 7: Example of widening of abstract piecewise-defined ranking functions. The result of widening v # 1 (shown in (a)) with v # 2 (shown in (b) is shown in (c).

A → B is the set of partial maps from a set A to a set B.

pre(X) {s ∈ Σ | ∀s ′ ∈ Σ : s, s ′ ∈ τ ⇒ s ′ ∈ X}.

∪ joins partial functions with disjoint domains: (f1 ∪f2)(x) f1(x), if x ∈ dom(f1), and (f1 ∪f2)(x) f2(x), if x ∈ dom(f2), where dom(f1) ∩ dom(f2) = ∅.

In a similar way as the join of polyhedra was reused to define ⊔ F in Section 3.2.

Acknowledgments. We are deeply grateful to Patrick Cousot, Radhia Cousot, Antoine Miné, Xavier Rival, Jérôme Feret, Damien Massé and the anonymous referees for all their useful comments and helpful suggestions.

Join. The join operator ⊔ P , given two partial functions ρ

. . , x n ) and f # 2 ≡ y = f 2 (x 1 , . . . , x n ). The operator ⊔ F basically reuses the join of polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF]; it transforms f # 1 and f # 2 into two set of constraints of the form:

Then, it computes their convex hull:

and transforms it back to ρ # , f # , where f # ≡ y = f (x 1 , . . . , x n ). In case the convex hull contains more than one constraint on y (except for the constraint 0 ≤ y), we are in presence of several not comparable choices for f # . In such situation, we prefer a deterministic behavior for ⊔ F , and we choose f # = ⊤ F .

Example 3. Let us consider the abstract functions

x 2 + 4 (see Figure 4).

⊓ ⊔

In the particular case where

The following result proves the soundness of the join operator ⊔ P .

Assignments. In order to handle assignments X := A, the abstract domain P is equipped with an operation to substitute an arithmetic expression A for a variable X within an abstract function f # . Given ρ # , f # ∈ E # × F # , the backward abstract transformer ASSIGN P , applies the assignment independently to ρ # , by means of ASSIGN E , and to f # . Let f # ≡ f (x 1 , . . . , X, . . . , x n ). The transformer ASSIGN F has to take into account the assignment X := A and increase the value of f # : the result is the function f (x 1 , . . . , A, . . . , x n ) + 1.

Fig. 8: Abstract Semantics into account with widening around loops [START_REF] Bourdoncle | Efficient Chaotic Iteration Strategies with Widenings[END_REF]. The upward iteration sequence with widening

is ultimately stationary and we prove that its limit lfp

Proof. Follows from the soundness of the function φ # and Lemma 3.

⊓ ⊔

Finally, thanks to the soundness of all abstract operators, with the following result we establish the soundness of the program semantics r # τ for proving program termination for initial states in I.

. Then, a program P , with trace semantics described by a transition system Σ, τ , terminates for all traces starting from initial states in I ∈ ℘(Σ).

Implementation

We have implemented a research prototype static analyzer, based on our abstract domain of segmented ranking functions. It is written in OCaml on top of the Apron library [START_REF] Jeannet | Apron: A Library of Numerical Abstract Domains for Static Analysis[END_REF], and we have used it to analyze programs written in the small non-deterministic imperative language presented in Section 2.2.

To improve precision, we avoid trying to compute a ranking function for the non-reachable states: our tool runs an iterated forward and backward invariance analysis to over-approximate the reachable states definitely leading to final states [START_REF] Cousot | Abstract Interpretation and Application to Logic Programs[END_REF]. Then, it runs the backward analysis to infer the ranking function, intersecting its domain at each step with the states identified by the previous analysis.


Gwenaël Guillaume
email: guillaume.gwenael@neuf.fr

Pierre Aumond

Benoit Gauvreau

Guillaume Dutilleux

Application of the transmission line matrix

Time-domain methods, Transmission Line Matrix model, Meteorological effects, Outdoor sound propagation

Introduction

Many numerical models have been developed in order to simulate meteorological effects on outdoor sound propagation. One can cite analytical formulations such as geometrical methods (e.g. ray or gaussian beam tracing approaches) [START_REF] Ostashev | Acoustics in Moving Inhomogeneous Media, E & FN SPON[END_REF][START_REF] Salomons | Computational Atmospheric Acoustics[END_REF] or numerical models based on the resolution of the wave equation. Among these latter models, the Parabolic-Equation (PE) based method has been widely used for this purpose [START_REF] Salomons | Computational Atmospheric Acoustics[END_REF][START_REF] Lihoreau | Outdoor sound propagation modeling in realistic environments: Application of coupled parabolic and atmospheric models[END_REF][START_REF] Van Renterghem | Comparison of measurements and predictions of sound propagation in a valley-slope configuration in an inhomogeneous atmosphere[END_REF][START_REF] Cotté | Estimates of the relevant turbulent scales for acoustic propagation in an upward refracting atmosphere[END_REF]. Over the last decade, with the increasing power of computational resources, time-domain methods have also been developed and applied successfully in environmental acoustics [START_REF] Chopard | Lattice boltzmann computations and applications to physics[END_REF][START_REF] Blumrich | A linearized eulerian sound propagation model for studies of complex meteorological effects[END_REF][START_REF] Ostashev | Equations for finite-difference, time-domain simulation of sound propagation in moving inhomogeneous media and numerical implementation[END_REF][START_REF] Hornikx | The extended fourier pseudospectral time-domain method for atmospheric sound propagation[END_REF]. The most popular time-domain approach is undoubtedly the finite-difference in the time-domain (FDTD) method. Dragna has investigated for instance sound propagation over a 100 m distance within a realistic context in a frequency range between 100 Hz and 2 kHz [START_REF] Dragna | Modélisation par une approche temporelle de la propagation acoustique en milieu extérieur : traitement de frontières complexes et validation sur site ferroviaire[END_REF]. An alternative time-domain method is the Transmission Line Matrix (TLM) approach [START_REF] Kagawa | Discrete Huygens' model approach to sound wave propagation[END_REF]. This model seems very promising for describing complex outdoor sound propagation yet has not been used extensively. In order to incorporate the atmospheric effects, Hofmann has proposed an interesting formulation, which is however limited to temperature effects [START_REF] Hofmann | Simulation of outdoor sound propagation with a transmission line matrix method[END_REF]. A first attempt to define a TLM scheme with unidirectional mean flow (e.g. wind field) into the TLM grid has been provided by Kagawa and his co-workers, but its method is only successful for single wind speed direction effects [START_REF] Kagawa | Discrete Huygens' modelling simulation of sound wave propagation in velocity varying environments[END_REF]. In this paper, the approach, inspired by a method proposed by Dutilleux [START_REF] Dutilleux | Applicability of TLM to wind turbine noise prediction[END_REF], consists of mod-ifying the sound speed at each point of the discretized domain as a function of the temperature and wind speed projection on the wave front direction. This paper aims to present the integration of meteorological effects in the TLM model and then its comparison with a PE model in academic cases.

The associated paper (part 2) addresses its validation by comparison with results stemming from Lannemezan's 2005 experimental campaign [START_REF] Junker | Meteorological classification for environmental acoustics -Practical implications due to experimental accuracy and uncertainty[END_REF]. The wind and temperature fields are obtained from the meso-scale meteorological model Meso-NH [START_REF] Lafore | The Meso-nH atmospheric simulation system. Part I: Adiabatic formulation and control simulations[END_REF][START_REF] Aumond | Including drag effects of canopies: Real case large-eddy simulation studies[END_REF].

The first section presents the TLM model. In section 2 the formulation taking into account wind speed and temperature effects is described. The last section proposes evaluating the ability of the TLM to treat outdoor sound propagation problems through a comparison with PE results in two academic cases.

TLM modelling

The TLM method is based on the Huygens' principle, which states that a wavefront consists of a set of secondary sources radiating spherical wavelets whose envelopes can be broken down into a new generation of secondary sources as well. Hofmann has shown the equivalence of this approach with the resolution of the discretized wave equation [START_REF] Hofmann | Simulation of outdoor sound propagation with a transmission line matrix method[END_REF]. Other authors have also derived the two-dimensional homogeneous cartesian formulation of TLM from a Lattice Boltzmann model by removing nonlinear terms, in choosing a suitable viscosity and selecting a square grid [START_REF] Martin | Low Cost Parallelizing: A Way to be Efficient[END_REF].

The TLM statement allows describing sound propagation through both a spatial and temporal discretization of the medium as well as the propa-gation phenomena. This concept is numerically conveyed by replacing the propagation medium with a transmission lines network, through which sound propagates in the form of sound pulses. Thereby, as shown in Fig. 1, each junction, or node, links N = 4 or N = 6 transmission lines to each other in two dimensions (2D) or three dimensions (3D) respectively. Thereafter, the number of dimensions is called d such that d = 2 and d = 3 for creating a 2D and 3D model respectively. An additive branch, of index N + 1, is inserted at each node of the transmission line network, in order to consider the inhomogeneities of the propagation medium (i.e. branch 7 in Fig. 1). According to the TLM concept, sound propagates in the form of pulses. Thus, incident and scattered pulses are considered at each transmission lines junction and time increment. The propagation medium is discretized by means of a uniform cartesian meshing of mesh size (∆l) d , with ∆l being the spatial step such that:

∆l λ √ d 10 , (1)
with λ the minimal wavelength of the simulation.

The scattered pulses at time increment t and node of discrete coordinates

r such that r =    (i, j) for d = 2 (i.e. in 2D), (i, j, k) for d = 3 (i.e. in 3D), (2)
are related with the incident pulses at this node at the same time iteration by the following matrix relation:

t S r = t D r × t I r , (3)
where t I r and t S r are the vectors composed of the incident pulses t I n r and scattered pulses t S n r through each transmission line n (n = 1 to N + 1) respectively. t D r is a (N + 1) × (N + 1) scattering matrix given by:

1 2 3 4 5 6 7 t S 1 (i ,j ,k ) t S 2 (i ,j ,k ) t S 3 ( i , j , k ) t S 4 ( i , j , k ) t S 5 (i,j,k) t S 6 (i,j,k) t S 7 ( i , j , k ) 1 2 3 4 5 6 7 t I 1 (i ,j ,k ) t I 2 (i ,j ,k ) t I 3 ( i , j , k ) t I 4 ( i , j , k ) t I 5 (i,j,k) t I 6 (i,j,k) t I 7 ( i , j , k ) x y z
t D r = 2 t η r + 2d            t a r 1 . 1 t η r 1 t a r . 1 t η r . . . . . 1 1 . t a r η r 1 1 . 1 t b r            , (4)
with

t a r = - t η r + 2 (d -1) 2 (5)
and

t b r = t η r -2d 2 , ( 6
)
where t η r allows locally modifying, and if needed during the simulation, the sound speed in the propagation medium. In other words, this term is used in order to model an inhomogeneous atmosphere and is defined in section 3.1.

Finally, the nodal pressure is written as a combination of all incident pulses, i.e.:

t p r = 2 t η r + 2d N -1 n=1 t I n r + t η r t I N r . (7)
In addition, the scattered pulses from nodes adjacent to node (i, j, k) at time increment t become the incident pulses to this node at the next time iteration t + ∆t, with ∆t representing the time step defined by:

∆t = ∆l √ d c 0 , (8)
with c 0 the adiabatic sound speed. This diffusion process is governed by connection laws depicted in Fig. 2 such as:

t+∆t I n r = t S m r ± n (9)
and

t+∆t I N r = t S N r , (10)
with

   n r ± n    =                         m -1 r -    if m is even,    m + 1 r +    if m is odd, (11)
and

r ± n =          (i ± 1, j, k) , for n = 1 or 2,
(i, j ± 1, k) , for n = 3 or 4, (i, j, k ± 1) , for n = 5 or 6.

t+ ∆ t I 1 (i ,j ,k ) t+ ∆ t I 2 (i ,j ,k ) t + ∆ t I 3 ( i , j , k ) t + ∆ t I 4 ( i , j , k ) t+∆t I 5 (i,j,k) t+∆t I 6 (i,j,k) t + ∆ t I 7 ( i , j , k ) t S 2 (i -1, j, k) t S 1 (i + 1, j, k) t S 4 ( i , j - 1 , k ) t S 3 ( i , j + 1 , k ) t S 6 (i,j,k-1) t S 5 (i,j,k+1) t S 7 ( i , j , k ) (i -1, j, k) (i + 1, j, k) (i, j -1, k) (i, j + 1, k) (i, j, k -1) (i, j, k + 1)
x y z Boundaries are implemented in the TLM model at a distance ∆l/2 from the nearest node in order to ensure the synchronism of sound pulses. They can be characterized by a reflection coefficient in pressure [START_REF] Kagawa | Discrete Huygens' model approach to sound wave propagation[END_REF] or by an impedance boundary condition [START_REF] Guillaume | Time-domain impedance formulation for transmission line matrix modelling of out-door sound propagation[END_REF]. In addition, absorbing layers can be introduced in order to model an unbounded propagation medium as depicted in Ref. [START_REF] Guillaume | A simple absorbing layer implementation for transmission line matrix modeling[END_REF].

TLM formulation for acoustic propagation in a meteorological field

Regarding outdoor sound propagation, the temperature and wind fields combine to produce local variations of sound speed. The literature review above has shown that the implementation of thermal gradients is straightforward in TLM since sound speed is defined at the local level, whereas a suitable implementation for wind gradients is still underdeveloped. In order to address the general case of outdoor sound propagation, both thermal and wind effects must be taken into account simultaneously.

In order to allow for wind speed gradients in the TLM model, the approach developed in this section satisfies the previous requirement since it is based on the so-called effective sound speed. This approach requires knowledge of the local direction of the wavefront. A proof of concept of this approach for the TLM method has been proposed by one of the authors in Ref. [START_REF] Dutilleux | Applicability of TLM to wind turbine noise prediction[END_REF].

Effective sound speed

The effective sound speed is expressed as follows [START_REF] Salomons | Computational Atmospheric Acoustics[END_REF]:

t c effr = γ R t T r + t u r • t n r ( 13
)
where γ = 1.41 and R = 287 J.kg -1 .K -1 , representing the specific heat ratio and the perfect gas constant for air respectively. t T r is the temperature, t u r is the wind speed vector and t n r is the wavefront direction. The sound speed at a point r of the TLM grid verifies [START_REF] Guillaume | Application of the TLM method for the sound propagation modeling in urban area (Application de la méthode TLM à la modélisation de la propagation acoustique en milieu urbain)[END_REF]:

t c TLMr = c 0 2 t η r + 2d (14)
So, if one sets t c effr = t c TLMr , solving for the inhomogeneity parameter η leads to:

t η r = 2 √ γ R t T r + t u r • t n r ∆l 2 ∆t 2 -2d. ( 15
)
In order to ensure that η 0, the adiabatic sound speed c 0 must verify:

c 0 γ R T max + u max ( 16
)
where the subscript max is computed over the whole simulated domain and simulation duration.

Wavefront direction

Vector n defines the direction of the wavefront. This information is not readily available in the TLM approach, yet it can be approximated by a quantity relating the instantaneous sound intensity vector:

t I r = t p r • t v r ( 17
)
where t v r is the local instantaneous velocity defined in [START_REF] Kagawa | Discrete Huygens' model approach to sound wave propagation -Reverberation in a room. Sound source identification and tomography in time reversal[END_REF]:

t v r = 1 ρ 0 c 0 ( t S m r -t S n r ) ( 18
)
where m is even (see Eq. 11).

A purely local definition of the sound intensity is not suitable as an approximation for n because it is influenced by the reactive intensity which does not propagate. In order to eliminate the reactive intensity, a sible approach is to average intensity over space, for instance over a onewavelength-size domain. As a first approximation and since meteorological effects (e.g. wind-induced refraction) are a long-range phenomenon, this averaging approach is only valid far away from the source. Thus, the average intensity vector corresponds with the active intensity vector and is computed as follows:

t I avg,r = 1 (2a + 1) d rn+a rn-a t I rn , (19)
where a sets the span of the average around r n .

From Eq. ( 19), one defines:

t n r = I avg,r I avg,r . (20)
The angle θ between the wavefront and the wind directions can be defined in 2D as:

t θ r = t u r • t n r || t u r | | × || t n r | | . (21)
Fig. 3 illustrates the wave direction and the angle θ obtained without averaging (i.e. the vector t n r corresponds with the normalized instantaneous intensity vector) and by averaging the variables with a spatial span a = 10.

The reactive intensity contribution appears clearly when no averaging is applied, i.e. where the sign of the sound pressure changes. Spatial averaging significantly improves the determination of the wavefront propagation direction.

Comparison with PE results

In order to evaluate the ability of the proposed formulation to take into account meteorological effects (through wind and temperature fields) in the TLM model, 2D simulation results are compared with results obtained with the Parabolic Equation (PE) model [START_REF] Lihoreau | Outdoor sound propagation modeling in realistic environments: Application of coupled parabolic and atmospheric models[END_REF], which is widely used for this purpose.

Three simulation results are presented. The source is located alternatively at 0.15 m, 2.05 m and 5.05 m from the ground. First, the sound attenuation levels are compared over a line of receivers located at a height of 2.05 m and at a fixed frequency of 200 Hz. Then, the attenuation spectra are given at 150 m from the source. The upper frequency bound is fixed in order to limit the computation cost.

The simulation presented in Fig. 4 is performed over a rigid ground through an atmosphere characterized by a linear vertical gradient of temperature (dT /dz = 0.35 • C m -1 ) and a wind field set to zero. The sound attenuations levels are very similar. The discrepancy in the first 50 m can be explained by the PE limit at short distances from the source [START_REF] Salomons | Computational Atmospheric Acoustics[END_REF]. The depth peak differences are due to the sensitivity and numerical uncertainties of the two models. This academic case allows us to validate the effective sound speed approach without any air flow (c effr = √ γ R T r ).

Since the meteorological effets tend to increase ground effects in the case of downward refraction conditions, the second simulation proposes to consider an impedant ground defined by the Miki impedance model [START_REF] Miki | Acoustical properties of porous materials -Modifications of Delany-Bazley models[END_REF] with an air flow resistivity σ = 100 kN.s.m -4 . In addition, the effective sound speed field is calculated for a homogeneous temperature field (T = 20 • C) and for a realistic vertical wind gradient of 0.2 s -1 . Thus, it allows evaluating the In the second part of this paper, TLM simulations are performed in realistic cases (with measured meteorological fields as input data) using the approach presented in this part. Thus, numerical sound predictions are compared with experimental data obtained under various meteorological conditions.

Figure 1 :

 1 Figure 1: Representation of the incident (left) and the scattered (right) pulses at node (i, j, k) in 3D.

Figure 2 :

 2 Figure 2: Representation of the connection laws through the main transmission lines (n = 1to N ) at the node (i, j, k) in 3D.

Figure 3 :

 3 Figure 3: Computation of the wave propagation direction and of the angle θ. Representation of (a) the wavefront, and of the wave propagation direction and of the angle θ obtained from (b)-(c) the instantaneous acoustic intensity and (d)-(e) the averaged acoustic intensity with a spatial span a = 10.

Figure 4 :

 4 Figure 4: Comparison of the TLM model simulations (lines) with the PE ones (dots) for the sound propagation over a rigid ground with a linear temperature gradient such as dT /dz = 0.35 • C m -1 . The source is located at 0.15 m (blue), 2.05 m (green) and 5.05 m (red) from the ground.

Figure 5 :

 5 Figure 5: Comparison of the TLM model simulations (lines) with the PE ones (dots) for the sound propagation over a rigid ground with a linear wind gradient such as dU/dz = 0.2 s -1 . The source is located at 0.15 m (blue), 2.05 m (green) and 5.05 m (red) from the ground.


Palanichamy Kalyani
email: pkalyani@tce.edu

Anitha Ariharaputhiran

André Darchen

Kalyani Palanichamy

Andre Darchen

Activated carbon from grass -a green alternative catalyst support for water electrolysis

Keywords: grass, activated carbon, catalyst support, electrochemical studies, hydrogen, water electrolysis

HAL is

Introduction

Hydrogen is a promising energy source and hence significant research is currently being focused to test its feasibility to meet the world energy demand [START_REF] Sakintuna | Metal hydride materials for solid hydrogen storage: A review[END_REF][START_REF] Balat | Potential importance of hydrogen as a future solution to environmental and transportation problems[END_REF]. It is also ideal from an environmental standpoint-it burns cleanly producing water as the only product. Invariably it is stored in nature as water and hydrocarbons and one has to expend energy to generate H 2 from either water or hydrocarbons. A number of production methods including water electrolysis, steam reformation of natural gas, and coal gasification are the foci of widespread production research; but water electrolysis is one of the renowned technologies which provide domestically viable, CO 2 neutral and non-polluting H 2 . Noble metal like Pt or Ru based electrocatalysts are being employed for producing H 2 by electrolyzing water. Generally electrocatalysts are prepared by loading or supporting fine Pt or Ru particles on quality carbon powders -the so called catalyst support, such that more number of active sites will be available for efficient and complete electrolysis. In fact carbon black suits well for catalyst support applications [START_REF] Roskill | The economics of Activated Carbon[END_REF][START_REF] Donnet | Carbon Fibers[END_REF]. Vulcan XC-72 is the most utilized conducting carbon for fabricating electrocatalysts for water electrolysis for hydrogen gas generation [START_REF] Grigoriev | Evaluation of carbon-supported Pt and Pd nanoparticles for the hydrogen evolution reaction in PEM water electrolysers[END_REF][START_REF] Prabhuram | Synthesis and physical/electrochemical characterization of Pt/C nanocatalyst for polymer electrolyte fuel cells[END_REF]. But electrocatalysts are costly, hampering widespread commercialization of water electrolysers.

Consequently, there are two directions in which the cost factor can be addressed. Firstly, usage of less noble metal as catalysts and secondly, to use low-cost carbonaceous materials on which the metal particles can be supported. In fact our work aims at achieving the second factor by producing carbon support powders from a cheap and abundantly existing resource namely the biomass of grass blades. Obviously, the significance of adopting different types of biomass materials as starting materials in producing carbon electrodes lies in its abundance, cheap cost, simple and green methodologies in obtaining the carbon and the ability to become highly porous carbon or to get desired physical features after carbonization procedure.

Carbon materials function as a unique material and are characterized by high specific surface area and tunable porosity just to find utility in many vital technologies namely, energy conversion (fuel cells and solar cells), energy storage (super capacitors, batteries and H 2 sorption), sensors, environmental production of fine and bulk chemicals and catalysis [START_REF] Endo | Recent development of carbon materials for Li ion batteries[END_REF][START_REF] Dicks | The role of carbon in fuel cells[END_REF]. The choice of carbon as the electrode material is because of its unique properties of electrical conductivity and structural diversity. In addition to being good catalyst and catalyst support, carbon materials are effective in removing pollutants (both gaseous and liquid). Further carbon materials being insensitive to toxic substances and corrosive (acidic and basic) environments, its regeneration is possible and easy, rendering the industrial use of carbon materials an economically viable option [START_REF] Wang | Preparation of sludge-based activated carbon and its application in dye wastewater treatment[END_REF][START_REF] Chen | Physical and chemical properties study of the activated carbon made from sewage sludge[END_REF]. A fact observed by researchers that the specific physico -chemical properties that make carbon materials a potential adsorbent for pollutants are high specific surface area, porous architecture, high adsorption capacity and surface functionality [START_REF] Merzougui | Effect of oxidant treatment of date pit activated carbons application to the treatment of waters[END_REF]. Carbon consists of a highly porous structure with hydrophobic graphene layer as well as hydrophilic surface functional groups making them beneficial for sorption and catalytic applications.

It is now realized that wastes are unutilized resources. Hence chemical recycling of wastes has been recognized as one of the suitable methods of waste management and also to recover valuable products, the net result is zero-waste world. There have been many attempts to obtain lowcost carbon (activated) from agricultural wastes such as sunflower shell [START_REF] Chen | Physical and chemical properties study of the activated carbon made from sewage sludge[END_REF], pinecone [START_REF] Haykiri-Acma | Gasification of biomass chars in steam-nitrogen mixture[END_REF], cotton residues [START_REF] Haykiri-Acma | Gasification of biomass chars in steam-nitrogen mixture[END_REF], olive residues [START_REF] Haykiri-Acma | Gasification of biomass chars in steam-nitrogen mixture[END_REF], wheat [START_REF] Lanzetta | Pyrolysis kinetics of wheat and corn straw[END_REF], corn straw 13], olive stones [START_REF] Minkova | Effect of water vapour and biomass nature on the yield and quality of the pyrolysis products from biomass[END_REF][START_REF] Minkova | Thermochemical treatment of biomass in a flow of steam or in a mixture of steam and carbon dioxide[END_REF], bagasse [START_REF] Minkova | Effect of water vapour and biomass nature on the yield and quality of the pyrolysis products from biomass[END_REF][START_REF] Minkova | Thermochemical treatment of biomass in a flow of steam or in a mixture of steam and carbon dioxide[END_REF], birch wood [START_REF] Minkova | Effect of water vapour and biomass nature on the yield and quality of the pyrolysis products from biomass[END_REF][START_REF] Minkova | Thermochemical treatment of biomass in a flow of steam or in a mixture of steam and carbon dioxide[END_REF], miscanthus [START_REF] Minkova | Effect of water vapour and biomass nature on the yield and quality of the pyrolysis products from biomass[END_REF][START_REF] Minkova | Thermochemical treatment of biomass in a flow of steam or in a mixture of steam and carbon dioxide[END_REF], rapeseed [START_REF] Predel | Pyrolysis of rape-seed in a fluidized-bed reactor[END_REF], pine rayed [START_REF] Cetin | Influence of pyrolysis conditions on the structure and gasification reactivity of biomass chars[END_REF], eucalyptus maculata [START_REF] Cetin | Influence of pyrolysis conditions on the structure and gasification reactivity of biomass chars[END_REF],

sugarcane bagasse [START_REF] Cetin | Influence of pyrolysis conditions on the structure and gasification reactivity of biomass chars[END_REF][START_REF] Ahmedna | Production of granular activated carbons from select agricultural byproducts and evaluation of their physical, chemical and adsorption properties[END_REF], rice hulls [START_REF] Ahmedna | Production of granular activated carbons from select agricultural byproducts and evaluation of their physical, chemical and adsorption properties[END_REF], pecan shells [START_REF] Ahmedna | Production of granular activated carbons from select agricultural byproducts and evaluation of their physical, chemical and adsorption properties[END_REF], grape seeds [START_REF] Savova | Biomass conversion to carbon adsorbents and gas[END_REF], cherry stones [START_REF] Savova | Biomass conversion to carbon adsorbents and gas[END_REF],

hazelnut shells [START_REF] Aygun | Production of granular activated carbon from fruit stones and nutshells and evaluation of their physical, chemical and adsorption properties[END_REF], apricot stones [START_REF] Savova | Biomass conversion to carbon adsorbents and gas[END_REF][START_REF] Aygun | Production of granular activated carbon from fruit stones and nutshells and evaluation of their physical, chemical and adsorption properties[END_REF], almond shells [START_REF] Savova | Biomass conversion to carbon adsorbents and gas[END_REF][START_REF] Marcilla | Influence of thermal treatment regime on the density and reactivity of activated carbons from almond shells[END_REF], peach stones [START_REF] Tsai | Preparation and characterization of activated carbons from corn cob[END_REF], straw [START_REF] Minkova | Effect of water vapour and biomass nature on the yield and quality of the pyrolysis products from biomass[END_REF][START_REF] Minkova | Thermochemical treatment of biomass in a flow of steam or in a mixture of steam and carbon dioxide[END_REF][START_REF] Jensen | Pretreatment of straw for power production by pyrolysis and char wash[END_REF], oat hulls [START_REF] Fan | Steam activation of chars produced from oat hulls and corn stover[END_REF][START_REF] Zhang | Preparation of activated carbon from forest and agricultural residues through CO 2 activation[END_REF], corn stover [START_REF] Fan | Steam activation of chars produced from oat hulls and corn stover[END_REF][START_REF] Zhang | Preparation of activated carbon from forest and agricultural residues through CO 2 activation[END_REF], peanut hull [START_REF] Girgis | Characteristics of activated carbon from peanut hulls in relation to conditions of preparation[END_REF], nut shells [START_REF] Savova | Biomass conversion to carbon adsorbents and gas[END_REF][START_REF] Lua | Effects of pyrolysis conditions on the properties of activated carbons prepared from pistachio-nut shells[END_REF][START_REF] Ahmadroup | The preparation of activated carbon from macadamia nutshell by chemical activation[END_REF][START_REF] Yang | Characteristics of activated carbons prepared from pistachio-nut shells by physical activation[END_REF][START_REF] Ahmedna | The use of nutshell carbons in drinking water filters for removal of trace metals[END_REF], corn cob [START_REF] Tsai | Preparation and characterization of activated carbons from corn cob[END_REF][START_REF] Tsai | A low cost adsorbent from agricultural waste corn cob by zinc chloride activation[END_REF][START_REF] Tsai | Cleaner production of carbon adsorbents by utilizing agricultural waste corn cob[END_REF][START_REF] El-Hendawy | Adsorption characteristics of activated carbons obtained from corncobs[END_REF], corn hulls [START_REF] Zhang | Preparation of activated carbon from forest and agricultural residues through CO 2 activation[END_REF], rice husks [START_REF] Malik | Use of activated carbons prepared from sawdust and rice-husk for adsorption of acid dyes: a case study of Acid Yellow 36[END_REF][START_REF] Yalcin | Studies of the surface area and porosity of activated carbons prepared from rice husks[END_REF], rice straw [START_REF] Ahmedna | Production of granular activated carbons from select agricultural byproducts and evaluation of their physical, chemical and adsorption properties[END_REF][START_REF] Oh | Preparation and characteristics of rice-straw-based porous carbons with high adsorption capacity[END_REF] and used tea refuse [START_REF] Kalyani | Tea derived boric acid activated biomass carbon: Prospects as low-cost electrodes for capacitors[END_REF]. An exhaustive report on the various classes of biomasses used for supercapacitor, batteries and fuel cells has been made by the authors of the present paper [START_REF] Kalyani | Biomass carbon & its prospects in electrochemical energy systems[END_REF]. Although the above biomass have been utilized as resources for obtaining carbon powders for fabricating electrodes for the aforesaid energy devices, there has been no report on the usefulness of these biomass carbons as a catalyst supporting material. As for the knowledge of the authors of this communication goes, Kang et al [START_REF] Kang | Obtaining carbon nanotubes from grass[END_REF] describe a method of using grass for obtaining carbon nanotubes. Thus the reports on the utilization of grasses are only limited and so the current work may likely to get attention from researchers working on nonconventional energy sources and environmentalists as well.

Carbons have many advantageous features over metal oxide catalyst supports such as (i) a high specific surface area up to 3000m 2 g -1 , (ii) high stability in acidic and basic media, and (iii) easy recovery of supported metals by burning off the carbon. However, only specific carbon materials belonging to the class of carbon blacks namely Vulcan XC-72 [START_REF] Grigoriev | Evaluation of carbon-supported Pt and Pd nanoparticles for the hydrogen evolution reaction in PEM water electrolysers[END_REF][START_REF] Prabhuram | Synthesis and physical/electrochemical characterization of Pt/C nanocatalyst for polymer electrolyte fuel cells[END_REF] and black pearls 2000 1 (both from Cabot Corp.) and activated carbon material viz Nuchar carbon (from MWV corp.) with surface area 1400-1800 m 2 g -1 2 have been used as catalyst support. Recently, Andersen et al [START_REF] Ma Andersen | Durability of carbon nanofiber (CNF) & carbon nanotube (CNT) as catalyst support for Proton Exchange Membrane Fuel Cells[END_REF] have employed carbon nanofiber and carbon nanotube as catalyst support for PEM fuel cells. So finding conductive carbon support for electrocatalyst is an entirely new concept of research, which has not been reviewed that much elsewhere. Thus for our work we have planned to use hitherto unutilized and novel biomass waste namely grass to convert into active carbons for possible application as conductive support for electrocatalyst for water electrolysis for H 2 gas evolution. Our work therefore represents an essential, easy and innovative strategy to produce carbon powders from grass that may have electronic, scientific and industrial applications as conductive support for electrocatalysts for H 2 gas generation through electrolysis of water and the results have been presented in a simplified and systematic way. The work also stresses Green Energy from Waste concept, which is the want of the hour. It is to be stated that though there are hundreds of varieties of grasses exist comparison of properties of them serves another important and interesting theme of research, but right now it is not our intention. ____________ 1 www.cabot.com 2 http://www.meadwestvaco.com/mwv/groups/content/documents/document/mwv039306.pdf It may be interesting to the readers of this article for the fact that a database called Phyllis containing information on the composition of biomass and wastes is now available at http://www.ecn.nl/phyllis/ constructed at Energy Research Centre of the Netherlands. Phyllis enables making analysis data of individual biomass or waste materials available and offers the possibility to obtain the average composition of any combination of groups and/or subgroups.

Experimental

Preparation of grass derived activated biomass carbon (G-ABC)

A view of the freshly plucked turf grass bunch can be had from Fig. 1. Mature blades of turf grass bunches were collected from our Institute lawn, washed several times with hot distilled water to remove soil, dust and dirt and were dried under sun shade. The dried grass blades were shredded into small pieces and added to a solution of ZnCl 2 taken in the ratio of 1:1 w/w of biomass : ZnCl 2 . The contents were maintained at 60 0 C for 48 hours and finally heat treated at 250 0 C for 2 hours for charring.

The char was washed several times with doubly distilled water until all the ZnCl 2 is completely removed. Absence of Zn 2+ , Cl -, neutrality in pH and low conductivity of the washings ensures thorough washing of the sample. The powder was dried in oven and ground. The powder prepared in this way is called grass derived activated biomass carbon (G-ABC). Fig. 2 gives the methodology for producing G-ABC.

Preparation of 1% Pt on grass derived activated carbon powder (Pt@G-ABC)

Electrocatalyst powder was prepared by aqueous reduction using NaBH 4 as the reducing agent. To prepare 1% Pt@G-ABC powder, G-ABC powder is first made wet and homogenized with little amount of water and ethanol in a beaker. To this slurry appropriate amount of Pt(NH 3 ) 4 Cl 2 crystals in minimum quantity of water is added drop wise while stirring the contents slowly and thoroughly. Now large excess of NaBH 4 solution is added very slowly from a buret while ensuring constant mixing of the contents in the beaker. NaBH 4 reduces Pt 2+ ions to Pt 0 and gets deposited or precipitated over the biomass carbon particles. The beaker is left undisturbed overnight. Completion of reduction with NaBH 4 is known by testing an aliquot of the filtrate with KI solution. Absence of rose coloration with KI shows the complete reduction of Pt ions. The contents are now filtered and washed several times with distilled water until the washing is neutral in pH. The powder is dried and stored in an air-tight container. The above process is explained by the following equation [START_REF] Millet | Preparation of solid polymer electrolyte composites: investigation of the precipitation process[END_REF].

4[Pt(NH 3 ) 4 ] 2+ + NaBH 4 + 8OH - NaBO 2 + 4Pt o + 16NH 3 + 6H 2 O
The sequence of steps involved in the preparation of 1% Pt@G-ABC has been shown in Fig. 3.

Preparation of electrode for electrochemical studies

SS rods with circular ends of area 1cm 2 & 8cm length are employed for fabricating the electrodes. A typical catalyst ink with N-methyl 2 pyrrolidone was obtained by mixing together the BC powder or BC supported electro catalyst powder, commercial carbon powder and poly vinylidene fluoride binder in the % weight ratio 88:10:2 [START_REF] Kalyani | A new solution combustion route to synthesize LiCoO 2 and LiMn 2 O 4[END_REF] and was applied to the circular end of the SS rods.

The electrodes were dried at 80 0 C for 1hour. Heat shrinkable sleeve was used to mask rest of the electrode portion.

Physical characterization and electrochemical tests

Thermal degradation characteristics of the biomass refuse were studied using thermogravimetry. Experiments were performed on a TGA-50 Analyzer. 2mg of the sample was heated from room temperature to 450 o C at a ramp rate of 20 o Cmin -1 in air. Powder X-ray diffraction patterns were recorded between 10 • and 80 • on an X'Pert Pro X-ray diffractometer with CuK  radiation source. The ultimate analysis of the activated carbon was carried out using Vario ELIII CHNS/O Analyzer. Surface area of the G-ABC powder was determined by BET (Brunauer, Emmet and Teller) method using low temperature nitrogen adsorption (Quanta Chrome Nova 1000, US).

Surface morphology of the activated carbon was studied using S-3000H model microscope. Density of the activated carbon powder was estimated by Archimedes' principle using xylene [START_REF]Annual Book of ASTM Standards[END_REF].

Electro catalytic activity of the activated BC as well as the supported electro catalyst powder samples were assessed by performing liner sweep voltammetric and cyclic voltammetric studies (on Zahner electrochemical measurement unit; model No. IM6e) with the test cells assembled using SS rod loaded catalyst powder (or virgin carbon) as the working electrode, Saturated Calomel Electrode as the reference and a Pt wire (1mm diameter) as the counter electrode. The electrochemical measurements (linear sweep and cyclic voltammetry) made to evaluate the catalytic activity of the samples were carried out in de-aerated 1M H 2 SO 4 electrolyte. Electrode surfaces were first activated by cycling in the potential range of -0.2 to +1.1V vs. SCE, in order to obtain stable and reproducible voltammograms.

Results and Discussion

Burn-off

Conversion of grass biomass in to biomass carbon took place around 250 o C, also corroborated through TGA studies and the weight of the char was noted to calculate the yield (burn-off). Since the biomass was heated in a furnace a significant amount of carbon content might have been converted as CO 2 . Hence the yield is expected to be less and as expected the yield was only 46%. Higher yields could have been obtained if the samples were heated in an inert atmosphere.

Thermogravimetric (TG) Analysis

Thermal degradation characteristics of the grass sample (dried mass) were studied using thermogravimetry. Around 2mg of the sample was heated from room temperature to 400 o C at a heating rate of 10 o Cmin -1 under air atmosphere. The thermogram of the dried grass revealed that major decomposition occurred between 250-310 o C as shown in the Fig. 4. The weight loss around 52 % may be due to the escape of decomposition products like moisture, CO 2 , oxides of nitrogen and volatile organic compounds.

Ultimate analysis

Ultimate analysis report of the G-ABC sample shows 76.66 % C, 0.211% N, 0.011 % S & 1.253 % H and balance oxygen. Due to the preferential loss of H and O with heating, carbon concentration and degree of aromatisation may increase with pyrolysis. Significant % of N, S & H in the sample shows the presence of various organic functional groups. Fourier Transform Infra Red (FT-IR) data also bears support for these organic functional groups, the presence of which is expected to influence the electrochemical behavior of the carbon samples prepared.

Powder X-ray diffraction (PXRD) studies

X-ray diffraction patterns of the G-ABC and 1% Pt@G-ABC powders have been depicted in Fig. 5 and as an inset in Fig. 5. The appearance of a broad peak around 24 o in the XRD of the G-ABC indicates the presence of microporous carbon and the microporous structure is amorphous carbon in nature with non-crystalline structures [START_REF] Alcantara | NMR, and electrochemical studies of surface-modified carbon microbeads[END_REF]. More precisely, disordered single graphene layers and stacked structures of graphene sheets may be present simultaneously in the texture of the carbon powder [START_REF] Zhang | Microporous carbon derived from pinecone hull as anode material for lithium secondary batteries[END_REF] and the broad shape indicates highly disordered structure in the carbon [START_REF] Dahn | Dependence of the electrochemical intercalation of lithium in carbons on the crystal structure of the carbon[END_REF].

However the strong peaks in the middle of the humps suggest that an organized crystalline structure exists in the amorphous carbon structure of grass. The interplanar space (d 002 ) calculated for the virgin carbon is 4.03 Å, larger than that observed for graphite (3.354 Å) indicating considerable disorderliness in the carbon produced [START_REF] Kyotani | Formation of new type of porous carbon by carbonization in zeolite nanochannels[END_REF][START_REF] Cuesta | Comparative performance of X-ray diffraction and Raman microprobe techniques for the study of carbon materials[END_REF][START_REF] Wang | Characterizations of crystalline structure and electrical properties of pyrolyzed polyfurfuryl alcohol[END_REF]. Generally the value of d 002 is taken as a measure of estimating the degree of graphitization in the carbon and growing disorder is reflected in larger values of d 002 . Changes in the PXRD pattern of the Pt@G-ABC show the modification due to Pt particles on the grass. ( 111) & (200) peaks of Pt are observed (given as inset in Fig. 5) and it is a fact that the (002) peak of carbon is found to be suppressed here, revealing predominant and homogeneous existence of Pt particles over the entire carbon surface.

FT-IR vibrational studies

The electrochemical properties of activated carbon depend upon the physical properties as well as the nature and chemical reactivity of the functional groups present on the carbon surface.

Knowledge on surface functional groups would give insight to the electrochemical properties of the activated carbon. FT-IR data was collected for qualitative characterization of the surface functional groups of the activated carbon samples and is presented in Fig. 6. Various FT-IR signatures observed and respective assignment is given in Table 1. An analysis of the table 1 shows the presence of COOH, OH, nitro and C-H bonds on the surface of the activated carbon samples. These organic functionalities may help in the anchorage Pt particles throughout the carbon surface uniformly. Also these polar groups are expected to impart hydrophilicity to the electrode, paving way for the easy accessibility of the electrolyte in to the pores of the electrode particles, thus facilitating efficient electrolysis of water. Further, the absence of a peak around 3400cm -1 shows the evident absence of amino group. So the nitrogen present in the sample may probably due to nitro group. Subramanian et. al. [START_REF] Subramanian | Supercapacitors from Activated Carbon Derived from Banana Fibers[END_REF] have reported that the organic groups with oxygen, typically, phenols, carbonyls, lactones, quinine and quinine-like structures are expected to form on the surface during the thermal treatment of the biomass precursors and may appear at the edge carbon atoms. This fact may also be applied to grass samples and the effect or mechanism of action of these organics on the electroactivity/catalytic activity of the carbon samples may be complex and forms an exclusive research object. The presence of Pt over the carbon surface or the coordination of Pt with the organic functional groups can be confirmed only when FT-IR spectrum is recorded down to 300cm -1 , which is out of our reach as of now.

Scanning electron microscopic (SEM) studies, Surface area (S BET ) and density measurements

The SEM image of G-ABC is shown in the Fig. 7. It is observed that the carbon particles are of irregular size and ununiformly distributed. Also the particles appear as layers stacked or bundled together. The particles seem to lack porosity and hence it is not possible to offer any correlation between the particle morphology and the electrochemical activity as of now. Surface area of the G-ABC carbon sample was found to be 1201 m 2 g -1 . The surface area of G-ABC is observed to be higher than the commonly employed carbon support namely Vulcan XC-72 which has the value of around 250 m 2 g -1 [START_REF] Grigoriev | Evaluation of carbon-supported Pt and Pd nanoparticles for the hydrogen evolution reaction in PEM water electrolysers[END_REF]. High surface area may be indicative of the presence of enormous electrochemically accessible sites or area thereby resulting in increased catalytic activity to the Pt@G-ABC ultimately.

It is to be mentioned that surface functionalities would not be altered as a result of activating the sample and hence for these reasons the authors expect that the catalytic activity observed for the Pt@G-ABC sample may be due to the improved surface area.

Density of coconut, lignite, wood and coal activated carbon samples reported in the literature is in the range of 0.35 -0.48 gcc -1 3 while our G-ABC sample has density of 0.77 gcc -1 , a value higher than that of those seen above. It may convince the readers that the high density value might be the result of the presence of significant amount of O and N in our samples. But the notion that grass contains enormous cellulose fibers and hence carbon material obtained from the thermal treatment of fibrous precursor would be lighter, resulting in fibrous and porous carbon structure. Though this feature is not directly evident from SEM given in Fig. 7, it can still be presumed that the individual stack or bundle may be fibrous and porous based on the density criteria.

Further, higher density provides greater volume activity and normally indicates better quality activated carbon 4 . __________________ 3 http://www.carbochem.com/activatedcarbon101.html. 4 http://en.wikipedia.org/wiki/Activated_carbon.html.

Results of electrochemical or electrocatalytic characterization studies

Linear Sweep Voltammetric (LSV) studies

LSV study is undertaken to have an idea on the voltage at which H 2 gas evolution occurs from water. LSV plot of G-ABC & Pt@G-ABC electrodes are displayed in the Figs. 8 set. Voltage of the working electrode was swept from 0.0V to -0.4V Vs SCE at a scan rate of 20mVsec -1 . Fig. 8. LSV plot of (a) G-ABC & (b) 1% Pt@G-ABC electrodes in 1M H 2 SO 4 . Water decomposition setting in at -0.24V Vs SCE for 1% Pt@G-ABC is indicated in Fig. 8b and the rate of increase in current density is very much rapid with this electrocatalyst. For G-ABC no activity is observed since current density is comparatively less (Fig. 8a). The results suggest that the remarkable increase in the current density causes enhanced H 2 evolution (at lower voltages) when Pt@G-ABC catalyst is used.

Cyclic voltammetric (CV) studies

CV of the G-ABC & 1% Pt@G-ABC samples is presented respectively in Figs. 9a & b set.

CV was recorded between -0.4 to +1.0V at a sweep rate of 20mVsec -1 . LSV and CV offer almost the same results as far as our study is concerned. These experiments are valuable in letting us know the better performing biomass carbon sample(s) based electrocatalysts. The rate of change of 12 current density is taken as an index to measure the catalytic activity of the electrodes studied. No change in the current density and hence no electrochemical or catalytic activity with G-ABC (Fig. 9a) is observed while H 2 evolution is noticed around -0.2V Vs SCE in Pt@G-ABC (indicated as "**" in the Fig. 9b). Oxidation of organic moieties of Pt@G-ABC is also observed at positive potentials (indicated as "*" in Fig. 9b). A similar type of pattern of CV has been observed by Murakami et al [START_REF] Murakami | Preparation and characterization of an electrocatalytic electrode using amphiphilic carbonaceous material containing metal compound[END_REF] in their studies with perchloric acid electrolyte. Interestingly, rapid change in the current density is observed only in the Pt case. The improvement in the catalytic activity of Pt@G-ABC over G-ABC may be attributed to the physical nature and the high active surface area of the sample powders activated with ZnCl 2 . It can thus be regarded that the ZnCl 2 activated G-ABC powder may be useful as a conductive material for supporting electrocatalyst particles and undoubtedly, 1% Pt supported on activated carbon derived from grass blades emerge as one of the candidates of choice for H 2 gas evolution from acid electrolysis. This is established through various electrochemical studies with respect to electrocatalyzed H 2 gas generation by water electrolysis. This is considered as the prime novelty of our studies. It is to be stressed that commercial electrocatalysts contain 10% or higher Pt content supported on carbon and so the authors presume that 10% Pt@G-ABC would be definitely as good as the commercial ones or even better. Hence it is worth performing comparative studies with the commercial electrocatalysts supported on conducting carbon but has been reserved for the future.

Furthermore, an analysis of the cost of obtaining G-ABC and that of the most popular and commercially available Vulcan XC-72 and 10% Pt supported on Vulcan XC-72 both from Cabot Corp. is valid and has been presented here. The intention is that the findings of the cost analysis will influence the evolution of future research activities elsewhere involving grass or any other biomass for obtaining carbon supported catalysts. The cost of Vulcan XC-72 from Cabot Corp. is reported to be USD 20.00 per 250g and that of 10% Pt on Vulcan-XC-72 is USD 56.00 per gram 5 . Although G-ABC can be obtained from zero-cost biomass commercial success could be achieved only if electrode structures, pore volume, particle distribution and electrode stability during hydrogen generation in ____________ 5 www. fuelcellstore.com water electrolysers are optimized. However, our preliminary investigation suggests that G-ABC may be a better alternative to the traditional carbon supports in the near future.

The authors of the present article has extended similar type of studies with activated carbon derived from other biomass such as calotropis stem, palm leaves, coconut leaves etc. Since the physical features and chemical constituents influence the electrochemical or the catalytic properties we have diversified choice of sources of biomass carbon for utilizing as electrocatalyst conductive supports. Hence research may be oriented towards this area which could lead to carbon powders with unexpected properties tunable to the applications.

To summarize, we have described how biomass carbon powder from GREEN biomass waste namely GRASS can be produced and attempted to evaluate its potential as a conductive support for electrocatalysts for the electro-generation of H 2 gas from acidified water. Electrocatalyst powder samples are prepared using the thus produced biomass carbon supports with 1% Pt loading (Pt@G-ABC). Further applications of the biomass carbon supported electrocatalyst powder samples obtained through this work have also been highlighted.

Conclusion

The work shows how environmental wastes could be a useful source of obtaining novel engineering material like activated carbon or in other words, biomass carbon. In the present work grasses are considered as a safer, cheaper and greener way of utilizing them as a source of preparing activated carbon as well as conductive support for noble metal electrocatalysts. Even 1% Pt@G-ABC has been found to enhance the H 2 generation rate through electrolysis of acidified water remarkably. In our studies current density has been taken as the index of evaluating the catalytic activity of the samples. H 2 evolution from water catalyzed by 1% Pt@G-ABC was observed around -0.24V Vs SCE and the good performance of the same may be due to high % carbon content, favorable physical properties & uniform dispersion of Pt particles on G-ABC powder. Thus grass derived carbon could be an appropriate low-cost alternative to the conventional carbon supports for electrocatalysts for the renewable source of hydrogen gas. The developed electrocatalysts could be used in proton exchange membrane fuel cells as well and many other applications indicated in the previous section. The objective and the fundamental experimental results presented here would break through not only the limits of carbon sources but also the conventional idea of obtaining active carbon and then applying them into various technologies where carbon is vital.

FIGURE CAPTIONS

Fig. 1 .

 1 Fig. 1. A view of turf grass bunch.

Fig. 2 .

 2 Fig. 2. Flow sheet for the preparation of G-ABC.

Fig. 3 .

 3 Fig. 3. Flow sheet for preparing Pt particles supported on G-ABC (Pt@G-ABC).

Fig. 4 .

 4 Fig. 4. Thermogram of dried grass sample.

Fig. 5 .

 5 Fig. 5. Powder XRD of G-ABC sample. Inset: XRD of 1% Pt@G-ABC.

Fig. 6 .Fig. 7 .

 67 Fig. 6. FT-IR spectrum of G-ABC.

Fig. 8 .Fig. 9 .

 89 Fig. 8. LSV plot of (a) G-ABC & (b) 1% Pt@G-ABC electrodes in 1M H 2 SO 4 .

Fig. 1 .Fig. 2 .Fig. 3 .

 123 Fig. 1. A view of turf grass bunch.

Fig. 4 .

 4 Fig. 4. TG of dried grass sample. Fig. 4. TG of dried grass sample.

Fig. 5 .

 5 Fig. 5. Powder XRD of G-ABC sample. Inset: XRD of 1% Pt@G-ABC.

Fig. 6 .

 6 Fig. 6. FTIR spectrum of G-ABC.

Fig. 8 .Fig. 9 .

 89 Fig. 8. LSV plot of (a) G-ABC & (b) 1% Pt@G-ABC electrodes in 1M H 2 SO 4 .

TABLE CAPTIONS Table 1 .

 CAPTIONS1 FT-IR spectral data on G-ABC.

	20 21

Table 1

 1 FTIR spectral data on G-ABC.

	IR frequency (cm -1 )	Assignment
	3731	Free O -H groups
	2464	O -H stretch from strongly H-bonded -COOH group
	2913	O -H stretching of -COOH group
	1713	Free -C -O group stretching
	1562	Carboxylate anion stretching & NO 2 group
	1222	C -N stretching
	1377	C = N stretching
	1055	C -C stretching
	1498 & 1402	C -H bending

Acknowledgments

The authors thank The Management of Thiagarajar College of Engineering, Madurai and the experts at acknowledgment various R & D institutions for helping in instrumental analysis. The authors sincerely thank the reviewers for the critical evaluation of the MS.