Les problèmes traités et les résultats obtenus dans ce travail s'inscrivent essentiellement dans le domaine de la théorie des automates, la logique mathématique et leurs applications. Dans un premier temps on utilise les automates finis pour démontrer l'automaticité de plusieurs structures logiques sur des mots finis écrits dans un alphabet infini dénombrable. Ceci nous permet de déduire la décidabilité des théories logiques associées à ces structures. On a considéré par exemple la structure $X=(Sigma^*;prec,clone)$ où $Sigma^*$ désigne l'ensemble des mots finis sur l'alphabet infini dénombrable $Sigma$, $prec$ désigne la relation de préfixe et $clone$ désigne le prédicat qui est vrai pour un mot se terminant par deux lettres identiques. On a démontré l'automaticité de la structure $X$ et la décidabilité de sa théorie du premier ordre et de sa théorie monadique du second ordre. On a aussi considéré des extensions de la structure $X$ obtenues en ajoutant des prédicats comme $sim$ qui est vrai pour deux mots de même longueur. Nous avons en particulier démontré la $M$-automaticité de la structure $(Sigma^*;prec,clone,sim)$, d'où la décidabilité de sa théorie du premier ordre. On a par ailleurs étudié des structures qui comportent le prédicat $diff$ qui est vrai pour un mot dont les lettres sont toutes distinctes. En particulier on a démontré l'automaticité de la structure $D=(Sigma^*;prec,clone,diff)$ et la décidabilité de sa théorie du premier ordre et de sa théorie monadique du second ordre. On a également obtenu, par interprétation logique, des résultats de décidabilité et des résultats d'indécidabilité pour plusieurs variantes des structures $X$ et $D$, ainsi que pour des familles de structures appelées emph{structure d'applications exclusives} et emph{structure de décomposition}.Dans un deuxième temps on s'est intéressé au problème de la réduction du nombre de transitions dans les automates finis. On a commencé par étendre le concept de emph{Common Follow Sets} d'une expression régulière aux automates finis homogènes. On a montré comment établir une liaison assez directe entre des systèmes de CFS spécifiques et les arbres binaires complets. Ce lien est prouvé en utilisant un objet combinatoire appelé emph{triangle d'Ératosthène - Pascal}. Cette correspondance permet de transformer la valeur qui nous intéresse (le nombre de transitions) en une valeur assez naturelle associée aux arbres (le poids d'un arbre). En effet, construire un automate ayant un minimum de transitions revient à trouver un arbre de poids minimal. On a montré, d'une part, que ce nombre de transitions est asymptotiquement équivalent à $n(log_2 n)^2$ (la borne inférieure). D'autre part, les tests expérimentaux montrent que pour les petites valeurs de $n$, les automates minimaux en nombre de transitions coïncident (en nombre et en taille) avec ceux obtenus par notre construction. Cela nous mène à suggérer que notre réduction est finalement une minimisation pour les automates triangulaires. Dans un dernier temps on a présenté une étude expérimentale concernant l'application des automates à trous dans le domaine de la recherche approchée de motif dans les dictionnaires de mots. Contrairement aux complexités théoriques, temps de recherche et espace de stockage exponentiels, nos expérimentations montrent la linéarité de l'automate à trous / This work deals mainly with automata theory, mathematical logic and their applications. In the first part, we use finite automata to prove the automaticity of several logical structures over finite words written in a countable infinite alphabet. These structures involve predicates like $pred$, $clone$ and $diff$, where $x pred y$ holds if $x$ is a strict prefix of $y$, $clone(x)$ holds when the two last letters of $x$ are equal, and $diff(x)$ holds when all letters of $x$ are pairwise distinct. The automaticity results allow to deduce the decidability of logical theories associated with these structures. Other related decidability/undecidability results are obtained by logical interpretation. In the second part, we generalize the concept of Common Follow Sets of a regular expression to homogeneous finite automata. Based on this concept and a particular class of binary trees, we devise an efficient algorithm to reduce/minimize the number of transitions of triangular automata. On the one hand, we prove that the produced reduced automaton is asymptotically minimal, in the sense that for an automaton with $n$ states, the number of transitions in the reduced automaton is equivalent to $n(log_2 n)^2$ , which corresponds at the same time to the upper and the lower known bounds. On the other hand, experiments reveal that for small values of $n$, all minimal automata are exactly those obtained by our reduction, which lead us to conjecture that our construction is not only a reduction but a minimization. In the last part, we present an experimental study on the use of special automata on partial words for the approximate pattern matching problem in dictionaries. Despite exponential theoretical time and space upper bounds, our experiments show that, in many practical cases, these automata have a linear size and allow a linear search time

Le but de cette thèse est l'optimisation de la production de l'électricité renouvelable pour site isolé de faible puissance. Un système, utilisant deux sources renouvelables : photovoltaïque et éolienne, est étudié afin d'améliorer le rendement énergétique de l'énergie produite. Pour la chaîne de conversion photovoltaïque, un contrôleur pour suivre le point de puissance maximale est conçu en utilisant l'approche de recherche directe (méthode Perturbe & Observe) combinée avec la logique floue, tout en prenant en compte le sens de variation des perturbations. Avec cette combinaison, on peut éviter des défauts de la méthode Perturbe & Observe, s'affranchir des informations sur les caractéristiques du panneau photovoltaïque et des conditions climatiques. Egalement, pour la chaîne de conversion éolienne de petite puissance fonctionnant à vitesse variable couplée à un générateur synchrone à aimant permanent, un contrôleur pour suivre le point de puissance maximale est proposé qui est basé sur le même principe par rapport à la chaîne de conversion photovoltaïque. Cette approche proposée a l'avantage de l'utilisation d'un capteur de tension au lieu d'un capteur de vitesse, ceci présente un intérêt certain notamment pour sites isolés par rapport aux autres solutions. Enfin, pour la réalisation d'un système de production d'électricité hybride, un superviseur est conçu pour obtenir un comportement optimal du système en fonction des variations de la charge et de la production en prenant en compte du système de stockage et de délestage. Pour chaque point abordé, des études en simulation sont fournies pour montrer l'efficacité des approches proposées. / The objective of this thesis is to optimize the production of renewable electricity for small isolated network. A system using two renewable sources: solar and wind power, is studied in order to improve the efficiency of energy extracted. For the photovoltaic conversion system, a maximum power point tracking controller is designed using direct searching approach (method Perturbe & Observe) combined with fuzzy logic, taking into account the direction of perturbation. This combination can avoid the disadvantages of the method Perturbe & Observe, and not requires any information about the generator's characteristics or climate conditions. Similarly, for the variable speed wind turbine using permanent magnet synchronous generator, a controller to track the maximum power point, based on the same principle with photovoltaic conversion system, is proposed. This approach has the advantage of using a voltage sensor instead of a speed sensor, this presents a particular interest for stand-alone system comparing to other solutions. Finally, for the realization of hybrid generation system, a fuzzy supervisor is adapted to obtain an optimal behavior of the system according to the variations of load demand and extracted power, taking into account the storage and dissipation system. For each issue, simulation studies are provided to show the effectiveness of the proposed approaches.

La théorie de la preuve se développe depuis la correspondance de Curry-Howard suivant deux sources d’inspirations : les langages de programmation, pour lesquels elle agit comme une théorie des types de données, et l’étude sémantique des preuves. Cette dernière consiste à donner des modèles mathématiques pour les comportements des preuves/programmes. En particulier, la sémantique dénotationnelle s’attache à interpréter les deux-ci comme des fonctions entre des types, et permet en retour d’affiner notre compréhension des preuves/programmes. La logique linéaire (LL), introduite par Girard, donne une interprétation logique des notions d’algèbre linéaire, quand la logique linéaire différentielle (DiLL), introduite par Ehrhard et Regnier, permet une compréhension logique de la notion de différentielle.Cette thèse s’attache à renforcer la correspondance sémantique entre théorie de la preuve et analyse fonctionnelle, en insistant sur le caractère involutif de la négation dans DiLL.La première partie consiste en un rappel des notions de linéarité, polarisation et différentiation en théorie de la preuve, ainsi qu’un exposé rapide de théorie des espaces vectoriels topologiques. La deuxième partie donne deux modèles duaux de la logique linéaire différentielle, interprétant la négation d’une formule respectivement par le dual faible et le dual de Mackey. Quand la topologie faible ne permet qu’une interprétation discrète des preuves sous forme de série formelle, la topologie de Mackey nous permet de donner un modèle polarisé et lisse de DiLL, et de raffiner des résultats précédemment obtenus par Blute, Dabrowski, Ehrhard et Tasson. Enfin, la troisième partie de cette thèse s’attache à interpréter les preuves de DiLL par des distributions à support compact. Nous donnons un modèle polarisé de DiLL où les formules négatives sont interprétés par des espaces Fréchet Nucléaires. Nous montrons que enfin la résolution des équations aux dérivées partielles linéaires à coefficients constants obéit à une syntaxe qui généralise celle de DiLL, que nous détaillons. / Around the curry-coward correspondence, proof-theory has grown along two distinct fields : the theory of programming languages, for which formulas acts as data types, and the semantic study of proofs. The latter consists in giving mathematical models of proofs and programs. In particular, denotational semantics distinguishes data types which serves as input or output of programs, and allows in return for a finer understanding of proofs and programs. Linear Logic (LL) gives a logical interpretation of the basic notions from/of linear algebra, while Differential Linear Logic allows for a logical understanding of differentiation. This manuscript strengthens the link between proof-theory and functional analysis, and highlights the role of linear involutive negation in DiLL. The first part of this thesis consists in a quick overview of prerequisites on the notions of linearity, polarisation and differentiation in proof-theory, and gives the necessary background in the theory of locally convex topological vector spaces. The second part uses two classic topologies on the dual of a topological vector space and gives two models of DiLL: the weak topology allows only for a discrete interpretation of proofs through formal power series, while the Mackey topology on the dual allows for a smooth and polarised model of DiLL. Finally, the third part interprets proofs of DiLL by distributions. We detail a polarized model of DiLL in which negatives are Fréchet Nuclear spaces, and proofs are distributions with compact support. We also show that solving linear partial differential equations with constant coefficients can be typed by a syntax similar to the one of DiLL, which we detail.

Avec les réductions d'échelle, les circuits électroniques deviennent de plus en plus petits, plus performants, consommant moins de puissance, mais aussi moins fiables. En effet, la fiabilité s'est récemment érigée en défi majeur dans l'industrie micro-électronique, devenant un critère de conception important, au même titre que la surface, la consommation de puissance et la vitesse. Par exemple, les défauts physiques dus aux imperfections dans le procédé de fabrication ont été observés plus fréquemment, affectant ainsi le rendement des circuits. Par ailleurs, les circuits nano-métriques deviennent pendant leur durée de vie plus vulnérables aux rayonnements ionisants, ce qui cause des fautes transitoires. Les défauts de fabrication, aussi bien que les fautes transitoires, diminuent la fiabilité des circuits intégrés. En avançant dans les nœuds technologiques, les circuits logiques programmables de type FPGA sont les premiers à entrer sur le marché, grâce à leur faible coût de développement et leur flexibilité qui leur permet d'être utilisés pour n'importe quelle application. Les FPGA possèdent des caractéristiques attrayantes, notamment pour les applications spatiales et aéronautiques, où la reconfigurabilité, les hautes performances et la faible consommation de puissance peuvent être exploitées pour développer des systèmes innovants. Néanmoins, les missions ont lieu dans un environnement rude, riche en radiations pouvant produire des erreurs soft dans les circuits électroniques. Ceci montre l'importance de la fiabilité des FPGA en tant que critère de conception dans les applications critiques. La plupart des FPGA commerciaux ont une architecture matricielle et leurs blocs logiques sont regroupés en clusters. Ainsi, cette thèse s'intéresse à la tolérance aux fautes des blocs de base ( blocs logiques élémentaires (BLE) et boîtes d'interconnexion ) dans un FPGA de type « matrice de clusters ». Dans le but d'améliorer la fiabilité de ces blocs, il est impératif de pouvoir d'abord l'évaluer, pour ensuite sélectionner la bonne technique de durcissement selon le budget mis à disposition. C'est bien le plan principal de cette thèse. Elle a essentiellement deux objectifs : (a) analyser la tolérance aux fautes des blocs de base dans un FPGA de type « matrice de clusters », et identifier les composants les plus vulnérables. (b) proposer des méthodes de durcissement à différents niveaux de granularité, en fonction du budget de durcissement. En ce qui concerne le premier objectif, une méthodologie pour évaluer la fiabilité du cluster a été proposée. Cette méthodologie emploie une méthode analytique déjà existante pour évaluer la fiabilité des circuits logiques combinatoires. La même méthode est utilisée pour identifier les blocs les plus éligibles au durcissement. Quant au deuxième objectif, des techniques de durcissement ont été proposées aux niveaux multiplexeur et transistor. Au niveau multiplexeur, deux solutions de durcissement ont été présentées. La première solution a recours à la redondance spatiale et concerne la structure du bloc logique. Une nouvelle architecture de BLE baptisée « Butterfly » est introduite. Elle a été comparée avec d'autres architectures de BLE en termes de fiabilité et de surcoût. La deuxième solution de durcissement est une technique dite « sans redondance ». Elle est basée sur une synthèse intelligente qui consiste à chercher la structure la plus fiable parmi toutes celles proposées dans la librairie du fondeur, avant d'utiliser directement de la redondance. Ensuite, au niveau transistor, de nouvelles architectures de multiplexeur, à sortie unique ou différentielles, ont été proposées. Elles ont été comparées à d'autres assemblages différents de transistors, selon des métriques de conception appropriées. / As feature sizes scale down to nano-design level, electronic devices have become smaller, more performant, less power-onsuming, but also less reliable. Indeed, reliability has arisen as a serious challenge in nowadays’ microelectronics industry and as an important design criterion, along with area, performance and power consumption. For instance, physical defects due to imperfections in the manufacturing process have been observed more frequently, impacting the yield. Besides, nanometric circuits have become more vulnerable during their lifetime to ionizing radiation which causes transient faults. Both manufacturing defects and transient faults contribute to decreasing reliability of integrated circuits. When moving to a new technology node, Field Programmable Gate Arrays (FPGAs) are the first coming into the market, thanks to their low development and Non-Recurring Engineering (NRE) costs and their flexibility to be used for any application. FPGAs have especially attractive characteristics for space and avionic applications, where reconfigurability, high performance and low-power consumption can be fruitfully used to develop innovative systems. However, missions take place in a harsh environment, rich in radiation, which can induce soft errors within electronic devices. This shows the importance of FPGA reliability as a design criterion in safety and critical applications. Most of commercial FPGAs have a mesh architecture and their logic blocks are gathered into clusters. Therefore, this thesis deals with the fault tolerance of basic blocks (clusters and switch boxes) in a mesh of clusters FPGA. These blocks are mainly made up of multiplexers. In order to improve their reliability, it is imperative to be able to assess it first, then select the proper hardening approach according to the available budget. So, this is the main outline in which this thesis is conceived. Its goals are twofold: (a) analyze the fault tolerance of the basic blocks in a mesh of clusters FPGA, and point out the most vulnerable components (b) propose hardening schemes at different granularity levels, depending on the hardening budget. As far as the first goal is concerned, a methodology to evaluate the reliability of the cluster is proposed. This methodology uses an existent analytical method for reliability computation of combinational circuits. The same method is employed to identify the worthiest components to be hardened. Regarding the second goal, hardening techniques are proposed at both multiplexer and transistor levels. At multiplexer level, two hardening solutions are presented. The first solution resorts to spacial redundancy and concerns the logic block structure. A novel Configurable Logic Block (CLB) architecture baptized Butterfly is introduced. It is compared with other hardened CLB architectures in terms of reliability and cost penalties. The second hardening solution is a redundanceless scheme. It is based on a “smart” synthesis that consists in seeking the most reliable design in a given founder library, instead of directly using a redundant solution. Then, at transistor level, new single-ended and dual-rail multiplexer architectures are proposed. They are compared to different other transistor structures, according to suitable design metrics.

