L’objectif du project FerroCOTS est de faire évoluer l’architecture de contrôle-commande ferroviaire embarqué des relais électriques vers des Composant-sur-Etagère (COTS) programmables, ici des cartes FPGA (Field-Programmable Gate Array en anglais). Toutefois, l'absence d’une méthode appropriée de spécification et vérification formelles est un obstacle important au développement d’une architecture de contrôle-commande à base de COTS. Dans cette thèse, nous proposons tout d'abord des techniques systématiques de raffinement des exigences brutes et qui permettent de transformer des exigences informelles en des spécifications formelles, tout en guidant et assistant le processus de raffinement et l'étape de formalisation. En l'occurrence, deux méthodes de raffinement des exigences ont été développées. Le cadre de formalisation choisi pour cette méthode de formalisation des exigences est la logique temporelle CTL*, qui est un sur-ensemble des logiques CTL (Computation Tree Logic en anglais) et LTL (Linear Time Logic en anglais). Ainsi, les exigences raffinées peuvent être formalisées à l'aide de CTL*. En outre, ces formules en CTL* offrent une base formelle pour la vérification et la validation du système. Puis, à partir des spécifications formelles exprimées sous forme de propriétés CTL*, nous présentons une méthode pour générer des scénarios de test à partir des formules CTL*. La méthode de test utilise le concept de « non-vacuité » pour générer des scénarios de test « Intelligents », qui soient capables de conduire la simulation à une réfutation d’une propriété pour que les bugs dans un système sous test peuvent être détectés. / The goal of the FerroCOTS project is to develop an architecture of embedded railway command/control systems from electrical relays towards programmable Commercial-Off-The-Shelf (COTS) components, here some high-speed Field-Programmable Gate Array (FPGA) digital devices. However, the lack of appropriate formal specification and verification means is a huge obstacle to develop a COTS based control/command architecture. In this thesis, firstly we propose systematic requirement refinement techniques to transform informal requirements into formal specifications, while guiding and assisting the refinement process and the formalization step. In this case, two requirement refinement methods have been developed. The formalization framework chosen for requirement formalization is the temporal logic CTL*, which is a superset of the logic Computation Tree Logic (CTL) and the Linear Time Logic (LTL). Thus, the refined requirements are formalized using CTL*. In addition, the obtained CTL* formulas provide a formal basis for system verification and validation. On the other hand, based on formal specifications expressed as CTL* properties, we present a method for generating test cases from CTL* formulas. The test method uses the concept of non-vacuity to generate “Intelligent” test benches that are capable of driving the simulation to a property refutation so that the bug of the system under test can be detected.

