Étant donnés un planning aérien et des prévisions de demande, le problème d'affectation de flotte aérienne consiste à déterminer la meilleure façon de répartir les types d'appareils sur les vols. Cette répartition a un impact majeur sur le profit d'une compagnie aérienne, puisqu'elle détermine les quantités de places disponibles sur les itinéraires du réseau aérien, ainsi que le coût de fonctionnement de celui-ci. Des décennies de recherche ont rendues les modélisations de ce problème de plus en plus réalistes. Cette thèse s'inscrit dans la continuité de ces recherches en considérant le problème d'affectation de flotte dans un contexte où les demandes des passagers sont incertaines. Nous proposons dans un premier temps une étude autour des deux modèles de la littérature les plus utilisés dans l'industrie, FAM et IFAM. Nous montrons que FAM peut être vu comme une Relaxation Lagrangienne de IFAM, avec des multiplicateurs Lagrangiens particuliers. Nous implémentons cette relaxation, et nous appliquons des résultats connus pour l'étendre en une génération de colonnes basée sur une décomposition de Dantzig-Wolfe de IFAM. Nous étudions ensuite les effets que l'imprécision des prévisions peut avoir sur la performance d'IFAM, et nous présentons au terme de cette étude une nouvelle approche pour modéliser le problème d'affectation de flotte. Notre modèle, Market Driven Fleet Assignment Model (MDFAM), intègre les demandes par itinéraires comme variables de décision, et contraint ces demandes plutôt que de les considérer comme une entrée fixe. Nous appelons les contraintes résultantes des contraintes de Marché. Nous illustrons la flexibilité de cette approche à travers divers exemples, et nous proposons une série d'expériences visant à déterminer quelles sont les contraintes de marché donnant les meilleurs résultats. Nous comparons les différents modèles, et nous montrons que MDFAM peut atteindre des niveaux de performance similaires à ceux offert par IFAM, tout en étant plus facile à utiliser et à implémenter.

Dans ce mémoire, nous presentons les meta-heuristiques inspirées du comportement des fourmis lors de la recherche de nourriture, les OCF. Nous confrontons ces méthodes face aux principales méta-heuristiques connues. Pour cela, nous proposons de nous placer sous le point de vue de l'utilisation de la mémoire et nous présentons taxinomie qui étend celle des AMP. Nous proposons deux nouvelles adaptations du modéle des fourmis. La premiere est l'algorithme ANTabu, il s'agit d'une méthode hybride pour la résolution du PAQ. Il associe l'utilisation des fourmis artificielles et d'une méthode de recherche locale robuste : la recherche tabou. Le parallélisme intrinseque des systèmes de fourmis nous a amene a developper un modele paralléle pour ANTabu.<br />Cette méthode intègre également une puissante fonction de diversification et l'utilisation de bornes qui lui permettent d'eviter d'être piege au niveau d'optima locaux.<br />La seconde application développee est AP, cet algorithme est l'adaptation du modèle de coopération des fourmis a la programmation automatique. Son mécanisme de fonctionnement<br />est simple, puisque à chaque itération on crée une nouvelle population en utilisant l'information emmagasinée par la phéromone. L'intérêt de cette gestion de l'information est qu'elle n'utilise pas de mécanismes complexes. Nous présentons cette méthode face a l'algorithme de base tel que Koza l'a défini.

This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting of a phase of computations, then communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based ourselves on Why, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-Why, our tool for the proof of BSP programs. This tools uses a generation of a sequential program to simulate the parallel program in input, thus allowing the use of Why and the numerous associated provers to prove the proof obligations. We then show how BSP-Why can be used to prove the correctness of some basic BSP algorithms, and also on a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-Why tool, we give a formalisation of the language semantics, in the Coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program

La complexité arithmétique est l'étude des ressources nécessaires pour calcu- ler des polynômes en n'utilisant que des opérations arithmétiques. À la fin des années 70, Valiant a défini (de manière semblable à la complexité booléenne) des classes de polynômes. Les polynômes, ayant des circuits de taille polyno- miale, considérés faciles forment la classe VP. Les sommes exponentielles de ces derniers correpondent alors à la classe VNP. L'hypothèse de Valiant est la conjecture que VP ̸= VNP.Bien que cette conjecture soit encore grandement ouverture, cette dernière semble toutefois plus accessible que son homologue booléen. La structure algé- brique sous-jacente limite les possibilités de calculs. En particulier, un résultat important du domaine assure que les polynômes faciles peuvent aussi être cal- culés efficacement en paralèlle. De plus, quitte à autoriser une augmentation raisonnable de la taille, il est possible de les calculer avec une profondeur de calcul bornée par une constante. Comme ce dernier modèle est très restreint, de nombreuses bornes inférieures sont connues. Nous nous intéresserons en premier temps à ces résultats sur les circuits de profondeur constante.Bürgisser a montré qu'une conjecture (la τ-conjecture) qui borne supérieu- rement le nombre de racines de certains polynômes univariés, impliquait des bornes inférieures en complexité arithmétique. Mais, que se passe-t-il alors, si on essaye de réduire, comme précédemment, la profondeur du polynôme consi- déré? Borner le nombre de racines réelles de certaines familles de polynômes permetterait de séparer VP et VNP. Nous étudierons finalement ces bornes su- périeures sur le nombre de racines réelles.

Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C.