Cette thèse a pour objectif le développement d’un système multi-capteurs de gaz permettant une évaluation en continu et en temps réel des différentes types de pollution atmosphérique en zone urbain, en classifiant notamment les pollutions de type urbaine, photochimique, ou encore liée au trafic. Le projet se base sur l’utilisation de différents capteurs de gaz de type semi-conducteur disponibles dans le commerce qui sont intégrés dans un dispositif autonome et portable, afin qu’il puisse fonctionner sur site.Dans un premier temps, et en grande partie à Saint-Etienne, différents types de capteurs sont sélectionnés puis leurs performances sont testées sur un banc simulant les atmosphères polluées et développé pour l’occasion. Afin de pallier aux problèmes de non répétabilité et de dérive de la ligne de base et de la sensibilité, des procédures de prétraitement de standardisation sont mises au point.Dans un deuxième temps, et en grande partie à Douai, différents sites de tests sont identifiés et leurs historiques de pollution sont étudiés. Plusieurs campagnes en stations de mesure d’une semaine, recouvrant les différentes saisons et les différents types de sites, sont alors menées. Il y est collecté conjointement les signaux des capteurs et des analyseurs de gaz réglementés. Des méthodes basées sur les réseaux de neurones sont alors appliquées afin d’obtenir conjointement, à partir des signaux des capteurs, une classification parmi 3 types de pollutions (urbaine, trafic et photochimique) ainsi qu’un indicateur global de qualité de l’air. Ces méthodes utilisent une approche basée sur la logique floue afin d’éviter les problèmes d’effet de bord. / No english abstract

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal. / L'inférence d'un modèle tridimensionnel (3-D) d'une molécule d'ARN à partir d'informations biochimiques de faible résolution est une tâche complexe. Le développement de méthodes efficaces et objectives de modélisation est essentiel à la compréhension des mécanismes moléculaires impliquant des ARN. Le présent travail propose trois ajouts importants de ce domaine. Dans un premier temps, une définition de l'espace des conformations d'un ARN est établie et la technique de retour-arrière est décrite de façon à permettre une exploration complète de cet espace. Ensuite, un formalisme basé sur la logique floue est présenté. Cette approche permet d'utiliser l'information provenant de séquences multiples et est appliquée pour la modélisation du ribozyme activé par le plomb. Finalement, la flexibilité d'un système de modélisation 3-D utilisant une approche de satisfaction de contrainte est mise en évidence par l'ajout d'un nouveau type de contrainte dans l'engin de recherche, permettant la modélisation efficace de multimères cycliques. Ces ajouts permettent d'élargir le spectre des informations utiles à la modélisation 3-D des ARN et facilite l'intégration de nouveaux types d'informations à l'intérieur d'une méthode systématique. Les résultats obtenus sur des projets de modélisation spécifiques (ribozyme activé par le plomb et pRNA de çi>29) permettent de confirmer la pertinence de cette approche.