La programmation par contraintes permet de modéliser des problèmes et offre des méthodes de résolution efficaces. Cependant, sa complexité augmentant ces dernières années, son utilisation, notamment pour modéliser des problèmes, est devenue limitée à des utilisateurs possédant une bonne expérience dans le domaine. Cette thèse s’inscrit dans un cadre visant à automatiser la modélisation. Les techniques existantes ont montré des résultats encourageants mais certaines exigences rendent leur utilisation encore problématique. Dans une première partie, nous proposons de dépasser une limite existante qui réside dans la nécessité pour l’utilisateur de fournir des solutions du problème qu’il veut modéliser. En remplacement, il nous fournit des solutions de problèmes proches, c’est-à-dire de problèmes dont la sémantique de fond est la même mais dont les variables et leur domaine peuvent changer. Pour exploiter de telles données, nous proposons d’acquérir, grâce à des techniques de programmation logique inductive, un modèle plus abstrait que le réseau de contraintes. Une fois appris, ce modèle est ensuite transformé pour correspondre au problème initial que souhaitait résoudre l’utilisateur. Nous montrons également que la phase d’apprentissage se heurte à des limites pathologiques et qui nous ont contraints à développer un nouvel algorithme pour synthétiser ces modèles abstraits. Dans une seconde partie, nous nous intéressons à la possibilité pour l’utilisateur de ne pas donner d’exemples du tout. En partant d’un CSP sans aucune contrainte, notre méthode consiste à résoudre le problème de l’utilisateur de manière classique. Grâce à un arbre de recherche, nous affectons progressivement des valeurs aux variables. Quand notre outil ne peut décider si l’affectation partielle courante est correcte ou non, nous demandons à l’utilisateur de guider la recherche sous forme de requêtes. Ces requêtes permettent de trouver des contraintes à ajouter aux modèles du CSP et ainsi améliorer la recherche. / Constraint programming allows to model many kind of problems with efficient solving methods. However, its complexity has increased these last years and its use, notably to model problems, has become limited to people with a fair expertise in the domain. This thesis deals with automating the modeling task in constraint programming. Methods already exist, with encouraging results, but many requirements are debatable. In a first part, we propose to avoid the limitation consisting, for the user, in providing solutions of the problem she aims to solve. As a replacement of these solutions, the user has to provide solutions of closed problem, i.e problem with same semantic but where variables and domains can be different. To handle this kind of data, we acquire, thanks to inductive logic programming, a more abstract model than the constraint network. When this model is learned, it is translated in the very constraint network the user aims to model. We show the limitations of learning method to build such a model due to pathological problems and explain the new algorithm we have developed to build these abstract models. In a second part, we are interesting in the possibility to the user to not provide any examples. Starting with a CSP without constraints, our method consists in solving the problem the user wants in a standard way. Thanks to a search tree, we affect to each variable a value. When our tool cannot decide if the current partial affectation is correct or not, we ask to the user, with yes/no queries, to guide the search. These queries allow to find constraints to add to the model and then to improve the quality of the search.

