Zoltán Ésik

Uli Fahrenberg

Axel Legay

Karin Quaas

Kleene Algebras and Semimodules for Energy Problems

With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce generalized energy automata. These are finite automata whose edges are labeled with energy functions that define how energy levels evolve during transitions. Uncovering a close connection between energy problems and reachability and Büchi acceptance for semiring-weighted automata, we show that these generalized energy problems are decidable. We also provide complexity results for important special cases.

Introduction

Energy and resource management problems are important in areas such as embedded systems or autonomous systems. They are concerned with the question whether a given system admits infinite schedules during which (1) certain tasks can be repeatedly accomplished and (2) the system never runs out of energy (or other specified resources). Starting with [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF], formal modeling and analysis of such problems has recently attracted some attention [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF][START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF][START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Degorre | Energy and mean-payoff games with imperfect information[END_REF][START_REF] Fahrenberg | Energy games in multiweighted automata[END_REF][START_REF] Quaas | On the interval-bound problem for weighted timed automata[END_REF].

As an example, the left part of Fig. 1 shows a simple model of an electric car, modeled as a weighted timed automaton [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF]. In the working state W , energy is consumed at a rate of 10 energy units per time unit; in the two recharging states R 1 , R 2 , the battery is charged at a rate of 20, respectively 10, energy units per time unit. As the clock c is reset (c ← 0) when entering state W and has guard c ≥ 1 on outgoing transitions, we ensure that the car always has to be in state W for at least one time unit. Similarly, the system can only transition back from states R 1 , R 2 to W if it has spent at most one time unit in these states.

Passing between states W and R 1 requires 4 energy units, while transitioning between W and R 2 , and between R 2 to R 1 , requires 2 energy units. Altogether, this is intended to model the fact that there are two recharge stations available, one close to work but less powerful, and a more powerful one further away. Now

The reserach of this author is supported by the European Union and co-funded by the European Social Fund. Project title: 'Telemedicine-focused research activities on the field of mathematics, informatics and medical sciences'. Project number: T ÁMOP-4.2.2.A-11/1/KONV-2012-0073

W -10 R1 +20 R2 +10 -4 c ≥ 1 c ← 0 -4 c ≤ 1 c ← 0 -2 c ≥ 1 c ← 0 -2 c ≤ 1 c ← 0 -2 -2 W R fWR fRW x → ∞ fWR(x) = undef. (x < 12)
x -12 (x ≥ 12) fRW(x) = 2x + 12 (x < 2)

x + 14 (x ≥ 2)

Fig. 1. Simple model of an electric car as a weighted timed automaton (left); the corresponding energy automaton (right) assume that the initial state W is entered with a given initial energy x 0 , then the energy problem of this model is as follows: Does there exist an infinite trace which (1) visits W infinitely often and (2) never has an energy level below 0? This type of energy problems for weighted timed automata is treated in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF], and using a reduction like in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF], our model can be transformed to the energy automaton in the right part of Fig. 1. (The reduction is quite complicated and only works for one-clock timed automata; see [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF] for details.) It can be shown that the energy problem for the original automaton is equivalent to the following problem in the energy automaton: Given an initial energy x 0 , and updating the energy according to the transition label whenever taking a transition, does there exist an infinite run which visits W infinitely often? Remark that the energy update on the transition from R to W is rather complex (in the general case of n recharge stations, the definition of f RW can have up to n branches), and that we need to impose a Büchi condition to enforce visiting W infinitely often.

In this paper we propose a generalization of the energy automata of [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF] which also encompasses most other approaches to energy problems. Abstracting the properties of the transition update functions in our example, we define a general notion of energy functions which specify how weights change from one system state to another. Noticing that our functional energy automata are semiringweighted automata in the sense of [START_REF] Droste | Handbook of Weighted Automata[END_REF], we uncover a close connection between energy problems and reachability and Büchi problems for weighted automata. More precisely, we show that one-dimensional energy problems can be naturally solved using matrix operations in semirings and semimodules [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF][START_REF] Droste | Handbook of Weighted Automata[END_REF][START_REF] Ésik | An algebraic generalization of omega-regular languages[END_REF][START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF].

For reachability, we use only standard results [START_REF] Droste | Handbook of Weighted Automata[END_REF], but for Büchi acceptance we have to extend previous work [START_REF] Ésik | An algebraic generalization of omega-regular languages[END_REF][START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF] as our semiring is not complete. We thus show that reachability and Büchi acceptance are decidable for energy automata. For the class of piecewise affine energy functions, which generalize the functions of Fig. 1 and are important in applications, they are decidable in exponential time.

Structure of the Paper. We introduce our general model of energy automata in Section 2. In Section 3 we show that the set of energy functions forms a star-continuous Kleene algebra, a fact which allows us to give an elegant char-acterization of reachability in energy automata. We also expose a structure of Conway semiring-semimodule pair over energy functions which permits to characterize Büchi acceptance. In Section 4 we use these characterizations to prove that reachability and Büchi acceptance are decidable for energy automata. We also show that this result is applicable to most of the above-mentioned examples and give complexity bounds. To put our results in perspective, we generalize energy automata along several axes in Section 5 and analyze these generalized reachability and Büchi acceptance problems. Owing to space limitations, most of the proofs had to be omitted from this paper; these can be found in the extended version [START_REF] Ésik | Kleene algebras and semimodules for energy problems[END_REF]. Related Work. A simple class of energy automata is the one of integer-weighted automata, where all energy functions are updates of the form x → x + k for some (positive or negative) integer k. Energy problems on these automata, and their extensions to multiple weights (also called vector addition systems with states (VASS)) and games, have been considered e.g. in [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF][START_REF] Chan | The boundedness problem for three-dimensional vector addition systems with states[END_REF][START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Chatterjee | Generalized meanpayoff and energy games[END_REF][START_REF] Fahrenberg | Energy games in multiweighted automata[END_REF]. Our energy automata may hence be considered as a generalization of one-dimensional VASS to arbitrary updates; in the final section of this paper we will also be concerned with multi-dimensional energy automata and games.

Energy problems on timed automata [START_REF] Alur | A theory of timed automata[END_REF] have been considered in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF][START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Bouyer | Lower-bound constrained runs in weighted timed automata[END_REF][START_REF] Quaas | On the interval-bound problem for weighted timed automata[END_REF].

Here timed automata are enriched with integer weights in locations and on transitions (the weighted timed automata of [START_REF] Alur | Optimal paths in weighted timed automata[END_REF][START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF], cf. Fig. 1), with the semantics that the weight of a delay in a location is computed by multiplying the length of the delay by the location weight. In [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF] it is shown that energy problems for oneclock weighted timed automata without updates on transitions (hence only with weights in locations) can be reduced to energy problems on integer-weighted automata with additive updates.

For one-clock weighted timed automata with transition updates, energy problems are shown decidable in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF], using a reduction to energy automata as we use them here. More precisely, each path in the timed automaton in which the clock is not reset is converted to an edge in an energy automaton, labeled with a piecewise affine energy function (cf. Definition 4). Decidability of the energy problem is then shown using ad-hoc arguments, but can easily be inferred from our general results in the present paper.

