Sébastien Bardin

Alain Finkel

Jérôme Leroux
email: jleroux@irisa.fr

Philippe Schnoebelen

Flat acceleration in symbolic model checking

Keywords: verification of infinite-state systems, symbolic model checking, acceleration

Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called "acceleration techniques" enhance the convergence of fixpoint computations by computing the transitive closure of some transitions. In this paper we develop a new framework for symbolic model checking with accelerations. We also propose and analyze new symbolic algorithms using accelerations to compute reachability sets.

Introduction

Context. The development of model checking techniques [START_REF] Clarke | Model Checking[END_REF] for infinite-state systems is now an active field of research. These techniques allow considering models like pushdown systems [START_REF] Bouajjani | An efficient automata approach to some problems on context-free grammars[END_REF], channel systems [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF], counter systems [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF][START_REF] Ibarra | Counter machines and verification problems[END_REF][START_REF] Wolper | Verifying systems with infinite but regular state spaces[END_REF], and many other versatile families of models. Such models are very expressive and often lead to undecidable verification problems. This did not deter several research teams from developing powerful innovative model checkers for infinite-state systems. For example, tools for checking reachability properties of counter systems are ALV [START_REF]ALV[END_REF], BRAIN [START_REF] Rybina | Brain: Backward reachability analysis with integers[END_REF], LASH [33], TREX [START_REF] Annichini | TReX: A tool for reachability analysis of complex systems[END_REF], and our own FAST [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF]. For infinite-state systems, model checking must be "symbolic" since one manipulates (symbolic representations of) potentially infinite sets of configurations. The most popular symbolic representations are based on regular languages: these are quite expressive and automata-theoretical data structures provide efficient algorithms performing set-theoretical operations as well as pre-and post-image computations. With these ingredients, it becomes possible to launch a fixpoint computation for forward or backward reachability sets, as exemplified in [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF].

The problem of convergence. When dealing with infinite-state systems, a naive fixpoint computation procedure for reachability sets, in the style of Procedure 1 (section 3.2), has very little chance to terminate: convergence in a finite number of steps can only occur if the system under study is uniformly bounded (see section 3.2). To make fixpoint computations converge more frequently, so-called "acceleration techniques" have been developed. These techniques can compute subsets of the reachability set that are not uniformly bounded. This can be done, for example, by replacing a control loop "x:=x+1; y:=y-1" by its transitive closure "k:=random int(); x:=x+k; y:=y-k". Currently, many different acceleration techniques for different families of systems exist [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF][START_REF] Annichini | Symbolic techniques for parametric reasoning about counter and clock systems[END_REF][START_REF] Boigelot | The power of QDDs[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF][START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF][START_REF] Wolper | Verifying systems with infinite but regular state spaces[END_REF]. Some of them have been implemented [START_REF] Annichini | TReX: A tool for reachability analysis of complex systems[END_REF][START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF]33] and promising case-studies have been reported [1-3, 8, 9]. Acceleration shares some similarities with the widening techniques used in abstract interpretation [START_REF] Cousot | Abstract interpretation[END_REF] but also exhibits some clear differences: acceleration aims at exact computation for some given control structures, while widening mostly ignores control structures and usually trades exactness for termination.

A field in need of foundations. The existing acceleration results usually amount to a (sometimes difficult) theorem stating that the transitive closure of an action, or of a sequence of actions, can be effectively computed. The difficulty of these results usually lies in finding the precise conditions on the action and on the set of initial states that yield effectiveness. How to use acceleration results is not really known: the theorems and algorithms for computing reachability sets with acceleration methods do not exist in general! With some tools, e.g., LASH, the user has to choose which loops to accelerate and how to mix the outcomes with more standard symbolic computation; in other cases, e.g., with TREX, some default strategy is implemented outside of any theoretical framework and without discussions about its efficiency or completeness.

Our contributions. (1)

We propose the first theoretical framework for symbolic model checking with acceleration. We distinguish three natural levels for accelerations ( "loop", "flat", and "global"), depending on which sequences of transitions can be computed: transitive closure of cycles (resp. of length 1) for flat (resp. loop) acceleration; or any regular set of sequences for global acceleration. These levels can account for most acceleration results on specific systems (pushdown systems, channel systems, counter systems, . . . ). For each level we give a symbolic algorithm with acceleration computing reachability sets and we characterize the conditions necessary for its termination.

Flat acceleration is the most interesting level. As a matter of fact, loop acceleration is not sufficient for many of the example systems we have analyzed with our tool FAST. Furthermore, the majority of existing acceleration results stated at the loop acceleration level may be extended to the level of flat acceleration. At the other end of the spectrum, global acceleration is always sufficient but it occurs very rarely in practice and is essentially restricted to particular subclasses (e.g., pushdown systems, reversal-bounded counter systems [START_REF] Ibarra | Counter machines and verification problems[END_REF] or particular subclasses of Petri nets).

(2) We develop new concepts for the algorithmic study of flat acceleration. The notions of flattenings and of flattable systems provide the required bridge between flat acceleration and the effective computation of the reachability set.

We propose new symbolic procedures and analyze them rigorously. We show Procedure REACH2 terminates iff it is applied to a flattable (rather than flat) system, which is the first completeness result on symbolic model checking with acceleration. We remark that most of the case studies we analyzed in earlier works with FAST are flattable but not flat, underlining the relevance of this concept.

(3) Procedure REACH2 is schematic and it can be specialized in several ways. We propose one such specialization, REACH3, geared towards the efficient search of all flattenings of a nonflat system, without compromising completeness.

It appears that a key issue with REACH3 is the reduction of the number of circuits the procedure has to consider. FAST implements specific algorithms for counter systems that reduce exponentially the number of considered circuits and we show how to generalize these ideas to other families of systems. It is these algorithms that make FAST succeed in verifying several examples (see section 6) for which tools like LASH and ALV, based on similar technology but restricted heuristics, do not terminate. More generally, the comparisons in section 6 suggest that flat acceleration greatly enhances termination of symbolic reachability set computation, and is fully justified in practice.

Outline. We define the systems under study in section 2, and the symbolic frameworks in section 3. Section 4 introduces the three levels of accelerations and defines flattable systems. Section 5 provides our procedure for flattable systems, and gives several algorithmic and/or heuristic refinements. Section 6 compares several existing tools through the new framework. All omitted proofs can be found in the full version of this paper.

Systems and interpretations

Notations. A (binary) relation r on some set X is any subset of X × X. We write x r x when (x, x ) ∈ r and denote by r(x) the set {x ∈

X | x r x }. For Y ⊆ X, r(Y ) is x∈Y r(x). Given r 1 , r 2 ⊆ X × X, the compound relation r 1 • r 2 contains all pairs (x, z) s.t.
x r 1 y and y r 2 z for some y ∈ X. Note that, in r 1 • r 2 , relation r 1 is applied first. For i ∈ N, r i is defined inductively by r 0 = Id X and r i+1 = r • r i , where Id X is the identity on X. r * = i∈N r i is the reflexive and transitive closure of r.

Here, a system is a finite state control graph extended with a finite number of variables that range over arbitrary domains and are modified by actions when a transition is fired. Specific families of systems have been widely studied (see section 2.1). Formally: Definition 2.1 (Uninterpreted system). An uninterpreted system S is a tuple S = (Q, Σ, T ), where Q is a finite set of locations, Σ is a (possibly infinite) set of formulae called actions, T ⊆ Q × Σ × Q is a finite set of transitions. Given a uninterpreted system S = (Q, Σ, T ), the source, target and action mappings α : T → Q, β : T → Q and l : T → Σ are defined as follows: for any transition t = (q, σ, q ) ∈ T , α(t) = q, β(t) = q , l(t) = σ.

Definition 2.2 (Interpretation).

Given a (possibly infinite) set of formulae Σ and a set D, an interpretation I of Σ, shortly an interpretation, is a tuple I = (Σ, D, • ) such that • : Σ → 2 D×D maps formulae to relations on D.

Definition 2.3 (System

). An interpreted system S (shortly a system) is a pair (S, I) of an uninterpreted system S = (Q, Σ, T ) and an interpretation I = (Σ, D, • ) of Σ, shortly written S = (Q, Σ, T, D, • ).

Fig. 1 displays S 0 , a simple uninterpreted system, in graphical notation. q 1 q 2

x:=x + 1 / * a 1 * /

x = y? y:=y + x / * a 2 * / y:=y + 2;

x:=x -1 / * a 3 * / Fig. 1. S 0 , a simple uninterpreted system

In this example the actions may be assignments that can be guarded by Boolean expressions, but we will not specify it more precisely. A possible interpretation for a 1 ,a 2 and a 3 (the actions appearing in S 0 ) assumes that the domain D is Z {x,y} , or equivalently Z 2 , i.e., we decide that x and y range over integers. We then interpret the actions in the obvious way. For example a 2 = {((x, y), (x , y )) | x = y ∧ y = y + x ∧ x = x}. This turns S 0 into an interpreted system S 0 .

Behaviour. The set of configurations C S of S is Q × D, and each transition t ∈ T is interpreted as a relation t -→⊆ C S × C S defined by: (q, x) t -→ (q , x ) if q = α(t), q = β(t) and (x, x ) ∈ l(t) . This definition extends to sequences π ∈ T * of transitions. Let ε denote the empty word. Then

ε - →= Id CS and t•π -→= t - → • π - →. We also define L - → for any language L ⊆ T * by L - →= π∈L π - →.
Similarly • is extended to any language L ⊆ Σ * . In the following we omit the S subscript whenever this causes no ambiguities.

