des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Danish IT Policies and Strategies Experience and Issues

Kim Østrup

Formerly IBM, Denmark Kim@Ostrup.com

Summary

Since the beginning of the 90s the Danish government has appointed a number of committees to formulate IT policies and strategies for the Danish society in general and for different sectors. The focus will be on the 3 main reports.

Experiences

The reports have created awareness for Information Technology but the specific recommendations have only to a limited extent been adopted by the ministry responsible for implementation. The three policy reports all have a strong focus on education, health and e-government, but there has been no ownership in the ministries for the proposed policies and strategies.

The creation of the Digitalizing Agency (Digitaliseringsstyrelsen in Danish) has fostered a new era of administration policy with specific plans and milestones to increase cost efficiency by use of ICT in the public sector. It's interesting to note that with a few exceptions it has been difficult to find funding models to finance shared infrastructures and to agree on common open standards and open architectures.

The Achilles Heel in the Public Sector is the many IT projects, which do not meet target dates, have overrun budget or do not perform according to the business case. It seems that the procurement and project model have significant systemic flaws.

Politically, the Nyrup Rasmussen Government had a strong focus on the information society, whereas the Fogh Rasmussen / Løkke Rasmussen Government had few ICT initiatives (welfare technology) other than making public administration more efficient. The Thorning-Smith Government has continued this trend but has adopted new legislation e.g. mandating electronic communication between government and citizens/companies. This government recently established a growth team for ICT which presented their report in January 2014.

Surprisingly, the Government's Productivity Commission has not yet addressed the ICT potential to increase productivity directly. Nevertheless Denmark scores extremely high in international surveys on different aspects of ICT and society.

  1. "The Information Society 2000". This report was published in 1996 and covered the main sectors of the society. It was inspired of the US notion of "Super information highway" and was probably the first comprehensive government report dealing with the networked societyeven before the Internet was widely used. The report recommends principles for applying IT in the different sectors of government and for specific initiatives. 2. "Digital Denmark". The report was published in 2001 and formulates a number

objectives and initiatives in the areas of: Life long learning for all; Denmark as an E-commerce nation; More effective and cheaper service via digital administration; Danish Internet initiatives; and Creation of IT lighthouses in Denmark. 3. "The High-Speed Committee". The committee delivered its report in 2010 and addresses political ownership and stresses that the gap in the public sector between what can be done and what is actually done is increasing. It has recommendations for: Digitalizing of the public sector; Cloud computing; Environment, climate and green IT, and R&D in IT; Broad Band infrastructure in Denmark.


Sebastian Brand

Gregory J Duck

Jakob Puchinger

Peter J Stuckey

Flexible, Rule-based Constraint Model Linearisation

Nonlinear constraint satisfaction or optimisation models need to be reduced to equivalent linear forms before they can be solved by (Integer) Linear Programming solvers. A choice of linearisation methods exist. There are generic linearisations and constraint-specific, userdefined linearisations. Hence a model reformulation system needs to be flexible and open to allow complex and novel linearisations to be specified. In this paper we show how the declarative model reformulation system Cadmium can be used to effectively transform constraint problems to different linearisations, allowing easy exploration of linearisation possibilities.

Introduction

The last decade has seen a trend towards high-level modelling languages in constraint programming. Languages such as ESRA [START_REF] Flener | Introducing ESRA, a relational language for modelling combinatorial problems[END_REF], Essence [START_REF] Frisch | The design of ESSENCE: A constraint language for specifying combinatorial problems[END_REF], and Zinc [START_REF] Garcia De La Banda | The modelling language Zinc[END_REF] allow the modeller to state problems in a declarative, human-comprehensible way, without having to make subordinate modelling decisions or even to commit to a particular solving approach. Examples of decisions that may depend on the target solver are: the representation of variables of a complex type such as sets or graphs, and the translation of constraints into those provided by the solver to be used. Such decisions need to be taken if a concrete solver such as Gecode, ILOG Solver, CPLEX or Eclipse is to be used directly.

The problem solving process is thus broken into two parts. First, a highlevel, solver-independent, conceptual model is developed. Second, the conceptual model is mapped to an executable version, the design model. Typically, an iterative process of solver selection, model formulation or augmentation, and model transformation, followed by experimental evaluation, is employed.

An imbalance exists in how the steps of this process are supported in practice. For the task of model formulation, there are well-designed, open, high-level modelling languages. In contrast, the task of model transformation is typically done by fixed procedures inaccessible to the modeller. It is hard to see that there is a single best set of transformations that can be wrapped and packed away. We therefore conclude that a strong requirement on a model transformation process and platform is flexibility.

In this paper we describe how we transform high-level models written in the modelling language MiniZinc [START_REF] Nethercote | Mini-Zinc: Towards a standard CP modelling language[END_REF] (a subset of Zinc) into Integer Linear Programming (ILP) models. The transformations are written in our term-rewriting based model transformation language Cadmium [START_REF] Duck | ACD term rewriting[END_REF]. The rules and transformations are directly accessible to the modeller and can be freely examined, modified, and replaced. A major strength of Cadmium is its tight integration with the Zinc modelling language. The rules operate directly on Zinc expressions; as a result, transformations are often very compact and comprehensible. Another strength of the approach is easy reusability. For example, in the linearisation of MiniZinc models we reused transformations originally designed for transforming MiniZinc models to FlatZinc (a low-level CP solver input language).

Our computational experiments, where MiniZinc models are transformed into CPLEX LP format, demonstrate the advantages of our system. It allows the user to experiment with different ways of linearising logical constraints as well as high-level constraints such as all different [START_REF] Mckinnon | Constructing integer programming models by the predicate calculus[END_REF][START_REF] Refalo | Linear formulation of constraint programming models and hybrid solvers[END_REF].

2 Languages and systems

The Zinc family of modelling languages

Zinc [START_REF] Garcia De La Banda | The modelling language Zinc[END_REF] is a novel, declarative, typed constraint modelling language. It provides mathematical notation-like syntax (arithmetic and logical operators, iteration), high-level data structures (sets, arrays, tuples, Booleans), and extensibility by user-defined functions and predicates. Model and instance data can be separate. MiniZinc [START_REF] Nethercote | Mini-Zinc: Towards a standard CP modelling language[END_REF] is a subset of Zinc closer to existing CP languages that is still suitable as a medium-level constraint modelling language. FlatZinc, also described in [START_REF] Nethercote | Mini-Zinc: Towards a standard CP modelling language[END_REF], is a low-level subset of Zinc designed as a CP solver input language. It takes a role for CP systems comparable to that taken by the DIMACS and LP/MPS formats for propositional-satisfiability solvers and linear solvers, resp.

A Zinc model consists of an unordered set of items such as variable and parameter definitions, constraints, type definitions, and the solving objective. As an example, consider the following MiniZinc model of the Golomb Ruler problem. The problem consists in finding a set of small integers of given cardinality such that the distance between any pair of them differs from the distance between any other pair. constraint mark [START_REF] Flener | Introducing ESRA, a relational language for modelling combinatorial problems[END_REF] = 0; constraint % The marks are ordered, and differences distinct

forall ( i in 1..m-2 ) ( mark[i] < mark[i+1] ) ∧ all different(differences); constraint mark[2] -mark[1] < mark[m] -mark[m-1]; % Symmetry solve minimize mark[m];
Let us consider the items in textual order.

2

-The first and second lines declare the parameters m and n, both of type int.

-The following two lines declare the decision variables in arrays mark and differences. The variables of either array take integer values in the range 0..n. The index set of mark are the integers in the range 1..m. The array differences is defined by an array comprehension. -Next is a constraint item fixing the first element of mark to be zero. The remaining constraints order the marks, make the differences distinct, and finally break a symmetry. -The final item is a solve item, which states that the optimal solution with respect to minimising the final mark at position m should be found.

More detail about the Zinc language family is available in [START_REF] Garcia De La Banda | The modelling language Zinc[END_REF][START_REF] Rafeh | From Zinc to design model[END_REF][START_REF] Nethercote | Mini-Zinc: Towards a standard CP modelling language[END_REF]].

The Cadmium model transformation system

Cadmium [START_REF] Duck | ACD term rewriting[END_REF] is a declarative, rule-based programming language based on associative, commutative, distributive term rewriting. Cadmium is primarily targetted at Zinc model transformation, where one Zinc model is transformed into another by a Cadmium program (mapping). A rule-based system for constraint model transformation is a natural choice as such transformations are often described as rules in the first place.

Cadmium is well-suited for Zinc model transformation because of the tight representational integration between the two languages. A Cadmium program is a sequence of rules of the form

CCHead \ Head ⇔ Guard | Body
where Head and Body are arbitrary terms that in particular can involve Zinc expressions. Any expression from the current model matching Head is rewritten to the expression Body if the rule application requirements given by CCHead and Guard are satisfied (either of which can be absent). The rules in the program are repeatedly applied until no more applications are possible. The obtained model is the result of the transformation.

Cadmium has its roots in CHR [START_REF] Frühwirth | Theory and practice of Constraint Handling Rules[END_REF] but substantially extends it by several features, briefly described in the following. See [START_REF] Duck | ACD term rewriting[END_REF] for a thorough exposition.

Associative commutative matching. An operator

• is Associative Commu- tative (AC) if it satisfies x • (y • z) = (x • y) • z and x • y = y • x.
AC operators are common, e.g. +, * , ∧, ∨, ∪, ∩. Cadmium supports AC matching, which means the order and nested structure of expressions constructed form AC operators does not matter; e.g. 0 + a can match X + 0 with X = a. This reduces the number of rules required to express a transformation. AC matching is a standard feature of other term rewriting languages, e.g. Maude [START_REF] Clavel | The Maude 2.0 system[END_REF].

Conjunctive context matching. Cadmium supports matching based on the pseudo-distributive property

X ∧ f (Y 1 , ..., Y n ) = X ∧ f (Y 1 , ..., X ∧ Y i , ..., Y n )
of conjunction for all functions f . This is in contrast to performing classical distribution where the X disappears from the top-level and is distributed to all arguments at once. Using this approach, conjunct X is visible in any subexpression S of f : we say that X is in the conjunctive context (CC) of S.