Also another class of energy problems on weighted timed automata is considered in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF], in which weights during delays are increasing exponentially rather than linearly. These are shown decidable using a reduction to energy automata with piecewise polynomial energy functions; again our present framework applies.

We also remark that semigroups acting on a set, or more generally, semiringsemimodule pairs, have been used to describe the infinitary behavior of automata for a long time, see [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF][START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF][START_REF] Wilke | An Eilenberg theorem for infinity-languages[END_REF]. In this framework, the infinitary product or omega operation is defined on the semiring and takes its values in the semimodule. Another approach is studied e.g. in [START_REF] Mathieu | Verification of pushdown systems using omega algebra with domain[END_REF], where the omega operation maps the semiring into itself. It seems to the authors that there is no reasonable definition of an infinitary product or omega operation on energy functions that would again result in an energy function, hence we chose to use the framework of semiringsemimodule pairs.

x → x + 2; x ≥ 2 x → x + 3; x > 1 x → 2x -2; x ≥ 1 x → x -1; x > 1 x → x + 1; x ≥ 0

Energy Automata

The transition labels on the energy automata which we consider in the paper, will be functions which model transformations of energy levels between system states. Such transformations have the (natural) properties that below a certain energy level, the transition might be disabled (not enough energy is available to perform the transition), and an increase in input energy always yields at least the same increase in output energy. Thus the following definition.

