Le développement du Web a motivé l’apparition de nombreux types de formats de données semi-structurées pour les problèmes liés aux technologies du Web, comme le traitement des documents ou la gestion de base de données.Nous étudions ici la conversion des données semi-structurées d’un schéma à un autre. Pour le traitement de documents, c’est la technologie XML qui offre la solution la plus puissante à ce problème. En XML, les données semi-structurée sont des arbres de données dont les schémas peuvent être définis par des automates d’arbres avec contraintes sur les valeurs de données. Les transformations de documents sont spécifiées en XSLT, un langage fonctionnel muni de requêtes logiques XPath. Le cœur de XSLT correspond aux transducteurs d’arbres à macros avec navigation par requêtes XPath.Nous proposons de nouveaux algorithmes pour l’apprentissage des transducteurs d’arbres, basés sur des méthodes d’inférence grammaticale. Nous abordons la restriction de schéma, l’anticipation (lookahead), ou la concaténation dans la sortie.1. Nous donnons une forme normale et un algorithme d’apprentissage dans le modèle de Gold avec des ressources limitées pour les transducteurs d’arbres de haut en bas déterministes avec une inspection de domaine régulière.2. Nous montrons comment apprendre des fonctions rationnelles, décrites par les transducteurs de mots déterministes avec anticipation. Nous proposons une nouvelle forme normale qui permet un apprentissage avec des ressources polynomiales.3. Pour les transducteurs arbre-vers-mot linéaires, qui permet la concaténation dans sa sortie, nous présentons une forme normale, et montrons comment décider l’équivalence en temps polynomial. / Since the arrival of the Web, various kinds of semi-structured data formats were introduced in the areas of computer science and technology relevant for the Web, such as document processing, database management, knowledge representation, and information exchange. In this thesis, we study the conversion of semi-structured data from one schema to another.For document processing, the most powerful solutions to this problem were proposed by the XML technology. In the XML format, semi-structured data is restricted to data trees, so that schemas can be defined by tree automata, possibly enhanced by constraints on data values. Document transformations can be defined in XSLT, a purely functional programming language with logical XPath queries. The core of XSLT are macros tree transducers with navigation by XPath queries.We contribute new learning algorithms on tree transducers, that are based on methods from grammatical inference. We address three limitiations of previous approaches: schema restrictions, lookaheads, and concatenation in the output.1. For deterministic top-down tree transducers with regular domain inspection, we show a normal form and a Gold style learning algorithm in with limited resources.2. We show how to learn rational functions, described by deterministic transducers of words with lookahead. We propose a new normal form for such transducers which provides a compromise between lookahead and state minimization, that leads to a learning algorithm in Gold’s learning model with polynomial resources.3. For linear tree-to-word transducers with concatenation in the output, we present a normal form and show how to decide equivalence in polynomial time.

Cette thèse adresse les problèmes d'universalité et de complétude computationelle pour plusieurs modèles de calcul inspirés par la biologie. Il s'agit principalement des systèmes d'insertion/effacement, réseaux de processeurs évolutionnaires, ainsi que des systèmes de réécriture de multi-ensembles. Les résultats décrits se classent dans deux catégories majeures : l'étude de la puissance de calcul des opérations d'insertion et d'effacement avec ou sans mécanismes de contrôle, et la construction des systèmes de réécriture de multi-ensembles universels de petite taille. Les opérations d'insertion et d'effacement consistent à rajouter ou supprimer une sous-chaîne dans une chaîne de caractères dans un contexte donné. La motivation pour l'étude de ces opérations vient de la biologie, ainsi que de la linguistique et de la théorie des langages formels. Dans la première partie de ce manuscrit nous examinons des systèmes d'insertion/effacement correspondant à l'édition de l'ARN, un processus qui insère ou supprime des fragments de ces molécules. Une particularité importante de l'édition de l'ARN est que le endroit auquel se font les modifications est déterminé par des séquences de nucléotides se trouvant toujours du même côté du site de modification. En termes d'insertion et d'effacement, ce phénomène se modéliserait par des règles possédant le contexte uniquement d'un seul côté. Nous montrons qu'avec un contexte gauche de deux caractères il est possible d'engendrer tous les langages rationnels. D'autre part, nous prouvons que des contextes plus longs n'augmentent pas la puissance de calcul du modèle. Nous examinons aussi les systèmes d’insertion/effacement utilisant des mécanismes de contrôle d’application des règles et nous montrons l'augmentation de la puissance d'expression. Les opérations d'insertion et d'effacement apparaissent naturellement dans le domaine de la sécurité informatique. Comme exemple on peut donner le modèle des grammaires gauchistes (leftist grammar), qui ont été introduites pour l'étude des systèmes critiques. Dans cette thèse nous proposons un nouvel instrument graphique d'analyse du comportement dynamique de ces grammaires. La deuxième partie du manuscrit s'intéresse au problème d'universalité qui consiste à trouver un élément concret capable de simuler le travail de n'importe quel autre dispositif de calcul. Nous commençons par le modèle de réseaux de processeurs évolutionnaires, qui abstrait le traitement de l'information génétique. Nous construisons des réseaux universels ayant un petit nombre de règles. Nous nous concentrons ensuite sur les systèmes de réécriture des multi-ensembles, un modèle qui peut être vu comme une abstraction des réactions biochimiques. Pour des raisons historiques, nous formulons nos résultats en termes de réseaux de Petri. Nous construisons des réseaux de Petri universels et décrivons des techniques de réduction du nombre de places, de transitions et d'arcs inhibiteurs, ainsi que du degré maximal des transitions. Une bonne partie de ces techniques repose sur une généralisation des machines à registres introduite dans cette thèse et qui permet d'effectuer plusieurs tests et opérations en un seul changement d'état / The present thesis considers the problems of computational completeness and universality for several biologically-inspired models of computation: insertion-deletion systems, networks of evolutionary processors, and multiset rewriting systems. The presented results fall into two major categories: study of expressive power of the operations of insertion and deletion with and without control, and construction of universal multiset rewriting systems of low descriptional complexity. Insertion and deletion operations consist in adding or removing a subword from a given string if this subword is surrounded by some given contexts. The motivation for studying these operations comes from biology, as well as from linguistics and the theory of formal languages. In the first part of the present work we focus on insertion-deletion systems closely related to RNA editing, which essentially consists in inserting or deleting fragments of RNA molecules. An important feature of RNA editing is the fact that the locus the operations are carried at is determined by certain sequences of nucleotides, which are always situated to the same side of the editing site. In terms of formal insertion and deletion, this phenomenon is modelled by rules which can only check their context on one side and not on the other. We show that allowing one-symbol insertion and deletion rules to check a two-symbol left context enables them to generate all regular languages. Moreover, we prove that allowing longer insertion and deletion contexts does not increase the computational power. We further consider insertion-deletion systems with additional control over rule applications and show that the computational completeness can be achieved by systems with very small rules. The motivation for studying insertion-deletion systems also comes from the domain of computer security, for the purposes of which a special kind of insertion-deletion systems called leftist grammars was introduced. In this work we propose a novel graphical instrument for visual analysis of the dynamics of such systems. The second part of the present thesis is concerned with the universality problem, which consists in finding a fixed element able to simulate the work any other computing device. We start by considering networks of evolutionary processors (NEPs), a computational model inspired by the way genetic information is processed in the living cell, and construct universal NEPs with very few rules. We then focus on multiset rewriting systems, which model the chemical processes running in the biological cell. For historical reasons, we formulate our results in terms of Petri nets. We construct a series of universal Petri nets and give several techniques for reducing the numbers of places, transitions, inhibitor arcs, and the maximal transition degree. Some of these techniques rely on a generalisation of conventional register machines, proposed in this thesis, which allows multiple register checks and operations to be performed in a single state transition

Les travaux développés dans ce mémoire concernent la formalisation d'un processus sûr d'automatisation en vue de maîtriser la complexité induite par l'intégration de plus en plus importante de technologies de l'information et de la communication au cœur même des processus de production et des produits. Plus précisément, notre travail porte sur l'intégration d'approches méthodologiques, issues du Génie Automatique, et de modèles formels, issus du Génie Informatique et de l'Automatique des Systèmes à Evénements Discrets afin de garantir, a priori, le respect des exigences formulées par les utilisateurs. Notre contribution porte sur deux axes. Le premier concerne l'intégration de techniques de synthèse de la commande dans un processus d'automatisation, incluant les phases de modélisation et de génération d'un code implantable, et leur application à la reconfiguration de systèmes manufacturiers contrôlés par le produit. Le second est basé sur le raffinement formel ou semi-formel de modèles pour identifier et structurer les exigences exprimées à un niveau " système " puis les allouer et les projeter sur une architecture de fonctions, de composants ou d'équipements. Ces travaux ont été initiés dans le cadre de notre thèse en réponse aux besoins de R&D industriels de la Direction des Etudes & Recherche d'EDF, puis ont été poursuivis avec une cible relative aux systèmes manufacturiers et validés dans le cadre de collaborations industrielles variées.

Cette thèse traite des ensembles rationnels de mots indexés par des ordres linéaires et en particulier du problème de la fermeture par complémentation. Dans un papier fondateur de 1956, Kleene initie la théorie des langages en montrant que les automates sur les mots finis et les expressions rationnelles ont le même pouvoir d'expression. Depuis, ce résultat a été étendu à de nombreuses structures telles que les mots infinis (Büchi, Muller), bi-infinis (Beauquier, Nivat, Perrin), les mots indexés par des ordinaux (Büchi, Bedon), les traces, les arbres... Plus récemment, Bruyère et Carton ont introduit des automates acceptant des mots indexés par des ordres linéaires et des expressions rationnelles correspondantes. Ces structures linéaires comprennent les mots infinis, les mots indexés par des ordinaux et leurs miroirs. Le théorème de Kleene a été généralisé aux mots indexés par les ordres linéaires dénombrables et dispersés, c'est-à-dire les ordres ne contenant pas de sous-ordre isomorphe à Q. Pour la plupart des structures, la classe des ensembles rationnels forme une algèbre de Boole. Cette propriété est nécessaire pour traduire une logique en automates. La fermeture par complémentation restait un problème ouvert. Dans cette thèse, on résout ce problème de façon positive: on montre que le complément d'un ensemble rationnel de mots indexés par des ordres linéaires dispersés est rationnel. La méthode classique pour obtenir un automate acceptant le complémentaire d'un ensemble rationnel se fait par déterminisation. Nous montrons que cette méthode ne peut-être appliquée dans notre cas: tout automate n'est pas nécessairement équivalent à un automate déterministe. Nous avons utilisé d'autres approches. Dans un premier temps, nous généralisons la preuve de Büchi, basée sur une congruence de mots, et obtenons ainsi la fermeture par complémentation dans le cas des ordres linéaires de rang fini. Pour obtenir le résultat dans le cas général, nous utilisons l'approche algébrique. Nous développons une structure algébrique qui étend la reconnaissance classique par semigroupes finis : les semigroupes sont remplacés par les diamant-semigroupes qui possèdent un produit généralisé. Nous prouvons qu'un ensemble est rationnel si et seulement s'il est reconnu par un diamant-semigroupe fini. Nous montrons aussi qu'un diamant-semigroupe canonique, appelé diamant-semigroupe syntaxique, peut être associé à chaque ensemble rationnel. Notre preuve de la complémentation est effective. Le théorème de Schützenberger établit qu'un ensemble de mots finis est sans étoile si et seulement si son semigroupe syntaxique est fini et apériodique. Pour finir, nous étendons partiellement ce résultat au cas des ordres de rang fini.

Ces travaux s'inscrivent dans le cadre général de la théorie des automates, de la combinatoire des mots, de la combinatoire énumérative et de l'algorithmique. Ils ont en commun de traiter des automates et des langages réguliers, de problèmes d'énumération et de présenter des résultats constructifs, souvent explicitement sous forme d'algorithmes. Les domaines dont sont issus les problèmes abordés sont assez variés. Ce texte est compose de trois parties consacrées aux codes préfixes, à certaines séquences lexicographiques et à l'énumération d'automates.

Cette thèse porte sur l'exploitation des connaissances de domaine dans un processus de découvertes de sources de données biologiques sur le Web. Tout d'abord, des ensembles de métadonnées sont utilisés pour décrire le contenu et la qualité des sources de données. Ensuite, en s'appuyant sur ces métadonnées, les sources sont organisées dans un treillis de concepts en fonction de leurs caractéristiques communes. Le treillis de concepts constitue le support de la découverte de sources de données qui s'effectue de deux manières différentes et complémentaires : par navigation et par interrogation. Dans les deux cas la découverte de sources de données peut être guidée par des connaissances du domaine. Lors d'une découverte de sources de données par navigation, les connaissances sont utilisées soit pour réduire l'espace de recherche soit pour orienter la navigation vers des concepts sectionnés. Lors d'une découverte de sources de données par interrogation, les connaissances du domaine sont soit exprimées sous la forme de préférences entre métadonnées dans la requête soit utilisées pour l'enrichissement (ou reformulation) de la requête. Pour assurer une prise en compte des connaissances du domaine plus fidèle, nous avons introduit les treillis de concepts multivalués. L'organisation des sources de données sous la forme d'un treillis de concepts multivalués permet de contrôler la taille de l'espace de recherche et d'augmenter la flexibilité et les performances du processus de découverte dans ses deux modes. La navigation peut être effectuée dans des treillis de différents niveaux de spécialisation avec la possibilité d'effectuer des zooms dynamiques permettant le passage d'un treillis à l'autre. L'interrogation bénéficie d'une augmentation de l'expressivité dans les requêtes. / This thesis deals with knowledge-based biological data sources discovery. First, domain ontologies are used for encoding metadata describing the content of biological data sources. Then the data sources are organized into a concept lattice according to their common metadata. The data source discovery process can be performed either by navigation into the obtained concept lattice or by defining queries to be inserted into the concept lattice. In both cases, domain knowledge can be used to guide the discovery. In the case of navigation, domain knowledge is used to reduce the search space and/or to guide the navigation to some concepts rather than others. In the case of querying, domain knowledge is used to express preferences between the query keywords or to refine the query. In order to take more advantage of domain knowledge, we introduce many-valued concept lattices. Several many-valued concept lattices with different levels of precision can be built from the data sources metadata set based on domain knowledge. The use of such many-valued concept lattices allows to improve the discovery process in its both forms. In the case of navigation, it is possible to consider more than one lattice and to dynamically switch from one lattice to another in a zooming operation. In the case of querying, more complex expressive queries can be defined and inserted into the many-valued concept lattice.

Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version radicale de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondant: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans ce rapport une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple / Pedagogical formal systems have appeared recently for propositional calculus (up to the higher order), and it consists of systematically give examples of introduced notions (hypotheses). Formally, it means that to use a set Delta of formulas as hypotheses, one must first give a substitution sigma such that all the instances of formulas sigma(Delta) can be proved. This neccesity of giving examples has been pointed out by Poincaré (1913) as a common-sense practice: a definition of an object by means of assumptions has interest only if such an object can be constructed. This restriction applied to intuitionistic formal systems is consistent with the idea of negationless mathematics advocated by Griss (1946) in the middle of the past century, and shown as a more radical view of intuitionism. Through the Curry-Howard isomorphism (1980), the computational counterpart is the utility of programs defined in the associated functional systems: every function can be applied to a closed value. First results concerning propositional calculi up to the second-order has recently been published by Colson and Michel (2007, 2008, 2009). In this thesis we present an attempt to standardize and to extend to the Calculus of Constructions (CC) those previous results. First a formal and precise definition of pedagogical sub-systems of the Calculus of Constructions is introduced, and different such sub-systems are exhibited as examples

L'espace des lacets lisses C(S^1,M) associé à une variété symplectique M se voit doté d'une structure (quasi-)symplectique induite par celle de M.Nous traiterons dans cette thèse d'un analogue algébrique de cet énoncé.Dans leur article, Kapranov et Vasserot ont introduit l'espace des lacets formels associé à un schéma. Il s'agit d'un analogue algébrique à l'espace des lacets lisses.Nous generalisons ici leur construction à des lacets de dimension supérieure. Nous associons à tout schéma X -- pas forcément lisse -- l'espace L^d(X) de ses lacets formels de dimension d.Nous démontrerons que ce dernier admet une structure de schéma (dérivé) de Tate : son espace tangent est de Tate, c'est-à-dire de dimension infinie mais suffisamment structuré pour se soumettre à la dualité.Nous définirons également l'espace B^d(X) des bulles de X, une variante de l'espace des lacets, et nous montrerons que le cas échéant, il hérite de la structure symplectique de X. Notons que ces résultats sont toujours valides dans des cas plus généraux : X peut être un champs d'Artin dérivé.Pour démontrer nos résultats, nous définirons ce que sont les objets de Tate dans une infinie-catégorie C stable et complète par idempotence.Nous prouverons au passage que le spectre de K-théorie non-connective de Tate(C) est équivalent à la suspension de celui de C, donnant une version infini-catégorique d'un résultat de Saito.Dans le dernier chapitre, nous traiterons d'un problème différent. Nous démontrerons l'existence d'une structure d'algèbre de Lie sur le tangent décalé de n'importe quel champ d'Artin dérivé X. Qui plus est, ce tangent agit sur tout quasi-cohérent E, l'action étant donnée par la classe d'Atiyah de E.Ces résultats sont par exemple valides dans le cas d'un schéma X sans hypothèse de lissité. / If M is a symplectic manifold then the space of smooth loops C(S^1,M) inherits of a quasi-symplectic form. We will focus in this thesis on an algebraic analogue of that result.In their article, Kapranov and Vasserot introduced and studied the formal loop space of a scheme X. It is an algebraic version of the space of smooth loops in a differentiable manifold.We generalize their construction to higher dimensional loops. To any scheme X -- not necessarily smooth -- we associate L^d(X), the space of loops of dimension d. We prove it has a structure of (derived) Tate scheme -- ie its tangent is a Tate module: it is infinite dimensional but behaves nicely enough regarding duality.We also define the bubble space B^d(X), a variation of the loop space.We prove that B^d(X) is endowed with a natural symplectic form as soon as X has one.To prove our results, we develop a theory of Tate objects in a stable infinity category C. We also prove that the non-connective K-theory of Tate(C) is the suspension of that of C, giving an infinity categorical version of a result of Saito.The last chapter is aimed at a different problem: we prove there the existence of a Lie structure on the tangent of a derived Artin stack X. Moreover, any quasi-coherent module E on X is endowed with an action of this tangent Lie algebra through the Atiyah class of E. This in particular applies to not necessarily smooth schemes X.

