De nombreux bugs informatiques ont mis en lumière le besoin de certifier les programmes informatiques et la vérification de programmes a connu un développement important au cours des quarante dernières années. Parmi les méthodes possibles, on trouve le model-checking, développé par Clarke et Emerson dans les années 80. Le model-checking consiste à trouver un modèle abstrait pour le système et un formalisme logique pour le comportement puis à vérifier si le modèle vérifie la propriété exprimée dans la logique. La difficulté consiste alors à développer des algorithmes efficaces pour les différents formalismes. Nous nous intéresserons en particulier au formalisme logique de strategy Logic SL, utilisée sur les systèmes multiagents. SL est particulièrement expressif de par son traitement des stratégies (comportements possibles pour les agents du système) comme des objets du premier ordre. Dans sa définition, divers choix sémantiques sont faits et, bien que ces choix se justifient, d'autres possibilités n'en sont pas plus absurdes: tel ou tel choix donne telle ou telle logique et chacune permet d'exprimer des propriétés différentes. Dans cette thèse, nous étudions les différentes implications des différents choix sémantiques. Nous commencerons par introduire SL et préciserons l'étendue des connaissances actuelles. Nous nous intéresserons ensuite aux possibilités non explorées par la sémantique originale. Nous étudierons aussi la logique sur des systèmes quantitatifs (ajout de contraintes d'énergie et de contraintes de compteurs). Finalement, nous examinerons la question des dépendances dans SL[BG] (un fragment de SL). / With the proliferation of computerised devices, software verification is more prevalent than ever. Since the 80's, multiple costly software failures have forced both private and public actors to invest in software verification. Among the main procedures we find the model-checking, developed by Clarke and Emerson in the 80's. It consists in abstracting both the system into a formal model and the property of expected behaviour in some logical formalism, then checking if the property's abstraction holds on the system's abstraction. The difficulty lies in finding appropriate models and efficient algorithms. In this thesis, we focus on one particular logical formalism: the Strategy Logic SL, used to express multi-objectives properties of multi-agents systems. Strategy Logic is a powerful and expressive formalism that treats strategies (i.e. potential behaviours of the agents) like first-order objects. It can be seen as an analogue to first-order logic for multi-agents systems. Many semantic choices were made in its definition without much discussion. Our main contributions are relative to the possibilities left behind by the original definition. We first introduce SL and present some complexity results (including some of our owns). We then outline some other semantic choices within SL's definition and study their influence. Third, we study the logic's behaviour under quantitative multi-agents systems (games with energy and counter constraints). Finally, we address the problem of dependencies within SL[BG], a fragment of SL.

Cette thèse porte sur l'efficacité des algorithmes distribués de partage des ressources et des algorithmes de découvert de chemin en ligne. Dans la première partie de la thèse, nous analysons un jeu dans lequel les utilisateurs paient pour utiliser une ressource partagée. La ressource allouée à un utilisateur est directement proportionnel à son paiement. Chaque utilisateur veut minimiser son paiement en assurant une certaine qualité de service. Ce problème est modélisé comme un jeu non-coopératif de partage des ressources. A cause du manque des expressions analytiques de la discipline de file d'attente sous-jacente, nous pouvons résoudre le jeu que sous certaines hypothèses. Pour le cas général, nous développons une approximation basée sur un résultat fort trafic et nous validons la précision de l'approximation numériquement.Dans la deuxième partie, nous étudions l'efficacité des jeux de balance de charge, c'est à dire, nous comparons la perte de performance de routage non coopératif décentralisé avec un routage centralisé. Nous montrons que le PoA est une mesure très pessimiste car il est atteint que dans des cas pathologiques. Dans la plupart des scénarios, les implémentations distribués de balance de charge effectuent presque aussi bien que la mise en œuvre centralisée optimale.Dans la dernière partie de la thèse, nous analysons problème de découverte chemin optimal dans les graphes complets. En ce problème, les valeurs des arêtes sont inconnues, mais peuvent être interrogés. Pour une fonction donnée qui est appliquée à des chemins, l'objectif est de trouver un meilleur chemin de valeur à partir d'une source vers une destination donnée interrogation le plus petit nombre de bords. Nous vous proposons le rapport de requête en tant que mesure de l'efficacité des algorithmes qui permettent de résoudre ce problème. Nous prouvons une limite inférieure pour ne importe quel algorithme qui résout ce problème et nous avons proposé un algorithme avec un rapport de requête strictement inférieure à 2. / This thesis deals with the efficiency of distributed resource sharing algorithms and of online path discovery algorithms. In the first part of the thesis, we analyse a game in which users pay for using a shared resource. The allocated resource to a user is directly proportional to its payment. Each user wants to minimize its payment while ensuring a certain quality of service. This problem is modelled as a non-cooperative resource-sharing game. Due to lack of analytical expressions for the underlying queuing discipline, we are able to give the solution of the game only under some assumptions. For the general case, we develop an approximation based on a heavy-traffic result and we validate the accuracy of the approximation numerically. In the second part, we study the efficiency of load balancing games, i.e., we compare the loss in performance of noncooperative decentralized routing with a centralized routing. We show that the PoA is very pessimistic measure since it is achieved in only pathological cases. In most scenarios, distributed implementations of load-balancing perform nearly as well as the optimal centralized implementation. In the last part of the thesis, we analyse the optimal path discovery problem in complete graphs. In this problem, the values of the edges are unknown but can be queried. For a given function that is applied to paths, the goal is to find a best value path from a source to a given destination querying the least number of edges. We propose the query ratio as efficiency measure of algorithms that solve this problem. We prove a lower-bound for any algorithm that solves this problem and we proposed an algorithm with query ratio strictly less than 2.

Cette thèse d'HDR en anglais, présente l'essentiel de mes travaux de 1996 à 2005. Voir le résumé anglais pour plus de détails.