Definition 1. An energy function is a partial function f : R ≥0 - → R ≥0 which is defined on a closed interval [l f , ∞[ or on an open interval ]l f , ∞[,
for some lower bound l f ≥ 0, and such that for all x 1 ≤ x 2 for which f is defined,

f (x 2 ) ≥ f (x 1 ) + x 2 -x 1 . ( * )
The class of all energy functions is denoted by F.

Thus energy functions are strictly increasing, and in points where they are differentiable, the derivative is at least 1. 4 The inverse functions to energy functions exist, but are generally not energy functions. Energy functions can be composed, where it is understood that for a composition g • f (to be read from right to left), the interval of definition is {x ∈ R ≥0 | f (x) and g(f (x)) defined}.

We will generally omit the symbol • and write composition simply as gf . Definition 2. An energy automaton (S, T ) consists of finite sets S of states and T ⊆ S × F × S of transitions labeled with energy functions.

We show an example of a simple energy automaton in Fig. 2. Here we use inequalities to give the definition intervals of energy functions.

A finite path in an energy automaton is a finite sequence of transitions

π = (s 0 , f 1 , s 1 ), (s 1 , f 2 , s 2 ), . . . , (s n-1 , f n , s n ). We use f π to denote the combined energy function f n • • • f 2 f 1 of
such a finite path. We will also use infinite paths, but note that these generally do not allow for combined energy functions.

A global state of an energy automaton is a pair q = (s, x) with s ∈ S and x ∈ R ≥0 . A transition between global states is of the form ((s, x), f, (s , x )) such that (s, f, s ) ∈ T and x = f (x). A (finite or infinite) run of (S, T ) is a path in the graph of global states and transitions.

We are ready to state the decision problems with which our main concern will lie. As the input to a decision problem must be in some way finitely representable, we will state them for subclasses F ⊆ F of computable energy functions; an Fautomaton is an energy automaton (S, T ) with T ⊆ S × F × S.

Problem 1 (Reachability). Given a subset F of computable functions, an Fautomaton (S, T ), an initial state s 0 ∈ S, a set of accepting states F ⊆ S, and a computable initial energy x 0 ∈ R ≥0 : does there exist a finite run of (S, T ) from (s 0 , x 0 ) which ends in a state in F ? Problem 2 (Büchi acceptance). Given a subset F of computable functions, an F -automaton (S, T ), an initial state s 0 ∈ S, a set of accepting states F ⊆ S, and a computable initial energy x 0 ∈ R ≥0 : does there exist an infinite run of (S, T ) from (s 0 , x 0 ) which visits F infinitely often?

As customary, a run such as in the statements above is said to be accepting. We let Reach F denote the function which maps an F -automaton together with an initial state, a set of final states, and an initial energy to the Boolean values ff or tt depending on whether the answer to the concrete reachability problem is negative or positive. Büchi F denotes the similar mapping for Büchi problems.

The special case of Problem 2 with F = S is the question whether there exists an infinite run in the given energy automaton. This is what is usually referred to as energy problems in the literature; our extension to general Büchi conditions has not been treated before.

The Algebra of Energy Functions

In this section we develop an algebraic framework of star-continuous Kleene algebra around energy functions which will allow us to solve reachability and Büchi acceptance problems in a generic way. Let [0, ∞] ⊥ = {⊥} ∪ [0, ∞] denote the non-negative real numbers together with extra elements ⊥, ∞, with the standard order on R ≥0 extended by

⊥ < x < ∞ for all x ∈ R ≥0 . Also, ⊥ + x = ⊥ -x = ⊥ for all x ∈ R ≥0 ∪ {∞} and ∞ + x = ∞ -x for all x ∈ R ≥0 . Definition 3. An extended energy function is a mapping f : [0, ∞] ⊥ - → [0, ∞] ⊥ , for which f (⊥) = ⊥ and f (x 2 ) ≥ f (x 1 ) + x 2 -x 1 for all x 1 ≤ x 2 , as in ( * ). Moreover, f (∞) = ∞, unless f (x) = ⊥ for all x ∈ [0, ∞] ⊥ .
The class of all extended energy functions is denoted E. This means, in particular, that f (x) = ⊥ implies f (x ) = ⊥ for all x ≤ x, and f (x) = ∞ implies f (x ) = ∞ for all x ≥ x. Hence, except for the extension to ∞, these functions are indeed the same as our energy functions from the previous section. Composition of extended energy functions is defined as before, but needs no more special consideration about its definition interval.

We also define an ordering on E, by f ≤ g iff f (x) ≤ g(x) for all x ∈ [0, ∞] ⊥ . We will need three special energy functions, ⊥, id and ; these are given by

⊥(x) = ⊥, id(x) = x for x ∈ [0, ∞] ⊥ , and (⊥) = ⊥, (x) = ∞ for x ∈ [0, ∞].
Lemma 1. With the ordering ≤, E is a complete lattice with bottom element ⊥ and top element . The supremum on E is pointwise, i.e. (sup

i∈I f i )(x) = sup i∈I f i (x) for any set I, all f i ∈ E and x ∈ [0, ∞] ⊥ . Also, (sup i∈I f i )h = sup i∈I (f i h) for all h ∈ E.
We denote binary suprema using the symbol ∨;

hence f ∨ g, for f, g ∈ E, is the function (f ∨ g)(x) = max(f (x), g(x)).
Lemma 2. (E, ∨, •, ⊥, id) is an idempotent semiring with natural order ≤.

Recall [START_REF] Droste | Handbook of Weighted Automata[END_REF] that ≤ being natural refers to the fact that f ≤ g iff f ∨ g = g. For iterating energy functions, we define a unary star operation on E by

f * (x) = x if f (x) ≤ x , ∞ if f (x) > x .
Lemma 3. For any f ∈ E, we have f * ∈ E. Also, for any g ∈ E, there exists

f ∈ E such that g = f * if, and only if, there is k ∈ [0, ∞] ⊥ such that g(x) = x for all x < k, g(x) = ∞ for all x > k, and g(k) = k or g(k) = ∞.
By Lemma 1, composition right-distributes over arbitrary suprema in E. The following example shows that a similar left distributivity does not hold in general, hence E is not a complete semiring the sense of [START_REF] Droste | Handbook of Weighted Automata[END_REF]. Let f n , g ∈ E be defined by

f n (x) = x+1-1 n for x ≥ 0, n ∈ N + and g(x) = x for x ≥ 1. Then g(sup n f n )(0) = g(sup n f n (0)) = g(1) = 1, whereas (sup n gf n )(0) = sup n g(f n (0)) = sup n g(1 - 1 n ) = ⊥.
The next lemma shows a restricted form of left distributivity which holds only for function powers f n . Note that it implies that f * = sup n f n for all f ∈ E, which justifies the definition of f * above. Lemma 4. For any f, g ∈ E, gf * = sup n∈N (gf n ).

Proposition 1. For any f, g, h ∈ E, gf * h = sup n∈N (gf n h). Hence E is a starcontinuous Kleene algebra [START_REF] Kozen | On Kleene algebras and closed semirings[END_REF].

We call a subsemiring E ⊆ E a subalgebra if f * ∈ E for all f ∈ E . It is known [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF][START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Droste | Handbook of Weighted Automata[END_REF][START_REF] Kozen | A completeness theorem for kleene algebras and the algebra of regular events[END_REF] that when S is a star-continuous Kleene algebra, then so is any matrix semiring S n×n , for all n ≥ 1, with the usual sum and product operations. The natural order on S n×n is pointwise, so that for all n × n matrices A, B over S, A ≤ B iff A i,j ≤ B i,j for all i, j. Now a star-continuous Kleene algebra is also a Conway semiring, hence the Conway identities

(g ∨ f ) * = (g * f ) * g * and (gf ) * = g(f g) * f ∨ id (1)
are satisfied for all f, g ∈ E. Also, this implies that the matrix semiring E n×n is again a Conway semiring, for any n ≥ 1, with the star operation defined inductively for a matrix

M = a b c d ∈ E n×n , ( 2
)
where

a is k × k and d is m × m with k + m = n, by M * = (a ∨ bd * c) * (a ∨ bd * c) * bd * (d ∨ ca * b) * ca * (d ∨ ca * b) * ∈ E n×n . (3)
The definition of M * does not depend on how M is split into parts, and starcontinuity implies that for all matrices M, N, O,

N M * O = sup n∈N (N M n O) . (4)
Note again that this implies that M * = sup n M n for all matrices M . In a sense, this gives another, inductive definition of the star operation on the matrix semiring; the important property of star-continuous Kleene algebras is, then, that this inductive definition and the one in (3) give rise to the same operation.

We introduce a semimodule V over E. Let B = {ff , tt} be the Boolean algebra, with order ff < tt, and

V = {u : [0, ∞] ⊥ - → B | u(⊥) = ff , x 1 ≤ x 2 ⇒ u(x 1 ) ≤ u(x 2 )}.
Identifying ff with ⊥ and tt with ∞, we have an embedding of V into E; note that ⊥, ∈ V. [START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF]. Moreover, (sup i∈I u i )f = sup i∈I (u i f ) for any set I, all u i ∈ V and f ∈ E, and uf * = sup n∈N uf n for all u ∈ V.

Lemma 5. With action (u, f ) → uf : V×E -→ V, V is a right E-semimodule
So like the situation for E (cf. Lemmas 1 and 4), the action of E on V rightdistributes over arbitrary suprema and left-distributes over function powers.

We define an infinitary product operation E ω -→ V. Let f 0 , f 1 , . . . be an infinite sequence of energy functions and x 0 ∈ [0, ∞] ⊥ , and put

x n+1 = f n (x n ) for n ∈ N. Then we define ∞ i=0 f i )(x 0 ) = ff if ∃n ∈ N : x n = ⊥ , tt if ∀n ∈ N : x n = ⊥ .
Note that this product is order-preserving. By the next lemma, it is a conservative extension of the finite product. As E is not a complete semiring, it follows that (E, V) is not a complete semiring-semimodule pair in the sense of [START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF].

Lemma 6. For all f 0 , f 1 , . . . ∈ E, ( ∞ i=1 f i )f 0 = ∞ i=0 f i . For all indices 0 = n 0 ≤ n 1 ≤ . . . , ∞ i=0 f i = ∞ i=0 (f ni+1-1 • • • f ni ).
To deal with infinite iterations of energy functions, we define a unary omega operation E -→ V by

f ω (x) = ff if x = ⊥ or f (x) < x , tt if x = ⊥ and f (x) ≥ x . Note that f ω = ∞ i=0 f for all f ∈ E.
Proposition 2. (E, V) is a Conway semiring-semimodule pair.

Recall [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF] that this means that additionally to the identities (1),

(gf ) ω = (f g) ω f and (f ∨ g) ω = f ω (gf * ) * ∨ (gf * ) ω
for all f, g ∈ E. Like for Conway semirings, it implies that the pair (E n×n , V n ) is again a Conway semiring-semimodule pair, for any n ≥ 1, with the action of E n×n on V n similar to matrix-vector multiplication using the action of E on V, and the omega operation E n×n -→ V n given inductively as follows: for M ∈ E n×n with blocks as in ( 2), define

M ω = (a ∨ bd * c) ω ∨ d ω c(a ∨ bd * c) * (d ∨ ca * b) ω ∨ a ω b(d ∨ ca * b) * , (5)
M ω k = (a ∨ bd * c) ω (a ∨ bd * c) ω bd * .
The definition of M ω does not depend on how M is split into parts, but the one of M ω k does (recall that a is a k × k matrix). It can be shown [START_REF] Bloom | Iteration Theories: The Equational Logic of Iterative Processes[END_REF] that (5), and also (3), follow directly from certain general properties of fixed point operations.

Decidability

We are now ready to apply the Kleene algebra framework to reachability and Büchi acceptance for energy automata. We first show that it is sufficient to consider energy automata (S, T ) with precisely one transition (s, f, s ) ∈ T for each pair of states s, s ∈ S. This will allow us to consider T as a matrix S×S -→ E (as is standard in weighted-automata theory [START_REF] Droste | Handbook of Weighted Automata[END_REF]). Lemma 7. Let E ⊆ E be a subalgebra and (S, T ) an E -automaton. There exists an E -automaton (S, T ) for which Reach E (S, T ) = Reach E (S, T ) and Büchi E (S, T ) = Büchi E (S, T ), and in which there is precisely one transition (s, f, s ) ∈ T for all s, s ∈ S.

Hence we may, without loss of generality, view the transitions T of an energy automaton as a matrix T : S ×S -→ E. We can also let S = {1, . . . , n} and assume that the set of accepting states is F = {1, . . . , k} for k ≤ n. Further, we can represent an initial state s 0 ∈ S by the s 0 th unit (column) vector I s0 ∈ {⊥, id} n , defined by I s0 i = id iff i = s 0 , and F by the (column) vector F ≤k ∈ {⊥, id} n given by F ≤k i = id iff i ≤ k. Note that T ∈ E n×n is an n × n-matrix of energy functions; as composition of energy functions is written right-to-left, T ij ∈ E is the function on the transition from s j to s i . Theorem 1. Let E ⊆ E be a subalgebra. For any E -automaton (S, T ) with S = {1, . . . , n}, F = {1, . . . , k}, k ≤ n, s 0 ≤ n, and x 0 ∈ R ≥0 , we have Reach E (S, T )(F, s 0 , x 0 ) = tt if, and only if, t F ≤k T * I s0 (x 0 ) = ⊥.

Proof. Here t F ≤k denotes the transpose of F ≤k . By (4), we have t F ≤k T * I s0 = sup n ( t F ≤k T n I s0 ), so that t F ≤k T * I s0 (x 0 ) = ⊥ iff t F ≤k T n I s0 (x 0 ) = ⊥ for some n ∈ N, i.e. iff there is a finite run from (s 0 , x 0 ) which ends in a state in F . Referring back to the example automaton (S, T ) from Fig. 2, we display in Fig. 3 the automaton with transition matrix T * . Theorem 2. Let E ⊆ E be a subalgebra. For any E -automaton (S, T ) with S = {1, . . . , n}, F = {1, . . . , k}, k ≤ n, s 0 ≤ n, and x 0 ∈ R ≥0 , we have

f11 f12 f13 f22 f23 f32 f33 f11(x) = x; x ≥ 0 f12(x) = ∞; x > 1 f22(x) = x; x ≤ 2 ∞; x > 2 f23(x) = x -1; 1 < x ≤ 2 ∞; x > 2 f32(x) = x + 1; x ≤ 1 ∞; x > 1 f33(x) = x; x ≤ 1 ∞; x > 1 f13(x) = ∞; x > 1
Büchi E (S, T )(F, s 0 , x 0 ) = T ω k I s0 (x 0 ).
Proof. This is a standard result for complete semiring-semimodule pairs, cf. [START_REF] Ésik | A semiring-semimodule generalization of ω-regular languages, Parts 1 and 2[END_REF]. Now (E, V) is not complete, but the properties developed in the previous section allow us to show the result nevertheless. We need to see that for all M ∈ E n×n and 1 ≤ i ≤ n,

(M ω ) i = sup{• • • M k3,k2 M k2,k1 M k1,i : 1 ≤ k 1 , k 2 , . . . ≤ n} ,
which we shall deduce inductively from [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF].

Let a ∈ E × , d ∈ E m×m , for + m = n, and let i ∈ {1, . . . , }. Then the ith component of M ω is the ith component of (a ∨ bd * c) ω ∨ d ω c(a ∨ bd * c) * . By induction hypothesis, the ith component of (a ∨ bd * c) ω is the supremum of all infinite products (• • • M k2,k1 M k1,i ) such that 1 ≤ k j ≤ m for an infinite number of indices j, and similarly, the ith component of d ω c(a∨bd * c) * is the supremum of all infinite products (• • • M k2,k1 M k1,i ) such that 1 ≤ k j ≤ m for a finite number of indices j. Thus, the ith component of (a

∨ bd * c) ω ∨ d ω c(a ∨ bd * c) * is the supremum of all infinite products (• • • M k2,k1 M k1,i ).
We remark that our decision algorithms are static in the sense that the matrix expressions can be pre-computed and then re-used to decide reachability and Büchi acceptance for different values x 0 of initial energies.

Using elementary reasoning on infinite paths, we can provide an alternative characterization of Büchi acceptance which does not use the omega operations: Theorem 3. Let E ⊆ E be a subalgebra. For any E -automaton (S, T ) with S = {1, . . . , n}, F = {1, . . . , k}, k ≤ n, s 0 ≤ n, and x 0 ∈ R ≥0 , we have Büchi E (S, T )(F, s 0 , x 0 ) = tt if, and only if, there exists j ≤ k for which

t I j T T * I j t I j T * I s0 (x 0 ) ≥ t I j T * I s0 (x 0 ) = ⊥.
Corollary 1. For subalgebras E ⊆ E of computable functions in which it is decidable for each f ∈ E whether f (x) ≤ x, Problems 1 and 2 are decidable. For an energy automaton with n states and m transitions, the decision procedures use O(m + n 3 ), respectively O(m + n 4 ), algebra operations.

Proof. Maxima and compositions of computable functions are again computable, and if it is decidable for each f ∈ E whether f (x) ≤ x, then also f * is computable for each f ∈ E . Hence all matrix operations used in Lemma 7 and Theorems 1 and 3 are computable. The number of operations necessary in the construction in the proof of Lemma 7 is O(m), and, using e.g. the Floyd-Warshall algorithm to compute T * , O(n 3 ) operations are necessary to compute t I ≤k T * I s0 .

We proceed to identify two important subclasses of computable energy functions, which cover most of the related work mentioned in the introduction, and to give complexity results on their reachability and Büchi acceptance problems.

The integer update functions in E are the functions f k , for k ∈ Z, given by

f k (x) = x + k if x ≥ max(0, -k) , ⊥ otherwise ,
together with f ∞ := . These are the update functions usually considered in integer-weighted automata and VASS [START_REF] Bouyer | Infinite runs in weighted timed automata with energy constraints[END_REF][START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF][START_REF] Chaloupka | Z-reachability problem for games on 2-dimensional vector addition systems with states is in P[END_REF][START_REF] Chan | The boundedness problem for three-dimensional vector addition systems with states[END_REF][START_REF] Chatterjee | Energy parity games[END_REF][START_REF] Chatterjee | Generalized meanpayoff and energy games[END_REF][START_REF] Fahrenberg | Energy games in multiweighted automata[END_REF]. We have f f k = f k+ and

f k ∨ f = f max(k, ) , and f * k = f 0 for k ≤ 0 and f * k = f ∞ for k > 0, whence the class E int of integer update functions forms a subalgebra of E. A function f k ∈ E int
can be represented by the integer k, and algebra operations can then be performed in constant time. Hence Corollary 1 implies the following result. Theorem 4. For E int -automata, Problems 1 and 2 are decidable in PTIME.

Next we turn our attention to piecewise affine functions as used in Fig. 1.

Definition 4. A function f ∈ E is said to be (rational) piecewise affine if there exist x 0 < x 1 < • • • < x k ∈ Q such that f (x) = ⊥ iff x ≥ x 0 or x > x 0 , f (x j ) ∈ Q ∪ {⊥} for all j, and all restrictions f ]xj ,xj+1[ and f ]x k ,∞[ are affine functions x → a j x + b j with a j , b j ∈ Q, a j ≥ 1.
Note that the definition does not make any assertion about continuity at the x j , but ( * ) implies that lim x xj f (x) ≤ f (x j ) ≤ lim x xj f (x). A piecewise affine function as above can be represented by its break points x 0 , . . . , x k , the values f (x 0 ), . . . , f (x k ), and the numbers a 0 , b 0 , . . . , a k , b k . These functions arise in the reduction used in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF] to show decidability of energy problems for one-clock timed automata with transition updates. The notion of integer piecewise affine functions is defined similarly, with all occurrences of Q above replaced by Z.

Fig. 4 shows an example of a piecewise affine function.

The class E pw of piecewise affine energy functions forms a subsemiring of E: if f, g ∈ E pw with break points x 0 , . . . , x k , y 0 , . . . , y , respectively, then f ∨ g is piecewise affine with break points a subset of {x 0 , . . . , x k , y 0 , . . . , y }, and gf is piecewise affine with break points a subset of {x 0 , . . . , x k , f -1 (y 0 ), . . . , f -1 (y )}.

f (x) =                    .5 (x = 2) 1.5 x -2.5 (2 < x < 3) 2.3 (x = 3) x -.3 (3 < x < 4.5) 4.5 (x = 4.5) 2 x -4.5 (x > 4.5)
Fig. 4. A piecewise affine energy function

Let, for any k ∈ Q, g - k , g + k : [0, ∞] ⊥ - → [0, ∞] ⊥ be the functions defined by g - k (x) = x for x < k , ∞ for x ≥ k , g + k (x) = x for x ≤ k , ∞ for x > k .
By Lemma 3 (and noticing that for all f ∈ E pw , sup{x | f (x) ≤ x} is rational), E pw completed with the functions g - k , g + k forms a subalgebra of E. Remark that, unlike E pw , the class E pwi of integer piecewise affine functions does not form a subsemiring of E, as composites of E pwi -functions are not necessarily integer piecewise affine. As an example, for the functions f, g ∈ E pwi given by

f (x) = 2x , g(x) = x + 1; x < 3 , x + 2; x ≥ 3 , we have g(f (x)) = 2x + 1; x < 1.5 , 2x + 2; x ≥ 1.5 .
which is not integer piecewise affine. Similarly, the class of rational affine functions x → ax + b (without break points) is not closed under maximum, and E pw is the semiring generated by rational affine functions.

Theorem 5. For E pw -automata, Problems 1 and 2 are decidable in EXPTIME.

Proof. We need to show that it is decidable for each f ∈ E pw whether f (x) ≤ x.

Let thus f be a piecewise affine function, with representation (x 0 , . . . , x k , f (x 0 ), . . . , f (x k ), a 0 , . . . , a k , b 0 , . . . , b k ). If x < x 0 , then f (x) = ⊥ ≤ x. If x = x j for some j, we can simply compare x j with f (x j ).

(-1, 1) (0, -2) Fig. 5. A simple two-dimensional VASS Assume now that x ∈ ]x j , x j+1 [ for some j. If a j x j +b j ≤ x j and a j x j+1 +b j ≤ x j+1 , then also f (x) ≤ x by ( * ). Likewise, if a j x j + b j > x j and a j x j+1 + b j > x j+1 , then also f (x) > x. The case a j x j + b j > x j , a j x j+1 + b j ≤ x j+1 cannot occur because of ( * ), and if a j x j + b j ≤ x j and a j x j+1 + b j > x j+1 , then a j > 1, and f (x) ≤ x iff x ≤ bj 1-aj . For the case x ∈ ]x k , ∞[, the arguments are similar: if

a k x k + b k > x k , then also f (x) > x; if a k x k + b k ≤ x k and a k = 1, then also f (x) ≤ x, and if a k > 1 in this case, then f (x) ≤ x iff x ≤ b k
1-a k . Using Corollary 1, we have hence shown decidability. For the complexity claim, we note that all algebra operations in E pw can be performed in time linear in the size of the representations of the involved functions. However, the maximum and composition operations may double the size of the representations, hence our procedure may take time O(2 m+n 3 p) for reachability, and O(2 m+n 4 p) for Büchi acceptance, for an E pw -automaton with n states, m transitions, and energy functions of representation length at most p.

In the setting of E pw -automata and their application to one-clock weighted timed automata with transition updates, our Theorem 3 is a generalization of [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF]Lemmas 24,[START_REF] Kozen | A completeness theorem for kleene algebras and the algebra of regular events[END_REF]. Complexity of the decision procedure was left open in [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF]; as the conversion of a one-clock weighted timed automaton to an E pw -automaton incurs an exponential blowup, we now see that their procedure is doubly-exponential.

Considerations similar to the above show that also the setting of piecewise polynomial energy functions allows an application of Theorem 3 to show energy problems on the exponentially weighted timed automata from [START_REF] Bouyer | Timed automata with observers under energy constraints[END_REF] decidable.

Multi-dimensional Energy Automata and Games

Next we turn our attention to several variants of energy automata. We will generally stick to the set E pwi of integer piecewise affine energy functions; the fact that E pwi is not a subsemiring of E will not bother us here.

An n-dimensional integer piecewise affine energy automaton, or E n pwi -automaton for short, (S, T ), for n ∈ N + , consists of finite sets S of states and T ⊆ S × E n pwi × S of transitions. A global state in such an automaton is a pair (s, x) ∈ S × N n , and transitions are of the form (s, x) f -→ (s , x ) such that (s, f , s ) ∈ T and x (i) = f (i)(x(i)) for each i ∈ {1, . . . , n}.

For reachability in E n pwi -automata (with n ≥ 2), our algebraic results do not apply. To see this, we refer to the reachability problem in Fig. 5: with initial energy (1, 1), the loop needs to be taken precisely once, but with initial energy (2, 0), one needs to loop twice. Hence there is no static algorithm which can decide reachability for this VASS.

However, we remark that E n pwi -automata are well-structured transition systems [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], with ordering on global states defined by (s, x) (s , x ) iff s = s and x(i) ≤ x (i) for each i = 1, . . . , n (here we also have to assume x 0 ∈ N).

Also, the reachability problem for energy automata is a control state reachability problem in the sense of [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF]. Decidability of the reachability problem for E n pwi -automata thus follows from the decidability of the control state reachability problem for well-structured transition systems [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF]. Note that Büchi acceptance is not generally decidable for well-structured transition systems (it is undecidable for lossy counter machines [START_REF] Schnoebelen | Lossy counter machines decidability cheat sheet[END_REF]), so our reduction proof does not imply a similar result for Büchi acceptance. Theorem 6. The reachability problem for E n pwi -automata with x 0 ∈ N is decidable.

Next we show that if the requirement ( * ) on energy functions, that f (x 2 ) ≥ f (x 1 ) + x 2 -x 1 for each x 1 ≤ x 2 , is lifted, then reachability becomes undecidable from dimension 4. We call such functions flat energy functions; remark that we still require them to be strictly increasing, but the derivative, where it exists, may be less than 1. The class of all flat energy functions is denoted Ē and its restrictions by Ēpw , Ēpwi .

Theorem 7. The reachability problem for Ē4

pw -automata is undecidable.

Next we extend our energy automata formalism to (turn based) reachability games. Let (S, T ) be an n-dimensional energy automaton such that S = S A ∪ S B forms a partition of S and T ⊆ (S A × E n pwi × S B ) ∪ (S B × E n pwi × S A ). Then (S, S A , S B , T ) induces an n-dimensional energy game G. The intuition of the reachability game is that the two players A and B take turns to move along the game graph (S, T ), updating energy values at each turn. The goal of player A is to reach a state in F , the goal of player B is to prevent this from happening.

The reachability game is a coverability game in the sense of [START_REF] Raskin | Games for counting abstractions[END_REF]. In general, the reachability game on well-structured transition systems is undecidable [START_REF] Abdulla | Monotonic and downward closed games[END_REF]. Indeed, the games on VASS considered in [START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF] are a special case of reachability games on energy automata with integer update functions; their undecidability is shown in [START_REF] Abdulla | Monotonic and downward closed games[END_REF][START_REF] Brázdil | Reachability games on extended vector addition systems with states[END_REF]. It is hence clear that it is undecidable whether player A wins the reachability game in 2-dimensional E int -automata. As a corollary, we can show that for flat energy functions, already one-dimensional reachability games are undecidable.

Theorem 8. Whether player A wins the reachability game in E 2 int -automata is undecidable.

Theorem 9. It is undecidable for Ēpw -automata whether player A wins the reachability game.

Proof (sketch). The proof is by reduction from reachability games on 2-dimensional E int -automata to reachability games on 1-dimensional Ēpwi -automata. The intuition is that the new energy variable x encodes the two old ones as x = 2 x1 3 x2 , and then transitions in the 2-dimensional game are encoded using gadgets in which the other player may interrupt to demand proof that the required inequalities for x 1 and x 2 were satisfied. The energy functions in the so-constructed 1-dimensional automaton are piecewise affine because the original ones were integer updates. The details of the proof are in [START_REF] Ésik | Kleene algebras and semimodules for energy problems[END_REF].

Conclusion

We have in this paper introduced a functional framework for modeling and analyzing energy problems. We have seen that our framework encompasses most existing formal approaches to energy problems, and that it allows an application of the theory of automata over semirings and semimodules to solve reachability and Büchi acceptance problems in a generic way. For the important class of piecewise affine energy functions, we have shown that reachability and Büchi acceptance are PSPACE-hard and decidable in EXPTIME. As our algorithm is static, computations do not have to be repeated in case the initial energy changes. Also, decidability of Büchi acceptance implies that LTL model checking is decidable for energy automata.

In the last part of this paper, we have seen that one quickly comes into trouble with undecidability if the class of energy functions is extended or if twoplayer games are considered. This can be remedied by considering approximate solutions instead, using notions of distances for energy automata akin to the ones in [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF] to provide quantitative measures for similar energy behavior.

Another issue that remains to be investigated is reachability and Büchi problems for one-dimensional energy automata with flat energy functions; we plan to do this in future work.

Fig. 2 .

 2 Fig. 2. A simple energy automaton.

Fig. 3 .

 3 Fig. 3. The closure of the automaton from Fig. 2.

Remark that, in relation to the example in the introduction, the derivative is taken with respect to energy input, not time. Hence the mapping from input to output energy in state W is indeed an energy function in our sense.


Yacine Baziz
email: bazizyacine@gmail.com

Moufida Maimour
email: moufida.maimour@univ-lorraine.fr

Bouabdellah Kechar
email: bouabdellah.kechar@univ-oran.dz

EvalVSN : a New Tool for Video Quality Evaluation in Wireless Sensor Networks

Keywords: Wireless Video Sensor Networks (WVSN), Video/Image Quality Evaluation, EvalVSN, PSNR, SSIM

Wireless video sensor networks (WVSN) are foreseen to be a key driver of the development of pervasive applications of every-day life. They trigger very challenging problems due to their constrained nature in terms of energy, bandwidth, processing and storage means. In order to be able to assess the performances of their proposals, WVSN's researchers community needs a transmission and evaluation tool that considers WSN specific characteristics. In this paper, we propose EvalVSN, a new tool for video transmission and evaluation targeted to WVSN. EvalVSN allows both real and simulation-based video transmission and evaluation in WSN. Currently application modules that make use of EvalVSN trace files are available in TinyOS, ns2 and Castalia environments.

I. INTRODUCTION

Recent technological advances have led to the emergence of small low-power devices that integrate sensors with onboard processing and wireless communication capabilities. Pervasive networks of such sensors open new vistas for a wide spectrum of applications. Nowadays, making use of Wireless Sensor Networks (WSN) is foreseen to be a crucial element to allow a major evolution in numerous applications. WSN are constrained networks since they have very limited resources in terms of energy, bandwidth, processing and storage means. This is why, WSN were traditionally targeted to relatively low rate event-driven applications where a limited amount of data is transferred from a sensor node to the collect station or the sink. This is the case for instance of applications concerned with temperature and humidity measures.

More recently, devices with low-cost and low-power visual modules [START_REF] Rahimi | Cyclops: in situ image sensing and interpretation in wireless sensor networks[END_REF], [START_REF] Feng | Panoptes: A scalable architecture for video sensor networking applications[END_REF] have emerged allowing for fostering the development of Wireless Video Sensor Networks (WVSN). These latter provide significant benefit to many sensor networking applications such as surveillance, target tracking, environmental monitoring, and traffic management systems. However, WVSN generate unique challenging problems and should be designed to satisfy limited resources while providing a good quality of service (QoS). A significant effort has to be made by the research community to make WVSN applications a reality. To do so, a video transmission and evaluation tool targeted to WSN is required.

In WSN, a tool called Sim-LIT [START_REF] Orellana-Romero | Sim-lit: A simulation framework for image quality assessment in wireless visual sensor networks under packet loss conditions[END_REF] is proposed but it is targeted to image instead of video transmission evaluation.

One popular tool used to evaluate video quality in computer networks is EvalVid [START_REF] Klaue | Evalvid -a framework for video transmission and quality evaluation[END_REF]. However, the set of encoders such as MPEG-4, H.263 or H.264 supported by EvalVid are resourceshungry and as a result are not adapted to constrained networks such as WSN. In the last couple of years, a significant effort has been made to provide energy-aware encoding techniques that are more suitable to WSN. Work in [START_REF] Aghdasi | An energyefficient and high-quality video transmission architecture in wireless video-based sensor networks[END_REF] makes use of a modified version of MPEG-2 where video frames are assumed to be in gray-scale with the possibility to split each block data into priority levels. In [START_REF] Makkaoui | Fast zonal dct-based image compression for wireless camera sensor networks[END_REF], the effort is made in optimising the DCT (Discrete Cosine Transform) computation which is known to consume a significant amount of energy. The authors propose to use a fast zonal DCT which combine pruned DCT [START_REF] Wang | Pruning the fast discrete cosine transform[END_REF] with a fast DCT algorithm [START_REF] Loeffler | Practical fast 1-d dct algorithms with 11 multiplications[END_REF].

In this paper, we propose EvalVSN (publicly available at [START_REF] Baziz | Evalvsn[END_REF]), a new video transmission and evaluation tool that follows the same principle of EvalVid [START_REF] Klaue | Evalvid -a framework for video transmission and quality evaluation[END_REF] while being specific to WSN. EvalVSN can help a network researcher to assess network protocols targeted to video applications in WSN. It implements a modified version of MPEG-2 similar to the one proposed in [START_REF] Aghdasi | An energyefficient and high-quality video transmission architecture in wireless video-based sensor networks[END_REF] with priority assignment but additionally provides different DCT implementations as the one proposed in [START_REF] Makkaoui | Fast zonal dct-based image compression for wireless camera sensor networks[END_REF]. Application modules that allow the use of EvalVSN with more realistic loss patterns are also provided in the TinyOS [START_REF] Lu | Berkley motes and tinyos[END_REF], ns2 [START_REF]Network simulator 2[END_REF] and Castalia [12] environments.

The remainder of this paper is organised as follows. Section II gives background preliminaries. The EvalVSN architecture and main functionalities are presented in Section III. An illustrative example of a possible use of EvalVSN is given in IV. Section V concludes the paper.

II. BACKGROUND PRELIMINARIES

A. M-MPEG Codec Overview

In this first version of EvalVSN, we implemented M-MPEG (Modified-MPEG) [START_REF] Aghdasi | An energyefficient and high-quality video transmission architecture in wireless video-based sensor networks[END_REF] based on MPEG-2 with some changes that will be reported in Section III-B. In M-MPEG, each video frame is supposed to be in gray-scale. Two types of video frames are considered Main-Frame (M-Frame) and Difference-Frame (D-Frame). M-Frames are compressed before transmission, using an extended JPEG method [START_REF]Digital Image Processing Using MATLAB (DIPUM)[END_REF]. Compared with JPEG, the extended JPEG method has an additional step that prioritises image data. A DCT [START_REF] Chen | Video compression using integer dct[END_REF] is applied to each 8×8 block (after subtracting 128), then the less important DCT coefficients are wiped out using quantisation matrix. A quality coefficient can be used to adjust compression ratio to get the expected video frame quality. Afterwards, the elements of each block are partitioned into up to 13 levels using a zigzag scanning. Finally, the 64 elements of each block are linearised and run-length encoding (RLE) is applied to the result.

A D-frame is the result of subtracting current frame from the previous M-Frame. Each 8 × 8 block is assigned a priority depending on the number of zeros it contains. Blocks with minimum number of dissimilar pixels (maximum of zeros) have the lowest priority and can be prevented from being transmitted. Finally, RLE and then Huffman coding are applied. In [START_REF] Aghdasi | An energyefficient and high-quality video transmission architecture in wireless video-based sensor networks[END_REF], it is suggested to use a variable length GOP (Group of Pictures) instead of transmitting an M-frame at regular intervals.

B. Optimising DCT Computation

Since radio is the main energy consumer in a sensor node, a WVSN with longer lifetime can result from reducing the amount of data to be transmitted/received. Video compression appears to be a good start ; however methods used nowadays in computer networks are not suitable to constrained networks such as WSN. In fact, a DCT consumes about 60% of the total consumed energy to encode an image [START_REF] Marcelloni | A simple algorithm for data compression in wireless sensor networks[END_REF]. This is why DCT complexity has to be reduced. Methods to reduce the DCT computation complexity can be either based on zonal or fast DCT algorithms. Only a subset of the DCT coefficients are computed in the zonal DCT while in the fast DCT, redundant operations are eliminated. In order to be more adapted to WSN, authors of [START_REF] Makkaoui | Fast zonal dct-based image compression for wireless camera sensor networks[END_REF] combined these two methods and proposed fast zonal DCT. They considered both square and triangular [START_REF] Mammeri | Modeling and adapting jpeg to the energy requirements of vsn[END_REF] forms of the zonal DCT along with LLM algorithm to fast compute the DCT. Another fast DCT that is based on shift instead of multiplication operations called binDCT-C is proposed in [START_REF] Liang | A fast multiplierless block transform for image and video compression[END_REF].

As shown in Figure 1, given an 8×8 block, only the upperleft square or triangular portion, with side length K ∈ [2..8], is considered. In this way the DCT complexity is reduced as shown in Figures 2 and3 where the flow graph of LLM and binDCT-C algorithms respectively for K = 4 are illustrated. Table I summarizes the cost in terms of the number of required operations (addition, multiplication, shift) of fast zonal DCT using LLM and binDCT-C algorithms.

III. EVALVSN ARCHITECTURE AND MAIN FUNCTIONALITIES

EvalVSN (Figure 4) follows the main principle behind EvalVid where the interface with the real or simulation-based experiment is insured through the use of trace files : the sender and the receiver trace files. Based on the user parameters (the video clip to be encoded, the DCT computation method, the number of priority levels . . . ), EvalVSN generates a sender trace file (ST) that gives the sender application the required information about the data packets to be sent. In order to generate the ST file, two phases are required : a pre-processing and an encoding phase. A post-processing phase is performed in order to construct the received video and provide statistics based on the receiver trace file (RT) that results from the conducted simulated or real experiment. In our package, we provide application modules that make use of EvalVSN trace files in TinyOS [START_REF] Lu | Berkley motes and tinyos[END_REF], ns2 [START_REF]Network simulator 2[END_REF] and Castalia[12] environments.

A. Pre-processing Phase

This phase is required to make the video clip more realistic with respect to WSN characteristics. In fact, in the current state of the art, sending video sequences with an FPS (frames per seconds) of 30 fps is simply unfeasible due to the limited resources of a WSN. In order to be able to use reference video sequences such as those available at [START_REF]Yuv video sequences[END_REF], we introduce this pre-processing phase that allows to consider only a subset of the frames resulting in a more reasonable FPS. For instance, consider the Hall Monitor video sequence that lasts 10 seconds and consists of 300 frames in QCIF resolution (176 × 144). If we want to consider this sequence as a video captured at 1f ps, then only 1 frame every 30 is kept in the reduced video clip with only 10 frames. It is worth mentioning that this phase is optional and the user can keep the original FPS.

B. Video Encoding Phase

In this phase, MMPEG codec (overviewed in Section II-A) is applied on the video clip with the following changes :

• The work in [START_REF] Makkaoui | Compression d'images dans les réseaux de capteurs sans fil[END_REF] showed that depending on the sensor node hardware, image compression (even based on fast zonal DCT) may introduce additional energy consumption compared to the case where the image is transmitted without compression. This is why in our tool, we give the user the possibility to not compress a given frame if a minimal variance with the previous frame is observed. In this case, the application can additionally decide to not transmit the frame at all. To do so, the user has to give a positive value to the threshold similarity parameter. If this latter is set to 0 then all the frames will be compressed.

• The first frame is always encoded as an M-frame. A subsequent frame is either encoded as an M-frame or a D-frame depending on its similarity with the previous M-frame. Let X × Y be the resolution of a frame and F ZP be the number of zero pixels in the result of subtructing the previous M-frame from the current frame. If F ZP < qualityCoef × (X × Y ) then the current frame is encoded as an M-frame otherwise it is encoded as a D-frame. This means that when qualityCoef is increased then the number of Mframes is increased. This parameter has to be specified in the configuration file by the user.

• We allow the user to use the traditional DCT implementation and give him the ability to experiment less complex DCTs that are more suitable to WSN. In this version, LLM and binDCT-C fast zonal DCTs are implemented using a triangular pattern. We chose to implement a triangular rather than a square pattern since the former is more adequate to the decomposition in priority levels using the zigzag scan. Higher priority data are located in the upper-left triangle in the 8 × 8 blocks. If for some reason, only a subset of the data can be transmitted then the application layer can take the decision to only encode and transmit data with the highest priority. This allows saving the video sensor resources from encoding all the frame while only a subset can effectively be delivered to the sink.

• Based on our experiments, we found that applying Huffmann coding in addition to RLE on D-frames may generate very large D-frames. We chose to use only RLE encoding.

The output of the encoding phase is the sender trace file (ST) whose each line is structured as follows :

1) time at which this packet has to be sent ; 2) the number of the frame to which belong the data of this packet ; 3) the type (M or D) of the frame to which belong the data of this packet ; 4) this packet priority ; 5) this packet payload size ; 6) this packet payload (data) in hexadecimal.