Depuis l'antiquité jusqu'à aujourd'hui, le domaine de la logique a gagné une importance remarquable et contribue désormais à de nombreuses autres branches, telles que la philosophie, les mathématiques, la fabrication de matériel informatique, la linguistique, l'informatique, l'intelligence artificielle, etc. À chacun de ces scénarios correspondent des besoins spécifiques, qui vont d'exigences très concrètes, telles qu'une méthode d'inférence efficace, à des propriétés théoriques plus abstraites, telles qu'un système d'axiomes élégant. Étant donnée cette grande diversité d'utilisations, une palette hétéroclite de langages formels a été développée. Pendant de nombreuses années, les langages classiques (notamment la logique du premier ordre) étaient la seule alternative concevable, mais cet assortiment d'applications a rendu d'autres types de logiques également désirables dans de nombreuses situations. Imaginez que l'heure de choisir une logique pour une tâche spécifique arrive. Comment choisir la plus appropriée? Quelles propriétés devrions-nous rechercher? Comment "mesurer'' une logique par rapport aux autres? Ce sont des questions difficiles, et il n'existe pas de recette générale à suivre. Dans cette thèse, nous allons simplement restreindre ces questions à une famille particulière de logiques, et dans ce contexte, nous explorerons les aspects théoriques qui aideront à répondre à ces préoccupations. Beaucoup peut être découvert par une analyse attentive des cas les plus intéressants, et notre contribution sera développée selon cette philosophie. Les logiques modales propositionnelles offrent une alternative aux langages traditionnels. Elles peuvent être considérées comme un ensemble d'outils permettant de concevoir des logiques adaptées à des tâches précises, possédant un contrôle fin sur leur expressivité. De plus, il s'est avéré que les logiques modales possèdent un bon comportement computationnel, qui se trouve être robuste y compris malgré l'ajout d'extensions. Ces caractéristiques, parmi d'autres, ont élevé les logiques modales au rang d'alternatives désirables aux langages classiques. Dans ce thèse, nous allons présenter une nouvelle famille de logiques modales appelée logiques mémorielles. Les logiques modales traditionnelles permettent de décrire les structures relationnelles d'un point de vue local. Mais pourquoi ne pas changer cette structure? Nous voulons étudier l'ajout d'une structure de stockage explicite aux logiques modales, une mémoire, qui permet de modéliser un comportement dynamique à travers des opérateurs mémoriels explicites. Ces opérateurs sauvent ou restaurent de l'information vers et à partir de la mémoire. Naturellement, selon le type de structure de sauvegarde désiré et les opérateurs mémoriels disponibles, la logique résultante possèdera différentes propriétés qui valent la peine d'être étudiées. Cette thèse est organisée de la façon suivante. Dans le Chapitre 1, nous commençons par rappeler brièvement comment la logique modale est née, en montrant les différents points de vue historiques la concernant. Puis, nous présentons formellement la logique modale de base et un ensemble d'opérateurs étendus qui aident à capturer le ``goût'' modal de langages plus riches. Nous finissons ce chapitre en donnant un premier aperçu des logiques mémorielles, et montrons comment elles peuvent aider à modéliser l'état quand nous choisissons d'utiliser un ensemble comme une structure de sauvegarde. Le Chapitre 2 est dédié à la présentation détaillée des logiques mémorielles. Nous montrons quelques exemples qui peuvent être décrits en ajoutant un ensemble à des structures relationnelles usuelles, ainsi que les opérateurs ensemblistes usuels permettant l'ajout d'élément et le test d'appartenance. Puis, nous montrons que d'autres opérateurs mémoriels peuvent être envisagés, et nous discutons de la possibilité d'ajouter des contraintes à l'interaction entre la mémoire et les opérateurs modaux. Ces contraintes peuvent être vues comme une manière d'avoir un contrôle fin sur l'expressivité de la logique. Comme nous avons fait des changements aux logiques modales classiques, nous nous intéressons à l'analyse de l'impact de ces changements sur les logiques résultantes. Ainsi, le reste de ce chapitre présente une boite à outils logique basique avec laquelle nous pouvons analyser cette nouvelle famille de logiques. Cette boite à outils peut être vue comme un plan qui organise le reste de cette thèse et qui permet d'analyser les logiques mémorielles en termes d'expressivité, de complexité, d'interpolation et de théorie de la preuve. Le reste des chapitres consiste à étudier en détail chacun de ces aspects. Dans les Chapitres 3 et 4, nous explorons l'expressivité de plusieurs logiques mémorielles et nous étudions la décidabilité de leur problème de satisfiabilité. Dans les cas décidables, nous déterminons leur complexité. Nous analysons l'impact des différents opérateurs mémoriels considérés, et leur interaction. Nous étudions également d'autres conteneurs mémoriels, tels que la pile. Puis, dans le Chapitre 4, nous analysons l'interpolation de Craig et la définabilité de Beth pour certains fragments des logiques mémorielles. Nous étudions également les logiques mémorielles du point de vue de la théorie de la preuve. Dans les Chapitres 6 et 7, nous passons aux axiomatisations à la Hilbert et aux systèmes de tableaux, et nous caractérisons plusieurs fragments de la famille des logiques mémorielles, en utilisant principalement des techniques empruntées aux logiques hybrides. Nous concluons dans le Chapitre 8 avec quelques remarques, des problèmes ouverts et des directions pour de futures recherches. / From ancient times to the present day, the field of logic has gained significant strength and now it actively contributes to many different areas, such as philos- ophy, mathematics, linguistic, computer science, artificial intelligence, hardware manufacture, etc. Each of these scenarios has specific needs, that range from very concrete requirements, like an efficient inference method, to more abstract theoretical properties, like a neat axiomatic system. Given this wide diversity of uses, a motley collection of formal languages has been developed. For many years, classical languages (mainly classical first order logic) were the alternative, but this assortment of applications made other types of logics also attractive in many situations. Imagine that the time for choosing a logic for some specific task arrives. How can we decide which is the one that fits best? Which properties should we look for? How can we “measure” a logic with respect to others? These are not easy questions, and there is not a general recipe one can follow. In this thesis we are just going to restrict these questions to a particular family of logics, and in that context we will investigate theoretical aspects that help to answer some of these concerns. Much can be discovered by carefully analyzing appealing cases, and our contribution will be developed having that philosophy in mind. Propositional modal logics offer an alternative to traditional languages. They can be regarded as a set of tools that allow to design logics specially tailored for specific tasks, having a fine-grained control on their expressivity. Additionally, modal logics turned out to have a good computational behavior, which proved to be quite robust under extensions. These characteristics, among others, placed modal logics as an attractive alternative to classical languages. In this dissertation we are going to present a new family of modal logics called memory logics. Traditional modal logics enables to describe relational structures from a local perspective. But what about changing the structure? We want to explore the addition of an explicit storage structure to modal logics, a mem- ory, that allows to model dynamic behavior through explicit memory operators. These operators store or retrieve information to and from the memory. Natu- rally, depending on which type of storage structure we want, and which memory operators are available, the resulting logic will enjoy different properties that are worth investigating. The thesis is organized as follows. In Chapter 1 we start by giving a brief recap of how modal logic was born, showing the different historical perspectives used to look at modal logic. Then we formally present the basic modal logic and a set of extended operators that helps grasp the modal “flavor” of some richer languages. We finish this chapter by giving a first glance of memory logics, and showing how they can help to model state when we choose to use a set as storage structure. Chapter 2 is devoted to present memory logics in detail. We show some examples that can be described by adding a set to standard relational structures, and the usual set operators to add elements and test membership. We then show some other memory operators that can be considered, and we discuss the possibility of adding constraints to the interplay between memory and modal operators. These constraints can be regarded as a way to have a finer-grained control on the logic expressivity. Since we have made changes to classical modal logics, we are interested in analyzing the impact those changes cause in the resulting logics. Therefore, the rest of this chapter presents a basic logic toolkit through which we can analyze this new family of logics. This toolkit can be seen as an outline that organizes the rest of the thesis and that allows to analyze memory logics in terms of expressivity, complexity, interpolation and proof theory. The rest of the chapters investigate each of these aspects in detail. In Chap- ters 3 and 4 we explore the expressive power of several memory logics and we study the decidability of their satisfiability problem. In the decidable cases, we determine their computational complexity. We analyze the impact of the differ- ent memory operators we consider, and how they interact. We also study other memory containers, such as a stack. Then, in Chapter 5, we analyze Craig inter- polation and Beth definability for some memory logic fragments. We also study memory logics from a proof theoretical perspective. In Chapter 6 and 7 we turn to Hilbert style axiomatizations and tableau systems, and we characterize several fragments of the memory logic family mostly using techniques borrowed from hy- brid logics. We close in Chapter 8 with some concluding remarks, open problems and directions for further research.

