Nous nous intéressons à la représentation de graphes dans le prouveur Coq. Nous avons choisi de les représenter par des types coinductifs dont nous voulions explorer l'utilisation. Ceux-ci permettent de rendre succincte et élégante la représentation et d'obtenir la navigabilité par construction. Nous avons dû contourner la condition de garde dont le but est d'assurer la validité des opérations effectuées sur les objets coinductifs. Son implantation dans Coq est restrictive et interdit parfois des définitions sémantiquement correctes. Une formalisation canonique des graphes dépasse ainsi l'expressivité directe de Coq. Nous avons donc proposé une solution respectant ces limitations, puis nous avons défini une relation sur les graphes nous permettant d'obtenir la même notion d'équivalence qu'avec une représentation classique tout en gardant les avantages de la coinduction. Nous montrons qu'elle est équivalente à une relation basée sur des observations finies.

Ce travail porte sur la production de code séquentiel à partir du langage flot de données synchrone Lustre. La difficulté essentielle provient de l'aspect déclaratif du langage. En effet, il n'y a pas d'instruction de contrôle dans le langage Lustre ; toute la structure de contrôle du code objet doit donc être synthétisée par le compilateur. Cette synthèse consiste à construire un automate fini en simulant exhaustivement le comportement des variables booléennes du programme. Le code produit est particulièrement rapide ; en effet, la plupart des calculs booléens sont effectués une fois pour toute dès la compilation. En contrepartie, l'aspect exhaustif de cette démarche provoque parfois une véritable explosion de la taille du code. Ce problème peut être dû à la complexité intrinsèque du programme source ; il faut dans ce cas chercher un compromis entre rapidité et taille mémoire. Mais l'explosion peut être causée par la méthode de construction, qui produit très souvent des automates non minimaux ; nous avons donc étudié et développé un algorithme original qui construit à coup sûr des automates minimaux. Cet algorithme fait appel à de nombreuses manipulations symboliques de fonctions booléennes, que nous avons pu implémenter efficacement grâce à une représentation basée sur les graphes binaires de décision.

Dans cette thèse, nous étudions deux problèmes de théorie des graphes largement étudiés ces trois dernières décennies: les codes correcteurs d'erreur et la domination.<br />Nous étudions d'abord deux généralisations des codes correcteurs d'erreurs : les codes parfaits sur des alphabets mixtes et les codes pondérés de rayon un. Ces problèmes ont beaucoup été étudiés sur la métrique de Hamming.<br />Nous les étudions dans la métrique de Lee, et nous montrons des résultats aussi bien d'existence que d'inexistence.<br />Nous montrons aussi que le rapport de dualité entre la domination et les codes est fort pour la grille carrée lorsque l'on considère des boules sans le centre.<br />Puis, nous étudions la domination dans les produits de graphes. Depuis que Vizing a conjecturé en 1968 que la domination est surmultiplicative pour le produit cartésien de graphes, les relations entre des variantes du nombre de domination d'un produit de graphes et ses facteurs ont attiré beaucoup d'attention. Après avoir donné quelques bornes sur le nombre de domination totale du produit direct de graphes, nous déterminons le nombre de domination de puissance des produits de chemins.<br />Puis, nous montrons une conjecture ``à la Vizing'' pour le nombre de domination totale supérieure du produit cartésien.<br />Ensuite, nous étudions la domination avec une approche structurelle. En continuation de l'étude de Favaron et Henning, nous fournissons plusieurs bornes supérieures sur le nombre de paire-domination des graphes sans étoiles, pour chaque nombre de branches, et des graphes sans P_5. Nous proposons aussi des familles infinies de graphes pour lesquels ces bornes sont atteintes.<br />Enfin, nous comparons la domination totale supérieure et la paire-domination supérieure, deux variantes de la domination qui ont attiré l'attention récemment, et nous donnons des bornes précises pour les arbres.

