Cette thèse s'inscrit dans l'étude de familles de graphes infinis de présentation finie, de leurs propriétés structurelles, ainsi que des comparaisons entre ces familles. Étant donné un alphabet fini Σ, un graphe infini étiqueté par Σ peut être caractérisé par un ensemble fini de relations binaires (Ra )a∈Σ sur un domaine dénombrable V quelconque. De multiples caractérisations finies de tels ensembles de relations existent, soit de façon explicite grâce à des systèmes de réécriture ou à divers formalismes de la théorie des automates, soit de façon implicite. Après un survol des principaux résultats existants, nous nous intéressons plus particulièrement à trois problèmes. Dans un premier temps, nous définissons trois familles de systèmes de réécriture de termes dont nous démontrons que la rela- tion de dérivation peut être représentée de façon finie. De ces résultats découlent plusieurs questions sur les familles de graphes infinis correspondantes. Dans un se- cond temps, nous étudions deux familles de graphes dont les ensembles de traces forment la famille des langages contextuels, à savoir les graphes rationnels et les graphes linéairement bornés. Nous nous intéressons en particulier au cas des langages contextuels déterministes, ainsi qu'à la comparaison structurelle de ces deux familles. Enfin, d'un point de vue plus proche du domaine de la vérifica- tion, nous proposons un algorithme de calcul des prédécesseurs pour une famille d'automates à pile d'ordre supérieur.

La contribution principale de cette thèse est un système de preuve correct et complet pour les implications entre les prédicats inductifs, fréquemment rencontrées lors de la vérification des programmes qui utilisent des structures de données récursives allouées dynamiquement. Nous introduisons un système de preuve généralisé pour la logique du premier ordre et nous l'adaptons à la logique de séparation, car ceci est un cadre qui répond aux plusieurs difficultés posées par le raisonnement sur les tas alloués dynamiquement. La correction et la complétude sont assurées par quatre restrictions sémantiques et nous proposons également un semi-algorithme de recherche de preuves qui devient une procédure de décision pour le problème d'implication lorsque les restrictions sémantiques sont respectées.Ce raisonnement d'ordre supérieur sur les implications nécessite des procédures de décision de premier ordre pour la logique sous-jacente lors de l'application des règles d'inférence et lors de la recherche des preuves. Ainsi, nous fournissons deux procédures de décision pour la logique de séparation, en considérant le fragment sans quantificateurs et le fragment quantifié de façon Exists*Forall*, qui ont été intégrées dans le solveur SMT open source CVC4.Finalement, nous présentons une implémentation de notre système de preuve pour la logique de séparation, qui utilise ces procédures de décision. Étant donné des prédicats inductifs et une requête d'implication, un avertissement est émis lorsqu'une ou plusieurs restrictions sémantiques sont violées. Si l'implication est valide, la sortie est une preuve. Sinon, un ou plusieurs contre-exemples sont fournis. / The main contribution of this thesis is a sound and complete proof system for entailments between inductive predicates, which are frequently encountered when verifying programs that work with dynamically allocated recursive data structures. We introduce a generalized proof system for first-order logic, and then adapt it to separation logic, a framework that addresses many of the difficulties posed by reasoning about dynamically allocated heaps. Soundness and completeness are ensured through four semantic restrictions and we also propose a proof-search semi-algorithm that becomes a decision procedure for the entailment problem when the semantic restrictions hold.This higher-order reasoning about entailments requires first-order decision procedures for the underlying logic when applying inference rules and during proof search. Thus, we provide two decision procedures for separation logic, considering the quantifier-free and the Exists*Forall*-quantified fragments, which were integrated in the open-source, DPLL(T)-based SMT solver CVC4.Finally, we also give an implementation of our proof system for separation logic, which uses these decision procedures. Given some inductive predicate definitions and an entailment query as input, a warning is issued when one or more semantic restrictions are violated. If the entailment is found to be valid, the output is a proof. Otherwise, one or more counterexamples are provided.

L'objet de cette thèse est l'étude d'une classe de séries entières solutions de certaines équations fonctionnelles, dites mahlériennes. Ces séries interviennent en combinatoire avec des problèmes de comptage de mots et en analyse d'algorithmes où elles sont liées aux récurrences diviser pour régner. La résolution des équations mahlériennes est fondée sur les propriétés des fractions rationnelles vis à vis de l'opérateur fondamental, analogue de la dérivation pour les équations différentielles, et sur l'arithmétique des opérateurs sous-jacents à ces équations. Les méthodes décrites fournissent à la fois des procédés effectifs de calcul et des résultats qualitatifs sur les propriétés de clôture de cette classe et, dans le cas complexe, sur les propriétés analytiques des solutions. Une sous-classe importante de séries mahlériennes est fournie par les séries B-régulières, généralisation des séries B-automatiques. Elles sont la traduction, via la numération en base B, des séries rationnelles en indéterminées non commutatives de la théorie des langages formels et héritent de leurs propriétés. On peut par exemple définir les notions de représentation linéaire, de rang et de matrice de Hankel. Sous certaines conditions simples, une série mahlérienne est B-régulière ; en particulier la plupart des récurrences diviser pour régner fournissent des séries B-régulières. L'analyse asymptotique des coefficients des séries mahlériennes complexes sàppuie sur une classification qui met en valeur l'importance des séries B-régulières, sur des techniques d'algèbre linéaire et sur des méthodes de théorie analytique des nombres. Les résultats obtenus permettent de traiter les exemples rencontrés dans la pratique. Ils montrent pour les séries B-régulières un lien entre le comportement asymptotique des coefficients et le spectre des représentations linéaires et dans beaucoup de cas un phénomène de périodicité en échelle logarithmique.

Durant cette thèse, nous avons travaillé sur l'adaptation des algorithmes d'inférence grammaticale pour la recherche des propriétés communes à un ensemble de protéines. L'inférence grammaticale positive cherche à générer, à partir d'un ensemble de mots appartenant à un langage cible particulier inconnu, une représentation grammaticale qui est "optimale" par rapport à ce langage, c'est-à-dire qui rassemble et organise les particularités des mots du langage. Nous avons utilisé le diagramme de Taylor, qui classe les acides aminés suivant leurs propriétés physico-chimiques, pour construire, sous forme de treillis, un ordre sur les groupes d'acides aminés. Nous avons aussi développé une méthode d'inférence (SDTM) qui calcule les meilleurs alignements locaux entre les paires de protéines suivant un score fondé à la fois sur cet ordre et sur les propriétés statistiques de l'ensemble de protéines donné. Le résultat est une machine séquentielle proche de celle de Mealy avec des sorties réduites à "accepte" et "rejette". L'algorithme commence par construire le plus grand automate reconnaissant exactement les mots du langage et le généralise par fusions successives des paires de transitions correspondant aux acides aminés appariés dans les alignements sélectionnés. Les expérimentations ont montré l'intérêt de cette combinaison de méthodes importées de la découverte de motifs et de l'inférence grammaticale.

Déterminer la structure 3D des protéines expérimentalement est une tâche très lourde et coûteuse, qui peut s'avérer parfois impossible à réaliser. L'arrivée massive de données provenant des programmes de séquençage à grande échelle impose de passer d'une approche biochimique à une approche bioinformatique, et nécessite en particulier de développer des méthodes de prédiction sur des séquences.<br />Cette thèse propose l'exploration de deux nouvelles pistes pour progresser dans la résolution de prédiction de ponts disulfures dans les protéines. Cette liaison covalente stabilise et contraint fortement la conformation spatiale de la protéine et la connaissance des positions où elle intervient peut réduire considérablement la complexité du problème de la prédiction de la structure 3D. Pour cela, nous utilisons dans un premier temps, l'inférence grammaticale et plus particulièrement les langages de contrôle introduit par Y. Takada, puis dans un deuxième temps, la programmation logique inductive.<br />Diverses expériences visent à confronter un cadre théorique d'apprentissage et des algorithmes généraux d'inférence grammaticale régulière à une application pratique de prédiction d'appariements spécifiques au sein d'une séquence protéique. D'autres expérimentations montrent que la programmation logique inductive donne de bons résultats sur la prédiction de l'état oxydé des cystéines en inférant des règles interprétables par les biologistes. Nous proposons un algorithme d'induction heuristique dont l'idée est d'effectuer plusieurs phases d'apprentissage en tenant compte des résultats obtenus aux phases précédentes permettant ainsi de diminuer considérablement la combinatoire dans les espaces d'hypothèses logiques en construisant des règles de plus en plus discriminantes.

Une ligne de recherche présente dans la littérature depuis les années soixante est celle des \emph{théorèmes de représentation}. Son résultat fondateur est le théorème de Chomsky--Schützenberger qui stipule qu'un langage est algébrique si et seulement si il est l'image par homomorphisme de l'intersection entre un langage régulier et le langage de Dyck. Ce résultat a connu depuis diverses généralisations à différentes familles de langages. Dans cette thèse, nous proposons plusieurs généralisations de ce résultat aux langages d'ordres supérieurs. En particulier, nous introduisons une notion de langages de Dyck d'ordres supérieurs, nous définissons et étudions des classes de transductions que nous qualifions d'$\varepsilon$-sûres et nous montrons qu'un langage appartient à un niveau $k+l$ de la hiérarchie des ordres supérieurs si et seulement si il est l'image d'un langage de Dyck de niveau $k$ par une transductions $\varepsilon$-sûre de niveau $l$. Ces résultats nous permettent aussi d'obtenir d'autres types de caractérisations tels que des caractérisations logiques. / Amongst the classical results of the language theory, one can cite the known characterization of algebraic languages proved by Chomsky and Schützenberger and which states that a language is algebraic if and only if it is the homomorphic image of a regular set intersected with the Dyck language. This result has opened a new line of research and defined a new type of characterizations known as \emph{representation theorems}. In this thesis, we prove various representation theorems for the higher order languages hierarchy. In particular, we introduce a notion of higher order Dyck languages and a hierarchy of classes of transductions that we call $\varepsilon$-stable (or $\varepsilon$-safe) transductions and we prove that a language belongs to some level $k+l$ of the higher order hierarchy if and only if it can be represented as the image of a level-$k$ Dyck language by a level-$l$ $\varepsilon$-stable transduction. These representations also allow us to approach other types of characterizations such as logical characterizations.