La divergence comportementale des utilisateurs sur le web résulte un problème de fluctuation de performance chez les systèmes de recommandation (SR) qui exploitent ce comportement pour recommander aux utilisateurs des items qu’ils vont apprécier. Ce problème est observé dans l’approche de filtrage collaboratif (FC) qui exploite les notes attribuées par les utilisateurs aux items, et l’approche à base de confiance (SRC) qui exploite les notes de confiance que les utilisateurs attribuent l’un à l’autre. Nous proposons une approche hybride qui augmente le nombre d'utilisateurs bénéficiant de la recommandation, sans perte significative de précision. Par la suite, nous identifions plusieurs caractéristiques comportementales qui permettent de constituer un profil comportemental de l’utilisateur. Ce qui nous permet de classifier les utilisateurs selon leur comportement commun, et d’observer la performance de chaque approche par classe. Par la suite, nous focalisons sur les SRC. Le concept de confiance a été abordé dans plusieurs disciplines. Il n'existe pas véritablement de consensus sur sa définition. Cependant, toutes s'accordent sur son effet positif. La logique subjective (LS) fournit une plateforme flexible pour modéliser la confiance. Nous l’utilisons pour proposer et comparer trois modèles de confiance, dont l’objectif est de prédire à un utilisateur source s’il peut faire confiance à un utilisateur cible. La recommandation peut s’appuyer sur l’expérience personnelle de la source (modèle local), un système de bouche à oreille (modèle collectif), ou encore la réputation du cible (modèle global). Nous comparons ces trois modèles aux termes de la précision, la complexité, et la robustesse face aux attaques malicieuses / Recommender systems (RS) exploit users' behaviour to recommend to them items they would appreciate. Users Behavioral divergence on the web results in a problem of performance fluctuations to (RS). This problem is observed in the approach of collaborative filtering (CF), which exploites the ratings attributed by users to items, and in the trust-based approach (TRS), which exploites the trust relations between the users. We propose a hybrid approach that increases the number of users receiving recommendation, without significant loss of accuracy. Thereafter, we identify several behavioral characteristics that define a user profile. Then we classify users according to their common behavior, and observe the performance of the approaches by class. Thereafter, we focus on the TRS. The concept of trust has been discussed in several disciplines. There is no real consensus on its definition. However, all agree on its positive effect. Subjective logic (LS) provides a flexible platform for modeling trust. We use it to propose and compare three trust models, which aims to predict whether a user source can trust a target user. Trust may be based on the personal experience of the source (local model), or on a system of mouth (collective model), or the reputation of the target (global model). We compare these three models in terms of accuracy, complexity, and robustness against malicious attacks