C. Post-processing Phase

The experiment tool has to provide a receiver trace file (RT) that is potentially different from the ST file due to network losses. Missing lines in the RT tell about the set of packets that have been lost in the network before achieving the sink. Statistics on the conducted experiment are generated by EvalVSN based on the trace files (ST and RT) in addition to the sent and the received (reconstructed) video clips. The provided metrics can be either network-related or video-related.

We implemented the PSNR (Peak Signal to Noise Ratio) and the SSIM (Structural SIMilarity) [START_REF] Wang | Image quality assessment: from error visibility to structural similarity[END_REF] metrics to assess the quality of both the encoded video before transmission (Reference PSNR or SSIM) and the received video with respect to the initial lossless encoded video. EvalVSN provides the mean PSNR computed on a per frame basis. The PSNR between the sent (s) and the received (r), possibly distorted video frame is computed using :

P SN R(s, r) = 20log V peak M SE(s, r) (1)
M SE is the mean square error which is the average of the square of the errors (pixel differences) of the two images and V peak is the maximum possible pixel value.

SSIM exhibits much more consistency with subjective measure compared to PSNR and includes comparisons of luminance, contrast and structure as follows :

SSIM = 2µ x µ y + C 1 µ 2 x + µ 2 y + C 1 × 2σ x σ y + C 2 σ 2 x + σ 2 y + C 2 × σ xy + C 3 σ x σ y + C 3 (2)
where x and y are two nonnegative image signals, µ x , σ x and µ y , σ y are the mean and standard deviation of x and y respectively. σ xy is the sample cross-covariance between x and y. We give the following values for the three constant parameters :