A Cadmium rule in which a CCHead prefix is present uses CC matching. In order for the rule to fire, CCHead must match (part of) the conjunctive context of the expression that matches Head . CC matching can for example be used to implement parameter substitution in constraint models by the rule

X = C \ X ⇔ C.
If an equation X = C appears in the conjunctive context of an X, then this rule rewrites X to C. Consider the expression f(a,a+b,g(a)) ∧ a = 3. Equation a = 3 is in the CC of all occurrences of a in the rest of the expression. After exhaustively applying the rule, the result is f(3,3+b,g(3)) ∧ a = 3.

CC matching is very powerful because it allows the user to match against nonlocal information. As far as we are aware, CC matching is unique to Cadmium.

User-definable guards. Cadmium supports rule with guards. A rule in which a guard is present can only be applied if the guard holds, that is, if the Guard expression can be rewritten to true. Cadmium provides a number of simple guards, such as is int(X) to test whether X is an integer constant. Importantly, guards can also be defined by the user via rules.

Staged transformations. Beyond atomic transformations that consist of a single rule set, Cadmium also supports composite, staged transformations: sequences of atomic transformations. Each atomic transformation is applied to the model in sequence, with a commitment to the intermediate results.

Representation of Zinc models in Cadmium

Conceptually, Cadmium operates directly on Zinc expressions and items (we emphasise this by printing Zinc keywords in bold). The following details of the Zinc representation in Cadmium term form are worth pointing out:

-All Zinc items in the model are joined by conjunction. Thus the Zinc model constraint X = 3; solve satisfy;

is treated as

constraint X = 3 ∧ solve satisfy.
The advantage is that Zinc items are in each other's conjunctive context. -The conjunction of Zinc items is wrapped by a top-level model functor.

This representation allows top-down model transformation in the way nonterm-rewriting-based approaches work, rewriting the entire model at once:

model Model ⇔ ...
However, in our experience, top-down model transformations are almost never needed.

Transforming nonlinear MiniZinc into linear Integer Programming format

There are several ways of linearising constraints. A generic method is the Big-M approach, used to convert a logical combinations of linear constraints into a conjunction of linear constraints. A finite domain constraint can always be written as a logical combination of linear constraints, by reverting to some logical definition of it.

For some high-level constraints, alternative definitions can be given that tightly reflect their structure onto auxiliary variables, for example, 0/1 integer variables encoding assignments of original variables.

The generic Big-M transformation

At the core of this linearisation approach is the fact that a disjunction (x 0)∨b, where b is a propositional variable, is equivalently written as the inequation x ubound (x) • b, where ubound is an upper bound on the value of the variable x. Our transformation first normalises a MiniZinc model and then transforms it into negation normal form. The next steps are based on the work by McKinnon and Williams [START_REF] Mckinnon | Constructing integer programming models by the predicate calculus[END_REF] and Li et al. [START_REF] Li | Modelling integer programming with logic: Language and implementation[END_REF]. We simplified their transformation and made some steps, such as Boolean normalisation, more explicit.

Li et al. [START_REF] Li | Modelling integer programming with logic: Language and implementation[END_REF] define the modelling language L + , which consists of linear arithmetic constraints, Boolean operators, and some additional constraints such as at most and at least. Steps of the transformation described in [START_REF] Li | Modelling integer programming with logic: Language and implementation[END_REF] are:

-Transformation of L + into negation normal form. -Transformation of simplified L + -formulas into Γ -formulas. A Γ -formula is of the form Γ m {P 1 , .
. . , P n } and is true if at least m of {P 1 , . . . , P n } are true. Each P i is a Γ -formula, a linear constraint, or a propositional literal. -Flattening of nested Γ -formulas.

-Transformation of Γ -formulas into linear constraints.

Our transformation is based on this procedure. After several normalisation and decomposition steps, we generate Γ -formulas which are then further transformed into a linear form of MiniZinc. In the decomposition steps we provide several alternative transformations, and we allow the user to experiment with possible combinations of those alternatives. As a final step, we currently write out the obtained linear model in CPLEX LP format, for directly feeding it into most of the currently available ILP solvers.

We outline the major transformation steps in the following, giving actual Cadmium example rules for illustration.

Model normalisation. MiniZinc allows substantial freedom in the way models are written and so adapts to the preferred visual style of the model writer. The first step in our conversion is to rewrite simple, equivalent notations into a normal form. Examples are the joining of constraint items and the replacement of synonyms:

(constraint C) ∧ (constraint D) ⇔ constraint C ∧ D; X == Y ⇔ X = Y;
Predicate inlining. We currently use a top-down transformation, traversing the entire model term, to replace a call to a predicate (or function) by the respective instantiated predicate body. This is our only case of a model-wide top-down transformation. We are currently moving towards a modified Zinc term representation in which predicate applications are wrapped in a reserved functor. Matching can then take place against this functor, and the need for a top-down transformation will be removed.

Parameter substitution and comprehension unfolding. The next steps, while defined separately and listed in sequence, depend on and enable one another. In a non-term-rewriting approach, an explicit iteration loop would be needed to compute the mutual fixpoint. In Cadmium, each individual atomic transformation corresponds to a set of rules, and the composite transformation is the union of these rule sets. Once the composite transformation has reached stabilisation, the mutual fixpoint of the separate rule sets is obtained.

1. Parameter substitution.

We use the conjunctive context of a parameter to retrieve its value:

X = C \ X ⇔ is int(C) | C;

Evaluation.

Parameter substitution may allow us to simplify the model. We here apply rules that do so by taking into account the semantics of Zinc constructs:

X ∨ true ⇔ true; X + Y ⇔ is int(X) ∧ is int(Y) | X !+ Y; X C ⇔ is int(C) ∧ ubound(X) ! C | true;
The first rule simplifies a Boolean expression, the second evaluates addition of integer constants using the Cadmium built-in !+, while the third removes constraints X C that are redundant w.r.t. to the declared domain of X.

Compound built-in unfolding.

This step inlines predicates/functions such as forall, sum that are compound built-ins in MiniZinc:

sum([]) ⇔ 0; sum([E ! Es]) ⇔ E + sum(Es);
Note the Cadmium syntax for array literal decomposition shown here. 4. Comprehension unfolding.

An example for a simple case are these rules:

[E | X in L..U] ⇔ L > U | []; [E | X in L..U] ⇔ [subst(X=L, E) ! [E | X in L+1..U]];
The subst term denotes a substitution and is reduced accordingly.

These transformations are not specific to the MiniZinc linearisation task. Indeed, they are also used in the MiniZinc to FlatZinc transformation.

Decomposition of high-level constraints. In addition to the previously defined normalisations and decompositions, we decompose different generic constraints such as the domain constraint, here in Zinc notation:

X in A..B ⇔ is int(A) ∧ is int(B) | A X ∧ X B; X in S ⇔ is set(S) | exists([ X = D | D in S ]);
We discern two cases of the respective set. If it is in range form, the constraint can be mapped onto two inequalities. Otherwise, it is mapped to a disjunction over the set values, which can be written using Zinc comprehension notation.

An array lookup with a variable index, corresponding to an element constraint, is transformed into a disjunction over all possible index values:

Y = A[X] ⇔ is variable(X) | exists([ X = D ∧ A[D] = Y | D in dom(X) ]);
The expression dom(X) using the Zinc built-in dom is rewritten into the declared domain of the variable X, by rules we omit here. Zinc has a variety of such built-ins; index set to retrieve an array index set is another useful one. An all different constraint is simply decomposed into a conjunction of inequations of the variable pairs:

all different(X) ⇔ forall([ X[I] = X[J] | I,J in index set(X) where I < J ]);
Minimum and maximum constraints are similarly decomposed. Furthermore, strict inequalities and disequalities are rewritten into expressions using only inequalities.

Since the decomposition of high-level constraints may introduce comprehensions and since further expression simplification can often be done, the rules for comprehension unfolding and expression evaluation are again imported into this stage.

Negation normal form. We transform formulas into negation normal form in the usual way. For example

(x -y < 5 ∧ y -x < 5) → (z 1)
is rewritten into

((x -y 5) ∨ (y -x 5
)) ∨ (z 1).

N -ary conjunction and disjunction. We conjoin these binary connectives into an n-ary form, (using functors conj,disj), which is then transformed into Γ -formula form: disj(Cs) ⇔ gamma(Cs, 1); conj(Cs) ⇔ gamma(Cs, length(Cs));

The second argument to gamma is the minimum number of subformulas that need to hold. The formula from the example above becomes:

gamma([gamma([x -y 5, y -x 5], 1), z 1], 1).

Big-M linearisation. This is the central step. It relies on the fact that all constraints were previously normalised. We proceed top-down, starting at the top-most gamma formula.

B → E F ⇔ E-F lbound(E-F) * (1-bool2int(B));
The second and third rule transform a formula B → Γ m (C ) into a conjunction of implications B i → C i . The B i are accumulated in a list, which is used for the constraint B → i B i m. An implication whose consequence is a gamma formula is turned into implied gamma form again (not shown here for brevity).

The last rule finally rewrites a simple implied linear inequation into pure linear form. The lbound term is rewritten into a safe lower bound of its argument expression which may include decision variables. We optimise the linearisation by distinguishing special cases such as in

implied gamma(B, [Bi ! Cs], M, Bs) ⇔ is variable(Bi) | implied gamma(B, Cs, M, [bool2int(Bi) ! Bs]);
which leads to fewer auxiliary Boolean variables being created.

Let us revisit part of our example. Assume x and y are in 0..10.

gamma([x -y 5, y -x 5], 1)

is stepwise transformed as follows (where we omit bool2int for brevity):

B → gamma([x -y 5, y -x 5], 1) implied gamma(B, [x -y 5, y -x 5], 1)

(B1 → x -y 5) ∧ (B2 → y -x 5) ∧ (B → B1+B2 1) (x -y -5 -15*(1 -B1)) ∧ (y -x -5 -15*(1 -B2)) ∧ (B1 + B2 -1 -1*(1 -B))
Boolean variables to 0/1 variables. In this step, we recast Boolean variables as 0/1 integer variables, by simply substituting the type:

bool ⇔ 0..1; bool2int(B) ⇔ B;
Output to LP format. The concluding stage prints out the linear model in CPLEX LP format using Cadmium's I/O facilities. The result of applying the transformations to the Golomb Ruler problem of Section 2.1 is given in the Appendix.

Equality encoding for high-level constraints

For a constraint such as all different, the Big-M -linearisation applied to its naive decomposition does not result in a so-called sharp formulation: one that represents the convex hull of the constraint. Sharp formulations for a number of common constraints are given in Refalo [START_REF] Refalo | Linear formulation of constraint programming models and hybrid solvers[END_REF]. At the core of many sharp formulations is the explicit encoding of variable assignments. Given a variable x with domain D(x), for each a ∈ D(x) a propositional variable for the assignment x = a is introduced. We write such a variable as [[x = a]].

In this way, a sharp linear formulation of the domain constraint

x ∈ S is a∈D [[x = a]] = 1 ∧ x = a∈D a[[x = a]].
For the all different constraint over variables x i with respective domain D(x i ), one can use the linear constraints

n i=1 [[x i = a]] 1 for each a ∈ n i=1 D(x i ).
They represent the fact that each value in any variable domain can be used by at most one variable. The Cadmium rule setting up this encoding is as compact: The array Xi eq a collects the [[ x = a ]] variables. In order to share these encoding variables between different high-level constraints, the link between an original variables x and its associated encoding variables is maintained by encoding tokens (terms). These tokens are installed at the model top-level during the encoding stage and are thus in the conjunctive context of any constraint whose translation needs them.

To contrast the available approaches for all different, consider the Mini-Zinc fragment:

array [1..n] of var -n..n: x; constraint all different(x);

The Big-M translation of all different gives:

array[1..n, 1..n] of 0..1: B1; array[1..n, 1..n] of 0..1: B2; constraint forall(i in 1..n, j in i+1..n) ( x[i] -x[j] + 1 (2 * n + 1) * (1 -B1[i, j]) ∧ x[j] -x[i] + 1 (2 * n + 1) * (1 -B2[i, j]) ∧ B1[i, j] + B2[i, j]
1 ); while the transformation using the equality encoding results in:

array[1..n, -n..n] of 0..1: xv; constraint forall(i in 1..n) ( sum([ a * xv[i, a] | a in -n..n ]) = x[i] ∧ sum([ xv[i, a] | a in -n..n ]) = 1 ); constraint forall(a in -n..n) ( sum([ xv[i, a] | i in 1..n ]) 1 );
The element constraint z = a[x] for a variable x and an array a of integer constants can be represented as

z = i∈D(x) a[i] • [[x = i]],
which is embodied in the rule

element equality encoding(A, X, Y, X eq d) ⇔ Y = sum([ A[D] * X eq d[D] | D in dom(X) ]);
This encoding is not applicable in the case when the array has variable elements. Our transformation verifies this and falls back to the naive Big-M decomposition approach if needed. The basis for these linearisations of high-level constraints comes from the linear representation of disjunctive programs [START_REF] Balas | Disjunctive programming: Properties of the convex hull of feasible points[END_REF]. A further generalisation would be to directly apply this linearisation to the constraint in negation normal form.

Context-dependent constraint generation

If we take into account the context of a constraint we may be able to simplify its translation. The Tseitin transformation [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF] for converting Boolean formulas into clausal form takes this into account, usually reducing the number of clauses by half. For (Integer) Linear Programming there are common modelling "tricks" that make use of context. For example, the max(y,z) expression in both of the following cases constraint 8 max(y,z); solve minimize max(y,z); can be replaced by a new x constrained by x y ∧ x z. In the first case, we only need to require the existence of any value between 8 and y,z, and in the second case, minimisation will force x to equal either y or z.

In general if a variable is only bounded from above in all constraints, we can translate an equation defining the variable as an inequality that bounds it from below. For example x = max(y,z) is replaced by x y ∧ x z as above if x is only bounded from above, and replaced by x t ∧ (t y ∨ t z), where t is a new variable, if x is only bounded from below.

This reasoning can be concisely implemented in rule form: We add a polarity marker to each occurrence of a nonlinear expression in question. Polarity markers then travel upwards in the expression tree until the toplevel, recording possible polarity changes. (The rules for invert, not shown here, map pos to neg and vice versa, and all to itself). Once at the top-level, the polarity of the expression occurrence is known, and it can be replaced accordingly.

Constraint relaxations

Given we have completely captured the meaning of a high-level constraint such as element or all different by some linearisation, we are free to add other linear relaxations of the constraints to the model in order to improve the solving behaviour. Hooker [START_REF] Hooker | Integrated Methods for Optimization[END_REF] describes a number of simple and complex linear relaxations for various high-level constraints.

As an example, consider the element constraint Y = A[X] where A is a fixed array. We can add bounds to Y as follows:

Y = A[X] ⇔ is variable(X) ∧ fixed array(A) | exists([X = D ∧ A[D] = Y | D in dom(X)]) ∧ Y min([A[D] | D in dom(X)]) ∧ Y max([A[D] | D in dom(X)]);

Case studies

In this section we report on evaluations of various choices in transforming Mini-Zinc into LP format. We show that the best choice is problem-dependent and, therefore, that an open transformation system facilitating experimentation is important. For reference, we also give results on transforming MiniZinc to the low-level CP solver input language FlatZinc. The experiments were performed on a 3.4 Ghz Intel Pentium D with 4 Gb RAM computer running Linux. The FlatZinc models were solved by the G12 finite domain solver using its default (first-fail) search. The LP models were solved using CPLEX 10.0 with default parameter settings. The solvers were aborted if they did not return a result within a reasonable amount of time; this is indicated in the tables. perfsq: find a set of integers whose sum of squares is itself a square (maximum integer 10, 20, or 30); -warehouses: a warehouse location problem.

The results are shown in Table 1. The problems are grouped according to the translation features they can make use of. The eq20 and mdknapsk problems are linear and used to gauge the performance of the parts of the transformation not concerned with linearisation as such. The job-shop, packing and queens problems are nonlinear models without the use of high-level constraints, so the equality encoding variant does not differ from the Big-M variant for them. The alpha and golomb problems use all different constraints, whereas element constraints occur in perfsq and warehouses.

First, from these experiments we can see that while the FlatZinc translations are often smaller, and faster to achieve than the LP format, the speed of the ILP solver means that the LP translations are often better overall.

That the translation to LP is typically slower than to FlatZinc is not unexpected as linearisation creates more constraints. A second, central factor is that, while FlatZinc is output by a non-Cadmium Zinc pretty printer, the LP format generator uses a preliminary, primitive Cadmium I/O module to write the files. We plan to address this issue by passing the linear model to the ILP solver directly rather than via files; and we will also optimise Cadmium I/O. Some of the slightly bigger examples (golomb8, jobshop8x8, mdknapsk100 5, perfsq30, and queens 20) show that translations times do scale, but the solve times can increase dramatically. For some examples (queens, golomb, jobshop) we can see a clear advantage of the FD solver, whereas for other examples (mdknapsk, perfsq) the ILP solver performs better.

For the linearisation choice, we find that for our example problems the sharp equality encodings works well for element, whereas surprisingly all different does not benefit from it.

Context-dependent max constraints

For this set of benchmarks we use a model of a cancer radiation therapy problem [START_REF] Baatar | Minimum cardinality matrix decomposition into consecutive-ones matrices: CP and IP approaches[END_REF]. The model is linear with the exception of multiple occurrences of max constraints. We compare the generic, complete linearisation and the contextdependent one (Section 3.3). Table 2 shows the results.

One observation is that the LP translation time grows quickly with the instance size. In good part this is due to Cadmium's current suboptimal I/O module: for example, approximately one third of the time for size 8 instances is spent in the final step of printing the LP format text file.

The major observation in these benchmarks results, however, is the very surprising fact that the complete linearisation is better in the majority of cases than the context-dependent translation, which is less than half the size. This appears to be a consequence of an ill-guided ILP search in CPLEX in the contextdependent case. While correct bounds on the solutions are often found quickly, the search struggles to find integer solutions. We have been able to drastically improve the behaviour for some instances by an informed modification of CPLEX parameters. 1A study of this unexpected observation is not the task of this paper. This puzzling result does, however, support our claim that the flexibility to experiment with different model translations is important.

Concluding remarks

Cadmium is one of only a few purpose-built systems targetting constraint model transformation, and among these, has particular strengths. Constraint Handling Rules (CHR) is less powerful in the sense that CHR rules can only rewrite items at the top-level conjunction. CHR implementations are also not deeply integrated with high-level modelling languages in the way Cadmium and Zinc are. The Conjure system [START_REF] Frisch | The rules of constraint modelling[END_REF] for automatic type refinement accepts models in the high-level constraint specification language ESSENCE and transforms them into models in a sublanguage, ESSENCE', roughly corresponding to a Zinc-to-Mini-Zinc translation. Conjure's focus is on automatic modelling: the generation of a family of correct but less abstract models that a given input model gives rise to. Our current goal with Cadmium somewhat differently is to have a convenient, all-purpose, highly flexible 'plug-and-play' model rewriting platform.

We have only really begun to explore the possibilities of linearisation of Mini-Zinc models using Cadmium. There are other decompositions based on Boolean variables [[x d]] which could be explored; see e.g. [START_REF] Tamura | Compiling finite linear CSP into SAT[END_REF][START_REF] Ohrimenko | Propagation = lazy clause generation[END_REF]. There are many relaxations and combinations to explore. We can investigate how many IP modelling "tricks" can be implemented using concise Cadmium analysis and rewriting.

On the technical side, we believe data-independent model transformation is a promising direction to take. It would for example mean to postpone unfolding comprehensions, and to transform according to the derived rather than present kind of an expression (i.e. constant vs. variable at solve time). We would expect transformation efficiency to greatly improve in this way.

Minimize mark{3}