La logique de l’implicite est une recherche comparative entre différents systèmes métaphysiques qui visent à dégager la forme de l’argumentation philosophique propre à chacun de ces systèmes. L’étude porte sur Parménide, Platon, Aristote, Descartes, Spinoza, Leibniz, Hume, Kant, Hegel, et Nietzsche – Deleuze. L’approche consiste en un suivi au plus près des textes majeurs des philosophes cités, suivi qui contracte et résume leurs argumentations en montrant des points de rencontre et de divergence dans la manière de produire leurs positions ontologiques. Il s’agit donc de lire ces textes du point de vue de la construction du raisonnement, et par suite il s’agit de dégager les outils constructifs qui caractériseraient la manière de faire philosophique. Le contenu n’est considéré alors que du point de vue de son rapport à ces formes argumentatives.La logique de l’implicite de la part ces différentes études de cas se propose donc comme un projet de philosophie abstraite c’est à dire une approche qui vise à dégager les éléments et relations de l’argumentation ontologique. L’attention est portée sur des styles généraux – comme l’approche par choc ou par distinction –, sur certain éléments récurrents dans tous les systèmes – comme la plus petite différence, le point double, la qualification extensive ou compréhensive –, et enfin sur les relations – l’explication, l’implication, et la complication. Il est avancé que l’implicite occupe une place centrale dans l’argumentation métaphysique dans la mesure où c’est depuis cette place que peut se poser toute explication ou connaissance. / Logic of the implicit is a research that compares different metaphysical systems and aims at extracting the form of philosophical argumentation proper to each of these systems. The study is carried on Parmenides, Plato, Aristotle, Descartes, Spinoza, Leibniz, Hume, Kant, Hegel, and Nietzsche – Deleuze. The approach consists in following as close as possible the fundamental texts of the above cited authors, an approach aimed at summarizing their argumentations and showing points of encounter or divergence in their way of producing their ontological positions. What is at stake then is to read these texts from the point of view of the construction of their arguments, and then to extract the constructive tools that characterize the philosophical way of doing things. The content is only considered from the point of view of its relation to these argumentative forms. Logic of the implicit, through these different case studies, proposes itself as a project of abstract philosophy, because it aims at extracting the elements and relations that are proper to the ontological argumentation. The attention is focused on showing the existence of general styles – such as the approach by choc or by distinction –, on certain elements recurrent in all the systems – such as the smallest difference, the double point, the extensive or comprehensive qualifications –, and at last on the relations – explication, implication, and complication. It is argued that the implicit occupies a central place in the metaphysical argumentation to the extent that it is from that place that any explanation is possible and thus any knowledge.