C 1 = (K 1 L) 2 , C 2 = (K 2 L) 2 , C 3 = C 2 /2 with K 1 = 0.01, K 2 = 0.03 and L = 255.
Other statistics such as the number of M-frames and Dframes as well as the number of generated packets per priority level in addition to experienced loss ratios related to each frame type and priority level are provided by the post-processing phase.

IV. SIMULATIONS

In this section, we limit ourselves to give a use example of EvalVSN rather than optimizing the transmission process which is beyond the scope of this paper. The reader can refer to [START_REF] Zeghilet | The effects of interference on video quality over wireless sensor networks[END_REF] for another use example of EvalVSN where the performances of a multipath routing protocol along with a multiqueue multipriority scheme is performed. Here, we aim to illustrate the use of EvalVSN on the hall monitor video clip using ns2 simulator with the parameters summarized in table II. FPS is set to 1 so only 10 among 300 frames are considered. In order to get all these 10 frames encoded, the similarity threshold is set to 0. The quality coefficient is set to 0.1 which results in encoding only the first frame as an M-frame ; the 9 others are encoded as D-frames. We repeated the same simulation with the three DCT implementations and varied the parameter K of the fast zonal DCTs.

As stated before, EvalVSN provides the reference PSNR (SSIM) that allows assessing the video compression quality before transmission. This is done in order to separate the distorsion due to compression from the one due to experienced losses in the WSN. The obtained mean reference PSNR (SSIM) are reported in table III. We can see that the traditional DCT achieves the best PSNR (SSIM) since all the data of each frame are encoded. When using a triangular fast zonal DCT, the PSNR of reference decreases and especially when K decreases. This distortion can be acceptable if we consider the compression complexity reduction induced by the fast zonal DCT algorithm (see table I). One can consider the tradeoff between distortion and compression cost in the design of WVSN applications. Using the ST file, the sender application agent (at the video sensor) developped for ns2 performs a CBR (constant bit rate) transmission of the video data packets. The receiver application agent (that runs at the sink side) records the received data packets in the RT file. The post-processing phase of EvalVSN is applied to reconstruct the video clip based on the received data packets and generate statistics on the conducted experiment. Figure 5 shows the 5th frame of the reduced hall monitor video before transmission and after it is received by the sink for different DCT algorithms and K values.

