Pierre Lescanne

Dependent Types for Extensive Games

Keywords: extensive game, infinite game, sequential game, coinduction, Coq, proof assistant

Extensive games are tools largely used in economics to describe decision processes of a community of agents. In this paper we propose a formal presentation based on the proof assistant Coq which focuses mostly on infinite extensive games and their characteristics. Coq proposes a feature called "dependent types", which means that the type of an object may depend on the type of its components. For instance, the set of choices or the set of utilities of an agent may depend on the agent herself. Using dependent types, we describe formally a very general class of games and strategy profiles, which corresponds somewhat to what game theorists are used to. We also discuss the notions of infiniteness in game theory and how this can be precisely described.

Introduction

Extensive games are used in formalization of economics and in decision processes. Rational decision is logic, but it is not exaggerated to claim that rational decision is essentially a computational process and therefore it should be based on computational logic, like the calculus of inductive construction of Coq and on induction. Moreover, an adequate description of the decision process requires the framework to be infinite. Indeed there is no reason to assume that the process is a priori finite, since if we do so we put strong constraints on the model which prevents some behaviors, like for instance escalation. Beware, in the framework of games where agents interact, we do not say that the world is infinite, but we say that the agents believe that the world is infinite. Indeed, saying that the model is finite precludes the phenomenon of escalation, and proving, in that case, that escalation cannot exist is begging the question. Since we require a computational approach to infinite processes, the natural concept in modern logic is this of coinduction as proposed in [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF][START_REF] Lescanne | Rationality and escalation in infinite extensive games[END_REF][START_REF] Lescanne | A simple case of rationality of escalation[END_REF]. But in this paper, by using dependent types, we revise our previous works. Thus we allow considering formal presentations of very general classes of games, for instance, games with very general sets of choices depending on agents or very general sets of utilities also depending on agents. For instance, an agent may have an infinity of choices and another may have only one choice, or two, whereas utilities are just ordered sets, even completely trivial ones in some counterexamples, which shows their generality. Similarly agents may have their own sets of utility. Agents may prefer flowers for their colors whereas agents use their fragrances. By very small changes in the formalism, we may easily describe multistage games, that are games in which agents move simultaneously at each stage.

All the formalism has been developed in Coq [START_REF] Barras | The Coq Proof Assistant Reference Manual[END_REF]. The reader can find scripts on GitHub at https://github.com/PierreLescanne/DependentTypesForExtensiveGames.

The paper has 8 sections. The second section presents games and strategy profiles. Section 3, Section 4 and Section 6 talk about concepts connected with finiteness. Section 8 considers the way infiniteness is addressed in books on game theory. Section 9 is the conclusion.

Games and Strategy Profiles

This presentation of extensive games differs from this of [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF][START_REF] Lescanne | Rationality and escalation in infinite extensive games[END_REF][START_REF] Lescanne | A simple case of rationality of escalation[END_REF][START_REF] Abramsky | Coalgebraic analysis of subgameperfect equilibria in infinite games without discounting[END_REF] in the use of dependant types. However it has connections with composition games [START_REF] Ghani | A compositional approach to economic game theory[END_REF][START_REF] Hedges | Selection equilibria of higher-order games[END_REF]. Indeed, for simplicity, in those papers, only binary games were considered 1 , that is that only two choices were offered to the agents. In this paper, using dependent types, we can propose a more general framework. Associated with a game, a strategy profile is a description of the choices taken by the agents. The formal definitions of games and strategy profiles relies on three entities, a set of agents written Agent, a set of choices depending on an agent a written Choice a and a set of utilities depending on an agent a written Utility a. Moreover there is a preorder on Utility a. In particular, unlike most of the presentations of games, utilities need not be natural numbers, but can be any ordered set used by the agent. The sets of infinite games and of infinite strategy profiles are defined coinductively and are written respectively Game and StratProf.

Game.

A game which does not correspond to a terminal position and which we call a node is written <|a,next|> and has two arguments:

• an agent a, the agent whom the node belongs to,

• a function next of type Choice a → Game.

We call leaf a terminal position. A leaf consists in a function (∀ a:Agent, Utility a) → Game i. e., a function form an agent a to and element of Utility a, which is the utility assignment at the end of the game and which is written <| f |>. Notice that the utility depends on the agent. A node game is made of an agent and of a function which returns a game given a choice. Assume that the agent is a and the function is next, then a node game is written <|a,next|>. The formal definition of a game is given in Coq by: CoInductive Game : Set := | gLeaf : (forall a:Agent, Utility a) -> Game | gNode : forall (a:Agent), (Choice a -> Game) -> Game.

Since this defines a coinductive, this covers finite and infinite extensive games.

Example 1 Here is game with choices blue, green and red for A and black and dotted for B and {weak, medium, strong} as utilities for A, and N as utilities for B.

A G G A 9 9 G G A →medium,B →0 B G G r r B 7 7 A →weak,B →2 A →strong,B →1
A →weak,B →1

Strategy profile.

A strategy profile corresponds to a non terminal position. We call it a node and we write it a,c,next . It has three components:

• an agent a, the agent whom the node belongs to,

• a choice c, which is the choice taken by agent on this specific node,

• a function next of type Choice a → StratProf.

A strategy profile which is a terminal position is a function The two main differences with the approach of [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF][START_REF] Lescanne | Rationality and escalation in infinite extensive games[END_REF][START_REF] Lescanne | A simple case of rationality of escalation[END_REF][START_REF] Abramsky | Coalgebraic analysis of subgameperfect equilibria in infinite games without discounting[END_REF] lie in the fact that the set of choices and the set of utilities are not fixed (the same for all agents, namely a pair) but depend on the agent (dependent type). This way we can describe a larger class of games. In Example 1, we have shown a game with choices and games actually depending on the agents. For instance, as we will see in Section 4, the sets of choices can easily be infinite. Since the built-in Coq equality is not adequate, we define coinductively an equality on games, We prove that Uassign is a functional relation, namely that forall s ua ua', Uassign s ua -> Uassign s ua' -> ua=ua'.. Notice that for proving this property we need an inversion tactic which is somewhat subtle when dealing with dependent types [START_REF] Chlipala | Certified Programming with Dependent Types[END_REF][START_REF] Monin | Handcrafted inversions made operational on operational semantics[END_REF]. 2 Moreover for all convergent strategy profiles (i.e., for all strategy profiles of interest, see next section) we can prove that the function is total, i.e., that there exists always a utility assignment associated with this convergent strategy profile.

Several notions associated with finiteness

On infinite games and strategy profiles there are several predicates capturing notions of finiteness.

Finite Games.

A game is finite if it has a finite number of positions. It is naturally an inductive 3 . Clearly a leaf is finite. A game which is a node is finite if the set of the choices of the agent is finite 4 and if for all the choices, the next games are finite. This is made precise by the following definition. Games with only finitely many strategy profiles.

Osborne and Rubinstein [START_REF] Osborne | A Course in Game Theory[END_REF] call "finite", a game with only finitely many strategy profiles 5 . In order not to interfere with the previous definition, we prefer to say that the game is finitely broad. 6 This is translated by the fact that for a game g to have only finitely many strategy profiles, there shall exist a list that collects all the strategy profiles that have this game g as underlying game.

Since in Coq lists are finite this yields the desired property:

Definition FinitelyBroad (g:Game): Prop := exists (l: list StratProf), forall (s:StratProf), game s == g <-> In s l.

Games with only finite histories.

A game has only finite histories if it has only finitely many paths (histories) from the root to the leaves. This can be described as follows:

Inductive FiniteHistoryGame : Game -> Prop := | finHorGLeaf: forall f, FiniteHistoryGame <|f|> | finHorGNode: forall (a:Agent)(next: Choice a -> Game), (forall c':Choice a, FiniteHistoryGame (next c')) -> FiniteHistoryGame <|a,next|>.

Those games should not be confused with games with finite horizon. Notice that Osborne and Rubinstein [START_REF] Osborne | A Course in Game Theory[END_REF] require a game with a finite horizon to have only finitely many strategy profiles (p. 90: "[Given a finite game] if the longest history is finite then the game has finite horizon"), whereas Osborne [START_REF] Osborne | An Introduction to Game Theory[END_REF] does not require the set of strategy profiles associated to the game to be finite (see Section 8). For strategy profiles we have:

Inductive FiniteHistoryStratProf : StratProf -> Prop := | finHorSLeaf: forall f, FiniteHistoryStratProf <<f>> | finHorSNode: forall (a:Agent) (c:Choice a) (next: Choice a -> StratProf), (forall c':Choice a, FiniteHistoryStratProf (next c')) -> FiniteHistoryStratProf <<a,c,next>>.

Convergent strategy profiles.

The finiteness does not apply to all paths (histories) leading to leaves, but applies only to paths corresponding to the choices of the agents. Mutatis mutandi, the expression The predicate Always Convergent is shortened in ⇓. ⇓ s means that s is convergent and also all subprofiles are convergent. It plays a main role in the definition of other concepts related to strategy profiles, namely equilibria and escalation. Always convergent strategy profiles are the right objects, that game theorists are interested in. "Always Convergence" captures the notion of continuity in the spirit of Brouwer [START_REF] Bell | Continuity and infinitesimals[END_REF]. 7

A game with only finite histories and no longest history

In this section we show how Coq can be used to prove formally properties about games. Specifically we give an example of a game with only finite histories and no longest history as a counterexample to Osborne (see [START_REF] Osborne | An Introduction to Game Theory[END_REF] p. 157) definition of finite horizon. The game has two agents whom we call Alice and Bob and its definition uses a feature of dependent types, namely that the choices may depend on the agent. In this case, Alice has infinitely many choices, namely the set nat of natural numbers and Bob has one choice, namely the set unit. Notice that Choice and Utility are functions which take an agent and return a set. Said otherwise, the set of choices is the result of the function Choice applied to agents and the set of utilities is the result of the function Utility applied to agents. If the agent is Alice, the set of choices is nat and the set of utility is unit. If the agent is Bob the set of choices and the set of utilities are unit (a singleton). In other words, the set of choices depends on the agents and the set of utilities looks depending on the agents, but doesn't. The game has infinitely many threadlike subgames of length n: Let us call triv the utility assignment Alice => tt, Bob => tt. We can picture GameWFH like in Figure 1. One can prove that ThreadlikeGame n has only finite histories:

Proposition FiniteHistoryGameWFH: FiniteHistoryGame AliceBob Choice Utility GameWFH.

Clearly GameWFH has no longest history.

Subgame Perfect Equilibrium

An agent is rational if her strategy is based on a strategy profile which is a subgame perfect equilibrium. So let us present subgame perfect equilibria. Subgame perfect equilibria are specific strategy profiles that fulfill some "good" properties. Therefore they are presented by a predicate which we call SPE. In Coq this is a function of type StratProf -> Prop. A strategy profile, which is a node, is a subgame perfect equilibrium if first it is always convergent. This is necessary to be able to compute the utility assignment. Moreover the choice of the agent is better than or equal to other choices w.r.t. to the utility assignment and all the strategy subprofiles of this strategy profile are themselves subgame perfect equilibria. A leaf is a subgame perfect equilibrium. This can be formalized in Coq:

CoInductive

The simplest escalation

We discussed already the rationality of escalation in infinite games [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF][START_REF] Lescanne | A simple case of rationality of escalation[END_REF]. For dependent choice games, escalation is a somewhat simple concept and consists in adjusting the types. The simplest escalation is probably as follows. It may occur in a game in which there are two agents Alice and Bob, where each agent has two choices down and right and in which there are two non ordered utilities ying and yang. We use ying and yang to insist on the fact that there is no need for numbers and no need for an actual order among the utility values.

A r B B d Ù Ù B r B B d Ù Ù A r B B d Ù Ù B r B B d Ù Ù A r B B d Ù Ù B r @ @ d Ù Ù r 7 7 d Ù Ù
ying,yang yang,ying ying,yang yang,ying ying,yang yang,ying ying,yang This is basically the game studied in [START_REF] Lescanne | A simple case of rationality of escalation[END_REF], with the difference that the preference in Utility = {ying, yang} is just the equality. In other words, agents do not need to prefer one item over the other, just a trivial preference may lead to an escalation. The agents are like Buridan's ass [START_REF] Wikipedia | Buridan's ass -wikipedia, the free encyclopedia[END_REF], they may not know what to choose and therefore go forever. This may look strange, but as shown by the Coq script, the proof is based on exactly the same proof technique as this of the rationality of the escalation of the dollar auction [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF]

Multi-stage games

Multi-stage games are introduced in [6] (Section 3.2). We view them as games in which a node does not belong to an agent and the choices or the moves of all the agents are simultaneous. Let us call MSGame the multi-stage games. The simultaneous or collective choice corresponds to the type: Example 2 T show the complexity of multistage games, we draw a picture of a simple multistage game with the same choices and utilities as Example 1.