Cette thèse développe un modèle sémiotique de l’abduction pour représenter un processus de conception architecturale. Elle formalise ce processus par une dualisation hypostatique du rapport sémiotique entre un problème de conception, saisi en tant que signe, et la possibilité de sa matérialisation géométrique. La dualisation réintègre ce signe dans le domaine des systèmes de savoir-concevoir utilisés en conception architecturale, et par conséquent, elle génère de nouvelles solutions architecturales. L’abduction modifie les connaissances préalables engagées dans la production d’une solution (l’hypothèse) et en introduit de nouvelles. La complexité du processus de conception implique, au niveau méthodologique et à partir d’une position épistémologique constructiviste, l’intégration de la subjectivité du concepteur dans le modèle. Ainsi résulte une incertitude des interactions entre problème de conception, production de solution, concepteur et contexte. La sémiotisation de l’abduction architecturale explicite le rôle central de l’interprétation dans la création d’une solution. D’ailleurs, la dualisation s’appuie sur la théorie des possibilités pour opérationnaliser le calcul interprétatif incertain et pour valider les hypothèses générées. En retour, la gestion de la propagation de cette incertitude, dans le modèle sémiotique, facilite l’identification et la formulation des solutions, et rend possible une émergence observationnelle de la nouveauté. Le modèle développé est appliqué à un cas de transformations architecturales géométriques dans un milieu urbain fortement caractérisé. / This thesis develops a semiotic model of abduction to represent a process of architectural design. It formalizes this process by the means of a hypostatic dualization, applied to the semiotic relationship between, on the one hand, a design problem, considered as a sign, and on the other, the possibility of its geometric materialization. The dualization reintegrate this sign in the domain of know-how systems used in architectural design, and consequently, it generates new architectural solutions. Abduction modifies and augments the prior knowledge involved in producing the solution (the hypothesis). From a constructivist stance and the ensuing methodological viewpoint, the complexity of the design process implies embedding the designer’s subjectivity in the model. Thus arises an uncertainty about the interactions among design problem, solution production, designer and context. Semiotizing architectural abduction reveals the central role played by interpretation in creating a solution. Besides, dualization relies on possibility theory to formalize the resulting, and uncertain, interpretation calculus, and to validate the obtained hypotheses. In return, managing the uncertainty propagation within the semiotic model, facilitates the identification and the formulation of architectural solutions and allows for an observational emergence of novelty. The developed model is applied to a case of architectural geometric transformations in a heavily characterized neighborhood.

Québec Université Laval, Bibliothèque 2018

No description available.