On trouve dans la littérature de nombreux exemples de jeux où les stratégies souhaitées sont soumises à des contraintes ''transversales'' portant sur des ensembles de parties, reliées entre elles par quelque relation sémantique. L'exemple le plus fameux est celui des stratégies dans les jeux à information imparfaite, et les jeux où la condition de gain a un aspect épistémique en sont d'autres. Cependant, aucune étude approfondie n'a à notre connaissance été menée sur ce type de contraintes dans leur généralité. C'est ce que nous nous proposons de commencer dans cette thèse. Nous définissons donc une notion générale de stratégies uniformes. Les propriétés d'uniformité des stratégies sont exprimées dans un langage logique qui étend CTL∗ avec deux quantificateurs originaux. Ces quantificateurs sont très proches des opérateurs de connaissance classiques en logique épistémique, et font intervenir des ensembles de parties reliées entre elles par des relations binaires. Nous montrons comment cette notion de stratégies uniformes capture les exemples connus de la littérature, puis nous étudions en profondeur le problème de la synthèse de stratégies uniformes, en considérant que les relations binaires entre les parties sont reconnaissables par des automates finis (relations rationnelles). Nous établissons plusieurs résultats de décidabilité et de complexité, reposant largement sur des techniques d'automates : nous introduisons notamment comme outils les automates d'arbres bondissants et les automates d'ensembles d'informations. Par ailleurs, nos résultats permettent d'améliorer des résultats existants et d'en établir de nouveaux, dans les domaines du model-checking des logiques temporelles et épistémiques, ainsi que de la planification épistémique.

Les méthodes de recherche de similarités les plus fréquemment utilisées dans le cadre de la génomique sont heuristiques.<br />Elles se basent sur un principe de filtrage du texte qui permet de localiser les régions potentiellement similaires.<br />Dans cette thèse, nous proposons de nouvelles définitions de filtres pour la recherche de similarités sur les séquences génomiques et des algorithmes associés pour mesurer leurs caractéristiques.<br /> Plus précisément, nous avons étudié le modèle des graines espacées, et proposé un algorithme d'évaluation de l'efficacité des graines sur des similarités d'une classe particulière (similarités dites homogènes). Nous avons également développé un algorithme général pour la mesure de l'efficacité des graines, ainsi qu'un nouveau modèle de graine appelé graine sous-ensemble, extension du modèle des graines espacées. Enfin nous donnons, dans le cadre du filtrage sans perte, une extension à l'aide de graines multiples, que nous analysons et appliquons au problème de la conception d'oligonucléotides.<br /> Nous avons réalisé et donnons accès à des outils pour la conception des filtres, ainsi que pour la recherche de similarités.

Dans un espace discret, comme l'ensemble des points à coordonnées entières, la modélisation de l'isotropie pose des difficultés théoriques notables. À ce jour, aucune théorie géométrique sur $\ZZ^n$ n'est apte à rendre compte de l'isotropie telle qu'elle est décrite par la géométrie euclidienne. Dans l'optique de contribuer à cette problématique, nous nous intéressons à la conception d'algorithmes capables de donner aux rotations discrètes des propriétés proches de celles de la rotation euclidienne. Ces algorithmes doivent de plus fonctionner à base d'arithmétique entière. Après avoir montré la non-existence de rotation discrète transitive sur $\ZZ^n$, nous introduisons un codage de rotations discrètes que nous relions à la fois à la dynamique symbolique et aux automates cellulaires. Il s'agit alors de mener une étude locale des rotations discrètes. Cette étude se situe au carrefour entre géométrie discrète et systèmes dynamiques symboliques. La pertinence des configurations obtenues est justifiée par l'existence de transducteurs planaires capables d'effectuer des rotations à partir des configurations. Ensuite, afin de réinterpréter ces configurations dans le cadre de la théorie des systèmes dynamiques, nous étendons des notions classiques de cette théorie à la dimension 2. Pour la rotation discrétisée, la dynamique symbolique associée est conjuguée avec un jeu de deux translations orthogonales sur un tore bidimensionnel. Après analyse, nous constatons que les configurations obtenues sont des superpositions de configurations de faible complexité. Cela évoque alors les généralisations planaires des mots sturmiens étudiées entre autres par Valérie Berthé et Laurent Vuillon. Des résultats analogues sont aussi obtenus pour les rotations $3$-transvections. L'analyse les rotations discrètes par le biais de systèmes dynamiques a permis de nombreux résultats : mise en évidence de la quasipériodicité des configurations, calcul de la fréquence des symboles, caractérisation des rotations discrétisées bijectives, ce qui est aussi la réciproque du théorème d'Éric Andrès et Marie-Andrée Jacob. Nous avons aussi étudié les discontinuités du processus de rotation. Ces discontinuités ont lieu pour des angles issus d'un sous-ensemble des angles quadratiques (i.e. les angles charnières). En combinant ces remarques, nous aboutissons à deux algorithmes. Le premier algorithme réalise des rotations sans faire aucun calcul à virgule flottante et sans calculer aucun sinus ni aucun cosinus. Il fonctionne de manière incrémentale et en ordre de complexité optimal. Le second algorithme est une implémentation de la rotation $3$-transvections sur automates cellulaires. D'autres pistes pour la conception d'algorithmes sont mentionnées dans la thèse. En outre, nous nous intéressons aussi aux méthodes substitutives qui engendrent les configurations de rotations. Pour les angles quadratiques, nous montrons que les configurations de rotations sont des entrelacements de configurations autosimilaires; et nous présentons le schéma d'une approche basée sur les graphes de Rauzy pour l'inférence de substitutions planaires. En combinant ces deux approches, nous mettons en avant les éléments essentiels de la démonstration de l'autosimilarité de $C_{\pi/4}$. Les applications potentielles de cette thèse concernent à terme l'implémentation d'algorithmes de rotations pour processeurs graphiques. Elle contribue aussi à l'étude des méthodes algorithmiques pour la modélisation physique en milieu discret de phénomènes isotropes.