Subject To mark{0} = 0 mark{1} >= 1 mark{2} -1 differences{3} -1 mark{1} = 0 mark{3} -1 differences{4} -1 mark{1} = 0 mark{3} -1 differences{5} -1 mark{2} = 0 differences{0} -mark{1} = 0 differences{1} -mark{2} = 0 differences{2} -mark{3} = 0 mark{1} + mark{2} -1 mark{3} <= -1 mark{1} -

  int: m = 4; int: n = m*m; array[1..m] of var 0..n: mark; array[1..(m*(m-1)) div 2] of var 0..n: differences = [ mark[j] -mark[i] | i in 1..m, j in i+1..m ];

  constraint gamma(Cs, M) ⇔ constraint implied gamma(true, Cs, M, []); implied gamma(B, [], M, Bs) ⇔ B → sum(Bs) M; implied gamma(B, [C ! Cs], M, Bs) ⇔ let { var bool: Bi } in ((Bi → C) ∧ implied gamma(B, Cs, M, [bool2int(Bi) ! Bs]));

  all different equality encoding(Xs, Xi eq a) ⇔ forall([ sum([ Xi eq a[I,A] | I in index set(Xs) ]) 1 | A in array union([ dom(Xs[I]) | I in index set(Xs) ]) ]);

  max(X, Y) ⇔ pol(ID, pos, max context(X,Y, ID)); E + pol(ID, P, F) ⇔ pol(ID, P, E + F); E -pol(ID, P, F) ⇔ pol(ID, invert(P), E -F); pol(ID, P, E) F ⇔ pol(ID, P, E F); pol(ID, P, E) F ⇔ pol(ID, invert(P), E F); pol(ID, , E) = F ⇔ pol(ID, all, E = F); constraint pol(ID, P, E) ⇔ pol(ID, P) ∧ constraint E; solve minimize pol(ID, P, E) ⇔ pol(ID, P) ∧ solve minimize E; pol(ID, all) \ max context(X,Y, ID) ⇔ max complete(X,Y); pol(ID, pos) \ max context(X,Y, ID) ⇔ max bounded above(X,Y);

4. 1

 1 Big-M decomposition and equality encoding For this comparison we use the following examples: -eq20: twenty linear constraints; -jobshop: square job scheduling (2 × 2, 4 × 4, 6 × 6, 8 × 8); -mdknapsk: multidimensional knapsack problem ( n, m ∈ { 5, 3 , 100, 5 }); -packing: packing squares into a rectangle (size 4); -queens: the N-queens problem (sizes 8, 10, 20); -alpha: a crypt-arithmetic puzzle; -golomb: the Golomb ruler problem (m ∈ {4, 6, 8});

Table 1 .

 1 Results of the described transformations on several different models

	name	MiniZinc	FlatZinc	LP Big-M decomp. LP equality enc.
		lines	lines transl. solve lines transl. solve lines transl. solve
	eq20	63	82 0.31s 0.18s 43 0.44s 0.00s
	jobshop2x2	20	18 0.28s 0.10s 37 0.40s 0.00s
	jobshop4x4	22	141 0.31s 0.18s 227 0.48s 0.02s
	jobshop6x6	24	492 0.49s 8.65s 749 0.67s 1.72s
	jobshop8x8	26	1191 0.73s >300s 1771 1.11s >300s
	mdknapsk5 3	21	16 0.29s 0.07s 25 0.42s 0.00s
	mdknapsk100 5	75	176 0.60s >300s 217 1.36s 0.61s
	packing	32	237 0.33s 0.16s 378 0.53s 0.00s
	queens 8	9	86 0.31s 0.17s 613 0.56s 0.06s
	queens 10	9	137 0.32s 0.15s 974 0.72s 0.36s
	queens 20	9	572 0.49s 0.21s 4039 2.42s >300s
	alpha	52	53 0.29s 0.16s 2356 1.64s 0.13s 1511 1.32s 0.51s
	golomb4	11	14 0.30s 0.07s 144 0.46s 0.00s 272 0.47s 0.01s
	golomb6	11	25 0.31s 0.18s 807 0.69s 0.10s 1249 1.02s 0.53s
	golomb8	11	40 0.32s 1.49s 2763 1.70s 19.36s 3878 3.28s >300s
	perfsq10	16	89 0.28s 0.17s 949 0.91s 0.12s 493 0.60s 0.10s
	perfsq20	16	161 0.30s 1.55s 3069 3.36s 1.92s 1353 1.14s 0.42s
	perfsq30	16	233 0.29s 111.29s 6389 9.10s 21.00s 2613 2.34s 0.66s
	warehouses	45	476 0.45s 2.29s 1480 1.14s 1.34s 1322 0.96s 0.08s

Table 2 .

 2 Radiation problems: generic and context-dependent translations

	Instance MiniZinc FlatZinc	LP complete	LP context-dependent
		lines	lines transl. lines transl. solve lines transl.	solve
	8 0	12	2387	3.20s 7458 16.30s 5.86s 2530	3.92s 287.27s
	8 1	12	2387	2.74s 7458 16.23s 3.53s 2530	3.58s	1.71s
	8 2	12	2387	2.76s 7458 16.16s 1.11s 2530	3.61s	1.11s
	8 3	12	2387	2.70s 7458 16.10s 3.42s 2530	3.66s 22.32s
	8 4	12	2387	2.73s 7458 16.22s 1.22s 2530	3.64s	1.38s
	8 5	12	2387	2.70s 7458 16.07s 1.74s 2530	3.63s >20min
	9 0	13	3008	3.92s 9547 25.63s 2.87s 3211	5.46s	5.28s
	9 1	13	3008	3.90s 9547 25.62s 2.35s 3211	5.45s	2.55s
	9 2	13	3008	3.94s 9547 25.61s 6.42s 3211	5.47s	2.29s
	9 3	13	3008	3.88s 9547 25.69s 14.01s 3211	5.35s 170.71s
	9 4	13	3008	3.90s 9547 25.40s 1.63s 3211	5.42s 588.70s
	9 5	13	3008	3.93s 9547 25.76s 20.88s 3211	5.49s 21.04s
	10 0	14	3701	5.72s 11894 39.28s 16.21s 3974	8.02s	1.83s
	10 1	14	3701	5.73s 11894 38.74s 14.25s 3974	8.02s 660.17s
	10 2	14	3701	5.67s 11894 39.43s 7.88s 3974	8.00s	8.90s
	10 3	14	3701	5.68s 11894 39.07s 1.45s 3974	7.96s	5.50s
	10 4	14	3701	5.67s 11894 39.44s 11.82s 3974	7.95s	7.52s
	10 5	14	3701	5.65s 11894 39.31s 1.76s 3974	8.01s >20min

Interestingly an FD approach outperforms ILP when a specialised search approach is used[START_REF] Baatar | Minimum cardinality matrix decomposition into consecutive-ones matrices: CP and IP approaches[END_REF], but this is not currently expressible in MiniZinc.

Acknowledgements. This work has taken place with the support of the members of the G12 project.

A Resulting LP format

The following is the result of applying the MiniZinc-to-LP format transformation (using the Big-M linearisation of all different) to the Golomb Ruler problem of Section 2.1:


d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

IT developed to be Backbone for Business and Society

Hans Erik Mørk

To cite this version:

Hans Erik Mørk. IT developed to be Backbone for Business and Society. 4th History of Nordic Computing (HiNC4), Aug 2014, Copenhagen, Denmark. pp.383, 10.1007/978-3-319-17145-6. hal


Mobile ICT

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Mobile ICT, the Development of the Past 30 Years

Ole Mørk Lauridsen ole_ml@post3.tele.dk

Summary

During World War II, radio communication between tanks, flights and mobile army units demonstrated the great gains, which mobile radio communication can deliver. In Denmark, that came through the war relatively unharmed, Great Nordic explored the possibility of founding a new industrial activity: STORNO, in 1948, based on mobile communication. This would turn out to be a groundbreaking further development of a proud Danish radio tradition, in direct continuity of the "Poulsen Arc", M.P. Pedersen, Elektromekano as well as P.O. Pedersen's professorship from 1912 on the subject of telecommunication.

In the 30 years since NMT (Nordic Mobile Telephony) was introduced in 1984 the fixed telephone network, as the dominant ICT infrastructure, has been replaced by mobile technologies like GSM, LTE and 5th generation, having substituted our 130 years old analogue telephone network. Services as Netflix and LTE are even competing DVB-T broadcasted TV!

We have seen ICT change during the 1980s, a period where the analogue systems, one by one, was digitized and combined with the IP technology, leading to a world with a complete fusion of the different elements in ICT, as ICT is becoming a more and more important infrastructure in the modern society! Aalborg University, as personalized by Professor Jørgen Bach Andersen, has played a dominant role here. The first "European Digital Radio Engineers" were educated here. It soon led to a booming Danish mobile industry. In year 2000 the "Danish Radio Society" was so strong, that all players in the global mobile industry had development facilities in either Aalborg or Copenhagen. In that year also 60% of all global GSM type approvals were done at Telelaboratoriet by TDC in Taastrup, Copenhagen.

The present Danish frame conditions, in regards of production, are unfortunately the reason that no mobile industry exists in Denmark today. This development is completely parallel to the fate of the TV industry in Denmark. In 1963, 350.000 TV sets were produced each year by 16 competing factoriesnow "only" B&O is left! Mobile ICT is now changing our society, Twitter and Facebook are the sources of the most mobile data communication, and the mobile possibility of being on the INTERNET around the clock now takes more of our time than even TV. PDAs are used extensively in the social and health care sector, and many remote control functions are performed by APS on them. The mobile communication computer, "Smart Phone" is even substituting our PC and credit cards: "The money has gone mobile".


Silvia Bonomi
email: bonomi@dis.uniroma1.it

Antonella Del Pozzo
email: delpozzo@dis.uniroma1.it

Maria Potop-Butucaru
email: maria.potop-butucaru@lip6.fr

Sébastien Tixeuil
email: sebastien.tixeuil@lip6.fr

Antonella Del Pozzo ⋆ †

Approximate Agreement under Mobile Byzantine Faults

come

Introduction

