Etant donné trois entiers k, s et a, nous prouvons dans le premier chapitre qu'il existe un graphe k-régulier fini (resp. un graphe k-régulier connexe fini) dont le groupe d'automorphismes a exactement s orbites sur l'ensemble des sommets et a orbites sur l'ensemble des arêtes si et seulement si (s,a)=(1,0) si k=0, (s,a)=(1,1) si k=1, s=a>0 si k=2, 0< s <= 2a <= 2ks si k>2. (resp. (s,a)=(1,0) si k=0, (s,a)=(1,1) si k=1 ou 2, s-1<=a<=(k-1)s+1 et s,a>0 si k>2.) Nous étudions les polyèdres convexes de R³ dans le second chapitre. Pour tout polyèdre convexe P, nous notons Isom(P) l'ensemble des isométries de R³ laissant P invariant. Si G est un sous-groupe de Isom(P), le f_G-vecteur de P est le triple d'entiers (s,a,f) tel que G ait exactement s orbites sur l'ensemble sommets de P, a orbites sur l'ensemble des arêtes de P et f orbites sur l'ensemble des faces de P. Remarquons que (s,a,f) est le f_{id}-vecteur (appelé f-vecteur dans la littérature) d'un polyèdre si ce dernier possède exactement s sommets, a arêtes et f faces. Nous généralisons un théorème de Steinitz décrivant tous les f-vecteurs possibles. Pour tout groupe fini G d'isométries de R³, nous déterminons l'ensemble des triples (s,a,f) pour lesquels il existe un polyèdre convexe ayant (s,a,f) comme f_G-vecteur. Ces résultats nous permettent de caractériser les triples (s,a,f) pour lesquels il existe un polyèdre convexe tel que Isom(P) a s orbites sur l'ensemble des sommets, a orbites sur l'ensemble des arêtes et f orbites sur l'ensemble des faces. La structure d'incidence I(P) associée à un polyèdre P consiste en la donnée de l'ensemble des sommets de P, l'ensemble des arêtes de P, l'ensemble des faces de P et de l'inclusion entre ces différents éléments (la notion de distance ne se trouve pas dans I(P)). Nous déterminons également l'ensemble des triples d'entiers (s,a,f) pour lesquels il existe une structure d'incidence I(P) associée à un polyèdre P dont le groupe d'automorphismes a exactement s orbites de sommets, a orbites d'arêtes et f orbites de sommets.

Dans cette thèse nous nous intéressons à une technique de vérification basée sur les approximations par réécriture dans le but de l'automatiser et d'étendre son domaine d'application. L'utilisation de cette technique permet la vérification de propriétés pour des systèmes informatique. Une sur-approximation des termes atteignables par réécriture est calculée et nous pouvons déterminer si des termes indésirables (représentant la propriété) appartiennent à la sur-approximation. Si ils n'appartiennent pas à la sur-approximation alors on est sûr que les termes indésirables ne sont pas atteignables par le système et la propriété est vérifiée, sinon nous ne pouvons pas conclure à cause de la sur-approximation. C'est dans ce cadre que se placent les contributions de cette thèse. Tout d'abord nous présentons une méthode de raffinement d'approximation, s'inspirant du paradigme CEGAR (Counterexample-Guided Abstraction Refinement), déterminant comment construire automatiquement une approximation qui ne contient pas de terme indésirable. Si cette construction échoue alors des termes indésirables sont atteignables et on peut conclure que le système analysé ne vérifie pas la propriété. De plus, à partir d'un graphe des réécritures, nous présentons comment vérifier trois modèles de propriétés LTL exprimant des conditions sur l'ordre d'application des règles de réécriture. D'autre part, nous présentons dans cette thèse deux nouvelles applications de cette technique : la vérification de spécifications écrites avec l'algèbre de processus CCS (sans renommage) et l'analyse d'atteignabilité par approximation de deux problèmes indécidables pour les machines de Turing.