Alors que l'on observe une disponibilité croissante de données décrivant des objets 3D, il semble essentiel de disposer de moyens de traitement efficaces de ces derniers. Ainsi, nous présentons dans ce mémoire un ensemble d'outils de manipulation de surfaces, qui exploitent à la fois leurs propriétés géométriques et topologiques. Après avoir décrit différents résultats classiques de topologie, et les structures et résultats fondamentaux de la topologie algorithmique, nous présentons les concepts de M-tuiles et M-pavages, offrant notamment une grande souplesse combinatoire, et permettant de décrire finement le résultat d'algorithmes de découpage topologique. En s'appuyant sur les possibilités de description de ce formalisme, nous présentons différents algorithmes de découpage de surface, prenant en compte non seulement la topologie et la géométrie des surfaces, mais également les propriétés des M-tuiles issues de ces découpages. Nous présentons également dans ce mémoire une généralisation des lacets par les n-cets, permettant notamment de décrire une approche originale de pavage de surfaces en cylindres puis en quadrangles. Enfin, deux applications de ces outils de découpage sont présentées. Dans un premier temps, nous déclinons ces algorithmes de découpage dans le contexte de l'infographie, en proposant un ensemble d'outils d'aide à la manipulation de surfaces. Puis nous présentons dans un second temps une chaîne complète de traitement de données issues de l'imagerie médicale, permettant la visualisation dynamique de données complexes sur des cartes planes de la surface du cerveau, en illustrant sa pertinence dans le contexte de la stimulation corticale. En conclusion de ces travaux, nous présentons les perspectives que laissent entrevoir ces développements originaux, notamment en exploitant les possibilités offertes par les n-cets et les M-pavages, qui semblent multiples. Nous soulignons également la richesse qu'assure une exploration des domaines applicatifs par des outils issus de la géométrie algorithmique.

Dans un système multi-agent (SMA) réactif, le lien entre le comportement collectif et celui des individus qui composent ce système est difficile à établir. Obtenir un comportement particulier est donc également difficile. Nous défendons le principe de maîtriser le comportement d'un SMA par une approche de contrôle. Pour cela, nous agissons sur le SMA à partir d'informations relatives à ses comportements globaux. Pour y parvenir, nous proposons tout d'abord de modéliser la dynamique globale du SMA sous forme d'un graphe d'états. Des outils d'apprentissage par renforcement permettent de construire ce graphe et de calculer une politique qui indique quelle action effectuer en fonction de l'état courant et d'un comportement cible à atteindre. Ensuite, cette politique est exploitée pour contrôler le SMA. L'originalité de notre proposition est de s'appuyer sur la dynamique du SMA décrite à son niveau global. Ainsi, les différents comportements du SMA sont exprimés dans notre proposition au même niveau de description que celui du comportement à atteindre. La proposition est appliquée au contrôle d'un SMA inspiré du déplacement de piétons dans un couloir. Nous la comparons à d'autres approches destinées à maîtriser le comportement d'un SMA. Nous vérifions que le principe du contrôle au niveau global fonctionne. Nous montrons que notre proposition fournit de bonnes performances de contrôle et permet d'atteindre un comportement cible plus fréquemment que les autres approches testées. Nous posons ainsi les premières pierres d'un cadre paradigmatique pour le contrôle au niveau global des systèmes multi-agents.