La réduction continuelle des dimensions dans les technologies CMOS a ouvert la porte à la conception de circuits complexes multi-cœurs (SoC). Malheureusement dans les technologies nanométriques, les performances des systèmes intégrés après fabrication ne sont pas complètement prédictibles. En effet, les variations des procédés de fabrication sont très importantes aux échelles des puces. Par conséquent, la conception de tels systèmes dans les technologies nanométriques est désormais contrainte par de nombreux paramètres tels que la robustesse aux variations des procédés de fabrication et la consommation d'énergie. Ceci implique de disposer d'algorithmes efficaces, intégrés dans la puce, susceptibles d'adapter le comportement du système aux variations des charges des processeurs tout en faisant face simultanément aux variations des paramètres qui ne peuvent pas être prédits ou modélisées avec précision au moment de la conception. Dans ce contexte, ce travail de thèse porte sur la conception de systèmes dit « GALS » (Globally Asynchronous Locally Synchronous) conçus autour d’un réseau de communication intégré à la puce (Network-on-Chip ou NoC) exploitant les nouvelles générations de technologie CMOS. Une nouvelle méthode permettant de contrôler dynamiquement la vitesse des différents îlots du NoC grâce à un contrôle de la tension et de la fréquence en fonction de la qualité locale des procédés de fabrication sur chaque îlot est proposée. Cette technique de contrôle permet d’améliorer les performances du système en consommation, et d’augmenter son rendement en fabrication grâce à l’utilisation des synergies au sein du système intégré. La méthode de contrôle est basée sur l’utilisation d'un anneau asynchrone programmable capable de prendre en compte la charge de travail dynamique et les effets de la variabilité des procédés de fabrication. Le contrôleur évalue en particulier la limite supérieure de fréquence de fonctionnement pour chaque domaine d'horloge. Ainsi, il n'est plus nécessaire de garantir les performances temporelles de chaque nœud au moment de la conception. Cela relâche considérablement les contraintes de fabrication et permet du même coup l'amélioration du rendement. / Continuous scaling of CMOS technology push circuit designs towards multi-core complex SoCs. Moreover, with the nanometric technologies, the integrated system performances after fabrication will not be fully predictable. Indeed, the process variations really become huge at the chip scale. Therefore the design of such complex SoCs in the nanoscale technologies is now constrained by many parameters such as the energy consumption and the robustness to process variability. This implies the need of efficient algorithms and built-in circuitry able to adapt the system behavior to the workload variations and, at the same time, to cope with the parameter variations which cannot be predicted or accurately modeled at design time. In this context, this thesis work addresses the design of GALS-based NoC architectures in the upcoming CMOS technologies. A novel methodology to dynamically control the speed of different voltage-frequency NoC islands according to the process variability impact on each domain is proposed. This control technique can improve the performances, the energy consumption, and the yield of future SoC architectures in a synergistic manner. The control methodology is based on the design of an asynchronous programmable self-timed ring where the controller takes into account the dynamic workload and the process variability effects. The controller especially considers the operating frequency limit which does not exceed the maximum locally allowed value for a given clock domain. With such an approach, it is no more required to separately guaranty the performance for each node. This drastically relaxes the fabrication constraints and helps the yield enhancement.