L'objet principal de cette thèse est l'étude de la dimension conforme Ahlfors régulière d'un espace métrique. C'est un invariant numérique par quasisymétrie, introduit par P. Pansu, permettant la classification à quasi-isométrie près des espaces homogènes de courbure négative. Elle joue actuellement un rôle important en théorie géométrique des groupes et en dynamique conforme. A partir d'une suite de recouvrements d'un espace métrique compact on construit des distances de dimension contrôlée appartenant à la jauge conforme (Ahlfors régulière). On peut ainsi caractériser toutes les métriques de la jauge à homéomorphismes bi-Lipschitz près. On montre comment calculer la dimension conforme AR à partir de modules combinatoires en considérant un exposant critique. Comme conséquence de cette égalité on obtient un critère général de dimension un. Les conditions sont données en termes de points de coupure locale.On donne par ailleurs des applications de ces résultats aux bords des groupes hyperboliques et aux ensembles de Julia des fractions rationnelles semihyperboliques. / In this thesis we study the Ahlfors regular conformal dimension of a metric space. This is a quasisymmetric numerical invariant, introduced by P. Pansu, which was used to classify negatively curved homogeneous spaces up to quasi-isometries. It plays nowadays an important role in geometric group theory and in conformal dynamics.Using a sequence of finite coverings of a compact metric space, we construct distances in the (Ahlfors regular) conformal gauge of controlled dimension. We obtain in this way a combinatorial characterization (up to bi-Lipschitz homeomorphisms) of all the metrics of the gauge.We show how to compute the conformal dimension (AR) using the critical exponent associated to the combinatorial modulus. As a consequence of this equality we obtain a general criterion ensuring dimension one. The conditions are stated in terms of local cut points.Finally, we give applications of these results to the boundaries of Gromov hyperbolic groups and to the Julia sets of semi-hyperbolic rational maps.

Cette thèse présente des résultats obtenus dans deux domaines : la théorie des langages, et la théorie des graphes. En théorie des langages, on s’intéresse à des problèmes de caractérisation de classes de langages réguliers. Le problème générique consiste à déterminer si un langage régulier donné peut être défini dans un certain formalisme. Les méthodes actuelles font intervenir un problème plus général appelé séparation. On présente ici deux types de contributions : une généralisation d’un résultat de décidabilité au cadre des langages de mots infinis, ainsi que des bornes inférieures pour la complexité du problème de séparation. En théorie des graphes, on considère le problème classique de coloration de graphes, où on cherche à attribuer des couleurs aux sommets d’un graphe de sorte que les sommets adjacents reçoivent des couleurs différentes, le but étant d’utiliser le moins de couleurs possible. Dans le cas des graphes peu denses, la méthode de déchargement est un atout majeur. Elle a notamment joué un rôle décisif dans la preuve du théorème des quatre couleurs. Cette méthode peut être vue comme une construction non conventionnelle d’un schéma de preuve par induction, spécifique à la classe de graphes et à la propriété considérées, et où la validité du schéma est rarement immédiate. On utilise des variantes de la méthode de déchargement pour étudier deux types de problèmes de coloration. / In this thesis, we present results obtained in two fields: formal language theory and graph theory. In formal language theory, we consider some problems of characterization of classes of regular languages. The generic problem consists in determining whether a given regular language can be defined in a fixed formalism. The current approaches use a more general problem called separation. We present here two types of contributions: a generalization of a decidability result to the setting of infinite words, together with lower bounds for the complexity of the separation problem. In graph theory, we consider the classical problem of graph coloring, where we assign colors to vertices of a graph in such a way that two adjacent vertices receive different colors. The goal is to use the fewest colors. When the graphs are sparse, a crucial tool for this is the discharging method. It is most notably decisive in the proof of the Four-Color Theorem. This method can be seen as an unconventional construction of an inductive proof scheme, specific to the considered problem and graph class, where arguing the validity of the scheme is rarely immediate. We use variants of the discharging method to study two types of coloring problems.