The first observation we can make is that all the received images have experienced distortion due to transmission losses. It is worth saying that general conclusions can not be done from these simulations since each simulation is repeated once and the purpose of this section is only to illustrate the use of EvalVSN. However, we can see that better performances can be achieved using a zonal DCT. For instance, When K = 8 or even K = 4 (for LLM version), we can see that it is possible to obtain a higher PSNR for the received frame than the traditional DCT.

In order to be able to interprete the achieved video quality results depicted by Figure 5, information about loss rates are necessary. Figure 6 shows the loss ratio experienced by data packets that belong to M or D-frame in addition to the overall loss ratio. We can see that in this set of experiments, the LLM DCT gets the lowest loss ratio compared to the traditional and binDCT-C which explains its highest achieved PSNR.

V. CONCLUSION

In this paper, we presented a new transmission and evaluation tool targeted to WSN called EvalVSN and showed how this tool can be used to evaluate a video transmission in WSN. EvalVSN allows to make use of priority levels in addition to In the future, we expect to implement other encoding techniques as the image compression community is currently active in proposing new ones. Other application modules are also planned to be developped in other environment such as Contiki. Moreover, we aim to enhance our application modules by providing a more realistic energy model for data encoding. Finally, a C++ library is under developpment to allow better integration of compression algorithms to simulation environment so a decision on how to encode a given frame is performed on the fly and on a per-frame basis depending on the network status.