The emergent area of sensor networks or mobile robot networks revived recently the research on one of the most studied building blocks of distributed computing: Approximate Agreement [START_REF] Li | Approximate byzantine consensus in sparse, mobile ad-hoc networks[END_REF][START_REF] Su | Reaching approximate byzantine consensus with multi-hop communication[END_REF][START_REF]Asynchronous convex hull consensus in the presence of crash faults[END_REF][START_REF] Fekete | Asymptotically optimal algorithms for approximate agreement[END_REF][START_REF] Buhrman | Optimal resiliency against mobile faults[END_REF][START_REF] Garay | Reaching (and maintaining) agreement in the presence of mobile faults[END_REF][START_REF] Sasaki | Mobile byzantine agreement on arbitrary network[END_REF][START_REF] Banu | An improved byzantine agreement algorithm for synchronous systems with mobile faults[END_REF][START_REF] Ostrovsky | How to withstand mobile virus attacks (extended abstract)[END_REF]. Indeed, gathering environmental data such as temperature or atmospheric pressure, or synchronizing clocks in large scale sensor networks, typically do not require perfect agreement between participating nodes. Also, requiring autonomous mobile robots to gather at some specific location e.g. to communicate or to setup a new task tolerates a difference in the final robot positions after gathering. This is due to the robots physical size. Accepting a predetermined difference in the agreement process permits to avoid many impossibility results occurring in the perfect agreement case.

The Approximate Agreement problem [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF][START_REF]Asynchronous approximate agreement[END_REF] is nevertheless complex to solve in systems prone to Byzantine faults. In sensor networks, sensors may not transmit their values or may transmit erroneous values due to permanent or temporary failures. In mobile autonomous robot networks, some robots may move in the opposite direction as the one intended due to hardware malfunction of buggy software. In both cases the signals (transmitted data, or perceived position) sent by the faulty participants may have a tremendous impact on the approximated value that is computed by the correct ones. The main criterium for evaluating the complexity of Approximate Agreement in a particular setting is by providing the maximum proportion of participants that may exhibit arbitrary behavior in any system execution (w.r.t. the total number of participants). The other participants are considered to never deviate from their specification.

The problem becomes even more difficult to solve when faults are mobile. That is, when the faulty behavior may impact different participants over time. For example, in sensor or mobile robot networks, the possibility of intermittent external perturbations (e.g. magnetic fields) may affect different processes of the network at various moments during system execution. Participants that are located in such affected areas may exhibit Byzantine behavior. Obviously, in these systems the definition of a "correct" and "corrupted" process is not trivial since a correct process may be corrupted temporarily afterwards, while a corrupted process may behave again according to its specifications, once the external perturbation ceased. When faults are mobile, every process may exhibit Byzantine behavior in a given system execution. So, complexity criteria that were valid for the static case must be redesigned from scratch in systems with dynamically evolving faults.

Our Contribution. This paper considers the Approximate Agreement problem, where processes start with real values from some interval, and are required to converge, after a sequence of voting rounds, to a set of values that are within ǫ of each other, where ǫ denotes a (strictly) positive real number. When the environment is prone to Byzantine faults, faulty processes may exhibit arbitrary behavior and in particular may play against the correct ones in order to prevent their convergence. We address the Approximate Agreement problem under the Mobile Byzantine Faults model, where an adversary controls Byzantine agents and moves them from one process to another. When such an agent is located at a process, this process may behave arbitrarily (and even maliciously). We consider a round-based synchronous computational model where the movements of the agents are synchronized with the change of rounds. This paper studies conditions to achieve Approximate Agreement in the four existing synchronous Mobile Byzantine Faults models, that differ in the diagnosis capabilities of processes, e.g., when processes can diagnose their failure state (that is, they are aware that the mobile agent has left them), and when processes cannot self-diagnose. We prove lower bounds (that are different from the static case) on the number of correct processes, n, that is necessary to achieve Approximate Agreement in the presence of f Mobile Byzantine Faults (that is, f agents) for each of the four models. Then we extend the correctness proof of the MSR (Mean-Subsequence-Reduce) class of Approximate Agreement algorithms, [START_REF] Lamport | The byzantine generals problem[END_REF], to the Mobile Byzantine faults model. Our correctness proof makes use for the fist time in this context of a mapping between the Mobile Byzantine Faults models and the Mixed-Mode Faults model [START_REF] Lamport | The byzantine generals problem[END_REF] composed of asymmetric (classical Byzantine), symmetric and benign static faults. The benign faults are self-incriminating (immediately self-evident to all non faulty processes). The behavior of symmetric faults is perceived identically to all correct processes, while the asymmetric faults have a totally arbitrary behavior. Our mapping is of independent interest and a similar approach can be used to to prove the correctness of other classical distributed building blocks (e.g. agreement, clock synchronization, interactive consistency etc) under Mobile Byzantine Faults model.

Related Works

The Byzantine Agreement problem, introduced first by Lamport et al. [START_REF] Fischer | Easy impossibility proofs for distributed consensus problems[END_REF] is one of the most studied building blocks in distributed computing and is specified as the conjunction of the following three properties [START_REF]Asynchronous approximate agreement[END_REF]: (Termination) All correct processes eventually decide; (Agreement) No two correct processes decide on different values; (Validity) If all correct processes start with the same value v, then v is the only possible decision value for a correct process.

In this paper we are interested in the Approximate Byzantine Agreement where processes start with real numbers as inputs, and eventually decide a real number as output. The difference with the (exact) Byzantine Agreement is that instead of agreeing exactly, processes are allowed to disagree within a small positive margin ǫ. The specification of the Approximate Byzantine Agreement [START_REF]Asynchronous approximate agreement[END_REF] has the same termination property as the Byzantine Agreement. However, it has different agreement and validity properties: (ǫ-Agreement) for any ǫ > 0, the decision values of any pair of correct processes are within ǫ of each other; (Validity) any decision value for a correct process is in the range of the initial values of the correct processes.

Approximate Byzantine Agreement

The Approximate Byzantine Agreement problem has been studied since the eighties [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF]. Most of the presented solutions are based on successive rounds of exchanges of the latest values each process stores locally. Upon collecting each set of values, a correct process applies a function (e.g. average) and adopts as next value the value returned by the function. The interested reader may refer to reference textbooks [START_REF]Asynchronous approximate agreement[END_REF] and references herein [START_REF] Vaidya | Iterative approximate byzantine consensus in arbitrary directed graphs[END_REF][START_REF] Dolev | Reaching approximate agreement in the presence of faults[END_REF].

Allowing different kinds of faults was investigated by Kieckhafer et al. [START_REF] Lamport | The byzantine generals problem[END_REF], as they unify different algorithms into the class of MSR-algorithms (Mean-Subsequence-Reduced), which compute the mean of a subsequence of the reduced multi-set of values. The authors analyze the convergence rate and the fault-tolerance of this class of algorithm in a so-called Mixed-Mode faults model. In this model faults are partitioned into asymmetric (classical Byzantine), symmetric and benign. The benign faults are self-incriminating (immediately self-evident to all non faulty processes). The behavior of symmetric faults is perceived identically to all correct processes, while the asymmetric faults have a totally arbitrary behavior. That is, the behavior of processes being subject to asymmetric faults may be perceived differently by different correct processes.

Stolz et al. [START_REF] Bonnet | Tight bound on mobile byzantine agreement[END_REF] recently proposed an Approximate Byzantine Agreement solution where processes have to approximate the median value of the input values. Their algorithm achieves agreement for n > 3f + 1 within f + 1 rounds, where f denotes the number of faulty (a.k.a. Byzantine) processes, while n denotes the total number of processes. Their algorithm is not included in the MSR-class of [START_REF] Lamport | The byzantine generals problem[END_REF] since they use a variant of the King algorithm [START_REF]Optimal byzantine-resilient convergence in uni-dimensional robot networks[END_REF]. Multidimensional agreement has been investigated by Mendes et al. [START_REF] Stolz | Byzantine approximate agreement with median validity[END_REF][START_REF] Berman | Towards optimal distributed consensus (extended abstract)[END_REF], where the authors also highlight the connexion between approximate agreement and convergence in mobile autonomous robot networks [START_REF] Li | Approximate byzantine consensus in sparse, mobile ad-hoc networks[END_REF][START_REF] Su | Reaching approximate byzantine consensus with multi-hop communication[END_REF]. Li et al. [START_REF] Fekete | Asymptotically optimal algorithms for approximate agreement[END_REF] and Charron-Bost et al. [START_REF]Asynchronous convex hull consensus in the presence of crash faults[END_REF] consider extensions to dynamic networks. In a sustained line of work, Tseng et al. [START_REF] Buhrman | Optimal resiliency against mobile faults[END_REF][START_REF] Garay | Reaching (and maintaining) agreement in the presence of mobile faults[END_REF][START_REF] Sasaki | Mobile byzantine agreement on arbitrary network[END_REF][START_REF] Banu | An improved byzantine agreement algorithm for synchronous systems with mobile faults[END_REF][START_REF] Ostrovsky | How to withstand mobile virus attacks (extended abstract)[END_REF] investigate approximate agreement problem within various faults models (link crash, process crash, byzantine) in multi-hop networks (both for the directed and the undirected cases).

Mobile Byzantine Faults

As singled out by Yung [START_REF] Reischuk | A new solution for the byzantine generals problem[END_REF], it is worth considering mobile adversaries (a.k.a. Byzantine mobile agents). Mobile adversaries have been primarily introduced in the context of multi-party computation, to model an attacker or an adversarial environment that is able to progressively compromise computational entities, but only for a limited period of time. Therefore, tolerating Mobile Byzantine Faults is, in some sense, like having a bounded number of compromised entities at any given time but the set of such entities evolves over time.

From a theoretical point of view, mobile adversaries have been formalized for different Mobile Byzantine Faults models [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]. In Mobile Byzantine Faults models, there are two main research directions: (i) Byzantines with constrained mobility, and (ii) Byzantines with unconstrained mobility. Byzantines with constraint mobility were first studied by Buhrman et al. [START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF]. In their paper, they consider that Byzantine agents move from one node to another only when protocol messages are sent (similarly to how viruses would propagate). Buhrman et al. [START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF] studied the problem of Mobile Byzantine Agreement. They proved a tight bound for the problem solvability (i.e., n > 3t, where t is the maximal number of simultaneously faulty processes), and proposed a time optimal protocol that matches this bound.