Une tresse est une classe d'équivalence de mots de tresse. Diverses formes normales sur les tresses ont été décrites dans la littérature, c'est-à-dire, divers moyens de sélection, pour toute tresse, d'un mot de tresse distingué la représentant. Définie de façon naturelle sur les monoïdes de tresses de Birman-Ko-Lee (ou duaux), la forme normale tournante peut être étendue au groupe de tresses tout entier. Ici, nous donnons des contraintes de nature combinatoire satisfaites par cette nouvelle forme normale. Nous en obtenons ainsi une caractérisation et montrons que l'ensemble des formes normales tournantes des tresses duales constitue un langage régulier.<br /><br />Un résultat de P. Dehornoy (1992) affirme que toute tresse non triviale admet un représentant sigma-défini. Ce résultat est à la base de la construction de l'ordre des tresses. A l'aide de la forme normale tournante et de ses propriétés, nous montrons que toute tresse admet un représentant sigma-défini de longueur quasi-géodésique, ce qui résout une question ouverte depuis une quinzaine d'années. <br /><br />Un résultat de R. Laver montre que les monoïdes de Birman-Ko-Lee munis de l'ordre des tresses sont bien ordonnés mais laisse ouvert la détermination de leurs longueurs.<br />A l'aide de la forme normale tournante, nous obtenons une caractérisation de l'ordre des tresses sur le monoïde de Birman-ko-Lee à n brins à partir de sa restriction sur celui à (n-1) brins. Une conséquence de ce résultat est une nouvelle démonstration du résultat de R. Laver ainsi que la détermination de la longueur des monoïdes de tresses duaux munis de l'ordre des tresses.

Étude des règles de pivotage dans la résolution d'un certain nombre de problèmes lies aux manipulations de matrices.

On introduit dans cette thèse le concept nouveau de platitude. Un système est différentiellement plat (ou plus simplement plat) si son comportement peut être complètement décrit par un ensemble de fonctions différentiellement indépendantes dépendant des variables du système et de leurs dérivées : toute trajectoire du système peut s'obtenir à partir de cet ensemble de fonctions sans intégrer d'équations différentielles. La platitude se définit par l'intermédiaire d'une relation d'équivalence. Deux systèmes S et T sont équivalents s'il existe une correspondance bijective entre les trajectoires de S et celles de T. Par définition, un système est plat s'il est équivalent à un système "sans dynamique", c'est à dire un ensemble de fonctions arbitraires.

Ce travail porte sur l'analyse asymptotique d'un problème de transmission avec couche mince dans un domaine bidimensionnel à coin. Précisément, on construit un dévelop\-pement asymptotique de la solution en fonction de l'épaisseur de la couche. La présence d'un coin engendre des singularités qui compromettent la construction habituelle du développement, par résolution alternative entre le domaine intérieur et la couche. Celles-ci sont traitées par l'introduction de profils construits dans un domaine infini avec couche d'épaisseur 1 à l'aide de la transformation de Mellin. On s'intéresse ensuite à la performance de la condition aux limites approchée, dont on sait qu'elle remplace l'effet de la couche mince jusqu'à l'ordre 3 dans le cas d'un domaine régulier. On montre que la présence d'un coin détériore son efficacité, ce d'autant plus que l'angle d'ouverture est grand. Des calculs numériques ont été effectués, qui confirment les résultats théoriques obtenus.

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq. / We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant.

Les travaux décrits dans cette thèse portent sur le problème de vérification des systèmes avec espaces d’états infinis, et, en particulier, avec des structures de données chaînées. Plusieurs approches ont émergé, sans donner des solutions convenables et robustes, qui pourrait faire face aux situations rencontrées dans la pratique. Nos travaux proposent une approche nouvelle, qui combine les avantages de deux approches très prometteuses: la représentation symbolique a base d’automates d’arbre, et la logique de séparation. On présente également plusieurs améliorations concernant l’implementation de différentes opérations sur les automates d’arbre, requises pour le succès pratique de notre méthode. En particulier, on propose un algorithme optimise pour le calcul des simulations sur les systèmes de transitions étiquettes, qui se traduit dans un algorithme efficace pour le calcul des simulations sur les automates d’arbre. En outre, on présente un nouvel algorithme pour le problème d’inclusion sur les automates d’arbre. Un nombre important d’expérimentes montre que cet algorithme est plus efficace que certaines des méthodes existantes. / This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating that the new algorithm outperforms other existing approaches.