Cette thèse s’intéresse à la sémantique dénotationnelle (en théorie desmodèles et en théorie des jeux) de quatre langages de programmation logique: - LP, le plus restrictif de tous, - DLP, une extension de LP aux disjonctions, - LPN, une extension de LP aux négations, et - DLPN, qui inclut les deux.Ce manuscrit apporte trois contributions principales:(1) Un cadre abstrait pour la sémantique de la programmation logique yest défini, et toutes les approches sémantiques que nous étudions par lasuite prennent place dans ce cadre.Nous définissons la notion générale d'espace de valeurs de vérité commeune structure algébrique spécifique, satisfaisant un certain ensembled'axiomes. Les booléens forment l'exemple canonique d'un tel espace,mais nous devons étudier des cas plus généraux si nous voulonsconsidérer la "négation par l'échec". Pour cela, nous définissons etétudions une famille infinie d'espaces, paramétrée par un ordinal.(2) Une sémantique des jeux pour LP a été définie en 1986, et son étudea été approfondie en 1998. Elle a ensuite été étendue au cas desprogrammes LPN en 2005.Ici nous développons en détails une sémantique pour les programmes DLP.Nous prouvons qu'elle est correcte et complète par rapport aux modèlesminimaux de Minker.(3) Nous définissons un opérateur sémantique qui, étant donnée une sémantique abstraite d'un langage non disjonctif, la transforme en une sémantique disjonctive associée.La correction de cette transformation découle du fait qu'elle conserveles équivalences de sémantiques.Nous en présentons ensuite quelques applications qui permettent, entre autres, d'obtenir la première sémantique des jeux pour DLPN. / In this thesis, we study denotational semantics (model-theoretic andgame-theoretic) of four logic programming languages:- LP which is the most restrictive one;- DLP which extends LP by allowing disjunctions;- LPN which extends LP by allowing negations; and- DLPN which allows both.The three main contributions of this dissertation can be summarized as follows:(1) An abstract framework for logic programming semantics is definedand all semantic approaches that we study are placed within this framework.We define the general notion of a truth value space as an appropriate algebraicstructure that satisfies a set of axioms.The booleans form the canonical example of such a space, but we need toconsider much more general ones when dealing with negation-as-failure. Forthis we define and study an infinite family of spaces, parametrized over anordinal number.(2) A game semantics for LP was defined in 1986 and further studied in 1998.Then in 2005 it was extended for the case of LPN programs.Here a game semantics for DLP programs is developed in full detail; we provethat it is sound and complete with respect to the standard, minimal modelssemantics of Minker.(3) We define a semantic operator which transforms any given abstractsemantics of a non-disjunctive language to a semantics of the"corresponding" disjunctive one. We exhibit the correctness of thistransformation by proving that it preserves equivalences of semantics,and we present some applications of it, obtaining new game semantics forDLPN, among others.

Ce mémoire est constitué de 3 parties.La NP-complétude de la satisfaction de combinaisons booléennes de contraintes de sous-arbres est démontrée dans l'article [Ven87] ; la partie I de ce mémoire étudie dans quelle mesure l'ajout de contraintes régulières laisse espérer conserver la complexité NP. Ce modèle étendu définit une nouvelle classe de langages dont l'expressivité est comparée à celle des Rigid Tree Automata [JKV11]. Puis un début de formalisation des t-dags est donné.Les patterns ont été étudiés, principalement du point de vue des contraintes sur les données qu'ils demandent. La partie II de ce mémoire les étudie plus finement, en mettant de côté les données. Les squelettes sont définis en tant qu'intermédiaire de calcul et le fait que leur syntaxe caractérise leur sémantique est démontré. Puis un lemme de pompage est donné dans un cas restreint, un autre dans le cas général est étudié et conjecturé. Ensuite des fragments de combinaisons booléennes de patterns sont comparés en expressivité pour terminer avec l'étude de la complexité des problèmes de model-checking, satisfaisabilité et DTD-satisfaisabilité sur les dits fragments.Le contenu de la partie III constitue l'article [FMS11], c'est la démonstration de la caractérisation des langages des automates fortement déterministes de niveau 2 par des systèmes d'équations récurrentes caténatives. Celle-ci utilise, entre autres, des techniques de réécriture, la notion d'inconnues non-réécrivables et les ordres noethériens. Cette caractérisation constitue le cas de base de la récurrence démontrée dans [Sén07]. / This thesis is in 3 parts.The NP-completeness of satisfiability of boolean combinations of subtree constraints is shown in the article [Ven87] ; in the part I of this thesis, we study whether adding regular contraints lets hope for keeping the same complexity. This extended model defines a new class of languages which is compared in expressivity to the Rigid Tree Automata [JKV11]. Then a begining of formalisation of the t-dags is developped.The patterns have been studied mainly from the point of view of the constraints they demand on the data. The part II of this thesis study them more finely, by putting aside the data. The skeletons are defined as calculus intermediate and the characterisation holding between their syntax and their semantics is shown. Then a pumping lemma is prooved in a restreict case, another one is conjectured in the most general case. Then fragments of boolean combinations of patterns are compared in expressivity, this parts ends with the study of complexity of model-checking, satisfiability and DTD-satisfiability on these fragments.The content of part III constitutes the article [FMS11], it is the demonstration of the characterisation of strongly-deterministic 2-level pushdown automata by recurrent catenative equation systems. This proof uses in particular, some rewriting techniques, unrewritable unknowns and noetherian orders. This characterisation provides the base case of the recurrence shown in [Sén07].

Le travail présenté dans ce mémoire concerne une démarche de conception appliquée à une gestion modale pour les systèmes à événements discrets (SED). Un mode est une configuration particulière du système où celui-ci exploite un ensemble de composants et doit respecter un ensemble de spécifications. La problématique de la gestion de mode porte principalement sur la conception des modes et sur leurs commutations. Notre objectif est de proposer une démarche de conception complètement définie où les spécifications sont assurément respectées, et où seules les commutations désirées entre modes peuvent se produire. Il est également vérifié que toute commutation dans un mode mène de manière sûre dans un autre mode. Pour réaliser cet objectif, nous utilisons la théorie de contrôle par supervision qui permet de concevoir des modèles sûrs par construction tel que les spécifications utilisées pour la construction soient respectées. La démarche proposée possède plusieurs étapes séparant ainsi les différentes études de conception. La première concerne la formalisation du cahier des charges en modèles automate à états. L'étude suivante concerne le comportement interne où celui-ci doit respecter les spécifications propres aux modes, indépendamment des autres modes. Cette étape valide le comportement de chaque mode, avant d'étudier leurs commutations. La troisième étape étudie le comportement commutatif tel que les spécifications de commutations soient respectées. Cette étape spécifie les commutations désirées, et inversement celles non voulues. L'étape suivante est l'exécution d'une fonction de suivi de trajectoire qui vérifie que toutes les commutations mènent bien dans un autre mode. Dans le cas contraire, la fonction de suivi identifie et caractérise les commutations problématiques afin d'aider le concepteur dans la résolution de ces situations. Enfin, une étape de fusion d'états finalise la démarche afin de fournir un modèle par mode qui représente le comportement de celui-ci. Pour montrer l'applicabilité de la démarche proposée, et sa faculté à être utilisée en milieu industriel, nous l'utilisons sur un exemple de taille importante utilisée dans la littérature.

Le thème central de la présente thèse est le contenu sémantique des quantificateurs logiques. Dans leur forme la plus simple, les quantificateurs permettent d’établir l’existence, ou la non-existence, d’individus répondant à une propriété. En tant que tels, ils incarnent la richesse et la complexité de la logique du premier ordre, par delà la logique propositionnelle. Nous contribuons à l’analyse sémantique des quantificateurs, du point de vue de la théorie de la dualité, dans trois domaines différents des mathématiques et de l’informatique théorique. D’une part, dans la théorie des langages formels à travers la logique sur les mots. D’autre part, dans la logique intuitionniste propositionnelle et dans l’étude de l’interpolation uniforme. Enfin, dans la topologie catégorique et dans la sémantique catégorique de la logique du premier ordre. / The unifying theme of the thesis is the semantic meaning of logical quantifiers. In their basic form quantifiers allow to state theexistence, or non-existence, of individuals satisfying a property. As such, they encode the richness and the complexity of predicate logic, as opposed to propositional logic. We contribute to the semantic understanding of quantifiers, from the viewpoint of duality theory, in three different areas of mathematics and theoretical computer science. First, in formal language theory through the syntactic approach provided by logic on words. Second, in intuitionistic propositional logic and in the study of uniform interpolation. Third, in categorical topology and categorical semantics for predicate logic.