Reachability problems. We are interested in checking safety properties, which can be expressed in terms of reachability using standard techniques. For any X ⊆ C S and any L ⊆ T * , we define post S (L,

X) = {x ∈ C S | ∃x ∈ X; (x, x ) ∈ L - →}.
The set post(T, X) of all configurations reachable in one step from X is denoted by post(X). The set post(T * , X) of all configurations reachable from X is the reachability set of X, denoted by post * (X).

In practice, we usually ask whether post * (X 0 ) ⊆ P , for X 0 a set of initial configurations, and P a set of "safe" configurations. We focus here on the reachability set computation which is the key issue. Since post * (X 0 ) is not recursive in general, the best we can hope for are partially correct procedures, with no guarantees of termination, but that are efficient on interesting subclasses of systems, and in practical case-studies.

Backward computation.

One may also rely on backward reachability and check if, for a set P of "bad" configurations, pre * (P )∩X 0 is empty (with obvious definition for pre). Since, for our level of abstraction, adaptation to backward computation is straightforward, we consider only forward computation. However it is worth remembering that, depending on the case at hand, one of the approaches may be more adapted than the other. Along the paper specific results for backward computation are pointed out.

Transition relation computation.

A third approach is to compute the reachability relation T * -→ once and for all (e.g., [START_REF] Comon | Timed automata and the theory of real numbers[END_REF][START_REF] Esparza | Petri nets, commutative context-free grammars, and basic parallel processes[END_REF]). Then post * (X 0 ) = T * -→ (X 0 ). Our framework extends smoothly in this direction but, since it requires additional notations, we postpone this until the full version of this work.

Families of systems Definition 2.4 (Family of systems).

Given an interpretation I = (Σ, D, • ), the family of systems built on I (shortly the family of systems) denoted by F(I) is the class of all systems S = (Q, Σ, T, D, • ) using I to interpret actions.

Well known models can be obtained by instantiating Definition 2.4: Minsky machines: are obtained by defining D = N Var where Var = {x 1 , x 2 , . . .} is a set of variables, and Σ as the set of increments "x i :=x i + 1", guarded decrements "x i > 0? x i :=x i -1" and 0-tests "x i = 0?" with the obvious interpretation.

Counter systems [START_REF] Bultan | Symbolic model-checking of infinite state systems using Presburger arithmetic[END_REF][START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF]: are obtained by considering the same domain, or a variant D = Z Var , and all actions definable in Presburger arithmetic. Many restrictions exist, e.g., linear systems where actions are linear transformations with guards expressed in Presburger [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF][START_REF] Wolper | Verifying systems with infinite but regular state spaces[END_REF], reversal-counter systems [START_REF] Ibarra | Counter machines and verification problems[END_REF], many extensions of VASS (or Petri nets) and so on. Pushdown systems: the domain is D = Γ * , the set of all words on some stack alphabet Γ . Actions add or remove letters on or from the top of the stack. Channel systems [START_REF] Brand | On communicating finite-state machines[END_REF]: consider the domain is D = (Γ * ) C where C is a set of fifo channels, and Γ is some alphabet of messages. Actions add messages at one end of the channels and consume them at the other end. Timed automata [START_REF] Alur | A theory of timed automata[END_REF]:

consider the domain D = R Var + .
Here some actions are guarded by simple linear (in)equalities and they can only reset clocks. Other actions, left implicit in the standard presentation, account for time elapsing. Hybrid systems [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]: extend timed automata in that the real-valued variables do not increase uniformly when time elapses. Rather they each increase according to their own rate (as given by the current location).

A symbolic framework for symbolic model checking

In practice model checking procedures use symbolic representations (called here regions) to manipulate sets of configurations. The definition below follows directly from ideas expressed for example in [START_REF] Bouajjani | Regular Model Checking[END_REF][START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF][START_REF] Cousot | Abstract interpretation[END_REF].

3 Definition 3.1 (Symbolic framework). A symbolic framework is a tuple SF = (Σ, D, • 1 , L, • 2 ) where I = (Σ, D, • 1 ) is an interpretation, L is a set of formulae called regions, • 2 : L → 2 D is
a region concretization, and such that there exists a decidable relation and recursive functions , POST satisfying: 1. there exists an element ⊥∈ L such that

⊥ 2 = ∅, 2. ⊆ L × L is such that for all x 1 , x 2 ∈ L, x 1 x 2 iff x 1 2 ⊆ x 2 2 , 3. : L × L → L is such that ∀x 1 , x 2 ∈ L, x 1 x 2 2 = x 1 2 ∪ x 2 2 , 4. POST : Σ × L → L is such that ∀a ∈ Σ, ∀x ∈ L, POST(a, x) 2 = a 1 ( x 2 ).
Notation. Usually given an interpretation I = (Σ, D, • 1 ) and a set of regions L, • 2 is understood. Thus in the following, we write • for both • 1 and • 2 , and we denote symbolic frameworks as SF = (I, L). In the rest of the paper, we fix an arbitrary symbolic framework SF = (I, L). When referring to a system S, if nothing is specified we assume that S ∈ F(I).

Well-known symbolic frameworks for some of the families listed in section 2.1 are: Regular languages: have been used for representing sets of configurations of pushdown systems [START_REF] Bouajjani | An efficient automata approach to some problems on context-free grammars[END_REF], distributed protocols over rings of arbitrary size [START_REF] Kesten | Symbolic model checking with rich assertional languages[END_REF], and channel systems [START_REF] Pachl | Protocol description and analysis based on a state transition model with channel expressions[END_REF]. Restricted sets of regular languages are sometimes used for better algorithmic efficiency: languages closed by the subword relation [START_REF] Abdulla | Using forward reachability analysis for verification of lossy channel systems[END_REF] or closed by semicommutations [START_REF] Bouajjani | Permutation rewriting and algorithmic verification[END_REF]. (finite union of) Convex polyhedra [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]: are conjunctions of linear inequalities defining subsets of R Var + , relevant in the analysis of hybrid systems. Number Decision Diagrams [START_REF] Bultan | Symbolic model-checking of infinite state systems using Presburger arithmetic[END_REF][START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF]: are automata recognizing subsets of Z Var and have been used in the analysis of counter systems. Real Vector Automata [START_REF] Boigelot | Improved reachability analysis method for strongly linear hybrid systems[END_REF]: are Büchi automata recognizing subsets of R Var + and have been used in the analysis of linear hybrid systems. Difference Bounds Matrices [START_REF] Alur | A theory of timed automata[END_REF]: are a canonical representations for convex subsets of R Var + defined by simple diagonal and orthogonal constraints that appear in timed automata. Covering Sharing Trees [START_REF] Delzanno | Covering sharing trees: a compact data structure for parameterized verification[END_REF]: are a compact representation for upward-closed subsets of N Var . These sets appear naturally in the backward analysis of broadcast protocols [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] and several monotonic extensions of Petri nets.

Given a system S with a set of locations Q, and X ⊆ C S , post * (X) is of the form q∈Q {q} × D q where the D q are subsets of D. Assuming an implicit ordering on locations q 1 , . . . , q |Q| , we work on tuples of regions in L |Q| . We extend

• to L |Q| by (x 1 , . . . , x |Q| ) = |Q| i=1 {q i } × x i .

Extensions of and are component-based.

POST is extended into POST : T × L → L by: POST((q i , a, q j ), (x 1 , . . . , x |Q| )) is equal to (x 1 , . . . , x |Q| ) such that x p = ⊥ if p = j, POST(a, x i ) otherwise. POST is then extended to sequence of transition in the obvious way. We define POST : L |Q| → L |Q| by POST(x) = t∈T POST(t, x).

Limits of the symbolic approach

A subset of configurations X ⊆ C S is L-definable if there exists x ∈ L |Q| such that x = X. Obviously, computing post * (X) using regions is feasible only if post * (X) is L-definable and the question "is post * ( x ) L-definable?" is undecidable in general.

Furthermore, L-definability of post * (X) is not a sufficient condition for its computability. We say below that post * (or any other function) is effectively L-definable if there exists a recursive function g :

L |Q| → L |Q| such that ∀x ∈ L |Q| , post * ( x ) = g(x)
. (We often abuse terminology and write that "post * ( x )", instead of post * , "is effectively L-definable"). It can well be the case that post * ( x ) is L-definable but not effectively so (e.g., the family of lossy channel systems and the framework defined by simple regular expressions).

Standard symbolic model checking procedure

REACH1 (Procedure 1) is the standard symbolic procedure for reachability sets. It is only guaranteed to terminate on L-uniformly bounded systems. In practice systems are rarely L-uniformly bounded and Procedure 1 seldom terminates. A notable exception are the well-structured transition systems with upwardclosed sets as regions [START_REF] Finkel | Well-structured transition systems everywhere![END_REF][START_REF] Finkel | Well-abstracted transition systems: Application to FIFO automata[END_REF]. They are L-backward uniformly bounded so that a backward version of Procedure 1 always terminates.

x ∈ L |Q| , there exists n x ∈ N such that, for all c 1 ∈ Q × x and c 2 ∈ Q × D, if c 2 ∈ post * ({c 1 }) then c 2 ∈ i≤nx post i ({c 1 }).

Flat acceleration for flattable systems

Acceleration techniques

In order to improve the convergence of the previous procedure, acceleration techniques consist in computing the transitive closure of some transitions. We often write that "S", rather than (I, L), "supports loop acceleration, or flat, . . . " Consider S 0 from Fig. 1 and let A ⊆ D. Loop acceleration only concerns action a 3 , and comes down to computing a *

3 (A) = {(x , y ) ∈ Z 2 |∃(x, y) ∈ A; ∃k ∈ N; x = x -k ∧ y = y + 2 • k}. Flat acceleration requires computability of (a 1 • a 2 ) * (A), (a 1 • a 3 • a 2 ) * (A), (a 1 • a 3 • a 3 • a 2 ) * (A), (a 3 • a 2 • a 1 ) * (A)
and so on. Global acceleration requires the computation of more complex interleaving of actions, like (a 1 • a * 3 • a 2 ) * (A). Definition 4.1 applies to symbolic frameworks and hence uses sequences of actions. However, in practice, POST STAR is used with sequences of transitions. Let us illustrate this in the case of flat acceleration: Consider a sequence π = (q 1 , a 1 , q 2 ) • (q 3 , a 2 , q 4 ) • (q 5 , a 3 , q 6 ) of transitions. There are two cases. If the sequence is invalid (i.e., q 2 = q 3 or q 4 = q 5 ) then the associated relation is empty and POST STAR(π, (q, x)) is (q, x). If the sequence is valid, then the sequence is equivalent to (q 1 , a 1 • a 2 • a 3 , q 6 ). If the sequence is not a cycle (q 1 = q 6 ) it can be fired at most once and POST STAR(π, (q 1 , x)) is (q 6 , POST(a 1 • a 2 • a 3 , x)) + (q 1 , x). If the sequence is a cycle (i.e., q 1 = q 6 ) then POST STAR(π, (q, x)) is (q 1 , POST STAR(a 1 • a 2 • a 3 , x)) if q = q 1 , and (q, x) otherwise. Finally POST STAR is extended to L |Q| in the obvious way. The extension for global acceleration considers the intersections of the regular language e with the regular languages of transitions from a location q to another location q . Global acceleration. Reversal-counter systems [START_REF] Ibarra | Counter machines and verification problems[END_REF], 2-dim VASS [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF], lossy VASS and other subclasses of VASS with Presburger formulae [START_REF] Leroux | Flat counter automata almost everywhere![END_REF], pushdown systems with regular languages or semi-commutative rewriting systems with APC languages [START_REF] Bouajjani | Permutation rewriting and algorithmic verification[END_REF], support global acceleration.

Obviously "global ⇒ flat ⇒ loop". Loop acceleration is often easy to obtain, but rarely sufficient in fixpoint computations. Flat acceleration is more flexible, but often requires good compositional properties of Σ and more complex methods for POST STAR. Global acceleration is a very strong property that ensures post * is effectively L-definable. Clearly most interesting families of systems do not support global acceleration since they are Turing powerful. Then for our purpose, flat acceleration is likely to be the best compromise. The rest of the paper will focus on flat acceleration.

Restricted linear regular expressions

Flat acceleration allows to compute the effect of more general expressions than iterations of sequences of actions. Given an alphabet A, a restricted linear regular expression (rlre) over A is a regular expression ρ of the form u * 1 . . . u * n where, for all i, u i ∈ A * . This is closely related to semi-linear regular expressions [START_REF] Finkel | Well-abstracted transition systems: Application to FIFO automata[END_REF][START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF]. Proposition 4.3. Let S support flat acceleration. Then for any rlre ρ over T and for any x 0 ∈ L |Q| , post(ρ, x 0 ) is effectively L-definable.

Flat systems and flattenings

q 1 q 2 t 3 t 1 t 2
In general, flat acceleration does not ensure computability of the reachability set. However it does in some cases, for example with "flat" systems, that have no nested loops. Consider the system on the right: its reachability set can be computed by iterating first t 1 , then firing t 3 , and finally iterating t 2 . [START_REF] Comon | Multiple counters automata, safety analysis, and Presburger arithmetic[END_REF][START_REF] Finkel | Well-abstracted transition systems: Application to FIFO automata[END_REF][START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF]). An uninterpreted system S = (Σ, Q, T ) is flat if for any location q, there exists at most one elementary cycle containing q.

Definition 4.4 (Flat system

A system S = (Σ, Q, T, D, • ) is flat if S = (Σ, Q, T ) is flat.
In Fig. 1, S 0 is not flat because its two elementary cycles both visit q 2 . Proposition 4.5. If S is a flat system supporting flat acceleration, then post * S ( x ) is effectively L-definable. Not all systems of interest are flat, and a possible method for dealing with a non-flat system S is to find an equivalent flat system, called a flattening of S.

Definition 4.6 (Flattening).

A system S = (Q , Σ, T , D, • ) is a flattening of a system S = (Q, Σ, T, D, • ) if (1) S is flat, and ( 2) there exists a mapping z : Q → Q, called folding, such that ∀(q 1 , w, q 2 ) ∈ T , (z(q 1 ), w, z(q 2 )) ∈ T .

Flattening is a form of partial unfolding. The following figure shows a system (left) and one of its flattenings (right).

q 1 q 2 t 3 t 4 t 2 t 1 q 1 q 2 q 1 q 2 q 1 q 2 t 3 t 4 t 3 t 4 t 3 t 4 t 1 t 1 t 2
Assume S is a flattening of some S. The z folding extends to configurations of S by z((q , x)) = (z(q ), x). Extension of z to X ⊆ C S is defined by:

z q ∈Q {q } × D q = q∈Q {q} × q ∈z -1 (q) D q .
This gives an effective extension of z to L-definable subsets of C S . Given X ⊆ C S , Definition 4.6 ensures that z(post * S (X )) ⊆ post * S (z(X )) and that for any language L ⊆ T * , z(post S (L, x )) = post S (z(L), z( x )). A natural question is whether L-flattable systems are common or rare. It appears that many systems with L-definable reachability sets are flattable. For example 2-dim VASS [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF], timed automata [START_REF] Comon | Timed automata and the theory of real numbers[END_REF], k-reversal counter machines, lossy VASS and other subclasses of VASS [START_REF] Leroux | Flat counter automata almost everywhere![END_REF] and all L-uniformly bounded systems (see section 3) are Lflattable. Clearly, there is no equivalence in general: lossy channel systems have Ldefinable reachability sets but are not flattable. Interesting open questions are whether well-known subclasses with L-definable reachability sets (like Presburger definable VASS) are L-flattable or not.

We conclude by noting that L-flattability is undecidable in general, even when restricting to 2-counter systems: Theorem 4.9. Assuming the symbolic framework of 2-counter systems and Presburger formulae, the question of whether a 2-counter system S is L-flattable is undecidable.

Computing reachability set using flat acceleration

The previous characterization leads to a complete procedure for flattable systems: (1) enumerate all flattenings S of S; (2) for each S , compute its reachability set X; (3) check whether z(X) is closed by post in S.

However flattenings are not easy to handle and this motivates the following alternative characterization based on rlre's.

Theorem 5.1. A system S = (Q, Σ, T, D, • ) is L-flattable iff for all x ∈ L |Q| , there exists a rlre ρ over T such that post * ( x ) = post(ρ, x ).

Hence reachability set computation for flattable systems reduces to exploring the set of rlre over T , which can be achieved by increasing a sequence of rlre: see Procedure 2. Observe that REACH2 must choose "fairly". Here this means that, in a nonterminating execution of the procedure, each w ∈ T * is selected infinitely often. Many simple schemes ensuring such a fair choice are possible. Theorem 5.2. Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH2 terminates, REACH2(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH2 terminates on any input iff S is L-flattable (termination). x ← POST STAR(w, x) 5: end while 6: return x Procedure 2: Computing reachability sets with flat acceleration.

Faster enumeration of flattenings

A major practical issue with REACH2 is to implement Choose so that we converge quickly to the fixpoint. For this purpose the following heuristic proved very efficient in FAST: one picks a bound k ∈ N and restricts Choose to sequences w ∈ T ≤k , i.e., of length at most k. This method, called k-flattable, is eventually stopped by a Watchdog if it does not terminate. Then k is incremented and k-flattable is launched again.

This leads to Procedure REACH3 below. For "fairness" we require that Watchdog fires infinitely often, but only after Choose picked each w ∈ T ≤k at least once.

procedure REACH3(x0) parameter: S input: x0 ∈ L |Q| 1: x ← x0 ; k ← 0 2: k ← k + 1 3: start 4: while POST(x)
x do /* k-flattable */ 5:

Choose fairly w ∈ T ≤k 6:

x ← POST STAR(w, x) 7:

end while /* end k-flattable */ 8: with 9:

when Watchdog stops goto 2 10: return x Procedure 3: Flat acceleration and circuit length increasing Theorem 5.4. Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH3 terminates, REACH3(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH3 terminates for any input iff S is L-flattable (termination).

Technical issues. When implementing REACH3 one faces (at least) two practical problems. First the size 4 of the region x computed so far may be explosive. Then Watchdog needs some criterion. Below we describe the implementation choices made in FAST on these two issues, believing that these solutions may adapt to other domains. Let us point out that these choices do not respect exactly the specification for REACH3 since fairness is not ensured, and FAST should be improved in this way. Choose: In general there is no direct relationship between the size of a region x and the "size" of its concretization x . Intermediate regions may be much larger than the final region for post * ( x 0 ). To avoid such large regions, Choose selects a next w ∈ T ≤k such that |POST STAR(w, x)| < |x|. If there is no such w then the size of the current x is allowed to increase and the next w is picked. In practice, this enumeration works well (while a cyclic enumeration of T ≤k almost always runs out of memory). Watchdog: FAST's criterion is simply a fixed (but user-modifiable) limit on the number of iterations in k-flattable for any given value of k. This cannot be fair but it works well in practice since, once a k large enough is considered, the fixpoint is usually found within a few iterations.

Reduction of the number of cycles

A remaining issue in REACH3 is that the cardinal of T ≤k grows exponentially with k. We introduce the notion of reduction to compact the number of relevant transitions.

Definition 5.5 (k-Reduction). Given an interpretation

I = (Σ, D, • ), a k-reduction r maps each system S = (Q, Σ, T, D, • ) ∈ F(I) to a system S = (Q, Σ, T , D, • ) ∈ F(I) such that: (1) ∀t ∈ T , t - →⊆ T * -→, (2) ∀w ∈ T ≤k , ∃ρ ∈ rlre(T ). w * -→⊆ ρ - →, (3) |T | ≤ |T ≤k |.
Hence a k-reduction replaces T by a new set T that can stand for T ≤k but is smaller. In particular, if S is L-flattable, then r(S) is too, and they both have the same reachability set. Obvious (and naive) k-reductions are the removals of identity loops. More useful generic reductions are conjugation reduction: only keep one sequence of transitions among each conjugacy class (e.g., keep t Here are reduction results for the swimming pool protocol (a VASS with 7 transitions and 6 variables studied in [START_REF] Fribourg | Proving Safety Properties of Infinite State Systems by Compilation into Presburger Arithmetic[END_REF]). Computing the reachability set requires considering cycles of length k = 4. In the table V k ⊆ T ≤k is the set of valid sequences in T ≤k . T (resp. T ) is from the system after the reduction of [START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] (resp. further combined with commuting reduction). Our framework is useful when comparing ALV, FAST, LASH and TREX, four symbolic model checkers that can perform reachability analysis on counter systems (see section 2.1). We restrict this comparison to the exact forward computation of post * ( x 0 ). ALV [START_REF]ALV[END_REF] handles full counter systems. Regions are Presburger formulae. The heuristic used is similar to REACH1. Both FAST [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF] and LASH [33] handle linear counter systems with Presburger formulae: flat acceleration is supported for functions whose monoid is finite, but while FAST really takes advantage of full flat acceleration (Procedure REACH3), the heuristics in LASH are restricted to loop acceleration (Procedure REACH2 where w is chosen in T ≤1 instead of T * ). TREX [START_REF] Annichini | TReX: A tool for reachability analysis of complex systems[END_REF] handles restricted counter systems. Regions are arithmetic formulae (hence is not recursive). A partially recursive flat acceleration procedure is available. The heuristic is REACH2 restricted to T ≤k for a user-defined k. See [START_REF] Ch | About Fast and TReX accelerations[END_REF] for an in-depth comparison of FAST and TREX. UB, F and kF stands for L-uniformly bounded, L-flattable and L-flattable with length k (UB ⊆ 1F ⊆ kF ⊆ F). All case studies are infinite-state systems, taken from FAST's web site [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF]. Experimental results show strong relationship with the acceleration framework: flat acceleration (FAST) has the better termination results, loop acceleration (k = 1) is not always sufficient, while simple iteration (ALV) is not sufficient on these complex examples (results are consistent with [START_REF] Bartzis | Widening arithmetic automata[END_REF]). These experiments clearly suggest that flat acceleration greatly enhances termination and is fully justified in practice, at least for counter systems.

Conclusion: flat acceleration in practice

Procedure comparison on case studies

Tool design

The flat acceleration framework provides guidelines for designing new techniques and tools. FAST supports completely this framework. Complex case studies have been conducted [START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF][START_REF] Bardin | FASTer acceleration of counter automata[END_REF]. The following table shows performances of FAST on a significant pool of counter systems collected on the web sites of tools like ALV, BABYLON [START_REF] Babylon | [END_REF]

A Proofs missing in the main text

Notations. Given a set X, for any index i ∈ [1 . . . n], we denote by x[i] the i th component of a n-tuple x ∈ X n .

Theorem A.1. Given the symbolic framework of 2-counter systems and Presburger formulae, a 2-counter system S, and x 0 ∈ L |Q| , then whether post * ( x 0 ) is L-definable or not is undecidable.

Proof. We reduce the reachability problem, undecidable for 4-counter systems. It is not a restriction since 2-counter systems can encode any fixed number of counters. We consider a weaker variant, location reachability, still undecidable. The location reachability problem is the following. We consider a 4-counter system S 0 equipped with 4 variables x, y, y 0 and z ranging over N and a finite set Q of locations, an initial configuration (q 0 , c 0 ) where q 0 ∈ Q and c 0 ∈ N 4 , and a location q ∈ Q. Then we want to decide if there is a run of the counter system on input (q 0 , c 0 ) such that q is reached. Suppose that for any (S , q , c ) we can decide if post * S ((q , c )) is definable by a Presburger formula. Let us remind that Presburger formulae cannot expressed multiplication among variables (typically z = x × y). We proceed as follows. We transform S 0 into S 1 by: adding a finite number of new locations Q 1 and new transitions over Q 1 , starting at q 1 ∈ Q 1 , coding a multiplication of counter x by counter y, and the result is assigned to z in location q z ∈ Q 1 (counter y 0 is used to remember the value of y during the operation). Then we had some more transitions. A transition (q 0 , "x := 0, y := 0, z := 0", q 1 ), the transitions (q 1 , "x := x + 1", q 1 ), (q 1 , "y := y + 1", q 1 ), the transitions (q, "x := x + 1", q), (q, "x := x -1", q), (q, "y := y + 1", q), (q, "y := y -1", q) (q, "z := z + 1", q), (q, "z := z -1", q) and for all q ∈ Q 0 ∪ Q 1 a transition (q, "x := x, y := y, z := z", q ). Then it is easy to verify that post * S1 ((q 0 , c 0 )) is L-definable (and equals to (Q 0 ∪ Q 1 ) × N 3 ) iff q is reachable (otherwise the reachability set projected on q z is {(x, y, z)|z = x × y} ).

A.1 Proof of Theorem 3.3 Theorem 3.3. Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH1 terminates, REACH1(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH1 terminates on any input iff S is L-uniformly bounded (termination).

Proof. Partial correctness: when the procedure terminates, REACH1(x 0 ) is a fixpoint of POST, then REACH1(x 0 ) is a fixpoint of post. Moreover at each iteration of the procedure, x ⊆ post * ( x 0 ). This ensures that REACH1(x 0 ) is equal to the least fixpoint of post, i.e., post * ( x0 ).

Termination: We suppose S is L-uniformly bounded. Given x 0 ∈ L |Q| , there exists n x0 such that post * ( x 0 ) = i≤nx 0 post i ( x 0 ). It is straightforward that after n x0 iterations, REACH1 terminates. We suppose now that REACH1 terminates on any input. Then for any x 0 ∈ L |Q| , the fixpoint is reached after n x0 iterations. n x0 is the constant in the definition of L-uniformly bounded.

Procedure 1 :

 1 procedure REACH1(x0) parameter: S input: x0 ∈ L |Q| 1: x ← x0 2: while POST(x) x do 3: x ← POST(x) x 4: end while 5: return x Standard symbolic model checking algorithm (forward version) Definition 3.2 (L-uniformly bounded). A system S is L-uniformly bounded if for all

Theorem 3 . 3 .

 33 Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH1 terminates, REACH1(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH1 terminates on any input iff S is L-uniformly bounded (termination). Remark 3.4. Termination for L-uniformly bounded systems does not hold if or are weak.

Definition 4 . 1 (

 41 Acceleration). A symbolic framework SF = (I, L) supports 1. loop acceleration if there exists a recursive function POST STAR : Σ × L → L s.t. ∀a ∈ Σ, ∀x ∈ L, POST STAR(a, x) = a * ( x ); 2. flat acceleration if there exists a recursive function POST STAR : Σ * × L → L s.t. ∀π ∈ Σ * , ∀x ∈ L, POST STAR(π, x) = π * ( x ); 3. global acceleration if there exists a recursive function POST STAR : RegExp(Σ) × L → L s.t. for any regular expression e over Σ, for any x ∈ L , POST STAR(e, x) = e ( x ).

Example 4 . 2 .

 42 Loop acceleration. Minsky machines support loop acceleration in frameworks where formulae in L define upward-closed sets or semi-linear sets. But upwardclosed sets (for example) are not expressive enough to support flat acceleration. Flat acceleration. Counter systems (with finite monoid) equipped with Presburger formulae supports flat acceleration [26, theorem 2]. Other examples are channel systems with cqdd [14, theorem 5.1], non-counting channel systems with slre [27, theorem 5.2] or qdd[12, theorem 6], lossy channel systems with sre [1, corollary 6.5]. Restricted counter systems used by TREX equipped with arithmetics almost supports flat acceleration [2, lemma 5.1]: their POST STAR is not recursive.

Definition 4 . 7 (Theorem 4 . 8 .

 4748 L-flattable). A system S = (Q, Σ, T, D, • ) is L-flattable iff for any x ∈ L |Q| , there exists a flattening S = (Q , Σ, T , D, • ) of S and a x ∈ L |Q | such that z( x ) = x and z(post * S ( x )) = post * S (z( x )).Prop. 4.5 extends to flattable systems: If S is a L-flattable system supporting flat acceleration, then post * S ( x ) is effectively L-definable.

Remark 5 . 3 .

 53 Termination for L-flattable systems does not hold if the symbolic framework provides only a weak inclusion (or if POST STAR returns an over-approximation).

  procedure REACH2(x0) parameter: S input: x0 ∈ L |Q| 1: x ← x0 2: while POST(x) x do 3: Choose fairly w ∈ T * 4:

  1 • t 2 • t 3 but remove t 2 • t 3 • t 1 and t 3 • t 1 • t 2 ) and commuting reduction: if t 1 and t 2 commute, i.e., if • t 2 and t 2 • t 1 (works since Conjugation reduction and commuting reduction are k-reductions. Conjugation reduction satisfies |T | = O( |T k | k). Beyond these generic reductions, it is worth developing reductions dedicated to a specific interpretation. For linear counter systems with a finite monoid,[START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] presents a reduction where |T | remains polynomial in k (while |T ≤k | is exponential). This appears to be a key reason for FAST's performances.

	t1t2 -→= t2t1 -→, then remove both
	t 1 (t1•t2) * ----→= t * 1 t * 2 -→).
	Proposition 5.6. k |V k | |T | |T |
	1 7	7	7
	2 36 21 16
	3 156 56 28 4 578 126 47 5 1890 252 86

.

  The following table compares how ALV, FAST and LASH behave in practice. "Yes" means termination within 1200 seconds on a Pentium III 933 MHz with 512 Mb. k is the length of cycles FAST considered in Procedure REACH3.

  , BRAIN, LASH and TREX, and ranging from tricky academic puzzles (swimming pool) to complex industrial protocols (TTP). (More examples are given in the full version of this paper.) They all are infinite-state and are thus beyond the scope of traditional model checking techniques and tools. Furthermore, most of these systems also go beyond VASS or Petri nets, so that methods like covering trees or backward computation do not apply. The results are for forward computation of the reachability set, on an Intel Pentium 933 Mhz with 512 Mb. Comparing them with other complex case studies analyzed with ALV, LASH, and TREX[START_REF] Annichini | TReX: A tool for reachability analysis of complex systems[END_REF][START_REF]ALV[END_REF][START_REF] Bartzis | Widening arithmetic automata[END_REF]33] confirms that flat acceleration is a powerful technique for handling infinite-state systems.

	System	var |T | sec. Mb k	System	var |T | sec.	Mb k
	CSM	13 13 45.57 6.31 2	Synapse	3 3 0.30 2.23 1
	FMS	22 20 157.48 8.02 2	Illinois	4 6 0.97 2.64 1
	Multipoll	17 20 22.96 5.13 1	Berkeley	4 3 0.49 2.75 1
	Kanban	16 16 10.43 6.54 1	Firefly	4 8 0.86 2.59 1
	swimming pool 9 6 111 29.06 4	Dragon	5 8 1.42 2.72 1
	last i.-first s.	17 10 1.89 2.74 1	Futurebus+ 9 10 2.19 3.38 1
	PC Java(2)	18 14 13.27 3.81 1	lift -N	4 5 4.56 2.90 3
	PC Java(N)	18 14 723.27 12.46 2	barber m4 8 12 1.92 2.68 1
	Central server 13 8 20.82 6.83 2	ticket 2i	6 6 0.88 2.54 1
	Consistency	12 8 275 7.35 3	ticket 3i	8 9 3.77 3.08 1
	M.E.S.I.	4 4 0.42 2.44 1	TTP	10 17 1186.24 73.24 1
	M.O.E.S.I.	4 5 0.56 2.49 1

Some weakened versions of the symbolic framework are sometimes considered. A weak inclusion ensures only that x1 x2 implies x1 ⊆ x2 while a weak union satisfies x1 ∪ x2 ⊆ x1 x2 (typical widening in abstract interpretation[START_REF] Cousot | Abstract interpretation[END_REF]). In the following, we do not consider weakened framework.

Each set of regions has its own natural measure for size, depending on data structures and implementation.

This work was supported by the ACI Sécurité & Informatique (project Persée) funded by the French Ministry of Research. System ALV LASH FAST k TTP no yes yes 1 prod/cons (2) no yes yes 1 prod/cons (N) no no yes 2 lift control, N no no yes 2 train no no yes 2 consistency no no yes 3 CSM, N no no yes 2 swimming pool no no yes 4 PNCSA no no no ? IncDec no no no ? BigJAVA no no no ?

x 0 ∈ L |Q| , post(ρ, x 0 ) is effectively L-definable. Furthermore, computing x ∈ L |Q| such that x = post(ρ, x 0 ) can be done uniformly from ρ and x 0 .

Proof. We reason by induction on ρ. If ρ = ε then x = post(ε, x ) and the property is true. Otherwise if ρ = u * • ρ 1 where u ∈ T * , then we apply the induction hypothesis to post(ρ 1 , POST STAR(u, x) ). Proof. In [START_REF] Leroux | On flatness for 2-dimensional vector addition systems with states[END_REF] it is proved that for a flat system S, there exists a semi-linear regular expression (slre) ρ over T such that for all x ∈ L |Q| , post * ( x ) = post(ρ , x ). Moreover it is proved that ρ is effectively computable. Recall that a slre over T is a regular linear expression of the form

A.3 Proof of

, where u i,j , w i,j ∈ T * . Let us define the rlre ρ over T by ρ Proof. First notice that since regions are closed by finite union ( operator), z is easily extended into z : L |Q | → L |Q| . This construction is effective. Consider a system S and x ∈ L |Q| , we enumerate all (S , z, x ) such that S is a flattening of S with folding z, and x ∈ L |Q | such that z(x ) = x (using ). For each (S , z, x ), since S is flat we can compute x such that x = post * S ( x ) (Prop. 4.5). Then we compute y = z(x ) ∈ L |Q| and check whether POST S (y) y or not. When it is the case then y is an invariant of post S . By definition of flattenings and construction of y, y is included in post * ( x ). Hence y = post * ( x ). Since S is L-flattable, such a (S , z, x ) exists and will eventually be found (even if there are finitely many (S , z, x ), they can be enumerated).

A.5 Proof of Theorem 4.9 Theorem 4.9. Assuming the symbolic framework of 2-counter systems and Presburger formulae, the question of whether a 2-counter system S is L-flattable is undecidable.

Proof. This proof is essentially as for Theorem A.1. The location reachability problem is reduced in the same way. Notice that q is reachable iff S 1 is L-flattable (If q is reachable, compute N 3 on q then use each new transition once to propagate N 3 on every location q ∈ Q ∪ Q 1 ; otherwise post * S1 (c) is not L-definable for any c, then S 1 cannot be L-flattable). Proof. Given x ∈ L |Q| , if there exists a rlre ρ x such that post * S ( x ) = post S (ρ x , x ), we deduce naturally a flattening S X of S (intuitively the uninterpreted system of S X is the automata recognizing the language ρ X ⊆ T * ).

Let us prove the converse. Let us assume that S is L-flattable. By definition there exists a flat system S , a flattening z and x such that z( x ) = x and z(post * S x ) = post * S ( x ). Moreover we can build effectively (S , z, x ) by enumeration (see proof of Theorem 4.8). Since S is flat, using the proof of Prop. 4.5 we deduce that there exists ρ a rlre over T verifying post * S ( x ) = post S (ρ , x ). We denote ρ = z(ρ ). By definition of flattening, ρ is a rlre over T (each transition of a flattening corresponds to a transition in the original system, the property extends to sequences and languages). By reasoning on sequences of transitions and then languages, we can prove that for any L ⊆ T * , z(post S (L, x )) = post S (z(L), z( x )). We then deduce that z(post

Hence there exists x such that z( x ) = x and post * S ( x

A.7 Proof of Theorem 5.2 Theorem 5.2. Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH2 terminates, REACH2(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH2 terminates on any input iff S is L-flattable (termination).

Proof. Partial correctness: straightforward from the definition of POST STAR and . Termination: first remark that if REACH2 terminates it returns the fixpoint, since computations in our procedure are always under-approximations of the reachability set. The finite sequence of selected w ∈ T * during the successful computation provides a rlre ρ over T * such that post * ( x ) = post(ρ, x ). Thus if REACH2 terminates for all input, then S is L-flattable (Theorem 5.1). Assume now that S is L-flattable, and consider x 0 ∈ L |Q| . There exists a rlre ρ over T * such that post * ( x 0 ) = post(ρ, x 0 ) (Theorem 5.1). Let us denote ρ = u * 1 . . . u * n . Since Choose is fair, the sequence ρ of w selected by choose will eventually be of the form ρ = w * 1 . . . w * m where there exists i 1 , . . . , i n such that w i1 = u 1 , . . . , w in = u n . It will eventually be the case because all w ∈ T * are repeated infinitely often thanks to fairness condition. Moreover the identity relation being contained in each step of acceleration, each step of computation contains entirely the previous step. Then we get that post(ρ, x 0 ) ⊆ post(ρ , x 0 ) ⊆ post * ( x 0 ) (remember we can only compute under-approximation). Since post * ( x 0 ) = post(ρ, x 0 ), we get that post * ( x 0 ) = post(ρ , x 0 ) and the computation will stop at that stage (returning the fixpoint).

A.8 Proof of Theorem 5.4

Theorem 5.4. Given a symbolic framework SF = (I, L) and a system S ∈ F(I) 1. when REACH3 terminates, REACH3(x 0 ) = post * ( x 0 ) (partial correctness); 2. REACH3 terminates for any input iff S is L-flattable (termination).

Proof. Partial correctness: straightforward from the definition of POST STAR and . Termination: fairness of Choose on T ≤k and Watchdog, and re-using computations of each previous task k-flattable ensure fairness of Choose on T * . Then we use the same arguments than for theorem 6.2.

A.9 Proof of

B Practical use of flat acceleration: FAST

The following table extends the table from section 6.2. All examples are infinite-state, except those in the Bounded Petri Nets category.

The results are taken from forward computation of the reachability set, using an Intel Pentium 933 Mhz with 512 Mb. In the following table, |T | is the number of transitions, |A| is the size of the binary automaton that represents the reachability set (in FAST, the regions are binary automata). |w| is the length of the rlre computed so far, k is the maximal length of cycle (T ≤k ), the number of cycles is given after reductions (commuting transitions and specific reduction of section 5.2). We aborted all computations after 1800 seconds.

In principle there can be several reasons why FAST does not terminate: (1) the reachability set is not Presburger definable, (2) the system (with given x 0 ) is not L-flattable, (3) the monoid of the system is not finite and our techniques on counter systems do not apply, (4) time and space consumption are too high. Even if it is always difficult to pick one of these explanations when experiment fails, it seems that, on these examples, the main reason for failure is (4). We can rule out (3) in most cases since they are variants of VASS (with zero test or reset) for which finiteness of the monoid is guaranteed [START_REF] Bardin | FASTer acceleration of counter automata[END_REF].


Khaoula Tabet
email: tabetkhaoula@gmail.com

Riad Mokadem
email: riad.mokadem@irit.fr

Mohamed Ridda Laouar

A data replication strategy for document-oriented NoSQL systems

Keywords: cloud environment, NoSql databases, data replication, provider profit, performance

Cloud providers aim to maximise their profits while satisfying tenant requirements, e.g., performance. The relational database management systems face many obstacles in achieving this goal. Therefore, the use of NoSQL databases becomes necessary when dealing with heterogeneous workloads and voluminous data. In this context, we propose a new data replication strategy that balances the workload of nodes and dynamically adjusts the number of replicas while the provider profit is taken into account. Result analysis shows that the proposed strategy reduces the resource consumption, which improves the provider profit while satisfying the tenant performance requirement.

Introduction

The elastic management of voluminous and heterogeneous data is one of the most important research areas in cloud computing [START_REF] Hameurlain | SPECIAL ISSUE, Elastic Data Management in Cloud Systems[END_REF]. Companies have turned to cloud environments to host their applications and databases. They expect cloud providers to keep a certain agreed upon of set Service Level Objectives (SLO), e.g., performance, defined in a Service Level Agreement (SLA) [START_REF] Stantchev | Negotiating and enforcing QoS and SLAS in grid and cloud computing[END_REF], a contract between a provider and its tenants, while the 'pay as you go' model is considered [START_REF] Armbrust | A view of cloud computing[END_REF].

Data replication is an important technique that ensures availability and fault tolerance while the system performances are improved. It consists of having many copies of the same data across multiple servers [START_REF] Tabet | Data replication in cloud systems: a survey[END_REF]. Data replication is frequently used in: (i) Database Management Systems (DBMS) [START_REF] Perez | Branch replication scheme: a new model for data replication in large scale data grids[END_REF], (ii) parallel and distributed systems [START_REF] Loukopoulos | Continuous replica placement schemes in distributed systems[END_REF][START_REF] Benoit | Replica placement and access policies in tree networks[END_REF], (iii) mobile systems [START_REF] Tu | Replica placement algorithms for mobile transaction systems[END_REF] and (vi) large scale systems including P2P [START_REF] Xhafa | Data replication in P2P collaborative systems[END_REF] and data Grid systems (Mansouri et al., 2014). However, the existing proposed strategies are not adopted in cloud systems. They aim to obtain the best performance without taking into account the profit of cloud providers that aim to maximise their profits. This motivates the proposition of several data replication strategies in cloud systems, [START_REF] Wei | CDRM: a cost-effective dynamic replication management scheme for cloud storage cluster[END_REF][START_REF] Sakr | Sla-based and consumer-centric dynamic provisioning for cloud databases[END_REF][START_REF] Xue | Replica placement in cloud storage based on minimal blocking probability[END_REF][START_REF] Tos | A performance and profit oriented data replication strategy for cloud systems[END_REF]. Relational database management systems face many obstacles in achieving those needs. Therefore, the using of NoSQL databases becomes necessary over the last few years, especially when dealing with voluminous and heterogeneous data. One of the most known NoSQL systems is MongoDB [START_REF] Chodorow | MongoDB: The Definitive Guide: Powerful and Scalable Data Storage[END_REF] which is considered as the leading document store.

To the best of our knowledge, most of existing works in the literature focus on obtaining high performances by using different data replication strategies that are used through useful data placement and load balance. Some works have focused their attention on the improvement of auto-sharding, load balance, and auto-scaling algorithms, e.g., [START_REF] Liu | Research on the improvement of MongoDB Auto-Sharding in cloud environment[END_REF][START_REF] Gu | Analysis of data replication mechanism in NoSQL database MongoDB[END_REF][START_REF] Mohamed | A New Auditing Mechanism for Open Source NoSQL Database a Case Study on Open Source MongoDB Database[END_REF]. Other works analyse the differences of Mongo's data model, query and replication model with relational database management systems, e.g., [START_REF] Lima | An evaluation of data replication for bioinformatics workflows on NoSQL systems[END_REF][START_REF] Mansouri | Weighted data replication strategy for data grid considering economic approach[END_REF]. Many of these works are trying to take a closer look to performance by comparing capabilities of MongoDB with other NoSQL systems, e.g., performance comparison between MongoDB and Cassandra in [START_REF] Haughian | Benchmarking replication in cassandra and mongodb nosql datastores[END_REF]. Results show that MongoDB provides better performance. However, most of these works focus only on the improvement of system performance. For example, all replicas are read-only and are updated only from the master node in the master-slave replication model. This can cause problems when a master node fails down. To overcome this problem and guarantee the system performance, the replica set model was proposed. It overcomes the fail of a primary node by auto scheduling. Then, it offers an automatic system load balance which achieves performance [START_REF] Chodorow | MongoDB: The Definitive Guide: Powerful and Scalable Data Storage[END_REF]. However, replication costs, SLA violation and provider profit issues are neglected.

In this paper, we propose a new data replication strategy for MongoDB NoSQL databases. The proposed strategy aims to ensure both system performance for the tenant and a profitability for the cloud provider. A replication of a document is considered only if two conditions are satisfied simultaneously: (i) the estimated response time of a tenant query, before its execution, is greater than a response time threshold (RespT) agreed in SLA and then, (ii) if this replication occurs, the provider should have an economic profit.

Dealing with the MongoDB query response time estimation, we take into account the most important parameters that impact the query execution, e.g., data size, number of shards, I/O and Network Bandwidth (NB). When data replication is considered, only popular data, i.e., having a high access frequency during a period of time, that are situated in overload nodes are replicated. Thus, the workload of nodes is balanced, which affects the system performance. The proposed replication strategy is also based on a geographical [START_REF] Chodorow | MongoDB: The Definitive Guide: Powerful and Scalable Data Storage[END_REF] and NB level [START_REF] Park | Dynamic data grid replication strategy based on Internet hierarchy[END_REF] localities in order to place new replicas closer to data consumers and reduce the communication costs respectively, when replicating data. Furthermore, the number of replicas is adjusted dynamically in order to reduce the resource consumption, i.e., the least popular data replicas are removed. Finally, in order to take into account the provider profit, we estimate the revenues and expenses of the provider when dealing with data replication. The provider should have a real profit when considering this replication.

In order to validate the proposed strategy, we compared it to the already existing replication strategy in MongoDB. The results show that the proposed strategy provides better response times while the provider profit is taken into account. The organisation of the rest of the paper is as follows: Section 2 provides a summary of replication mechanisms in MongoDB. Section 3 details of the proposed replication strategy. Section 4 contains the performance evaluation of the proposed strategy. Finally, we conclude the paper and give some future work.

Background

MongoDB

MongoDB is an open source document-oriented NoSQL database system developed by 10gen in 2007 [START_REF] Membrey | The Definitive Guide to MongoDB: the noSQL Database for Cloud and Desktop Computing[END_REF]. It manages collections of BSON documents, provides high performance, high availability, easy scalability through replication and auto-sharding. The main concept in MongoDB is the documents that present the unit of data for MongoDB. It is equivalent to a row in a RDBMS and a collection can be equivalent to a relation [START_REF] Membrey | The Definitive Guide to MongoDB: the noSQL Database for Cloud and Desktop Computing[END_REF]. There are different replication mechanisms in MongoDB. We distinguish two models: the Master/Slave and the Replica set replication models. The main difference between them is that a replica set has the ability to an automatic failover when primary node is unavailable by electing new one from existing secondary nodes situated in the same cluster. In a master-slave replication model, all replicas are read-only and updated only from the master node after changes, which can cause problems. When the master node fails down, there is no possibility to write new data. Thus, the most suitable model for replication in MongoDB is the replica set model.

In addition to the replication mechanism, MongoDB uses another mechanism called sharding. Sharding is the process of splitting data uniformly across clusters to parallelise the access of data. But, it cannot ensure fault tolerance. In case a shard fails down, the data stored on that shard become unavailable. At the same time, the system is still able to operate even if some parts of data are missing. Therefore, we combine sharding with replication in the proposed strategy because some systems require high availability, and high fault tolerance such in the new generation of cloud-based computing platforms. By replicating each shard, in case a replica fails down, another replica can replace it. Then, the system becomes more failure tolerant. Moreover, a replica set's different members have the same documents, while different shards have different documents [START_REF] Rao | Sharded Parallel Mapreduce in Mongodb for online aggregation[END_REF] as shown in Figure 1.

Cloud architecture

Dealing with the considered cloud architecture, we consider a topology, i.e., composed of several geographical Data Centres (DCs). Let DC a set of data centres such as DC = {DC 1 , DC 2 ,..., DC n }, linked together through a high NB. Each data centre Dc i contains a set N of m nodes realised as Virtual Machines (VMs) with N = {N i1 , N i2 ,... N im }, as shown in Figure 3. Each node resides on physical hosts and has specific characteristics related to computing, storage and memory capacities, and network connectivity in order to achieve the execution of submitted queries. This leads to a system topology with two levels: DCs and nodes that host data. DCs and nodes are interconnected via hierarchy network bandwidths. DCs are connected via the internet with a low NB when the links between nodes across Dc i have moderately higher NB compared to the first level.

Proposed data replication strategy

An existing data replication mechanism is already supported by MongoDB. It allows to having an automatic failover and loading balance while the main purpose is to obtain a high fault tolerance in case of a primary (master) node crash. In this paper, we propose a novel MongoDB data replication strategy in order to obtain better performance while maximising the provider profit.

The aim of any data replication strategy is to determine what data should be replicated, when a replica should be created/deleted, how many replicas to create and where to place a new replica [START_REF] Mokadem | Data replication strategies with performance objective in data grid systems: a survey[END_REF]. In cloud environments, another issue is considered. A proposed replication strategy should also be profitable to the provider while tenant objectives are satisfied. We deal with all these issues in the next subsections.

When to replicate

The decision of the replication event depends on the verification of two conditions: (i) a response time is greater than a response time threshold and (b) a replication should be profitable to the provider.

Before the execution of each query Q, we estimate the response time of Q (RespQ) and compare it with the response time threshold RespT defined in SLA. In case RespQ is greater than RespT, some required datasets may be required to be replicated. As long as the provider is still estimated to be profitable, replication event is triggered as shown in the replica decision algorithm (Algorithm 1).

Algorithm 1 Replication decision algorithm

Response time estimation

The provider is based on response time estimation in order to decide whether to replicate data or not to meet the tenant requirement.

The parallelisation of tasks is one of the most important characteristics when using cloud computing. We benefit from several existing relational database studies, e.g., [START_REF] Özsu | Principles of Distributed Database Systems[END_REF][START_REF] Tos | Réplication de Données Dans les Systèmes de Gestion de Données à Grande échelle[END_REF], to propose a response time estimation model that is suitable for our proposed strategy. Estimating a query response time is based on resource consumption when executing this query. Traditionally, we distinguish two types of parallelism: intra-operator and inter-operator parallelism in order to process large amount of data and to improve performance.

In this paper, we focus on response time estimation for a query that have no dependent operations. In fact, most of NoSQL systems do not use the join operator. Precisely, classical MongoDB search queries are without joins. In consequence, we focus on the intra-operator parallelism that consists in the parallel execution of several operators executed on several cloud sites. Then, the result consists in the combination of the generated results from each site. Recall also that we are not discussing here how the sharding is done in MongoDB [START_REF] Özsu | Principles of Distributed Database Systems[END_REF]. There may be response variation between the execution of an operator on different shards because of individual hardware resources, memory, CPU etc.

Suppose that a tenant query Q is submitted to a cloud that contains several data centres, each one containing a number of nodes. Assume now that Q is delegated to a given node that should return a result to the tenant.

Q may be executed on several nodes and multiple shards. Let Q a tenant query that consists of several sub-queries Q={Q 1 , Q 2 ,...,Q i ,...,Q k } that are executed in parallel on k shards. Let Q i a sub-query that requires a collection C n . Suppose that the collection C n is splitted into l chunks as C n {C n,1 C n, 2 ,..., C n, l }, with replicas on j sites. In this case, we refer to this sub-query by Q j i,k .

The estimated response time of the submitted query is calculated as the sum of: (i) the longest estimated time it takes for Q Q j i,k , (ii) transfer time T Tr for transferring data between shards. The intermediate results are transferred from all the concerned shards to a final destination and (iii) produce time T pr for producing the results, e.g., an union operator is applied for grouping horizontally fragmented collections, and outputs, e.g., storing the results. The response time for the execution of the query RespQ is shown in the following equation ( 21 ,

j CPU j I O j i k i k i k Com j i k Resp Q Max T Q T Q T Q (2)
Estimated CPU time: The time related to CPU depends on how much time is spent when processing an operator, i.e., view as a number machine instructions executed on different shards for a unit amount of data. The estimation of a CPU time for the sub-query

Q j i,k is depicted in equation (3). , * # * 1 CPU j CPU i k T Q T Inst a (3)
with T CPU , is a time of a CPU instruction, and a >0 a weighting factor, including CPU hardware capabilities, e.g., the processing rate and caching capabilities on a node that influences query engine performance. (5)

Provider profit estimation

Most of existing replication strategies in the cloud aim to achieve better performance without considering the provider profit [START_REF] Tos | A performance and profit oriented data replication strategy for cloud systems[END_REF]. In our strategy, replication of a collection is considered only if a provider has an economic profit. In this context, we need to estimate both revenues and expenditures of the provider when executing Q that deals with data replication. From the provider point of view, the profit for executing Q (Profit Q ) is estimated as shown in equation ( 6).

Q Q Profitq Revenues Expenses (6)
All providers aim to maximise revenues paid by tenants.

Usually, the purpose of any cloud provider is to obtain much more gain, i.e., profit. This justifies the parallel query execution. Also, expenditures of the provider must be minimised. But in case of an SLA breach, the provider pays a penalty to the tenant. Hence, an interesting challenge consists to avoid the penalty cost paid by the provider to the tenant for not satisfying a given SLO. Then, the profitability of cloud providers is based on the minimisation of expenses caused by the agreements violation.

Revenue estimation: A tenant is not billed for the number of replicas required when its query is executed, i.e., this process is transparent for the tenant. However, a tenant has to periodically pay the provider for the computing time, operational cost and resources allocated when processing its query.

As proposed in Tos (2017), a per query revenue estimation depends on the maximum query arrival rate Max_AR and the duration of the Billing Period (BP), already specified in the SLA. It also depends on the amount of rent (Rent) that tenant pays to the cloud provider for the services acquired during a BP.

Expenditures estimation: Evaluating a query Q generates operational costs that are impacted by different parameters. Let Cost_t be a cost by unit of time u for using a node allocated to the Q evaluation [START_REF] Sousa | Towards elastic multi-tenant database replication with quality of service[END_REF], T_Q the estimated total time needed to evaluate Q, Nodes_Nber the number of the required nodes when evaluating Q during u, Netw_cost the cost of the NB usage including data migration from one node to another when creating a replica, Stor_cost the cost required to store replicas in disks. On the other hand, the provider pays a penalty to the tenant in case of an SLA breach. Hence, provider expenditures should include these penalties. In formula (7), the penalties paid from the provider to this tenant when one/several SLO i is/are not satisfied is also considered [START_REF] Tos | Ensuring performance and provider profit through data replication in cloud systems[END_REF]. The estimation of the provider expenditures when evaluating

Q (Expense Q ) is shown in formula (7). _ _ * _ _ _ Nodes Nber Q Expense I T Q Cost t
Netw cost Stor cost penalties (7)

What data should be replicated?

In case we found that an estimated response time of Q (RespQ) is greater than RespT, we have to select data that should be concerned by the replication. In the proposed strategy, we based on the access frequency of each dataset during a period of time, from the arrival time to actual time. This consists to select the dataset that has the highest popularity degree.

According to [START_REF] Mansouri | Weighted data replication strategy for data grid considering economic approach[END_REF], the access frequency of each file is analysed by considering the number of times the file was accessed during a given time interval. Here, the file with a greater value of Access Frequency is selected as the popular file. The Popularity Degree (PD) of a dataset d is to be calculated using formula (8) [START_REF] Sun | Modeling a dynamic data replication strategy to increase system availability in cloud computing environments[END_REF] When analysing the data popularity, only the popular dataset is replicated. We only replicate data that popularity exceeds PDT, with the PDT the PD threshold agreed on SLA. Therefore, it is not necessary to create replicas for all datasets, especially for less accessed files.

Algorithm 2 Selection of a dataset concerned by replication

The second criterion that we based on is the node workload Load. We consider the replication of data situated on overload nodes. Besides some particular data are accessed much more frequently than others, the load on nodes that hosts data will be augmented which can affect the system performance. To overcome this problem, we select data situated on an overload node and then, we place them in another node that is not overloaded. A workload of a particular node presents the amount of work, i.e., required to do. The definition of a node being overloaded can be given as follows: for each node N ip , we can have its load denoted as Load(N ip ), that depends on both computing and network capacities of N ip . In case we found that Load(N ip ) is bigger than LoadT, we declare that the current node N ip is overloaded. LoadT is the threshold load agreed in SLA as a result, we replicate sets of frequently used data in this node in order to decrease the workload of N ip as shown in Algorithm 2.

Where to place new replicas

When the estimated response time for a query, submitted on N ij DC i , is greater than RespT, we select data to be replicated such as RespQ < RespT. For this aim, we need to find the appropriate node to hold the new replica as shown in Algorithm 3. We profit from the NB level locality to place replicas in nodes that have a good NB with N ij . In consequence, the search of the replica placement node NFound should be done in the current DC. The selected node should also have enough storage space and not overloaded. This constitutes the first condition. The second condition consists in the fact that the provider should also have a profit when replicating data on this node. The profit of the provider is checked before executing a query that uses the concerned replica. Finally, if there is a real profit, the new replica is really placed on NFound.

Algorithm 3 Replica placement algorithm

If one of these two conditions is not satisfied for all nodes on the current DC, the search is done in other DCs so that we find the appropriate node. Firstly, we search the DC that has the best bandwidth to the DC that holds the dataset to be replicated. If the response time objective is not satisfied, the search is applied on the DC that offers the best storage prices. Of course, the searched node should have the storage possibility to hold a new replica and it should not be overloaded, i.e., the load should be less than LoadT.

Replica number adjustment

Cloud providers aim to satisfy the tenant requirements while maximising its benefits. For this aim, it should minimise expenditures when executing the tenant queries. We consider an elastic resource management that consists to remove all unrequired resources, i.e., replicas that are not required should be removed. This reduces the provider expenditures and then, increases the provider profit.

Let Q a submitted tenant query in DC i . For each node N ij , we save the history of data (replicas) access. When the estimated RT on N ip , is significantly slower than RespT, i.e., RespQ ip <<RespT, we estimate the popularity degree of each chunk of data, e.g., a replica Ri. We select replicas that have PD lower than PDT. Then, we delete it to gain more storage space as shown in the replica deletion algorithm (Algorithm 4).

Algorithm 4 Replica deletion algorithm 4 Performance evaluation

Simulation environment

In order to evaluate the impact of our proposed replication model on the performance of MongoDB, we used the Yahoo Cloud Serving Benchmark (YCSB), i.e., an open source development tool for evaluating the performance of different cloud data stores including Nosql systems, e.g., MongoDB [START_REF] Abubakar | Performance evaluation of NoSQL systems using YCSB in a resource austere environment[END_REF]. First, we evaluate and explore the performance of MongoDB when using the already existing replication mechanism. Then, we apply our proposed replication strategy in order to compare the obtained results. This evaluation is done in a single tenant environment, where its specifications and settings are indicated in Table 1.

Evaluation of existing MongoDB data replication strategy with different scenarios

For benchmarking purposes, we have to define a set of workloads that are used on MongoDB. In the context of YCSB, a workload contains a set of core workloads that define a basic benchmark for cloud systems. In our experiments, we used six different workloads, each one consists of 1,000 operations on 1KB records (10 fields, 100bytes each with default key) already loaded into a database. Table 2 shows the description of the tested workloads. Two metrics are measured: throughputs (in operations/s) and total execution time (in ms). Besides the throughput can be defined as a measurement that is used to determine the performance of a database system, it presents the amount of transactions produced over time during a test. On the other hand, the response time is the amount of time from the moment that a tenant sends a query until the application indicates that the query has completed with all results (http://searchnetworking.techtarget.com).

Figure 2 represents the obtained results when experimenting with each workload described in Table 2. We remark that the performance of MongoDB is more efficient when executing read only operations (workload C). This strengthens our choice of applying our strategy with read only operations, especially since the aim is to improve performances through data replication. Hence, we evaluate the proposed replication strategy when dealing with read only operations. This is why our strategy is proposed for OLAP applications.

Result analysis of the proposed strategy

Our main aim is to show that the proposed strategy improves the system performance while the provider profit is taken into account. We used Mongo java API to interact with MongoDB. Then, we added.jar files to netbeans IDE project (version 8.0.2) to have a java Mongo connection. After the implementation of the proposed replication strategy, first experiments consist to submit parallel read queries with several simulated workloads. We note the obtained execution time with the reading of 10, 100, 1,000, 10,000, 100,000 and 1,000,000 records in a collection. Recall that with the proposed strategy, the replication event is triggered only if the estimated response time is bigger than a response time threshold. We specified a response time threshold as 5,500ms for each query. Then, the replication should be profitable for the provider. Throughout the following experiments, we deal with two important metrics: (i) the response time and (ii) the number of replications. Recall that the response time is the amount of time from the moment that a tenant sends a query until the production of the first results [START_REF] Özsu | Principles of Distributed Database Systems[END_REF]. Figure 3 shows the variation of the response time with the two compared replication strategies while varying the workload. With a reduced number of queries, a slightly more important number of replicas are created by the existing replication strategy in MongoDB. But in contrast, the compared strategy doesn't take into consideration the profits of the provider. Fewer replications are required with our strategy since the response time is inferior to the response time threshold. Then, there is a marked disparity when the workload increases. Gradually, when we have more loads, subsequently more replications occur with our strategy in order to avoid the SLA breach. This is due to the fact that a replication is triggered each time the estimated response time is greater than a response time threshold. This responds to the aim of cloud providers. In fact, the provider profit should be maximised through the minimisation of SLA violation while the SLO response time is satisfied. Figure 4 shows the response time values obtained when experimenting with the two data replication strategies. With a small number of queries, we obtained a similar response time with both strategies. The response time of the proposed strategy is better when dealing with more than 100 parallel read queries. With a high load, it is clear that our replication strategy produces less important response times. Response time values of the proposed strategy should be inferior to the response time threshold. Otherwise, a data replication is triggered. This explains why we have a more important replications with the proposed strategy. Hence, we have better response time values with the proposed strategy. On the other hand, each time the compared replication strategy exceeds the response time threshold we have a SLA violation. In consequence, the provider should pay a penalty to the tenant when there is no penalty to pay with the proposed strategy. In consequence, the provider profit is maximised.

Furthermore, an elastic replica management is considered. The proposed strategy avoids unnecessary replications by removing replicas when these replicas are not required. This decreases both the storage and bandwidth consumptions while the already existing replication in MongoDB consumes more resources, i.e., more replicas. In the existing MongoDB balance algorithm, data are splitted and distributed unevenly among different shards. However, data distribution will directly affect the system performance [START_REF] Hamrouni | Impact of the distribution quality of file replicas on replication strategies[END_REF]. In order to solve this problem, the authors in [START_REF] Liu | Research on the improvement of MongoDB Auto-Sharding in cloud environment[END_REF] propose an improved algorithm named Frequency of Data Operation (FODO) that takes into consideration the load of servers and the frequency of data operations. The proposed algorithm can balance the data among shards, which improves the cluster's operations (read and write) performances. [START_REF] Gu | Analysis of data replication mechanism in NoSQL database MongoDB[END_REF] analyse different existing mechanisms of replication already used in MongoDB. The authors gave a profound explanation and description of the two used models of replication: Master/ slave and replica-set models. An interesting study [START_REF] Lima | An evaluation of data replication for bioinformatics workflows on NoSQL systems[END_REF] has been conducted to evaluate the impact of biological data replication on MongoDB and Cassandra. Some setting in the cluster and replication factors can certainly affect the results. Results showed an improvement in the data availability, but a loss in system performance and the impact of the replication factor on the execution time was higher. [START_REF] Haughian | Benchmarking replication in cassandra and mongodb nosql datastores[END_REF] evaluate and examined the impact on performance when using or not the replication under different levels of workloads and consistency. They experimented with MongoDB and Cassandra NoSQL data stores. Using benchmarking experiment's results, they affirm that replication and consistency have a direct impact on system performance. [START_REF] Tauro | A comparative analysis of different nosql databases on data model, query model and replication model[END_REF] present a comprehensive analysis of different existing NoSQL data stores, including MongoDB, and their features. Basing on the data model, querying, and replication model, this research provides knowledge for tenants to choose the appropriate NoSQL database.

When analysing different existing propositions that deal with replication mechanisms in MongoDB, we remark that most of them focus their attention on evaluating and benchmarking replication. Further researches gave a performance comparison between MongoDB and other popular NoSQL systems, as well as relational database management systems. However, no one of them draw attention to the replica management in MongoDB when used as the back-end by a cloud service provider. Furthermore, they neglect the provider profit. In this paper, we dealt with replica management in MongoDB in order to ensure both system performance and profitability of the cloud provider.

Conclusion

We propose a new data replication strategy for MongoDB, a document oriented NoSQL database Engine. The main aim of the proposed strategy is to satisfy the performance requirement for the tenant while the provider profit is taken into account. The replication is triggered only if the estimated response time of a submitted tenant query Q is greater than a response time threshold defined in the SLA. Then, the replication must be profitable for the provider when a replication is considered. We based on the estimation of: (i) the response time of Q before its execution, and (ii) both revenues and expenditures of the provider when considering data replication. Then, the most popular data is replicated on the less loaded node. Furthermore, existing replicas that have the lowest popularity are dynamically removed in order to decrease the resource consumption which increases the provider profit. We evaluated the proposed strategy through an experimental evaluation. We compared the actual existing replication strategy in MongoDB with our proposed strategy in term of response time and number of triggered replication. The obtained results confirm that the proposed strategy provides better results when considering simultaneously the tenant response time satisfaction and the provider economic profitability. As a future work, we intend to extend the proposed replica creation decision process by accepting to lose some profit when the provider executes queries of an important tenant within a multi-tenant environment. This should be advantageous for the provider within a long period with a condition that the provider will make again a profit with the same tenant afterwards. Also, we plan to implement the proposed strategy in a real cloud environment.

Figure 1

 1 Figure 1 Replication and sharding in MongoDB

  calculate the response time of the operator, i.e., executed on each shard in parallel , necessary to evaluate the amount of time contributed by computing resources, including CPU, disk I/O and communication times as shown in the following equation: / , , ,

Figure 2

 2 Figure 2 Query execution results under different scenarios

Figure 3

 3 Figure 3 Impact of the proposed strategy on MongoDB performances

Figure 4

 4 Figure 4 Number of replications

  IO r and IO ip the average I/O disk throughputs on a remote node and N ip , respectively (in bytes/s) including randomly and sequentially access to a page. Hence, the estimated I/O cost of Q j i,k (in sec) on N ip that require local documents and n remote documents is given by:

	T	/ I O	Q	j	, i k	n r	1	/ Sd IO Sd IO / r r l ip	(4)
	Estimated communication time: When a MongoDB query
	can require remote documents, the communication costs
	should be taken into consideration. This represents the time
	spent when transferring documents between nodes. We need
	to estimate the migration time of remote documents d , 1 / n j Com i k r ip r T Q sd NB

Estimated input / output time: Q may require document d l from a local node N ip (1 i m, 1 p n) and/or from a number r' of remote document d r distributed on remote nodes (d r may constitute intermediate results). Let Sd l the size of total local documents (in bytes) required on N ip , Sd r the size of remote documents ( remote node) required for the Q processing (in bytes), r into the local node. Let NB ip the average NB to N ip (in bytes/s). The estimation of a transfer time for Q j i,k that requires n remote documents d r is depicted in equation (

5

).

  . , t p , present respectively the start time and the present tim, an k (t i , t i+1 ) the number of access to d during the interval [t i , t i+1 ] and w(t i , t p ) a time-based forgetting function (w) with values within the interval [0, 1]. It is used to calculate the PD of a block of data at the present time t p basing on access frequency at the start time t s .

	d PD	p i t t t	s	, 1 i i an t t k	*	, i p w t t	(8)
	when t s

Table 1

 1 Machine specifications and settings

	Setting	Value
	OS	Ubuntu 16.04 LTS
	Word length	64-bits
	RAM	8GB
	Hard disk	1TB
	CPU speed	1.70GHz
	YCSB version	0.5.0
	Core	5