Malgré leur fort développement en assainissement domestique urbain, les bioréacteurs à membranes (BaM) pâtissent de phénomènes de colmatage, induisant des coûts énergétiques et de maintenance importants. L’aération séquencée des membranes par des grosses bulles est l’une des stratégies pour limiter le colmatage ; son impact a fait l’objet de plusieurs études mais reste globalement mal compris, notamment du fait de la complexité de ces systèmes, multiphasiques et opaques. L’hydrodynamique des réacteurs reste mal caractérisée en présence de boues. Pour apporter des éléments de compréhension aux mécanismes de limitation du colmatage par injection d’air, un pilote de filtration membranaire semi-industriel (2 m3, 3 sous modules fibres creuses Puron®) a été conçu, dimensionné et installé sur l’unité de traitement des jus (TDJ) de la station d’épuration Seine Aval (SIAAP), afin d’être alimenté en boues biologiques dans des conditions réelles de fonctionnement. Le suivi des paramètres opératoires du pilote et de ses performances de filtration sur une période de 5 mois avait un double objectif : (i) mieux caractériser la dispersion du gaz pour différentes conditions de fonctionnement (paramètres de l’aération, concentration en boues de l’alimentation), (ii) hiérarchiser les facteurs qui limitent le colmatage des membranes. Il s’agit in fine de proposer des stratégies d’aération adaptées et efficaces pour limiter le colmatage. Afin de caractériser la dispersion du gaz dans le réacteur, une méthodologie innovante basée sur la tomographie de résistivité électrique (ERT) a été adaptée au pilote. Les conditions d’utilisation de l’ERT (nombre d’électrodes de mesure, séquence de quadripôles) ont été sélectionnées à travers une étude numérique, de même que les paramètres d’inversion nécessaires pour reconstituer la cartographie des résistivités à partir des mesures expérimentales. Cette étude numérique poussée, réalisée sous COMSOL, a permis de conclure à l’intérêt de la méthode pour représenter la distribution des phases dans la géométrie considérée. L’ERT a donc été appliquée au pilote alimenté en boues, pour différentes conditions d’aération. Le jeu de données de filtration a par ailleurs été analysé par logique floue, à l’aide du logiciel FisPro. Les arbres de décision obtenus, en analysant les résultats de manière globale et en les regroupant par conditions opératoires similaires, ont mis en évidence l’impact prépondérant des variables suivantes sur la dérive de perméabilité observée (comprise entre - 9 et 2 LMH/bar) : la différence de DCO entre le surnageant des boues et le perméat (DDCO) traduisant une phase colloïdale complexe, et la concentration en matières en suspension (MES), ayant toutes deux un impact négatif sur les performances de filtration. Une augmentation du débit d’air conduirait à une limitation de la dérive de perméabilité, sauf lorsque la variable DCO est élevée (> à 500 mg/L), cette hypothèse restant cependant à vérifier sur une base de données plus conséquente. Le modèle ainsi obtenu par logique floue permet de mieux simuler les évolutions de perméabilité que les modèles obtenus par régression linéaire multivariée (erreurs de 0,61 et de 0,70 respectivement), et ce malgré une incertitude relative importante sur la mesure de perméabilité (jusqu’à 16 %). Ces résultats sont cohérents avec la dispersion du gaz observée par ERT : son homogénéité dépend de la concentration en MES et du débit d’air injecté. A forte concentration en MES (6 – 10 g/L), des zones préférentielles de passage des bulles ont été observées, en particulier à faible débit d’air, expliquant ainsi un colmatage plus important. L’utilisation nouvelle dans ce contexte de ces techniques, ERT et logique floue, donne des résultats qui confortent l’intérêt d’adapter l’aération (débit, séquençage) aux caractéristiques des boues notamment leurs concentrations, et qui permettent d’envisager des stratégies de contrôle de ces paramètres

La première partie de mon thèse s'intéresse aux problèmatiques de la technologie du semi-conducteur traditionnelle. Ensuite dans la deuxième partie je vais m'intérésser aux propriétés des nanocomposants. Ils se distinguent du CMOS classique selon plusieurs critères. Ayant une connaissance globale des architectures, j'ai choisi de développer plus amplement les réseaux de neurones en seconde partie. En effet, des fonctions logiques peuvent être émulées par les réseaux de neurones réalisés à partir des nanotubes de carbones et des mémoires multiniveaux. Pour la dernière partie, la robustesse d'une architecture de réseaux de neurones est évaluée par simulation qui montre la possibilité de construire un circuit robuste grâce à l'apprentissage.

Cette thèse traite des langages reconnaissables de mots indexés par des ordinaux. Plusieurs classes d'automates qui reconnaissent de tels mots ont été introduites par Büchi. Elles diffèrent par la longueur des mots reconnus par les automates. Nous en utilisons quatre: la classe pour les mots de longueur , celle pour les mots de longueur inférieure à , où n est un entier naturel, celle pour les mots de longueur dénombrable, et celle pour les mots de longueur quelconque. Nous y ajoutons la classe des automates de Kleene traditionnelle, sur les mots finis. Nous remontrons que ces différentes définitions d'automates sont équivalentes, c'est-à-dire que données deux de ces classes et un automate d'une des deux, la restriction du langage reconnu par l'automate aux mots du domaine le plus petit des deux classes est la restriction du langage reconnu par un automate de l'autre classe au même domaine. Nous donnons également une présentation unifiée de la déterminisation pour chacune des classes qui reconnaît au plus des mots de longueur dénombrable. Les semigroupes finis sont un formalisme équivalent aux automates pour définir des ensembles de mots finis. Perrin, Pin et Wilke ont introduits des structures algébriques adaptées à l'étude des langages de mots de longueur , qui, quand elles sont finies, sont équivalentes aux automates. Nous généralisons l'approche algébrique de la théorie des langages reconnaissables de mots de longueur aux mots de longueur inférieure à , puis aux mots de longueur dénombrable. Pour cela, nous définissons deux structures algébriques, les -semigroupes et les -semigroupes, qui, quand elles sont finies, sont équivalentes respectivement aux automates pour les mots de longueur inférieure à et aux automates pour les mots de longueur dénombrable. Comme pour le cas des mots de longueur , une algèbre syntaxique peut être canoniquement associée à chaque langage reconnaissable. Nous définissons le produit de Schützenberger et le produit en couronne sur les -semigroupes. Nous étendons également le théorème des variétés d'Eilenberg aux mots de longueur dénombrable. Finalement, nous remontrons l'équivalence entre langages reconnus par automates et langages définis par énoncés de logique monadique du second ordre quand on s'intéresse aux mots de longueur dénombrable. Le théorème d'équivalence de Schützenberger entre langages sans étoile et semigroupes finis apériodiques est étendu aux mots de longueur inférieure à , et le théorème d'équivalence entre langages sans étoile et langages définis par énoncés de logique du premier ordre de l'ordre linéaire de McNaughton et Papert est étendu aux mots de longueur quelconque.

Ce travail est devoué à la Réalisabilité de Krivine, se focalisant sur les aspects calculatoires des réalisateurs des formules. Chaque formule a un jeu associé. Chaque preuve fournit un therme capable d'implémenter une stratégie gagnante pour le jeux associé à la formule qu'elle démontre. Une preuve est, par adéquation, un combinateur capable de prendre des stratégies gagnantes pour les hypothèses et les combiner pour rendre une stratégie gagnante pour la conclusion. Y-sont abordés: A. Le problème de l'espécification, consistant a décrire en termes calculatoires les réalisateurs d'une formule donée. Des nombreaux examples y-sont traités. B. On étudie une preuve en tant que combinateur de stratégies gagnantes: On pose une implication $A\to B$ où $A$ et $B$ sont des formules $\Sigma^0_2$. Soit $C$ la forma normale prenexe de $A\to B$. On étudie une preuve de $A, C\to B$ en tant que combinateur de stratégies gagnantes. En faisant ce travail, certaines techniques sont développées pour tracer l'éxécution d'un processus, dont notamment la "méthode des fils".