Figure 1 .

 1 Figure 1. Zonal DCT patterns K = 4 (redrawn from [6])

Figure 2 .Figure 3 .

 23 Figure 2. Flow Graph of LLM K = 4 (redrawn from [6])

Figure 4 .

 4 Figure 4. EvalVSN Architecture

  DCT -P SN R = 45.66dB LLM K = 8 -P SN R = 37.33dB binDCT K = 8 -P SN R = 37.01dB LLM K = 4 -P SN R = 25.98dB binDCT K = 4 -P SN R = 25.87dB (a) Sent frames DCT -P SN R = 21.13dB LLM K = 8 -P SN R = 24.87dB binDCT K = 8 -P SN R = 21.76dB LLM K = 4 -P SN R = 24.41dB binDCT K = 4 -P SN R = 20.54dB (b) Received frames

Figure 5 .Figure 6 .

 56 Figure 5. The 5th frame with different DCT and K values

Table I .

 I FAST ZONAL DCT COST FOR DIFFERENT VALUES OF K

			LLM			binDCT-C
	K	1-D DCT	2-D DCT	1-D DCT	2-D DCT
		Add.	Mul.	Add.	Mul.	Add.	Shift	Add.	Shift
	8	29	11	464	176	30	13	480	208
	7	28	11	348	130	28	12	420	180
	6	26	10	364	140	28	12	392	168
	5	25	9	325	117	28	12	364	156
	4	24	9	288	108	27	11	324	132
	3	23	8	253	88	19	6	209	66
	2	20	6	200	60	13	2	130	20

Video Reducer Video Quality Evaluation MMPEG Encoder Received video MMPEG Decoder Experiment Statistics Simulation or Real Experiment Parameters Experiment Raw YUV Video Evaluation Sender Trace File Receiver Trace File (ST) (RT) Reduced Raw Video Network-related