Search

The purpose of this thesis is to develop a domain decomposition method suitable to solve the Stokes system discretized with stable mixte finite elements where pressure is continuous such as Hood-Taylor and Mini. The new method arises from the combinaison of FETI applied to the velocity and BDD applied to the pressure without decoupling the unknowns. It inherits and decouples the coarse projectors included in FETI and BDD. The methodology leads to a symmetric, positive semi-definite linear system that we solve by projected preconditioned conjugate gradient. The method contains two sparse coarse preconditionners and exact local preconditionners that ensure its scalability, its robustness and its efficiency. We use local projectors constructed from the constant pressure modes of the subdomains that enable an extension to mixte finite elements with discontinuous pressure and that make the coarse problem of BDD optional even in the presence of pressure on the interfaces. We have easily applied the method to incompressible and almost incompressible elasticity and it can be extended the same way to other saddle-point systems arising from minimization problems under constraints due to its algebraic property., L’objectif de cette thèse est de développer une méthode de décomposition de domaine pour la résolution du système de Stokes discrétisé avec les éléments finis mixtes stables où la pression est continue comme Hood-Taylor et Mini. La nouvelle méthode résulte de la combinaison de FETI qui est appliquée à la vitesse et de BDD qui est appliquée à la pression sans découpler les inconnues. Elle hérite et découple les projecteurs grossiers associés à FETI et à BDD. La méthodologie débouche sur un système linéaire symétrique, semi-défini positif que nous avons résolu par la méthode du gradient conjugué projeté préconditionné. La méthode contient deux préconditionneurs grossiers creux et des pré-conditionneurs locaux exacts qui assurent son extensibilié, sa robustesse et son efficacité. L’introduction de projecteurs locaux construits à partir des modes de pression des sous-domaines étend la méthode aux éléments finis mixtes discontinues en pression et rend le problème grossier de BDD facultatif même en présence de la pression aux interfaces. Nous avons aisément appliqué la méthode à l’élasticité incompressible et quasi-incompressible et elle peut s’étendre de la même façon au cadre plus général des systèmes de point-selle issus des problèmes de minimisation sous contraintes grâce à sa nature algébrique.

Controlling autonomous systems requires to make decisions depending on current observations and objectives. This involves some tasks that must be executed online--with the embedded computational power only. However, these tasks are generally combinatory; their computation is long and requires a lot of memory space. Entirely executing them online thus compromises the system's reactivity. But entirely executing them offline, by anticipating every possible situation, can lead to a result too large to be embedded. A tradeoff can be provided by knowledge compilation techniques, which shift as much as possible of the computational effort before the system's launching. These techniques consists in a translation of a problem into some language, obtaining a compiled form of the problem, which is both easy to solve and as compact as possible. The translation step can be very long, but it is only executed once, and offline. There are numerous target compilation languages, among which the language of binary decision diagrams (BDDs), which have been successfully used in various domains of artificial intelligence, such as model-checking, configuration, or planning. The objective of the thesis was to study how knowledge compilation could be applied to the control of autonomous systems. We focused on realistic planning problems, which often involve variables with continuous domains or large enumerated domains (such as time or memory space). We oriented our work towards the search for target compilation languages expressive enough to represent such problems. In a first part of the thesis, we present various aspects of knowledge compilation, as well as a state of the art of the application of compilation to planning. In a second part, we extend the BDD framework to real and enumerated variables, defining the interval automata (IAs) target language. We draw the compilation map of IAs and of some restrictions of IAs, that is, their succinctness properties and their efficiency with respect to elementary operations. We describe methods for compiling into IAs problems that are represented as continuous constraint networks. In a third part, we define the target language of set-labeled diagrams (SDs), another generalization of BDDs allowing the representation of discretized IAs. We draw the compilation map of SDs and of some restrictions of SDs, and describe a method for compiling into SDs problems expressed as discrete continuous networks. We experimentally show that using IAs and SDs for controlling autonomous systems is promising.; La conduite de systèmes autonomes nécessite de prendre des décisions en fonction des observations et des objectifs courants : cela implique des tâches à effectuer en ligne, avec les moyens de calcul embarqués. Cependant, il s'agit généralement de tâches combinatoires, gourmandes en temps de calcul et en espace mémoire. Réaliser ces tâches intégralement en ligne dégrade la réactivité du système ; les réaliser intégralement hors ligne, en anticipant toutes les situations possibles, nuit à son embarquabilité. Les techniques de compilation de connaissances sont susceptibles d'apporter un compromis, en déportant au maximum l'effort de calcul avant la mise en situation du système. Ces techniques consistent à traduire un problème dans un certain langage, fournissant une forme compilée de ce problème, dont la résolution est facile et la taille aussi compacte que possible. L'étape de traduction peut être très longue, mais elle n'est effectuée qu'une seule fois, hors ligne. Il existe de nombreux langages-cible de compilation, notamment le langage des diagrammes de décision binaires (BDDs), qui ont été utilisés avec succès dans divers domaines de l'intelligence artificielle, tels le model-checking, la configuration ou la planification. L'objectif de la thèse était d'étudier l'application de la compilation de connaissances à la conduite de systèmes autonomes. Nous nous sommes intéressés à des problèmes réels de planification, qui impliquent souvent des variables continues ou à grand domaine énuméré (temps ou mémoire par exemple). Nous avons orienté notre travail vers la recherche et l'étude de langages-cible de compilation assez expressifs pour permettre de représenter de tels problèmes. Dans la première partie de la thèse, nous présentons divers aspects de la compilation de connaissances ainsi qu'un état de l'art de l'utilisation de la compilation dans le domaine de la planification. Dans une seconde partie, nous étendons le cadre des BDDs aux variables réelles et énumérées, définissant le langage-cible des " interval automata " (IAs). Nous établissons la carte de compilation des IAs et de certaines restrictions des IAs, c'est-à-dire leurs propriétés de compacité et leur efficacité vis-à-vis d'opérations élémentaires. Nous décrivons des méthodes de compilation en IAs pour des problèmes exprimés sous forme de réseaux de contraintes continues. Dans une troisième partie, nous définissons le langage-cible des " set-labeled diagrams " (SDs), une autre généralisation des BDDs, permettant de représenter des IAs discrétisés. Nous établissons la carte de compilation des SDs et de certaines restrictions des SDs, et décrivons une méthode de compilation de réseaux de contraintes discrets en SDs. Nous montrons expérimentalement que l'utilisation de IAs et de SDs pour la conduite de systèmes autonomes est prometteuse.