In the case of unconstrained mobility the motion of Byzantine agents is not tied to protocol message exchanges. Several authors investigated the agreement problem in further variants of this model [START_REF] Bouzid | Byzantine convergence in robot networks: The price of asynchrony[END_REF][START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Mendes | Multidimensional approximate agreement in byzantine asynchronous systems[END_REF][START_REF] Mendes | Multidimensional agreement in byzantine systems[END_REF][START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]. Reischuk [START_REF] Mendes | Multidimensional agreement in byzantine systems[END_REF] investigates the stability/stationarity of malicious agents for a given period of time. Ostrovsky and Yung [START_REF] Mendes | Multidimensional approximate agreement in byzantine asynchronous systems[END_REF] introduce the notion of mobile virus and investigate an adversary that can inject and distribute faults. Furthermore, they advocate that the unconstraint mobility model abstracts the concept of insider threats (hacker, cracker, black hat) or attacks (DOS, Worms, viruses or Trojan horses). Garay [START_REF] Lynch | Distributed Algorithms[END_REF] and, more recently, Banu et al. [START_REF] Bouzid | Byzantine convergence in robot networks: The price of asynchrony[END_REF], Sasaki et al. [START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF], and Bonnet et al. [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF] consider, in their models, that processes execute synchronous rounds composed of three phases: send, receive, compute. Between two consecutive rounds, Byzantine agents can move from one node to another, hence the set of faulty processes has a bounded size although its members can change from one round to the next. The main difference between the aforementioned unconstrained models lies in the knowledge that processes that have been affected by a Byzantine agent have. In Garay's model, a process has the ability to detect its own infection after the Byzantine agent left it. More precisely, during the first round following the leave of the Byzantine agent, a process enters a state, called cured, during which it can take preventive actions to avoid sending messages that are based on a corrupted state. Garay [START_REF] Lynch | Distributed Algorithms[END_REF] proposed, in this model, an algorithm that solves Byzantine Agreement provided that n > 6f (this requirement was later dropped to n > 4f [START_REF] Bouzid | Byzantine convergence in robot networks: The price of asynchrony[END_REF]). Bonnet et al. [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF] investigated the same problem in a model where processes do not have the ability to detect when Byzantine agents have moved. However, differently from Sasaki et al. [START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF], cured processes have control on the messages they send. This subtle difference on the power of Byzantine agents has an impact on the bounds for solving the agreement. If in the Sasaki's model the bound on solving agreement is n > 6f , in Bonnet's model it decreases to n > 5f , and this bound is proven tight.

System Model and Problem Definition

We consider a distributed system composed of a set of n processes P = {p 1 , p 2 , . . . p n } each having a unique integer identifier i ∈ [1, n].

Communication model and timing assumptions. Processes communicate through message passing. It is assumed that processes in the distributed system may access a built-in communication abstraction used to disseminate messages to all the other processes. We assume that communications are authenticated (i.e., given a message m, the identity of its sender cannot be forged) and reliable (i.e. messages are not created, lost or duplicated).

The system is synchronous and evolves in sequential synchronous rounds r 0 , r 1 , . . . r i . . . . Every round is divided in three phases: (i) send where processes send all the messages for the current round, (ii) receive where processes receive all the messages sent at the beginning of the current round1 and (iii) computation where processes process received messages and prepare those that are sent in the next round. Failure model. Processes are affected by mobile Byzantine failures (MBF) [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF][START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]. Informally, in the mobile Byzantine failure model, faults are represented by powerful computationally unbounded agents that move arbitrarily from a process to another. When the agent is on the process, it can corrupt its local variables, forces it to send arbitrary messages (potentially different from process to process) etc... However, the agent cannot corrupt the identity of the process. We assume that, in each round r i , at most f processes can be affected by a mobile Byzantine failure. When an agent occupies a process p i we say that p i is faulty. If a process has been occupied by a Byzantine agent in the previous round then the process is said to be cured. If a process is neither faulty nor cured then it is said to be correct. We assume, similar to previous work [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF], that each process has a tamper-proof memory where it safely stores the correct algorithm code. When the agent leaves a process p i , it becomes cured and then can recover the correct algorithm code from the tamper-proof memory. Concerning the assumptions on agent movements and the process awareness on its cured state, different models have been defined. In this paper we consider all the variants of mobile Byzantine failures [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF][START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]:

• (M1) Garay's model [START_REF] Lynch | Distributed Algorithms[END_REF]. In this model, agents can move arbitrarily from a process to another at the beginning of each round (i.e. before the send phase starts). When a process is in the cured state it is aware of its condition and thus can remain silent for a round to prevent the dissemination of wrong information.

• (M2) Bonnet et al.'s model [START_REF] Charron-Bost | Approximate consensus in highly dynamic networks: The role of averaging algorithms[END_REF] and (M3) Sasaki et al.'s model [START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]. As in the previous model, agents can move arbitrarily from a process to another at the beginning of each round (i.e. before the send phase starts). Differently from the Garay's model, in both models it is assumed that processes do not know if they are correct or cured when the Byzantine agent moved. The main difference between these two models is that in the [START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF] model a cured process still acts as a Byzantine one extra round.

• (M4) Buhrman's model [START_REF] Tseng | Iterative approximate byzantine consensus under a generalized fault model[END_REF]. Differently from the previous models, agents move together with the message (i.e., with the send or broadcast operation). However, when a process is in the cured state it is aware of that.

Byzantine Approximate Agreement specification. The Byzantine Approximate Agreement problem has been accurately specified in [START_REF]Asynchronous approximate agreement[END_REF]. Processes start with real-valued inputs and eventually decide a real-valued output. The only difference with the exact Byzantine Agreement is that instead of agreeing exactly, processes are allowed to disagree within a small positive real-valued tolerance ǫ.

• Termination: All non faulty processes eventually decide;

• ǫ-Agreement: The decision value of any pair of non faulty processes are within ǫ of each other;

• Validity: Any decision value for a non faulty process is in the range of the initial values of the non faulty processes.

Note that the specification proposed in [START_REF] Fischer | Easy impossibility proofs for distributed consensus problems[END_REF] is similar (the termination properties being included in the agreement properties).

Mapping Mobile Byzantine Faults to Mixed-model Faults Model

In this paper, we extend the analysis done in [START_REF] Lamport | The byzantine generals problem[END_REF] for mixed-faults model and prove that the family of Mean-Subsequence-Reduce (MRS) algorithms works also in the Mobile Byzantine Faults models.

In this section, we provide some background notions from [START_REF] Lamport | The byzantine generals problem[END_REF] and propose an elegant mapping between the Mobile Byzantine Faults model and the Mixed-Mode faults.

The work in [START_REF] Lamport | The byzantine generals problem[END_REF] is focused on a specific family of Byzantine Approximate Agreement algorithms, namely convergent voting algorithms, that start from an initial set of proposed values {v 1 , v 2 , . . . v n } and guarantee that any process p i converges to a value v i satisfying the Byzantine Approximate Agreement specification. More in details, any algorithm in this family proceeds in rounds and during any round r j , every process p i executes the following actions:

1. send-phase: p i sends its "voted" value to the others; 2. received-phase: p i aggregates values in a multiset N r k ; 3. computation-phase: p i applies a deterministic function F(N r k ) to decide the value to vote in the next round r k+1 .

In [START_REF] Lamport | The byzantine generals problem[END_REF] convergent voting algorithms are called Mean-Subsequence-Reduce (MSR). Their computation function can be expressed in the general form:

F M SR (N r k ) = mean[Sel(Red(N r k ))]
where Sel is a selection function and Red is a reduction function used to filter values.

The correctness of MSR algorithms in the Mixed-mode faults model is guaranteed by the single-step convergence property. Informally, at the end of each round r k , the range of values voted by correct processes shrinks with respect to the beginning of the round. The failures considered in [START_REF] Lamport | The byzantine generals problem[END_REF] are benign, symmetric and asymmetric with the definitions below.

Definition 1 (Benign fault [START_REF] Lamport | The byzantine generals problem[END_REF]) A process p i is said to be benign faulty if it exposes a self-incriminating, or immediately self-evident fault to all non-faulty processes.

An example of benign fault is a crash failure or an omitted reply in a synchronous system. That is, in synchronous systems if the reply is not delivered within the expected time then the process can be immediately detected as faulty by every correct process .

Definition 2 (Symmetric fault [13]) A process p i is said to be symmetrically faulty if its behavior is perceived identically by all non-faulty processes.

A symmetric fault is generally a malicious fault such as unexpected message broadcast to all processes. Definition 3 (Asymmetric fault [START_REF] Lamport | The byzantine generals problem[END_REF]) A process p i is said to be asymmetrically faulty if its behavior may be perceived differently by different non-faulty processes.

An asymmetric fault is a classical arbitrary fault such as a broadcast where the sender can send different values to different correct processes.

In [START_REF] Lamport | The byzantine generals problem[END_REF], the authors proved that, given the number of benign faults b, the number of symmetric faults s and the number of asymmetric faults a, the minimum number of processes n needed to solve the Byzantine Approximate Agreement by an algorithm in the class MSR is n > 3a + 2s + b.

In the following, we propose a method to map the Mobile Byzantine faults model to the Mixed-mode faults then prove that the MSR algorithms are correct under the Mobile Byzantine fault model. In addition, we compute the number of processes n needed to tolerate f Mobile Byzantine faulty processes and solve the Byzantine Approximate Agreement problem under Mobile Byzantine faults model.

Note that the behavior of mobile Byzantines concerns only the send/receive phases of the MSR algorithms. Therefore, we focus on the behavior of the faulty processes during the execution of these phases. In order to match our models the send-phase of MSR algorithms should be sightly modified in order to prevent correct processes to participate to the communication as per the requirement of the M1 model. Proof A cured process, in M1 is aware of its failure state thus if it is forced to skip the send phase then it is detected by any correct process in round r k .

2 Lemma 1

Lemma 2 Let T s r k be the set of cured processes at the beginning of round r k in model M2. If the send phase send(vote) to all processes;

is executed by any p j ∈ T s r k then the computation executed in round r k is equivalent to the computation under Mixed-mode fault model executed with a = f and s = |T s r k |.

Proof A cured process in M2 is not aware of its state, hence it sends its vote to every process in the system. This value may be the result of a corrupted state. This is identical to the behavior of a process exhibiting a symmetric fault. Proof A cured process in M3 is not aware of its state hence it sends its vote to every process in the system. Moreover, Byzantine agent prepares the outgoing message queue (cf. [START_REF] Yung | The mobile adversary paradigm in distributed computation and systems[END_REF]). Thus, a cured process executes the sending phase as any correct process. However, differently from the correct processes it sends possibly different values (left behind by the Byzantine agent) to every process in the system. This is identical to the behavior of a process exhibiting an asymmetric fault.

2 Lemma 3

Lemma 4 Let T c r k be the set of cured processes at the beginning of round r k in model M4. If the send phase send(vote) to all processes; is executed by any p j ∈ T c r k then the computation executed in round r k is equivalent to the computation under Mixed-mode fault model executed with a = f .

Proof In this failure model, Byzantine agents move along with the messages. Thus during the sending phase there are no processes in T c r k .

2 Lemma 4

Table 1 summarizes the mapping results proven in Lemmas 1-4.

n M i M1 n > 3f + b = 4f M2 n > 3f + 2s = 5f M3 n > 3(f + a) = 6f M4 n > 3f = 3f
Table 2: Number of required replicas in each failure model.

MSR under Mobile Byzantine Faults

In the following we prove that in presence of mobile Byzantine agents the MSR family of algorithms verifies the Byzantine Approximate Agreement specification. We first characterize configurations produced by a MSR algorithm in presence of static Byzantine faulty nodes. Then, we prove that each configuration produced in presence of mobile Byzantine agents has the same characterization. Hence, the mobility of Byzantine agents does not affect the correctness of MSR family. Moreover, we prove that the necessary condition over the number of replicas in [START_REF] Lamport | The byzantine generals problem[END_REF] still holds in the Mobile Byzantine failures model with the mapping defined in the previous section.

Preliminaries

In the following we recall some definitions from [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF] :

• min(V): min(r ∈ R : V (r) > 0) = v 1 ; the minimum value of the elements in V ;

• max(V): max(r ∈ R : V (r) > 0) = v v ; the maximum value of the elements in V ;

• ρ(V ): [min(V ), max(V )] = [v 1 , v v ]; the real interval spanned by V. ρ(V ) is called the range of V; • δ(V ): min(V ) -max(V ) = v 1 -v v ;
the difference between the maximum and the minimum values of V . δ(V ) is called the diameter of V;

• N i r k : the multiset of values received in a given round r k by non-faulty process i. Let U : be the subset of N i r k , the values generated by non-faulty processes2 . Now we can recall the important properties of F M SR () as proved in [START_REF] Lamport | The byzantine generals problem[END_REF]. If n > 3a + 2s + b then the following two properties hold: P1 For each non faulty process p i , the computed value is in the range of non faulty values, i.e., F M SR (N i r k ) ∈ ρ(U ).

P2 For each pair of non faulty processes, p i and p j , the difference between their computed values is strictly less than the diameter of the submultiset of non faulty values received, i.e., |F M SR (N

i r k ) - F M SR (N j r k )| < δ(U ).
In the following v i r k denotes the value obtained at the end of round r k (computation phase) by process p i , applying the MSR function vector N i r k .

Definition 4 (correct value) Given a value v i r k ← F M SR (N i r k ), v i r k is said to be correct if it respects the two F M SR () function properties P 1 and P 2. Proof The proof is done by induction. During the first round r 0 no Byzantine agent moved yet. Thus, at the end of r 0 trivially |T * r 0 | = 0. In the next round r 1 Byzantine agents move thus affecting up to f processes. Therefore, at the beginning of r 1 there are up to f cured processes, |T * r 1 | ≤ f . If we substitute, for each model M1-M4 (cf. Table 1), values in n > 3a + 2s + b if follows that despite agents movement, n > n M i still holds. Thus, for the definition of F M SR () the value that each process computes at computation-phase is correct. Hence, at the end of round r 1 we have |T * r 1 | = 0. For each further r k the reasoning is similar.

2 Lemma 5

From Lemma 5 it follows that during each round there are not cured processes related to the previous round but only the ones due to the last Byzantine agents movement, hence the corollary below.

Corollary 1 Let T r k be the set of cured processes at the beginning of round r k . ∀r k , |T r k | ≤ f . Definition 5 (configuration C r k ) Let configuration C r k be a set of n tuples failure state, proposing value i representing the state of each process p i at round r k . Note that processes, depending on the failure model, may or may not be aware of their failure state. Definition 6 (AA r k ) Let AA be a generic instance of the MSR family and let AA r k be the r k -th execution of the protocol AA at round r k , such that C r k ← AA r k (C r k -1 ). It takes as input C r k -1 and returns C r k . Definition 7 (static computation) A sequence of k AA executions, such that C r k ← AA r k -1 (AA r k -2 (. . . AA r 1 (C r 0 )) . . . ) is said a static computation if in every configuration C r 1 , ..., C r k , there exists a subset of at least n -(3a + 2s + b) correct processes that are correct during the whole computation.

Note that with fixed a,s and b, the relation n > 3a + 2s + b always holds in a static computation of a MSR algorithm ( [START_REF] Lamport | The byzantine generals problem[END_REF]). Proof From Theorem 1, if n > n M i then algorithm AA generates a sequence of correct configurations, i.e., a sequence of converging values exactly as in [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF], thus the Termination property is satisfied in the same way this is satisfied by the [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF] Proof From Theorem 1, if n > n M i then algorithm AA generates a sequence of correct configurations, i.e., a sequence of converging values exactly as in [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF]. Thus, the ǫ-Agreement property is satisfied in the same way this is satisfied by the [START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF] solutions.

Definition 8 (mobile computation)

A sequence of k AA executions, such that C r k ← AA r k -1 (AA r k -2 (. . . AA r 1 (C r 0 )) . . . ) is
In the following we prove that once ǫ-Agreement is achieved among the currently non faulty processors, it is preserved among the (possible different) uninfected processors. Let us consider an arbitrarily long mobile computation C 0 , . . . , C k . If ǫ-Agreement is achieved then there exists a round r a , a ∈ [0, k] where all non faulty processes agree on values that are ǫ close to each other. Considering that n > n M i then from Theorem 1 the whole mobile computation C 0 , . . . , C k is correct. Thus from round to round the two properties P 1 and P 2 hold and correct processes values can not diverge from each other.

2 The three above lemmas provide the proof of the theorem below.

Theorem 2 If n > n M i then the class MSR verifies the Byzantine Approximate Agreement specification.

Lower Bounds

In order to formulate the strongest impossibility results related to Approximate Agreement in the Mobile Byzantine faults model we examine a weaker version of this problem referred in [START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF] as Simple Approximate Agreement. Each correct node has a real value from [0, 1] as input and chooses a real value. Correct behaviors must satisfy the following properties: Agreement: The maximum difference between values chosen by correct nodes must be strictly smaller than the maximum difference between the inputs, or be equal to the latter difference if it is zero. Validity: Each correct node chooses a value in the range of the inputs of the nodes.

We prove lower bounds for each Mobile Byzantine faults models: Garay's (M1), Bonnet's(M2), Sasaki's (M3) and Burhman's (M4). The bounds for the models (M3) and (M4) result from the classical bounds proved in [START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF] and the mapping defined in Section 3. In the case of models (M1) and (M2), since the behavior of cured processes cannot be totally controlled by the Byzantine adversary, specific proofs are needed.

Observation 2 Note that the lower bounds below do not concern the class of algorithms whose computations end before the end of the first round and that start in a configuration where there are f Byzantine processes and no cured ones. It is trivial that for this class of algorithms the lower bounds are the same as those proven in [START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF] (i.e., n ≥ 3f + 1).

Proof The proof follows directly from the lower bound for the Simple Approximate Agreement [START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF] and the mapping defined in Section 3. Note that in the Sasaski's model the number of processes with asymmetric behavior is 2f where f is the number of Byzantine agents.

2 T heorem 5

Theorem 6 (Lower bound for Burhman's model) There is no algorithm that solves Simple Approximate Agreement in the Burhman's model (M4) under the Mobile Byzantine faults model if n ≤ 3f .

Proof The proof follows directly from the lower bound for Simple Approximate Agreement [START_REF] Kieckhafer | Reaching approximate agreement with mixed-mode faults[END_REF] and the mapping defined in Section 4. Note that in the Burhman's model in each round there are exactly f asymmetric faulty processes. 2 T heorem 6

Conclusions

This paper proves lower and upper bounds for achieving Approximate Agreement in the Mobile Byzantine faults model. Our core technique is the first mapping between variants of Mobile Byzantine faults models, and the Mixed-mode faults model [START_REF] Lamport | The byzantine generals problem[END_REF]. Our mapping then permitted to prove that the class of MSR (Mean-Subsequence-Reduce) Approximate Agreement algorithms are correct in the Mobile Byzantine faults model. We believe that our technique can be reused for other classical problems in Byzantine fault tolerance (e.g. agreement, clock synchronization, interactive consistency etc).

Lemma 1

 1 Let T b r k be the set of cured processes at the beginning of round r k in model M1. If the send phase if (cured) nop; else send(vote) to all processes; is executed by any p j ∈ T b r k then the computation executed in round r k is equivalent to the computation under Mixed-mode fault model with a = f and b = |T b r k |.

2 3 Lemma 3

 233 Lemma Let T a r k be the set of cured processes at the beginning of round r k in model M3. If send phase send(vote) to all processes; is executed by any p j ∈ T a r k then the computation executed in round r k is equivalent to the computation under Mixed-mode fault model executed with a = f + |T a r k |.

Lemma 5

 5 Let T * r k be the set of cured processes at the beginning of round r k in the models M1-M4. If n > n M i and every p j ∈ T * r k executes computation-phase of a MSR-algorithm then at the end of r k we have |T * r k | = 0.

  said to be a mobile computation if for any two subsequent configurations C r k , C r k +1 , any process may change the failure state but the relation n > 3a + 2s + b holds at each round. Definition 9 (configurations equivalence) A configuration C r k is said to be equivalent to a configuration Cr k if:

Table 2

 2

	reports the required number of

Table 1 :

 1 Mapping between the behavior of faulty processes in the Mixed-Mode faulty model and faulty and cured processes in the four Mobile Byzantine faulty models.

  solutions. 2 Lemma 6 Lemma 7 (ǫ-Agreement) Let AA be an algorithm in the class MSR. If n > n M i , AA under Mobile Byzantine fault model verifies the ǫ-Agreement property of the Byzantine Approximation Agreement.

  Lemma 8 (Validity) Let AA be an algorithm in the class MSR. If n > n M i , AA under Mobile Byzantine fault model verifies the Validity property of the Byzantine Approximation Agreement.

	Lemma 7

Proof From Theorem 1, if n > n M i then algorithm AA generates a sequence of correct configurations, i.e., a sequence of converging values exactly as in the validity proof in

[START_REF]Iterative approximate consensus in the presence of byzantine link failures[END_REF][START_REF] Lamport | The byzantine generals problem[END_REF]

.

2 Lemma 8

Let us note that, in round-based computations, all messages are delivered during the receive phase.

Since the communication graph is fully connected then this set is equal for any correct process

• C r k and Cr k produce the same U ;

• ∀k, C r k has at least the same number of tuples correct, correct value as Cr k .

Note that in a static computation a correct process is correct for the whole computation, while in a mobile one is correct with respect to the observed round.

Definition 10 (correct computation) A computation C r 0 , . . . , C r k is a correct computation if it is possible to build a static computation Cr 0 , . . . , Cr k such that, ∀j ∈ [0, k], C r j is equivalent to Cr j .

Observation 1 [START_REF] Lamport | The byzantine generals problem[END_REF] Given a static computation Cr 0 , . . . , Cr k of an algorithm in the MSR class, if n > 3a + 2s + b, then each configuration Cr j , j ∈ [0, k], is characterized as follows:

• up to a asymmetric Byzantine processes;

• up to s symmetric Byzantine processes;

• up to b benign faults;

• at least n -(a + s + b) correct processes such that each p j of them computes a correct value v r j j .

The first three points are due to the failures static nature. The last one is given by the failures static nature plus the correctness of the algorithm in the static case (as proven in [START_REF] Lamport | The byzantine generals problem[END_REF]).

MSR correctness under Mobile Byzantine fault model

In the following we prove that despite Byzantines mobility, the MSR family of algorithms verifies the Approximate Agreement specification. In the presence of mobile Byzantine agents, each round is characterized by correct, cured and faulty processes. As we showed previously, depending on the failure model considered, cured processes behave accordingly to a different kind of fault (asymmetric, symmetric or benign).

The following theorem proves the mapping between the Mobile Byzantine faults model and the Mixedmode fault model. Let us start proving that if n > n M i then a mobile computation is also a correct computation, as defined in subsection 5.1.

Theorem 1 Let us consider a mobile computation C 0 , . . . , C k , ∀k ∈ N of an algorithm AA in the class MSR. If in each round n > n M i (cf. Table 2) then the sequence C 0 , . . . , C k is a correct computation.

Proof We have to show that for each iteration of AA we can build a static computation equivalent to the dynamic one. The proof is done by induction. Let us denote by C, T * and B the set of correct, cured and Byzantine processes respectively and let t * denote the cardinality of T * . Let us denote, in the static case, by C ′ , T ′ , and B ′ the set of correct, non correct (which may be asymmetric, symmetric, or benign), and asymmetric faulty processes, respectively, and let t ′ * denote the cardinality of T ′ .

• Rounds 0 → 1: At the begining of round 0, Byzantine agents never move. Thus, the configuration is as follows: 3 We use ⊥ to indicate that it can be any value 10

The protocol executes its first iteration. Processes exchange their value and each non Byzantine process p i updates its state: failure state, proposing value ← v 0 i = F M SR (V 0 ) . At this point the situation is as follow:

Up to now, the same happens in a static computation. At the begining of round 1, at most f Byzantine agents move affecting other processes. Thus there are up to t * = f cured processes storing a non correct value (e.g., v 0 / ∈ ρ(N 0 )).

-

At the begining of round 1, there are at least n -(f + t * ) correct processes. If we map it to the Mixed-mode failures model (cf. Table 1), this is equivalent to a static configuration where there are f asymmetric processes and t * non correct that may be asymmetric, symmetric or benign:

The mobile and static configurations are equivalent (cf. Observation 1). Thus the current mobile configuration (and the mobile computation up to now) is correct.

• Rounds 1 → 2: From the previous point, the configuration at the beginning of round 1 is correct. The second iteration of the protocol takes place. Processes exchange their value and each non Byzantine process p i updates its state: failure state, proposing value ← v 1 i = F M SR (N 1 i ) . At this point, for Lemma 5, each process in T * becomes correct. In other words, there are up to f Byzantine processes and at least n -f correct processes. We are in the same situation as at the end of previous round 0. At the beginning of next round, at most f Byzantine agents can move to other processes, leaving up to t * = f cured processes with non correct value. Thus there are at least n -(f + t * ) correct processes at the begining of round 2. The mobile and static configurations are equivalent (cf. Observation 1). Thus the current mobile configuration (and the mobile computation up to now) is correct.

• Rounds i → i + 1: generalizing, for each round starting with a correct configuration we can apply the previous reasoning ending in a subsequent round characterized by a correct configuration.

T heorem 1

In the following we prove the correctness of any algorithm in the class MSR under Mobile Byzantine failure model.

Theorem 3 (Lower bound for Garay's model) There is no algorithm that solves Simple Approximate Agreement in the Garay's model (M1) under the Mobile Byzantine faults model if n ≤ 4f .

Proof The proof goes by contradiction. Suppose that there exists an algorithm A verifying the Simple Approximate Agreement properties in the (M1) Mobile Byzantine faults model with n ≤ 4f . Consider w.l.g. a system with four processes and one Byzantine mobile agent. The generalization of the proof can be done by replacing any process with a group of f processes.

Consider the system with four processes denoted p 0 , p 1 , p 2 , p 3 and consider that p0 is occupied by the Byzantine agent while p 1 is cured and p 2 and p 3 are correct processes. Note that the cured process in (M1) model is silent. Consider three executions of A denoted E1, E2 and E3 constructed as follows. In E1 the correct processes propose both the value 0. It follows, from the Agreement and Validy properties of A, that the value chosen by p 1 , p 2 and p 3 should be 0 (independently of the value sent by the Byzantine process, assume it 1). In E2 the correct processes propose both 1. It follows, from the Agreement and Validity properties of A, that the value chosen by p 1 , p 2 and p 3 is 1 (independently of the value sent by the Byzantine process, assume it 0).

The E3 brings the contradiction: some correct processes choose 1 while others choose 0, which contradicts the Agreement property of A. The execution E3 is as follows: the process occupied by the Byzantine agent sends 0 to process p2 and 1 to process p3. Let us consider only the processes p 2 and p 3 . The multiset held by p 2 is {0,0,1}. This multiset is identical with the one p 2 gathered in E1, hence its choice in E3 should be 0 (identical to the one in E1). The multiset gathered by p 3 in E3 is {1,0,1} and identical with the one p 3 gathered in E2. Proof The proof follows the same general idea as the proof of Theorem . Suppose that exists an algorithm A verifying Simple Approximate Agreement properties in Mobile Byzantine model (M2) with n ≤ 5f . In all of them we consider five processes p 0 , p 1 , p 2 , p 3 and p 4 , where p 0 is occupied by a Byzantine agent while p 1 is cured (its state may be corrupted) and p 2 , p 3 and p 4 are correct processes. Consider three executions: E1, E2 and E3. Execution E1 starts in a configuration where p 2 , p 3 and p 4 propose 0 while p 1 proposes 1. Assume p 0 sends 1 to all processes. Each non faulty process gathers in E1 the multi-set {1,1,0,0,0} and following the Agreement and Validity properties of A , they have all to choose 0 in E1.

Execution E2 starts in a configuration where p 2 , p 3 and p 4 propose 1 while p 1 proposes 0. Assume p 0 sends 0 to all processes. Each non faulty process gathers in E2 the multi-set {0,0,1,1,1} and following the Agreement and Validity properties of A , they have all to choose 1 in E2.

Execution E3 brings the contradiction. Assume that in E3 p 0 sends 0 to p 2 and 1 to p 3 . p2 gathers the multiset {1,1,0,0,0} hence it has the same multi-set as in E1. p2 then chooses 0. p3 gathers the multiset {0,0,1,1,1} and since this multi-set is identical with the one gathered in E2, p3 has to make the same choice, namely 1. Execution E3 violates the Agreement property, hence A do not implement the Simple Approximate Agreement.

2 T heorem 4

Theorem 5 (Lower bound for Sasaki's model) There is no algorithm that solves Simple Approximate Agreement in the Sasaki's model (M3) under the Mobile Byzantine faults model if n ≤ 6f .


Ivan Thaulow

Lars Thygesen

Register Based Research Exploiting a Goldmine of Knowledge

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Ivan Thaulow (&) and Lars Thygesen Danmarks Statistik, Copenhagen, Denmark {ith,lth}@dst.dk

Summary

Researchers in Denmark have for many years had outstanding opportunities for exploiting data from a wide range of registers. They can carry out research based on a goldmine of information on social and demographic characteristics of the population, labour market participation, health data and medical treatment, and more. All these data can be combined, and longitudinal analysis can be made.

Researchers can access anonymous micro-data tailored to their needs in a secure setting at the Research Service of Statistics Denmark, who manages the service. Basic data originate from Danish official statistics that are largely based on administrative sources. As the statistics produced by Statistics Denmark cover mainly social and economic domains, cooperation arrangements have been agreed with the State Serum Institute, who manages the Danish health data. Other external data can be integrated into the datasets that are created for researchers, e.g. special surveys carried out among specific parts of the population.

The real challenge of such a service is balancing, on the one hand the need for exploiting the enormously rich data bases for the benefit of society, on the other hand the need to protect the individuals who are registered. For researchers it is of course important that access is easy and allows them to do all the things that will give them the desired results. Legislation on data protection sets limits to access. ICT systems and organizational measures must reconcile these concerns.

The lecture explains how the Research Service has been set up and how the challenges are managed; it also describes the performance of the arrangement and attempts to highlight results and benefits. Experience will be viewed from the researcher's as well as from the data manager's point of view. Finally we will present some of the challenges for the future: How to accommodate needs for cross-border research, and how to include data from emerging sources, commonly labelled Big Data.