J'ai travaillé sur les problèmes de modélisation du vivant avec l'hypothèse fondamentale qu'il s'agit de machines symboliques et la volonté d'aider le chercheur en biologie à traiter avec le bon niveau d'abstraction ces machines. Le cœur de mes travaux considère les ensembles de séquences que forment les macromolécules du vivant comme des langages formels et cherche à approfondir les concepts nécessaires pour mener à bien leur analyse linguistique. Il faut tout d'abord étudier le contenu lexical des séquences génomiques, son vocabulaire. Au niveau élémentaire, les facteurs répétés fournissent les unités de sens de la séquence. Cependant, la notion naturelle de répétition dans l'ADN est beaucoup plus complexe et nécessite à la fois d'être formalisée et d'être accompagnée d'une algorithmique de recherche spécialisée. J'ai particulièrement développé cet aspect dans l'étude d'éléments génétiques mobiles à l'intérieur d'un génome ou entre deux génomes. J'ai également travaillé sur le niveau syntaxique, ce qui a mené à l'élaboration d'un langage, Logol, qui permet au biologiste de construire un modèle grammatical hypothétique puis de le tester sur des séquences génomiques. Le langage défini autorise en particulier une notion de variable de chaîne avec une face abstraite qui représente la chaîne d'origine et une face concrète pour les différentes instances copies de cette chaîne d'origine. Ce cadre a été validé sur plusieurs problèmes biologiques de recherche de protéines ou d'éléments génétiques, dont la découverte de récepteurs olfactifs chez le chien et la découverte de défensines humaines. Lorsqu'aucun modèle n'est disponible, il faut tenter de l'inférer à partir d'exemples de séquences. J'ai lancé une série de recherches tant théoriques que pratiques sur ce thème. Au niveau théorique, le problème difficile de l'inférence de grammaires algébriques a été abordé à partir d'ordres partiels sur les non-terminaux ou les arbres de dérivation. La classe mieux maîtrisable des langages réguliers a fait l'objet des travaux les plus approfondis, sur une représentation par automates d'états finis. L'inférence devient alors un problème d'optimisation par gestion d'un ensemble de contraintes dynamiques sur les équivalences d'états. Du point de vue pratique, nous avons tout particulièrement étudié ces problèmes d'inférence sur des séquences de protéines, par exemple en étudiant la prédiction de certaines liaisons (ponts disulfures) entre des sites distants sur la séquence. Enfin, je propose à la fin de mon document d'habilitation un projet pour aborder de façon plus transdisciplinaire la modélisation du vivant en tant que machine symbolique. Les questions que pose la biologie, science expérimentale par excellence, s'expriment majoritairement en termes de raisonnement hypothétique. Je propose de mener des recherches en vue de la mise au point d'un assistant d'expérimentation biochimique sur puce sur cultures cellulaires. Le but global est le développement d'un environnement permettant de relier en boucle expérimentation, observations et acquisition de connaissances, en utilisant un système complet de raisonnement automatique (apprentissage abductif et inductif et planification).

Un automate temporisé est un automate augmenté avec plusieurs horloges qui mesurent le passage de temps et peuvent conditionner la modification de l'état du système. Les automates temporisés ont été introduits en tant que modèle formel pour les systèmes temps-réel, en espérant que leur rôle dans la vérification de tels systèmes sera similaire au rôle des automates finis dans la recherche systématique des erreurs de conception de systèmes non-temporisés. Dans notre thèse nous étudions plusieurs questions théoriques liés aux automates temporisés et aux langages temporisés. Dans une première partie nous étudions une sous-classe simple d'automates temporisés à une seule horloge qui est remise à zéro pendant chaque transition. Nous montrons que cette sous-classe supporte des résultats similaires à la théorie classique des automates finis: des théorèmes de Kleene, de Myhill-Nerode et de fermeture par complémentation. La deuxième et principale partie de la thèse est motivée par les expressions régulières temporisés de Asarin, Caspi et Maler. Depuis leur introduction, on sait qu'il faut employer l'intersection dans les expressions régulières pour que leur expressivité soit égale aux automates temporisés. Nous poursuivons alors une approche alternative en utilisant des parenthèses colorées pour définir les contraintes temporelles sur une séquence d'événements. Cette idée aboutit à une représentation alternative des langage des automates temporisés, basée sur une nouvelle classe de langages formels que nous appelons . Nous développons alors la théorie des expressions régulières sur les regminos et nous montrons que le problème de sémantique vide est indécidable en cas général, et décidable pour une sous-classe large de langages. L'application de ces résultats nous amène à des nouvelles structures de données et à des algorithmes pour le problème du langage vide dans les automates temporisés et les expressions régulières.