A partir de l'identification des 3 hypothèses que sont l'information imparfaite, l'asymétrie informationnelle et la rationalité limitée, la science économique a du profondément modifier la représentation et l'explication des phénomènes économiques du modèle standard. Ce mouvement a concerné à la fois la vision des marchés et celle de la firme. A partir de la notion de « firme processeur d'information » qui est celle largement retenue dans l'orthodoxie néo-classique ou apparentée, cette thèse propose de penser l'articulation entre organisation, information et pouvoir. Afin de dépasser la double tradition en économie qui consiste soit à postuler le pouvoir (approche des radicaux), soit à le nier (courant néo-classique), une démarche pragmatique essaie d'aller chercher en dehors des frontières de l'économie des modèles susceptibles de donner des pistes de représentation du pouvoir intra-organisationnel. Ce choix est renforcé par les travaux de micro-économie contemporain qui mobilisent eux-mêmes des travaux d'inspiration « sociologique » et qui permettent de penser l'introduction du pouvoir dans les modèles de al théorie standard. Cette démarche aboutit au choix d'une définition opérationnelle du pouvoir ouvrant la voie à une quantification de l'organisation. Celle-ci est menée en utilisant la théorie des graphes d'influence, qui allie la représentation topologique de la théorie des graphes au calcul matriciel de la méthodologie input-output. Les indicateurs qu'elle fournit sont calculés dans le cadre de l'étude d'une organisation concrète. La base de données est construite à partir des flux d'échange de mails. Ils fournissent une caractérisation assez fine de l'organisation en distinguant notamment le niveau global du niveau local. Ils permettent également de discuter de l'articulation entre la structure formelle et la structure informelle. <br />Finalement sur la base de trois définitions des notions d'organisation, d'information et de pouvoir, élaborées à partir d'une large revue de la littérature en économie des organisations, cette thèse propose des indicateurs permettant de déterminer qui a le pouvoir dans une organisation concrète définie comme une structure d'échanges d'informations.

Les jeux à deux joueurs sur des graphes finis ou infinis permettent de modéliser de nombreux problèmes liés à la vérification des systèmes. Le système spécifié dépend de la nature du graphe de jeu considéré tandis que la propriété à vérifier est décrite par la condition de gain. Le premier joueur, Eve, représente un programme qui évolue dans un environnement hostile représenté par le second joueur, Adam. Dans ce formalisme, Eve possède une stratégie gagnante si et seulement si le programme peut être contrôlé de sorte à satisfaire la propriété spécifiée par la condition de gain. On souhaite alors décider si Eve possède une stratégie gagnante et si oui la déterminer, afin de synthétiser ensuite un contrôleur. <br /><br />Dans cette thèse, les graphes de jeu considérés sont des graphes de processus à pile qui offrent une représentation finie simple de systèmes infinis relativement complexes. Sur de tels graphes, on peut considérer des conditions de gain classiques (accessibilité, Büchi ou parité) mais aussi des conditions plus spécifiques au modèle comme celles portant sur le bornage de la pile. On peut également combiner ces dernières entre elles. <br /><br />Une première contribution a été de fournir une représentation des ensembles de positions gagnantes pour les jeux de parité ainsi qu'une nouvelle présentation des résultats connus pour ces derniers. On a alors pu étendre de façon naturelle les techniques de preuves à d'autres conditions de gain, notamment à celles portant sur le bornage de la pile. <br /><br />Une autre contribution a été la description d'une famille de conditions de gain de complexité borélienne arbitraire finie pour lesquelles les jeux (sur des graphes finis ou sur des graphes de processus à pile) restent décidables. <br /><br />L'étude des jeux sur les graphes de BPA et sur les graphes de processus à compteur a permis de proposer des techniques propres à ces modèles qui fournissent alors des bornes de complexité meilleures que celles obtenues dans le cas général des graphes de processus à pile. <br /><br />Enfin, une dernière contribution a été de proposer une solution pour les jeux sur des graphes de processus à pile munis de conditions combinant des conditions régulières et des conditions sur la hauteur de pile et pour des conditions décrites par des automates à pile avec visibilité.

L'adaptabilité des applications logicielles peut être séparée en deux catégories. La première concerne l'adaptation comportementale appelée aussi adaptation algorithmique. Cette adaptation traite la redéfinition du comportement de l'application et de ses composants et implique, par exemple, l'introduction d'une nouvelle méthode dans l'interface d'un composant ou le changement du protocole d'orchestration qui coordonne un ensemble de services. Nos travaux, que nous classons dans une deuxième catégorie, traitent l'adaptation structurelle et considèrent une reconfiguration au niveau architectural. Ce type de reconfiguration traite l'organisation de l'architecture et consiste, par exemple, à remplacer un composant défaillant par un autre composant qui possède les mêmes fonctionnalités ou rediriger un client d'un service qui ne respecte pas le contrat de QdS vers un service susceptible d'offrir de meilleures garanties. Dans ce mémoire, nous définissons un méta-modèle relatif à la description et la gestion automatique des architectures dynamiques. Les instances des architectures sont décrites par des graphes étendus où les composants (ou les services) sont représentés par des n\oe uds, et les interdépendances (e.g. les connexions, les relations de contrôle ...etc) sont décrites par des arcs. Les styles architecturaux sont spécifiés par des grammaires de graphes étendues. Le méta-modèle admet des descriptions en considérant différents niveaux d'abstraction et offre des mécanismes pour raffiner ou abstraire les descriptions selon des points de vues spécifiques. Il permet, aussi, de décrire le protocole de gestion de l'architecture et de caractériser les propriétés architecturales à préserver pour chaque niveau architectural considéré. Nous avons développé un algorithme de recherche d'homomorphismes de graphes et un algorithme de transformation de graphes pour les grammaires de graphes étendus définis pour notre méta-modèle. L'analyse de complexité des algorithmes ains i que les résultats expérimentaux obtenus ont permis de conclure à leur efficacité. Une deuxième version des deux algorithmes a été définie profitant de la spécificité du contexte de la transformation de graphes. L'analyse de complexité de ces nouvelles versions donne des résultats encore plus performants pour le passage à l'échelle. Notre approche a été éprouvée en l'appliquant à un cas d'étude dans le contexte des activités d'opération d'intervention d'urgence. L'application implique des groupes structurés de robots ou de personnel militaire qui disposent de ressources inégales en capacités de communication, en CPU et en énergie. Les besoins d'adaptabilité découlent des changements du contexte d'exécution, de l'occurrence de pannes et du provisionnement de la QdS.

La recherche thérapeutique a de plus en plus recours à des techniques de modélisation, dites de criblage virtuel, visant à corréler la structure d'une molécule avec ses propriétés biologiques. En particulier, l'utilisation de modèles prédictifs quantifiant la toxicité d'une molécule ou son activité vis à vis d'une cible thérapeutique, permet de réduire de manière considérable le temps et les coûts nécessaires à la mise au point de nouveaux médicaments. Nous nous proposons d'aborder ce problème dans le cadre des méthodes à noyaux, qui permettent de construire de tels modèles de manière efficace dès lors que l'on dispose d'une fonction noyau mesurant la similarité des objets que l'on considère. Plus particulièrement, l'objet de cette thèse est de définir de telles fonctions noyaux entre structures bi- et tri-dimensionnelles de molécules. D'un point de vue méthodologique, ce problème se traduit respectivement comme celui de comparer des graphes représentant les liaisons covalentes des molécules, ou des ensembles d'atomes dans l'espace. Plusieurs approches sont envisagées sur la base de l'extraction et la comparaison de divers motifs structuraux qui permettent d'encoder les groupes fonctionnels des molécules à différents niveaux de résolution. Les validations expérimentales suggèrent que cette méthodologie est une alternative prometteuse aux approches classiques en criblage virtuel.

Thèse doctorat : Génie Electrique : Villeurbanne, INSA : 2003. / Titre provenant de l'écran-titre. Bibliogr. à la fin de chaque chapitre.

Thèse doctorat : Ingénierie Informatique : Villeurbanne, INSA : 1997. / Titre provenant de l'écran-titre. Bibliogr. p. 151-159.

Thèse doctorat : Productique : Automatique et Informatique industrielle : Lille 1 : 2003. / N° d'ordre (Lille 1) : 3424. Pagination ajoutée entre crochets pour les annexes et la bibliographie. Bibliogr. 12 p.