v v q q Ó Ó y y Ö Ö % % 7 7 ' ' E E @ @ 9 9 7 7 4 4 ( ( ! ! Ù Ù Ò Ò | | y y w w 9 9 7 7 4 4 ( ( ! ! Ù Ù Ò Ò | | y y w w # # " " × × | | x x u u q q n n k k Q Q H H E E A A 8 8 5 5 $ $ Ù Ù × × Ö Ö } } x x s s q q l l f f c cVV P P E E C C 8 8 3 3 % % ! ! A →weak,B →1 A →strong,B →0
8 Infinite and infinite

In this section, we look at the way infiniteness is dealt with in textbooks on game theory.

Two views of infiniteness

Infiniteness is discussed by Poincaré in his book Science et méthode [START_REF] Poincaré | Science et méthode[END_REF], where he distinguishes mathematical infinite which we would call today potential infinite, and actual infinite. Poincaré did not believe in such an actual infinite, but today we do accept a concept of actual infinite which is the foundation of the theory of coinduction and infinite games. Let us discuss these two concepts in the case of words on the alphabet {a, b}. {a, b} + represents all the (finite) words made with the letters a and b, like a, b, aa, ab, ba, bb, aaa, aab, aba, abb, baa, bab, bba, bbb, etc. One can also write:

{a, b} + = ∞ n=0 {a, b} {a, b} n . (1)
{a, b} + is the least fixpoint of the equation:

X = {a, b} ∪ {a, b}X
There are infinitely many such words. This is a first kind of infinite, indeed we can build words of all finite lengths. {a, b} ω is the set of infinite words. Each infinite word can be seen as a function N → {a, b}. An infinite word represents another kind of infinite. For instance the infinite word ababab... or (ab) ω corresponds to the function if even(n) then a else b and is a typical example of actual infinite. {a, b} ω is solution of the fixpoint equation:

X = {a, b}X.
In {a, b} + there is no infinite objects, but only approximations, whereas in {a, b} ω there are only infinite objects. Common Knowledge is a central concept in game theory, it relies on the concept of knowledge of an agent, which is a modality i.e., an operator of modal logic. 11Modality K a (knowledge of agent a) follows the laws of modal logic S 5 . For this and the group G of agents, we create a modality E G (shared knowledge):

E G (ϕ) = a∈G K a (ϕ).
The common knowledge modality is

C G (ϕ) = ∞ n=0 E n G (ϕ). ( 2
)
Usually there is no ambiguity on the group of agents, thus instead C G and E G one write just C and E. Clearly C has the flavor of + as shown by the analogy between equation (1) and equation ( 2) and their fixpoint definitions.

Infinite and fixpoint.

Infinite objects are associated with fixpoints. For instance, {a, b} + is the least fixpoint of the equation:

X = {a, b} ∪ {a, b}X whereas C(ϕ) is the least fixpoint of X ⇔ ϕ ∧ E(X).
which means that C(ϕ) is a solution:

C(ϕ) ⇔ ϕ ∧ E(C(ϕ)).

Infinite in textbooks.

In general in textbooks on game theory "infinite" is a vague notion which in not defined precisely and words like "ad infinitum" ([6] p. 542, [START_REF] Hargreaves | Game Theory: A Critical Introduction[END_REF] p. 27) or "infinite regress" ([6] p. 543) or three dots are used. It is often said that infinite games resemble repeated games, but this is not true, since repeated games are typically potential infinite presentations of infinite games, i.e., approximationonly sequences of games are considered, not their limit -whereas infinite games are defined by coinduction. Two main mistakes are worth noticing.

• In [START_REF] Hargreaves | Game Theory: A Critical Introduction[END_REF], Hargreaves and Varoufakis define common knowledge as follows: but they add "The idea reminds one of what happens when a camera is pointing to a television screen that conveys the image recorded by the very same camera : an infinite self-reflection", showing that they clearly mixed up the two kinds of notions. Indeed clearly the infinite self-reflection illustrates an actual infinite, a little like the infinite word (ab) ω or the Escher waterfall, whereas, as we said, common knowledge is a potential infinite. An expression like ad libitum should have been preferred and the image of a swing going further and further or a tessellation, like this of Figure 2 should have been more appropriate.

• In [START_REF] Osborne | An Introduction to Game Theory[END_REF], Osborne uses the "length of longest terminal history" to define finite horizon, without checking whether this longest history actually exists. A counterexample is shown in Section 4. We gather that he means the "least upper bound on N of the lengths of the histories".

Conclusion

If, when reaching this point, the reader has the feeling that there is no proof or almost no proof, this means that she (he) did not read the Coq files of the GitHub site, as indicated in the introduction. In those files, there is nothing but proofs. But those proofs which are mostly meant to be read by a computer are, at the present time, not part of a scientific paper [START_REF] Thomas | A formal proof of the Kepler conjecture[END_REF].

The formalization of infinite extensive games in Coq is only at an early stage. Among possible tracks to develop, there is the connection between multistage games and extensive (one-stage) games, that is between games where players move simultaneously and games where players play in alternation, using moves "do nothing" (see [START_REF] Fudenberg | Game Theory[END_REF] p. 70). More precisely we do not know how to intepret the sentence of Fudenberg and Tirole:

Common usage to the contrary "simultaneous moves" does not exclude games where players move in alternation, as we allow for the possibility that some of the players have the one-element choice set "do nothing".

(

  ∀ a:Agent, Utility a) → Game like for games. Indeed there is no choice. It is written <<f>>. The inductive definition in Coq of a strategy profile is: CoInductive StratProf : Set := | sLeaf : (forall a:Agent, Utility a) -> StratProf | sNode : forall (a:Agent), Choice a -> (Choice a -> StratProf) -> StratProf.

  CoInductive gEqual: Game -> Game -> Prop := | gEqualLeaf: forall f, gEqual (<| f |>) (<| f |>) | gEqualNode: forall (a:Agent)(next next':Choice a->Game), (forall (c:Choice a), gEqual (next c) (next' c)) -> gEqual (<|a,next|>) (<|a,next'|>). further written ==. Utility assignment. Since Coq accepts only terminating functions we define the utility assignment as a relation: Inductive Uassign : StratProf -> (forall a:Agent, Utility a) -> Prop := | UassignLeaf: forall f, Uassign (<<f>>) f | UassignNode: forall (a:Agent)(c:Choice a) (ua: forall a',Utility a') (next:Choice a -> StratProf), Uassign (next c) ua -> Uassign (<<a,c,next>>) ua.

  Inductive Finite : Game -> Set := | finGLeaf: forall f, Finite <|f|> | finGNode: forall (a:Agent)(next: Choice a -> Game), finite (Choice a) -> (forall c:Choice a, Finite (next c)) -> Finite <|a,next|>. Finite strategy profiles would be defined likewise. Inductive FiniteStratProf : StratProf -> Set := | finSLeaf: forall f, FiniteStratProf <<f>> | finSNode: forall (a:Agent)(c:Choice a)(next: Choice a -> StratProf), finite (Choice a) -> (forall c':Choice a, FiniteStratProf (next c')) -> FiniteStratProf <<a,c,next>>.

(

  forall c':Choice a, FiniteHistoryStratProf (next c')) is just replaced by Convergent (next c) hence without the forall c':Choice a Related to induction reasoning, this convergence of strategy profiles captures continuity. Like for the predicate FiniteHistoryGame a leaf is convergent. A strategy profile which is a node is convergent if the strategy subprofile for the choice made by the agent a (i.e., next c) is convergent. Inductive Convergent: StratProf -> Prop := | ConvLeaf: forall f, Convergent <<f>> | ConvNode: forall (a:Agent) (c:Choice a) (next: Choice a -> StratProf), Convergent (next c) -> Convergent <<a,c,next>>. The reader may notice the similarity of that definition with this of finite histories for games. We are now able to prove a theorem on the totality of Uassign: Lemma ExistenceUassign: forall (s:StratProf), (Convergent s) -> exists (ua: forall a, Utility a), Uassign s ua. Convergence is extended to all the strategy subprofiles of a given strategy profile by a modality Always, abbreviated , when used in expressions. Always applies to a predicate on StratProf i.e. a function P:StratProf → Prop Always P s means that P is fulfilled by all subprofiles of s. CoInductive Always (P:StratProf -> Prop) : StratProf -> Prop := | AlwaysLeaf : forall f, Always P (<<f>>) | AlwaysNode : forall (a:Agent)(c:Choice a) (next:Choice a->StratProf), P (<<a,c,next>>) -> (forall c', Always P (next c')) -> Always P (<<a,c,next>>).

  The utility of Alice and Bob are meaningless since they are singletons, namely the Coq built-in unit which contains the only element tt. In Coq we have: Definition Choice :(AliceBob -> Set) := fun a:AliceBob => match a with Alice => nat | Bob => unit end. and Definition Utility: AliceBob -> Set := fun a => unit.

Fixpoint

  ThreadlikeGame (n:nat): (Game AliceBob Choice Utility) := match n with | 0 => <|fun (a:AliceBob) => match a with | Alice => tt | Bob => tt end|> | (S n) => <|Bob,fun c:Choice Bob => match c with tt=>ThreadlikeGame n end|> end. The game we are interested in is called GameWFH and is defined as a node with agent Alice and with next games ThreadlikeGame n for Alice's choice n: Definition GameWFH:(Game AliceBob Choice Utility) := <| Alice, fun n:Choice Alice => ThreadlikeGame n |>.

Figure 1 :

 1 Figure 1: Picture of game with finite histories and no longest history

  SPE : StratProf -> Prop := | SPELeaf : forall (f: forall a:Agent, Utility a), SPE <<f>> | SPENode : forall (a:Agent) (c c':Choice a) (next:Choice a->StratProf) (ua ua':forall a':Agent, Utility a'), Always convergent <<a,c,next>> -> Uassign (next c') ua' -> Uassign (next c) ua -> (pref a (ua' a) (ua a)) -> SPE (next c') -> SPE <<a,c,next>>.

(

  forall a: Agent, Choice a) -> MSGame or written with products: a∈Agent Choice a. Leaves are almost unchanged. The function next is of type next: ( a∈Agent Choice a) → MSGame and a node is just the function next: CoInductive MSGame := | msgLeaf: (forall a: Agent, Utility a) -> MSGame | msgNode: ((forall a: Agent, Choice a) -> MSGame) -> MSGame.

Figure 2

 2 represents the two notions of infiniteness. On the left, the vault ceiling of Nasir ol Molk Mosque in Chiraz 9 pictures potential infiniteness. On the right, a drawing 10 inspired by M.C. Escher Waterfall pictures actual infiniteness.

Figure 2 :

 2 Figure 2: Two pictures of infinite

  (a) each person is instrumentally rational (b) each person knows (a) (c) each person knows (b) (d) each person knows (c) . . . and son on ad infinitum.

  as shown by the two following Coq statements and proofs:8

	Lemma AlongGoodAndDivergentInDollar :
	exists (s:StratProf dollar.Agent dollar.Choice dollar.Utility),
	AlongGood dollar.Agent dollar.Choice dollar.Utility dollar.pref s
	/\ Divergent s.
	Proof.
	exists (dollarAcBc 0).
	split.
	apply AlongGoodDolAcBc.
	apply DivergenceDolAcBc.
	Qed.
	and the proof of the escalation for the YingYang game:
	Lemma AlongGoodAndDivergentInYingYang :
	exists (s:StratProf yingYang.Agent yingYang.Choice yingYang.Utility),
	AlongGood yingYang.Agent yingYang.Choice yingYang.Utility yingYang.pref s
	/\ Divergent s.
	Proof.
	exists yingYangAcBc.
	split.
	apply AlongGoodYyAcBc.
	apply DivergenceYyAcBc.
	Qed.

After Vestergaard[START_REF] Vestergaard | A constructive approach to sequential Nash equilibria[END_REF] who introduced this concept for finite games and finite strategy profiles.

We thank Adam Chlipala and Jean-François Monin for their help on this specific example.

Roughly speaking, an inductive (definition) is a well-founded definition with basic cases and constructors

The predicate finite over choices is not defined here.

Actually they use the concept of "history" (path), instead of strategy profiles, but this is not essential.

Denoted by the predicate FinitelyBroad on Game in Coq

I like to thank Jules Hedges for pointing me this fact and the connection with Brouwer bar recursion[START_REF] Hedges | Towards compositional game theory[END_REF].

Notice that the parameters of StratProf are explicit!

From Wikimedia, due to User:Pentocelo.

From Wikimedia.

We follows the presentation of[START_REF] Lescanne | Mechanizing common knowledge logic using COQ[END_REF][START_REF] Lescanne | Common knowledge logic in a higher order proof assistant[END_REF], which took its origin from[START_REF] Fagin | Reasoning about Knowledge[END_REF].


Élise Lévêque

Sébastien Oliveau

Isabelle Blöss-Widmer

Yoann Doignon

Are fertility levels really converging around the Mediterranean ?

come


Alexandre X Martins
email: xmartins@decea.ufop.br

Christophe Duhamel
email: christophe.duhamel@isima.fr

Philippe Mahey
email: philippe.mahey@isima.fr

Rodney R Saldanha
email: rodney@cpdee.ufmg.br

Mauricio C De Souza
email: mauricio.souza@pq.cnpq.br

Variable Neighborhood Descent with Iterated Local Search for Routing and Wavelength Assignment

Keywords: Routing and assignment, Network design, Variable neighborhood descent, Local search

HAL is

Introduction

Optical networks with wavelength division multiplexing (WDM) provide users with very large bandwidths. In all-optical networks a traffic demand is carried from source to destination through a lightpath, which is a sequence of fiber links carrying the traffic optically from end to end [START_REF] Dutta | A survey of virtual topology design algorithms for wavelength routed optical networks[END_REF]. The wavelength continuity constraint implies that to a given lightpath a single wavelength must be assigned, i.e., a particular wavelength must be reserved to travel with the traffic on each link the lightpath traverses. Moreover, a particular wavelength cannot be assigned to two different lightpaths sharing a common physical link.

The Routing and Wavelength Assignment (RWA) problem deals with the routing and the assignment of wavelengths to lightpath requests between pairs of nodes. Given a set of lightpath requests, two variants of the RWA problem have been studied in the literature: max-RWA and min-RWA. In the former, the objective is to maximize the number lightpath requests that can be routed with a fixed number of wavelengths. In the latter, the objective is to minimize the number of wavelengths to route all the requests.

In this paper, we develop a Variable Neighborhood Descent (VND) with an Iterated Local Search (ILS) based perturbation for the min-RWA. Let G = (V, E) be a digraph where V is the set of nodes and E is the set of bidirectional arcs. We denote by Γ the set of lightpath requests where each r ∈ Γ is defined by an origin and destination pair (s r , d r ) ∈ V × V . Note that we can have two different requests with the same origindestination pair and in this case if they are to be routed with the same wavelength, then they have to be routed through two arc disjoint paths in G. The problem is to find a minimal partition of Γ in W subsets such that the requests in each Γ w , w = 1, . . . , W , can be routed through arc disjoint paths in G.

The paper is structured as follows. In the next section we discuss related works in the literature. In Section 3 we describe the VND-ILS heuristic for the min-RWA. Then, in Section 4 we report numerical results on some hardest benchmark instances from the literature. We end with concluding remarks and extensions for future work.

Related works

Chlamtac et al. [START_REF] Chlamtac | Lightpath communications: An approach to high bandwidth optical WAN's[END_REF] have shown that the RWA problem is NP-Complete, and proposed, to our knowledge, the first greedy heuristics for the problem. Dutta and Rouskas [START_REF] Dutta | A survey of virtual topology design algorithms for wavelength routed optical networks[END_REF] and Zang et al. [26] reviewed the literature on the RWA problem covering different approaches and variants developed in the 90's. For instance, Ramaswami and Sivarajan [START_REF] Ramaswami | Routing and wavelength assignment in alloptical networks[END_REF] derived upper bounds on the number of lightpath requests that can be routed, while in [START_REF] Ramaswami | Design of logical topologies for wavelengthrouted optical networks[END_REF] they proposed to minimize the network congestion subjected to average delay constraints. Banerjee and Mukherjee [START_REF] Banerjee | A practical approach for routing and wavelength assignment in large wavelength-routed optical networks[END_REF] partitioned large RWA problems into several smaller subproblems to be solved independently and efficiently. Mukherjee et al. [START_REF] Mukherjee | Some principles for designing a wide-area WDM optical network[END_REF] proposed to alternate two phases: simulated annealing to construct a topology, and flow deviation to route the traffic. See also Kennington et al. [12] for the RWA problem in survivable WDM networks.

Mathematical formulations have been developed for the RWA problem, with particular emphasis on path-based ones. Ramaswami and Sivarajan [START_REF] Ramaswami | Routing and wavelength assignment in alloptical networks[END_REF] first modeled the RWA problem using a path-based formulation. Krishnaswamy and Sivarajan [START_REF] Krishnaswamy | Algorithms for routing and wavelength assignment based on solutions of LP-relaxations[END_REF][START_REF] Krishnaswamy | Design of logical topologies: A linear formulation for wavelength-routed optical networks with no wavelength changers[END_REF] presented a mixed integer linear formulation which takes into account the maximum number of hops, among other logical and physical constraints, to minimize congestion. The authors developed heuristics based on rounding the solutions obtained by solving the respective LP-relaxation. Lee et al. [START_REF] Lee | An optimization approach to routing and wavelength assignment in WDM all-optical mesh networks without wavelength conversion[END_REF] proposed a column generation algorithm to deal with the exponential number of variables associated to potential feasible paths. Jaumard et al. [START_REF] Jaumard | ILP formulations for the RWA problem symmetrical systems[END_REF][START_REF] Jaumard | Comparison of ILP formulations for the RWA problem[END_REF], in comprehensive surveys, reviewed existing column generation formulations and proposed new ones. In particular, Jaumard et al. [START_REF] Jaumard | On column generation formulations for the RWA problem[END_REF] developed improvements to make column generation methods efficient on the RWA problem. In their work, several instances were solved to optimality for the first time.

Some studies and tests have been done in order to design new or improved heuristics. The heuristics described below were developed for the min-RWA version of the problem. Manohar et el. [START_REF] Manohar | Routing and wavelengths assignment in optical networks from edge disjoint path algorithms[END_REF] presented a greedy algorithm to do a partition of lightpath requests into subsets, each of which associated to a wavelength. Their algorithm explores techniques employed to solve the maximum edge disjoint paths problem. Noronha and Ribeiro [START_REF] Noronha | Routing and wavelength assignment by partition colouring[END_REF] used a decomposition scheme in two distinct phases. In the first phase, a number of alternative routes are computed for each lightpath request. A conflict graph is built to exploit efficient heuristics for coloring problems. A route computed generates a node in the conflict graph, and an edge is set up between two nodes whose routes share a common link in the original graph. The set of nodes of the conflict graph is partitioned such that each subset contains the routes computed for a given lightpath request. Noronha and Ribeiro [START_REF] Noronha | Routing and wavelength assignment by partition colouring[END_REF] proposed a tabu search for the partition coloring problem which is applied, in the second phase, over the conflict graph to assign wavelengths to routes. Skorin-Kapov [25] adapted ideas from bin packing heuristics to the min-RWA. For such purpose, she considered lightpath requests as items, and copies of the original graph as bins. The equivalent for the weight of an item is the number of links to route a lightpath. To say that a bin has not enough capacity to accommodate two items is equivalent to not being able to route two lightpath requests on a copy of the original graph without sharing a link. According to the bin packing analogy Skorin-Kapov [25] proposed four variants of best fit and first fit heuristics. In the numerical results reported in [25] the best fit decreasing (BFD) was the most successful among them. Noronha et al. [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF] improved performance of best fit and first fit heuristics. To do this, the authors worked on data structures and implementation strategies, such as double linked adjacency lists and dynamically updating of shortest paths. Noronha et al. [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF] introduced a broader set of testbed instances, and maximum running times were reduced to one quarter of those with a standard implementation of BFD (which was confirmed as the heuristic to perform best).

More recently, Noronha et al. [START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF] embedded BFD into a biased random-key genetic algorithm. The chromosomes are vectors of real numbers, denoted keys, in the interval [0,1]. The keys are used to bias a decoding heuristic in generating a feasible solution. Actually, each key is associated with a lightpath. Lightpaths are sorted in non-increasing order of the sum of their lengths and keys, and then BFD is applied. Computational experiments were conducted on the most studied instances and as well on the new benchmark ones introduced in [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF]. The genetic algorithm improved upon results from heuristics previously proposed in the literature. Noronha et al. [START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF] reported that it reached solutions better than or similar to those found by a multistart variant of BFD in 23% less time on average, and reduced on average to half gaps provided by the decomposition scheme proposed in [START_REF] Noronha | Routing and wavelength assignment by partition colouring[END_REF].

VND-ILS heuristic for the min-RWA

A feasible solution is characterized by a partition of Γ in W subsets along with arcs disjoints paths to route requests belonging to each Γ w , w = 1, . . . , W , in G. Let us define by F r ⊆ E the arcs of the path used to route a request r ∈ Γ in G. Each Γ w ⊆ Γ induces a subgraph G w = (V, E w ) of G where E w = E -∪ r∈Γw F r . In other words, G w contains the arcs not used to route requests belonging to Γ w .

Given a feasible solution, in a VND phase we employ three kinds of moves trying to rearrange requests between the subgraphs associated to subsets of the partition in attempt to eliminate one of them. When VND fails, we perform a ILS-based perturbation phase to disturb the requests distribution among the subsets of the partition. Thus, an iteration of the algorithm alternates between a VND phase and a ILS-based perturbation phase.

VND phase

VND is a search heuristic proposed by Mladenović and Hansen [START_REF] Mladenović | Variable neighbourhood search[END_REF] within the framework of variable neighborhood search methods, see Hansen et al. [START_REF] Hansen | Variable neighborhood search[END_REF][START_REF] Hansen | Variable neighborhood search: methods and applications[END_REF][START_REF] Hansen | Variable neighbourhood search: methods and applications[END_REF]. The VND works with k max neighborhood structures N k , k = 1, . . . , k max , designed for a specific problem. It starts with a given feasible solution as incumbent and sets k = 1. If an improvement is obtained within neighborhood N k , the method updates the new incumbent and sets k = 1. Otherwise, it increases the value of k and the next neighborhood is considered. The method stops when a local optimum for N kmax is found.

We propose a VND algorithm with k max = 3. Let Γ w be a subset contained in the partition characterizing a feasible solution. We consider two alternatives to chose Γ w. In the first alternative, denoted by VND r , Γ w is the subset of the partition with the least number of requests, i.e., w = arg min{|Γ w | : w = 1, . . . , W }. The idea is that it might be easier to empty by reallocating requests a set with a few of them. In the second one, denoted by VND e , Γ w is the subset whose induced graph G w has the greatest number of arcs, i.e., w = arg max{|E w | : w = 1, . . . , W }. If a fewer number of arcs were used to route requests belonging to Γ w then it might be possible to find paths to route them in the subgraphs induced by the other sets of the partition. In both alternatives, the requests belonging to Γ w form a list L w. The VND traverses L w and tries with each request r to perform moves within neighborhoods N 1 , N 2 , N 3 until it either succeeds to reallocate all requests belonging to Γ w or fails to reallocate a request within N 3 . In the former case, VND has emptied subset Γ w of the partition, and consequently reduced the number of wavelengths to be used. In the latter case, the ILS-based perturbation phase is called. We remark that an improving move, if it happens, occurs only when the last remaining request of Γ w is reallocated to another subset, while for |Γ w| ≥ 2 performing a move does not reduce the objective function's value. When VND succeeds to empty Γ w, we update the remaining subsets of the partition with respect to the criteria to select the next subset to which VND is to be applied, according to the alternatives VND r or VND e .

Suppose, traversing L w, the search is to consider a request r. A move in the first neighborhood N 1 tries to reallocate r to another subset of Γ. If the neighborhood N 1 is not empty with respect to a partition and a request, then there exists Γ w ′ ⊂ Γ, w ′ = w, whose induced graph G w ′ has a path between s r and d r (the request's origin and destination pair). In this case the search within N 1 stops when the first graph G w ′ to accommodate r is found, and r is transferred from Γ w to Γ w ′ . The search then continues to the next request in L w, or reduces a wavelength if r was the last of L w. The list L w is sorted in non-increasing order of shortest path lengths in G between origin and destination nodes. The motivation behind is to try to route in the subgraphs induced by the other sets first the requests using more arcs, and leave the requests using fewer arcs to try after since when a path is found to route a request in a subgraph its arcs are removed. If N 1 is empty, VND proceeds to neighborhood N 2 with the same request r under analysis.

The rationale in the second neighborhood is try first to make room for r in a graph G w ′ by transferring as many requests as possible from Γ w ′ to other subsets of Γ not equal to Γ w. This is done analogously to the search in neighborhood N 1 , i.e., we traverse L w ′ and try, for each request, to find a subset Γ ŵ, ŵ = w ′ and ŵ = w, such there is a path to route the request in G ŵ. If we are able to unload at least one request from Γ w ′ , then we can try to allocate r to it. Upon success, the search resumes from the next request in L w, if any, within neighborhood N 1 . Otherwise, VND proceeds to neighborhood N 3 still with the same request r under analysis. Assume that the subsets of the partition were built in a given order, w = 1, . . . , W . At each new search within N 2 we take only one subset of the partition, according to the order, to try to make room for r in it. That is, if we fail, during a search within N 2 , to make room in a graph G w ′ for request r, we do not try to perform a move considering another graph but proceeds to neighborhood N 3 . Then, the next time we proceed to N 2 the graph to be considered will be G w ′ +1 (assuming w = w ′ + 1).

A move in neighborhood N 3 seeks to swap request r with another request belonging to a subset of Γ different from Γ w. Given a request u, let min spl (u) be the number of arcs of the shortest path between s u and d u in G. The search considers requests with min spl smaller than min spl (r), sorted in non-decreasing order of min spl . The choice to consider only requests whose shortest paths in G have fewer arcs than r carries the idea that it might be easier to route such a request in other subgraphs of the partition when the search resumes from N 1 . Thus, if a request r ′ ∈ Γ w ′ , such that r can be routed in the subgraph induced in G by Γ w ′ -{r ′ }, and r ′ in the one by Γ w -{r}, is found, then a swap between r and r ′ is performed. After a successful move in N 3 we have r ′ ∈ Γ w and r ∈ Γ w ′ . In this case, the search resumes by trying to transfer r ′ from Γ w to another subset of the partition with a move in N 1 . Note that a move in N 3 does not reduce |Γ w|, but since it swaps r with r ′ , and min spl (r ′ ) < min spl (r), it may allow a reallocation of r ′ with a move in N 1 in the sequel. If it is not possible within N 3 to swap r with any other request having a smaller min spl , the search calls a ILS-based perturbation phase. This means that VND failed to empty Γ w, and it is not subsequently applied to another subset of the partition. Instead, a ILS-based perturbation phase is applied to disturb the current solution before another trial of VND.

Figure 1 illustrates searching moves within each neighborhood of VND. The idea in part 1(a) is to move request r from Γ w to a different subset Γ i , i = 1, . . . , W , i = w, as long as r can be routed in G i . Part 1(b) shows the attempt to accommodate r in Γ w ′ by reallocating as much requests from Γ w ′ as possible. Part 1(c) represents swap moves.

ILS-based perturbation phase

ILS employs perturbation techniques to escape from a current local optima. Let s * be a current solution, and let initially s be equal to s * , then ILS's iterative step has three components: (i) a local search applied to s generating s ′ ; (ii) an acceptance criterion to either update s * to s ′ or not; and (iii) a perturbation technique applied to s * generating a new solution s. The overall best solution is returned after a number of iterations. The reader is referred to Lourenço et al. [START_REF] Lourenço | Iterated local search[END_REF] for a broader discussion on ILS features. We exploit the idea of applying a perturbation technique, in the manner of ILS, after a solution had been obtained by the VND. Suppose the perturbation is applied when VND failed to swap a request r ∈ Γ w within N 3 . Note that at this point VND might have successfully performed moves when traversing the requests' list L w. We do not undo these moves and consequently, when perturbation is applied, the subsets of Γ characterizing the partition may have other elements than those at the beginning of the iteration. The perturbation relies upon an assignment problem built to rearrange requests among the subsets partitioning Γ -Γ w. We pull out a randomly chosen request

r i from each subset Γ i , Γ i ⊆ Γ -Γ w, of the partition. Let G a i = (V, E a i ) be the subgraph of G where E a i = E i ∪ F r i (the arcs used to route request r i are reactivated in G a i ).
The perturbation is done by finding the best way to assign W -1 requests chosen to W -1 subsets partitioning Γ -Γ w. The cost of assigning request r i ∈ Γ i to subset Γ j is given as follows:

• c r i j = 2, if j = i;
• c r i j = ∞, if there is no path to route request r i in the graph G a j ;

• c r i j = 1 -

min spl (r i ) min spl (r i )(G a j ) -max(min spl (r i )(G a i ) -min spl (r i )(G a j
), 0), otherwise; where min spl (r i )(G ′ ) is the number of arcs of the shortest path between s r i and d r i in graph G ′ (we remember that min spl (r i ) is the number of arcs of the shortest path in the original graph G). The assignment problem results in a feasible partition of Γ-Γ w because a solution that returns each r i to its original subset Γ i is always feasible and possess a cost of 2(W -1), which is smaller than the cost of any solution that assigns a request r i to a subset Γ j where there is no path to route r i in G a j . If the solution of the assignment problem has cost smaller than 2(W -1), then at least two requests were assigned to subsets other than their original ones while preserving feasibility in terms of arc disjoint paths to route requests of each subset. Thus, after solving the assignment problem, we check whether the allocation of requests to partition subsets has changed. If so, the algorithm resumes the VND by trying a move with r ∈ Γ w within N 1 . Otherwise, a perturbation step is done again. Figure 2 shows an example where Γ is partitioned in five subsets. Suppose VND failed to swap a request r ∈ Γ 4 within N 3 . Then, for each i, i ∈ {1, 2, 3, 5}, a request r i is randomly chosen and the assignment problem built. Note the graph G 4 ( w = 4) does not take part on the assignment. We propose two variants for choosing a request r i from subset Γ i to build the assignment problem used to guide the perturbation. In the first one, denoted ILS p , all requests belonging to Γ i have the same probability to be chosen. In the second one, denoted ILS 5p , requests whose paths pass through the origin s r i or the destination d r i of the request r ∈ Γ w for which VND failed to perform a move within N 3 have higher probability of being chosen. In fact, if the path used to route request r i ∈ Γ i in G has an outgoing (resp. incoming) arc from s r i (resp. to d r i ), then r i has five times more probability of being chosen.

Computational results

The computational experiments were structured into three comparative settings: comparison among combinations of VND-ILS strategies, evaluation of the effectiveness of the VND-ILS with respect to a multistart heuristic and robustness to initial solution, and comparison with the strongest metaheuristic in the literature. For such purpose, we used benchmark instances from the literature -the most studied realistic instances, and sets Y and Z introduced by Noronha et al. [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF]. The realistic instances are available on the web1 or were provided along with sets Y and Z by Noronha2 . Instances Y and Z are the most difficult ones. Set Y is formed by randomly generated instances with 100 nodes and different values for the probabilities of a link and a request between a pair of nodes. Set Z is formed by instances with 100 nodes on a grid embedded on a torus where each node is connected only to its nearest four nodes, and different values for the probability of a request between a pair of nodes. Computational experiments were carried out on a Core 2 Duo with 1.97 GHz and 4 GB of RAM, running MS Windows XP, and the proposed algorithms were coded on C++.

Table 1 presents average results to decide among VND-ILS alternatives the one that seems to work better. The first column lists the group of instances. The group Realistic has 26 instances, and each of the Z and Y groups has 5 and 25 instances, respectively. Then, for each combination VND-ILS we report average deviation gaps for 5 runs of the heuristic on each instance, each run limited to 5 minutes. The gaps are calculated as the difference in percentage between the upper bound UB obtained by the heuristic and the lower bound LB computed according to Jaumard et al. [START_REF] Jaumard | ILP formulations for the RWA problem symmetrical systems[END_REF][START_REF] Jaumard | On column generation formulations for the RWA problem[END_REF] and also used in the study conducted by Noronha et al. [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF][START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF], i.e., (UB-LB)/LB. It can be seen that if the VND strategy is fixed, ILS 5p leads consistently to better results. It shows that giving more chance, in the ILS-based perturbation, to requests passing through the origin or destination nodes of the request blocked during the precedent VND phase is more effective in rearranging wavelengths to another VND trial. The different VND strategies have similar behavior, with VND e obtaining slightly better results. Thus, we present in the sequel results comparing the VND e -ILS 5p with the powerful methods in the literature.

The second comparison setting aims to see whether VND and ILS are effective to improve results regarding a multistart variant of what is considered the best constructive heuristic in the literature, and on the other hand evaluate the robustness of the method with respect to initial solution. The initial solution for VND e -ILS 5p is given by one run of the BFD heuristic proposed by Skorin-Kapov [25]. Thus, we compare VND e -ILS 5p to a multistart variant of BFD where requests whose shortest paths in G have the same length are randomly ordered. We then apply solely VND e to the initial solution. Finally, we apply VND e -ILS 5p starting from a different initial solution which is obtained with the edge disjoint path (EDP) heuristic proposed by Manohar et al. [START_REF] Manohar | Routing and wavelengths assignment in optical networks from edge disjoint path algorithms[END_REF].

Table 2 presents results of the four methods -Multistart-BDF, BFD-VND e , VND e -ILS 5p , EDP-VND e -ILS 5p -on a set of realistic instances. For each method we performed again 5 runs on each instance, each of them limited to 5 minutes. The first column presents the instance's identification, and from the second to the fourth column the corresponding number of nodes, number of arcs, and number of lightpath requests. For the instances marked with ( * ) we randomly generated asymmetric requests. Then, in the next columns, we report for each method the minimum number of wavelengths obtained on 5 runs, that is the best solution found, and the average gap. The last column presents the lower bounds. It has seen in Table 1 that realistic instances are easier to solve than the ones in sets Y and Z. Nevertheless, Multistart-BFD and BFD-VND e were not able to find optimal solutions for all of them, whereas VND e -ILS 5p and EDP-VND e -ILS 5p did. We see from Table 2 that BFD-VND e improved results upon Multistart-BFD reducing the overall average gap from 3.27% to 2.50%, though BFD-VND e still shows some high average gaps of 20% and 15.37%. But when ILS 5p was coupled, the method VND e -ILS 5p closed all gaps independently of the initial solution.

Tables 3 to 5 present results on the set Y of instances [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF][START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF]. These 100 node instances are characterized by the probabilities that there is a pair of direct arcs between a pair of nodes, which are 0.03, 0.04, 0.05, and that there is a request between a pair of nodes, which are 0.2, 0.4, 0.6, 0.8, 1. There are 5 instances for each combination of probabilities. For example, instance y.3.60.4, has probability of 0.03 for arcs and 0.6 for requests, and it is the 4th instance with this combination. Results are reported analogously to those in Table 2, and again 5 runs limited to 5 minutes were performed for each instance. Comparing the four methods, they follow the general tendency observed in Table 2. The VND solely produces only slightly reductions on average gaps, and both versions employing ILS-based perturbation lead to significant smaller gaps than Multistart-BFD. We note that VND e -ILS 5p was able to improve gaps on all the 42 out of 75 instances for which Multistart-BFD was not able to find the optimum. Moreover, EDP-VND e -ILS 5p , starting from a different initial solution, was able to obtain smaller gaps than Multistart-BFD on 35 out of these 42 instances. The use of BFD as initial solution yields however better results, since for these harder instances VND e -ILS 5p clearly outperforms EDP-VND e -ILS 5p .

Table 6 presents results on the set Z of instances [START_REF] Noronha | Efficient implementations of heuristics for routing and wavelength assignment[END_REF][START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF]. These instances have approximately 100 nodes which are the vertices on grids of dimensions 10 × 10, 8 × 13, 6 × 7, 5 × 20, 4 × 25, with probability of 0.2, 0.4, 0.6, 0.8, 1 to have a request between a pair of nodes. For example, instance z.8 × 13.80, is a 8 × 13 grid with probability of 0.8 for requests. Results for 5 runs limited to 5 minutes for each method are reported in the same manner. Although gaps of 20% are not observed as in some cases of set Y , these instances seem to be more difficult because Multistart-BFD were not able to match lower bounds. And in this case VND e -ILS 5p was able to obtain better gaps than Multistart-BFD for all 25 instances in set Z. Besides, VND e -ILS 5p was able to find the optimum for 6 instances. As it can be seen from Table 6, the proposed approach of combining VND and ILS-based strategies is robust. EDP-VND e -ILS 5p , even though not using BFD to generate initial solutions, found better gaps than Multistart-BFD for 14 instances.

The third setting is intended to compare VND e -ILS 5p with the genetic algorithm GA-RWA proposed by Noronha et al. [START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF] which recently improved the state-of-the-art algorithms in the literature. Noronha et al. [START_REF] Noronha | A biased random-key genetic algorithm for routing and wavelength assignment[END_REF] selected a subset of 30 instances as the hardest ones, and their results showed that GA-RWA was able to improve average gaps on 29 of them. Table 7 presents a comparison between VND e -ILS 5p and GA-RWA on these 30 instances. Results of GA-RWA were obtained with a limit of 10 minutes on a Pentium IV with 3.4GHz, and those of VND e -ILS 5p with a limit of 5 minutes as an attempt to take into account the processor difference. The first column presents the instance. Then, the second and third (resp. the fourth and fifth) columns present the best solution and the average gap for 5 runs obtained by GA-RWA (resp. by VND e -ILS 5p ). The last column presents the lower bound. Table 7 shows quite competitive results regarding the state-of-the-art in the literature. VND e -ILS 5p found better solutions than GA-RWA in 26 out of 30 instances, and equal solutions for the other 4. Besides, VND e -ILS 5p was able to find 6 optima for instances that were still open. In terms of time consuming, on average, the time spent on neighborhoods N 1 and N 2 is about 5%, on neighborhood N 3 is about 25%, and the most time consuming phase is the ILS-based perturbation with 70% of the CPU time.

We now proceed to detailed analysis on the behavior of algorithm VND e -ILS 5p . The first analysis is an attempt to learn more about the performance of VND e -ILS 5p if it should run on less time than 5 minutes. For such purpose, we make use of the timeto-target (TTT) plots proposed by Aiex et al. [START_REF] Aiex | Probability distribution of solution time in GRASP: an experimental investigation[END_REF][START_REF] Aiex | TTT plots: a perl program to create time-to-target plots[END_REF]. The hypothesis behind is that CPU times fit a two parameter exponential distribution. Thus, for a given problem instance, TTT plots display on the ordinate axis the probability for the heuristic to obtain a solution as good as a given target value within a running time in seconds, shown on the abscissa axis. We had chosen 8 instances from Table 7 to do this. For each instance we ran VND e -ILS 5p 200 times with different seeds until the algorithm reaches the target value. Figures 3 to 6 show the TTT plots generated with 4 instances for which an average gap of 0% is reached -ATT, NSF.12, y.4.20.4, y.5.100.2. For these instances we set the target value to the optima. On the other hand, Figures 7 to 10 show the TTT plots generated with the instances for which a high average gap is observed -y.4.80.1, y.4.100.1, Z.10x10.60, Z.10x10.80. In these cases, we set the target value to one wavelength less than the best solution found by GA-RWA. TTT plots indicate that VND e -ILS 5p is likely to obtain high quality solutions in a short time. As it can be seen, on instances tested, VND e -ILS 5p has high probability to find very good solutions (optimum or better than the best known) in less than 2 minutes, except for instance y.5.100.2, for which a little more time is needed.

The second analysis tries to bring some insight on which neighborhood brings the best gain. We performed experiments with reduced versions of VND using, along with ILS-based perturbation, neighborhoods N 1 and N 2 separately and in combination with N 3 . Neighborhood N 3 is not tested separately since alone it cannot reduce the number of wavelengths. Table 8 shows numerical results for the reduced versions of VND. The first column presents the instance. Then, the subsequent pairs of columns present the best solution and the average gap for each reduced version of VND. As before, it is reported for each proposed algorithm the results of 5 runs with a time limit of 5 minutes each. The last column presents the lower bound. We remark that although N 3 alone cannot be used to improve solutions, the reduced versions of VND using it in combination with N 1 or N 2 lead to the better results. So, a move in neighborhood N 3 is an important instrument to rearrange requests to further improving moves. It also worth noting that neighborhood N 2 alone is not effective, but in combination with N 3 becomes the most successful reduced version of VND.

Conclusions

We propose an algorithm for the RWA problem that alternates between a VND phase and a ILS-based perturbation phase. In the VND phase we explore three neighborhoods by trying three kinds of moves. The purpose is to reduce one wavelength. The ILS-based phase is called to introduce a perturbation in the current partition of the lightpath requests' set. The perturbation itself does not improve a solution, but it leaves a rearrangement of lightpaths among subsets of the partition that may yield further improvements with another trial of VND. Even though better results were found taking BFD as constructive heuristic, VND-ILS is quite robust with respect to the initial solution and clearly outperforms a multistart variant of BFD. Computation experiments were conducted on the hardest benchmark instances, and significant improvements upon better upper bounds from the literature were achieved. An interesting research direction is to adapt the methods to deal with possibilities of traffic-grooming.

[25] N. Skorin-Kapov,"Routing and wavelength assignment in optical networks using bin packing based algorithms", European Journal of Operational Research 177 (2007), 1167-1179.

[26] H. Zang, J.P. Jue, and B. Mukherjee, "A review of routing and wavelength assignment approaches for wavelength-routed optical WDM networks", Optical Networks Magazine 1 (2000), 47-60.

N 3 Figure 1 :

 31 Figure 1: Searching moves within neighborhoods N 1 , N 2 , and N 3 of VND.

Figure 2 :

 2 Figure 2: ILS-based perturbation by means of an assignment problem.

Figure 3 :

 3 Figure 3: TTT plots produced for instance ATT -target value equal to 20.

Figure 4 :

 4 Figure 4: TTT plots produced for instance NSF.12 -target value equal to 38.

Figure 5 :

 5 Figure 5: TTT plots produced for instance y.4.20.4 -target value equal to 19.

Figure 6 :

 6 Figure 6: TTT plots produced for instance y.5.100.2 -target value equal to 73.

Figure 7 :

 7 Figure 7: TTT plots produced for instance y.4.80.1 -target value equal to 72.

Figure 8 :

 8 Figure 8: TTT plots produced for instance y.4.100.1 -target value equal to 89.

Figure 9 :

 9 Figure 9: TTT plots produced for instance Z.10x10.60 -target value equal to 86.

Figure 10 :

 10 Figure 10: TTT plots produced for instance Z.10x10.80 -target value equal to 114.

Table 1 :

 1 Deviation gaps in percentage for combinations of VND-ILS strategies.

	Set	VNDe-ILSp VNDr-ILSp VNDe-ILS 5p VNDr-ILS 5p
	Realistic	0.00	0.00	0.00	0.00
	Z.20	2.72	2.57	2.36	2.39
	Z.40	3.27	3.15	2.75	2.78
	Z.60	3.11	3.08	2.55	2.62
	Z.80	2.66	2.63	2.41	2.40
	Z.100	4.15	4.15	3.94	3.88
	Y.3	4.25	4.20	3.66	3.75
	Y.4	6.62	6.60	6.37	6.39
	Y.5	1.79	1.66	1.30	1.33
	Average	3.17	3.12	2.82	2.84

Table 2 :

 2 Comparison with multistart BFD on realistic instances.

		Multistart-BFD BFD-VNDe	VNDe-ILS 5p EDP-VNDe-ILS 5p
	Instance λ min	gap(%) λ min gap(%) λ min gap(%) λ min	gap(%) LB
	y.4.20.1	21	23.53	21	23.53	19	11.76	19	11.76 17
	y.4.20.2	28	0.00	28	0.00	28	0.00	28	0.00 28
	y.4.20.3	23	0.00	23	0.00	23	0.00	23	0.00 23
	y.4.20.4	20	8.42	20	7.37	19	0.00	19	0.00 19
	y.4.20.5	21	23.53	21	23.53	19	11.76	19	15.29 17
	y.4.40.1	38	22.58	38	22.58	35	12.90	36	16.13 31
	y.4.40.2	57	0.00	57	0.00	57	0.00	57	0.00 57
	y.4.40.3	43	0.00	43	0.00	43	0.00	43	0.00 43
	y.4.40.4	38	0.00	38	0.00	38	0.00	38	0.00 38
	y.4.40.5

Table 6 :

 6 Comparison with multistart BFD on set Z of instances.

		GA-RWA	VNDe-ILS 5p
	Instance	λ min gap(%) λ min gap(%) LB
	ATT	24	20.0	20	0.0 20
	ATT2	113	0.0	113	0.0 113
	Finland	46	0.4	46	0.0 46
	NSF.3	22	0.9	22	0.0 22
	NSF.12	39	2.6	38	0.0 38
	NSF2.12	35	0.6	35	0.0 35
	Z.10x10.20	31	15.6	29	7.4 27
	Z.6x17.40	87	4.0	85	1.2 84
	Z.10x10.60	87	13.2	84	9.1 77
	Z.4x25.60	195	2.0	193	0.5 192
	Z.10x10.80	115	12.4	112	9.5 103
	Z.8x13.80	134	3.9	130	1.1 129
	Z.6x17.80	176	3.0	171	0.5 171
	Z.5x20.80	209	2.0	206	0.5 205
	Z.4x25.80	260	1.3	258	0.5 257
	Z.5x20.100	257	2.8	253	1.5 250
	y.4.20.4	20	6.3	19	0.0 19
	y.3.40.5	59	12.8	56	7.4 53
	y.3.60.5	86	12.5	82	7.5 77
	y.4.60.5	58	18.4	55	12.2 49
	y.5.60.1	36	9.7	35	6.7 33
	y.3.80.1	122	15.5	115	9.3 106
	y.3.80.5	113	8.8	109	4.8 104
	y.4.80.1	73	55.3	70	48.9 47
	y.4.80.5	75	16.0	72	10.8 65
	y.5.80.1	47	11.2	46	7.0 43
	y.5.80.2	60	1.7	59	0.0 59
	y.4.100.1	90	18.4	86	14.2 76
	y.5.100.1	58	5.5	57	3.6 55
	y.5.100.2	74	1.6	73	0.0 73
	Average		9.3		5.5

Table 7 :

 7 Comparison with GA-RWA on a set of difficult instances. Instance λ min gap(%) λ min gap(%) λ min gap(%) λ min gap(%) λ min gap(%) LI

		N 1		N 2		N 1 + N 2	N 1 + N 3	N 2 + N 3
	ATT	20	0.0	26	33.3	20	0.0	20	0.0	20	0.0 20
	ATT2	113	0.0	115	2.0	113	0.0	113	0.0	113	0.0 113
	Finland	46	0.0	48	5.2	46	0.0	46	0.0	46	0.0 46
	NSF.3	22	0.0	22	0.0	22	0.0	22	0.0	22	0.0 22
	NSF.12	38	0.0	38	0.0	38	0.0	38	0.0	38	0.0 38
	NSF2.12	35	0.0	35	0.0	35	0.0

00

11 00 00 11 11 00 00 11 11 0 1

http://dag.cs.uni-kl.de/research/rwa/

personal communication

Acknowledgements

The authors wish to thank the two anonymous referees for helpful suggestions in improving this paper. The authors from Brazilian institutions were partially supported by CAPES, CNPq, and FAPEMIG, Brazil.

Multistart-BFD BFD-VNDe

VNDe-ILS 5p EDP-VNDe-ILS 5p Instance λ min gap(%) λ min gap(%) λ min gap(%) λ min gap(%) LB y. [START_REF] Banerjee | A practical approach for routing and wavelength assignment in large wavelength-routed optical networks[END_REF]