Les jeux de congestion dans les réseaux sous l’angle de la vérification

Les jeux de congestion sont un domaine de recherche bien étudié ; dans ce domaine, les jeux de congestion dans les réseaux permettent de représenter la congestion des réseaux de distribution, et d’étudier à quel point un modèle de réseau est bon ou mauvais en termes de coût total lorsque chaque joueur joue de façon égoïste, cherchant uniquement à optimiser son propre coût ; Nous considérons ces jeux de congestion du point de vue des méthodes formelles, cherchant à vérifier par exemple que, dans un réseaux fixé, il existe un profil de stratégies optimal qui satisfasse une propriété donnée. Nous définissons un modèle de jeux de congestion avec deux particularités : d’une part, le calcul du coût d’une transition dépend du nombre de joueurs utilisant simultanément une arête ; d’autre part, les joueurs choisissent leur chemin de façon dynamique en fonction des choix des autres joueurs. Nous montrons que dans ce modèle les équilibres de Nash existent toujours en montrant la convergence de la dynamique de meilleure réponse. Nous étudions ensuite le problème de vérification mentionné ci-dessus, résolvant le problème de l’existence d’un équilibre social, d’un équilibre de Nash ou d’un équilibre parfait en sous-jeux ayant un côut borné. Dans une deuxième partie, nous étudions les jeux de congestion paramétrés, dans lesquels le nombre de joueurs est un paramètre. Nous nous intéressons à l’évolution des équilibres de Nash en fonction du nombre de joueurs : notre objectif est de calculer efficacement l’ensemble des équilibres de Nash pour un nombre arbitrairement grand de joueurs, à partir des équilibres de Nash pour de petits nombres de joueurs. Nos premiers résultats portent sur les réseaux série-parall‘ele, sans les particularités ci-dessus. Nous conjecturons que ces résultats s’étendent à l’ensemble des graphes, ce qui donnerait lieu à un calcul efficace de tous les équilibres de Nash, quel que soit le nombre de joueurs.Congestion games are a well-studied areaof research, and Network congestion games (NCG) model the problem of congestion in flow networks. The most common problem is to study, broadly speaking, how well or how bad a model of NCG is in terms of total cost for all players when each player plays selfishly. We view network congestion games from a formal methods standpoint, in which we are interested in problems like given an instance (network and number of players fixed) of a chosen model of NCG and given a specification, does there exist an optimal profile satisfying the specification? We define a model of network congestion games with two peculiarities: first, the players bear congestion effect on their cost for an edge only if they use that edge with other players simultaneously; second, players can choose their path dynamically, at each step of their route, which differs from the classical setting where players choose their path at the beginning. We show that in this model Nash Equilibria always exist by showing convergence of best-response dynamics. Then we study three decision problems on Social optima, Nash Equilibria and Subgame perfect Equilibria, each of which asks whether, given an instance of our model and a bound, there is a corresponding strategy profile with bounded social cost. In the second part of the thesis, we study parameterized network congestion games, where the number of players is left as a parameter. Our main problem here is to compute Nash Equilibria for instances with many players, from instances with fewer players, instead of computing them from scratch. Here, we started solving the problem for the classical model of NCG, without the above mentioned two pecularities, and with the arena restricted to series-parallel graph. We obtained some preliminary results on this problem, and formulated a conjecture about how to efficiently compute all Nash equilibria for any number of players