The control of the quality of mechanical computations arouses a growing interest in both design and certification processes. It relies on error estimators the use of which leads to often prohibitive additional numerical costs on large computations. The present work puts forward a new procedure enabling to obtain a guaranteed estimation of discretization error in the setting of linear elastic problems solved by domain decomposition approaches. The method relies on the extension of the constitutive relation error concept to the framework of non-overlapping domain decomposition through the recovery of admissible interface fields. Its development within the framework of the FETI and BDD approaches allows to obtain a relevant estimation of discretization error well before the convergence of the solver linked to the domain decomposition. An extension of the estimation procedure to heterogeneous problems is also proposed. The behaviour of the method is illustrated and assessed on several numerical examples in 2 dimension.; Le contrôle de la qualité des calculs de structure suscite un intérêt croissant dans les processus de conception et de certification. Il repose sur l'utilisation d'estimateurs d'erreur, dont la mise en pratique entraîne un sur-coût numérique souvent prohibitif sur des calculs de grande taille. Le présent travail propose une nouvelle procédure permettant l'obtention d'une estimation garantie de l'erreur de discrétisation dans le cadre de problèmes linéaires élastiques résolus au moyen d'approches par décomposition de domaine. La méthode repose sur l'extension du concept d'erreur en relation de comportement au cadre des décompositions de domaine sans recouvrement, en s'appuyant sur la construction de champs admissibles aux interfaces. Son développement dans le cadre des approches FETI et BDD permet d'accéder à une mesure pertinente de l'erreur de discrétisation bien avant convergence du solveur lié à la décomposition de domaine. Une extension de la procédure d'estimation aux problèmes hétérogènes est également proposée. Le comportement de la méthode est illustré et discuté sur plusieurs exemples numériques en dimension 2.

Hiroshi Umeo (rapporteur étranger)Thomas Worsch (rapporteur étranger); In this memoir, the reader will be able to find two surveys on the research that I made these last years: the works about programming with cellular automata and the works about Boolean functions and their complexity.; Sont présentés les différents travaux que j'ai pu effectuer: dans le domaine des automates cellulaires et de leur programmation, puis les travaux portant sur les fonctions Booléennes et leur complexité.

In this memoir, the reader will be able to find two surveys on the research that I made these last years: the works about programming with cellular automata and the works about Boolean functions and their complexity., Sont présentés les différents travaux que j'ai pu effectuer: dans le domaine des automates cellulaires et de leur programmation, puis les travaux portant sur les fonctions Booléennes et leur complexité.

This document presents an adaptation of Data Decision Diagrams (DDD or D3 for short), proposed by LABRI (Bordeaux I University), for the representation of VHDL programs using boolean and integer variables. The paper describes the D3 model we defined, its interpretation for the representation of sets of states and transiton relations, and the main symbolic state space traversals based on this structure.; Ce document présente une adaptation des diagrammes de décisions de données (DDD ou D3), développés au LABRI, pour la représentation de programmes VHDL utilisant des variables booléennes et entières. Il décrit le modèle des D3 utilisés, leur interprétation pour la représentation d'ensembles d'états et de relations de transitions, ainsi que les principaux algorithmes de parcours d'espace d'états nécessaires à la vérification par model-checking.

This document presents an adaptation of Data Decision Diagrams (DDD or D3 for short), proposed by LABRI (Bordeaux I University), for the representation of VHDL programs using boolean and integer variables. The paper describes the D3 model we defined, its interpretation for the representation of sets of states and transiton relations, and the main symbolic state space traversals based on this structure.; Ce document présente une adaptation des diagrammes de décisions de données (DDD ou D3), développés au LABRI, pour la représentation de programmes VHDL utilisant des variables booléennes et entières. Il décrit le modèle des D3 utilisés, leur interprétation pour la représentation d'ensembles d'états et de relations de transitions, ainsi que les principaux algorithmes de parcours d'espace d'états nécessaires à la vérification par model-checking.

Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes