Finite-state automata are a central computational model in computer science, with numerous and diverse applications. In one such application, viz. model-checking, automata over infinite words play a central rˆole. In this thesis, we concentrate on B¨uchi automata (BA), which are arguably the simplest finite-state model recognizing languages of infinite words. Two algorithmic problems are paramount in the theory of automata: language inclusion and automata minimization. They are both PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected. In this thesis, we develop techniques to tackle these problems. In automata minimization, one seeks the smallest automaton recognizing a given language (“small” means with few states). Despite PSPACE-hardness of minimization, the size of an automaton can often be reduced substantially by means of quotienting. In quotienting, states deemed equivalent according to a given equivalence are merged together; if this merging operation preserves the language, then the equivalence is said to be Good for Quotienting (GFQ). In general, quotienting cannot achieve exact minimization, but, in practice, it can still offer a very good reduction in size. The central topic of this thesis is the design of GFQ equivalences for B¨uchi automata. A particularly successful approach to the design of GFQ equivalences is based on simulation relations. Simulation relations are a powerful tool to compare the local behavior of automata. The main contribution of this thesis is to generalize simulations, by relaxing locality in three perpendicular ways: by fixing the input word in advance (fixed-word simulations, Ch. 3), by allowing jumps (jumping simulations, Ch. 4), and by using multiple pebbles (multipebble simulations for alternating BA, Ch. 5). In each case, we show that our generalized simulations induce GFQ equivalences. For fixed-word simulation, we argue that it is the coarsest GFQ simulation implying language inclusion, by showing that it subsumes a natural hierarchy of GFQ multipebble simulations. From a theoretical perspective, our study significantly extends the theory of simulations for BA; relaxing locality is a general principle, and it may find useful applications outside automata theory. From a practical perspective, we obtain GFQ equivalences coarser than previously possible. This yields smaller quotient automata, which is beneficial in applications. Finally, we show how simulation relations have recently been applied to significantly optimize exact (exponential) language inclusion algorithms (Ch. 6), thus extending their practical applicability.

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.

In this thesis, we investigate the complexity of the membership problem for pattern languages. A pattern is a string over the union of the alphabets A and X, where X := {x_1, x_2, x_3, ...} is a countable set of variables and A is a finite alphabet containing terminals (e.g., A := {a, b, c, d}). Every pattern, e.g., p := x_1 x_2 a b x_2 b x_1 c x_2, describes a pattern language, i.e., the set of all words that can be obtained by uniformly substituting the variables in the pattern by arbitrary strings over A. Hence, u := cacaaabaabcaccaa is a word of the pattern language of p, since substituting cac for x_1 and aa for x_2 yields u. On the other hand, there is no way to obtain the word u' := bbbababbacaaba by substituting the occurrences of x_1 and x_2 in p by words over A. The problem to decide for a given pattern q and a given word w whether or not w is in the pattern language of q is called the membership problem for pattern languages. Consequently, (p, u) is a positive instance and (p, u') is a negative instance of the membership problem for pattern languages. For the unrestricted case, i.e., for arbitrary patterns and words, the membership problem is NP-complete. In this thesis, we identify classes of patterns for which the membership problem can be solved efficiently. Our first main result in this regard is that the variable distance, i.e., the maximum number of different variables that separate two consecutive occurrences of the same variable, substantially contributes to the complexity of the membership problem for pattern languages. More precisely, for every class of patterns with a bounded variable distance the membership problem can be solved efficiently. The second main result is that the same holds for every class of patterns with a bounded scope coincidence degree, where the scope coincidence degree is the maximum number of intervals that cover a common position in the pattern, where each interval is given by the leftmost and rightmost occurrence of a variable in the pattern. The proof of our first main result is based on automata theory. More precisely, we introduce a new automata model that is used as an algorithmic framework in order to show that the membership problem for pattern languages can be solved in time that is exponential only in the variable distance of the corresponding pattern. We then take a closer look at this automata model and subject it to a sound theoretical analysis. The second main result is obtained in a completely different way. We encode patterns and words as relational structures and we then reduce the membership problem for pattern languages to the homomorphism problem of relational structures, which allows us to exploit the concept of the treewidth. This approach turns out be successful, and we show that it has potential to identify further classes of patterns with a polynomial time membership problem. Furthermore, we take a closer look at two aspects of pattern languages that are indirectly related to the membership problem. Firstly, we investigate the phenomenon that patterns can describe regular or context-free languages in an unexpected way, which implies that their membership problem can be solved efficiently. In this regard, we present several sufficient conditions and necessary conditions for the regularity and context-freeness of pattern languages. Secondly, we compare pattern languages with languages given by so-called extended regular expressions with backreferences (REGEX). The membership problem for REGEX languages is very important in practice and since REGEX are similar to pattern languages, it might be possible to improve algorithms for the membership problem for REGEX languages by investigating their relationship to patterns. In this regard, we investigate how patterns can be extended in order to describe large classes of REGEX languages.

Cost automata are traditional finite state automata enriched with a finite set of counters that can be manipulated on each transition. Based on the evolution of counter values, a cost automaton defines a function from the set of structures under consideration to the natural numbers extended with infinity, modulo a boundedness relation that ignores exact values but preserves boundedness properties. Historically, variants of cost automata have been used to solve problems in language theory such as the star height problem. They also have a rich theory in their own right as part of the theory of regular cost functions, which was introduced by Colcombet as an extension to the theory of regular languages. It subsumes the classical theory since a language can be associated with the function that maps every structure in the language to 0 and everything else to infinity; it is a strict extension since cost functions can count some behaviour within the input. Regular cost functions have been previously studied over finite words and trees. This thesis extends the theory to infinite trees, where classical parity automata are enriched with a finite set of counters. Weak cost automata, which have priorities {0,1} or {1,2} and an additional restriction on the structure of the transition function, are shown to be equivalent to a weak cost monadic logic. A new notion of quasi-weak cost automata is also studied and shown to arise naturally in this cost setting. Moreover, a decision procedure is given to determine whether or not functions definable using weak or quasi-weak cost automata are equivalent up to the boundedness relation, which also proves the decidability of the weak cost monadic logic over infinite trees. The semantics of these cost automata over infinite trees are defined in terms of cost-parity games which are two-player infinite games where one player seeks to minimize the counter values and satisfy the parity condition, and the other player seeks to maximize the counter values or sabotage the parity condition. The main contributions and key technical results involve proving that certain cost-parity games admit positional or finite-memory strategies. These results also help settle the decidability of some special cases of long-standing open problems in the classical theory. In particular, it is shown that it is decidable whether a regular language of infinite trees is recognizable using a nondeterministic co-Büchi automaton. Likewise, given a Büchi or co-Büchi automaton as input, it is decidable whether or not there is a weak automaton recognizing the same language.

In this dissertation we solve several combinatorial problems in different areas of mathematics: automata theory, combinatorics of partially ordered sets and extremal combinatorics. Firstly, we focus on some new automata that do not seem to have occurred much in the literature, that of solvability of mazes. For our model, a maze is a countable strongly connected digraph together with a proper colouring of its edges (without two edges leaving a vertex getting the same colour) and two special vertices: the origin and the destination. A pointer or robot starts in the origin of a maze and moves naturally between its vertices, according to a sequence of specific instructions from the set of all colours; if the robot is at a vertex for which there is no out-edge of the colour indicated by the instruction, it remains at that vertex and proceeds to execute the next instruction in the sequence. We call such a finite or infinite sequence of instructions an algorithm. In particular, one of the most interesting and very natural sets of mazes occurs when our maze is the square lattice Z2 as a graph with some of its edges removed. Obviously, we need to require that the origin and the destination vertices are in the same connected component and it is very natural to take the four instructions to be the cardinal directions. In this set-up, we make progress towards a beautiful problem posed by Leader and Spink in 2011 which asks whether there is an algorithm which solves the set of all such mazes. Next, we address a problem regarding symmetric chain decompositions of posets. We ask if there exists a symmetric chain decomposition of a 2 × 2 × ... × 2 × n cuboid (k 2’s) such that no chain has a subchain of the form (a1,...,ak,0) ≺ ... ≺ (a1,...,ak,n−1)? We show this is true precisely when k≥5 and n≥3. Thisquestion arises naturally when considering products of symmetric chain decompositions which induce orthogonal chain decompositions — the existence of the decompositions provided in this chapter unexpectedly resolves the most difficult case of previous work by Spink on almost orthogonal symmetric chain decompositions (2017) which makes progress on a conjecture of Shearer and Kleitman. Moreover, we generalize our methods to other finite graded posets. Finally, we address two different problems in extremal combinatorics related to mathematical physics. Firstly, we study metastable states in the Ising model. We propose a general model for 1-flip spin systems, and initiate the study of extremal properties of their stable states. By translating local stability conditions into Sperner- type conditions, we provide non-trivial upper bounds which are often tight for large classes of such systems. The last topic we consider is a deterministic bootstrap percolation type problem. More specifically, we prove several extremal results about fast 2-neighbour percolation on the two dimensional grid.

O objetivo deste trabalho é apresentar o modelo dos autômatos adaptativos de segunda ordem e mostrar a forte conexão desse modelo com o aprendizado indutivo no limite. Tal modelo é definido com a utilização de um conjunto de transformações sobre autômatos finitos não - determinísticos e a conexão com o aprendizado no limite á estabelecida usando o conceito de mutação composta, onde uma hipótese inicial dá início ao processo de aprendizagem, produzindo, após uma sequência de transformações sofridas por essa primeira hipótese, um modelo final que é o resultado correto do aprendizado. Será apresentada a prova de que um autômato adaptativos de segunda ordem, usado como um aprendiz, pode realizar o processo de aprendizado no limite. O formalismo dos autômatos adaptativos de segunda ordem é desenvolvido sobre o modelo dos autômatos adaptativos de primeira ordem, uma extensão natural do modelo dos autômatos adaptativos clássicos. Embora tenha o mesmo poder computacional, o autômato adaptativo de primeira ordem apresenta uma notação mais simples e rigorosa que o seu antecessor, permitindo derivar novas propriedades. Uma dessas propriedades é justamente sua capacidade de aprendizado. Como consequência, o modelo dos autômatos adaptativos de segunda ordem aumenta a expressividade computacional dos dispositivos adaptativos através da sua notação recursiva, e também através do seu potencial para o uso em aplicações de aprendizado de máquina, ilustrados nesta tese. Uma arquitetura de aprendizado de máquina usando os autômatos adaptativos de segunda ordem é proposto e um modelo de identificação no limite, aplicado em processos de inferência para linguagens livre de contexto, é apresentado. / The purpose of this work is to present the second-order adaptive automaton under an transformation automata approach and to show the strong connection of this model with learning in the limit. The connection is established using the adaptive mutations, in which any hypothesis can be used to start a learning process, and produces a correct final model following a step-by-step transformation of that hypothesis by a second-order adaptive automaton. Second-order adaptive automaton learner will be proved to acts as a learning in the limit. The presented formalism is developed over the first-order adaptive automaton, a natural and unified extension of the classical adaptive automaton. First-order adaptive automaton is a new and better representation for the adaptive finite automaton and to also show that both formulations the original and the newly created have the same computational power. Afterwards both formulations show to be equivalent in representation and in computational power, but the new one has a highly simplified notation. The use of the new formulation actually allows simpler theorem proofs and generalizations, as can be verified in this work. As results, the second-order adaptive automaton enhances the computational expressiveness of adaptive automaton through its recursive notation, and also its skills for the use in machine learning applications were illustrated here. An architecture of machine learning to use the adaptive technology is proposed and the model of identification in limit applied in inference processes for free-context languages.

O objetivo deste trabalho é apresentar o modelo dos autômatos adaptativos de segunda ordem e mostrar a forte conexão desse modelo com o aprendizado indutivo no limite. Tal modelo é definido com a utilização de um conjunto de transformações sobre autômatos finitos não - determinísticos e a conexão com o aprendizado no limite á estabelecida usando o conceito de mutação composta, onde uma hipótese inicial dá início ao processo de aprendizagem, produzindo, após uma sequência de transformações sofridas por essa primeira hipótese, um modelo final que é o resultado correto do aprendizado. Será apresentada a prova de que um autômato adaptativos de segunda ordem, usado como um aprendiz, pode realizar o processo de aprendizado no limite. O formalismo dos autômatos adaptativos de segunda ordem é desenvolvido sobre o modelo dos autômatos adaptativos de primeira ordem, uma extensão natural do modelo dos autômatos adaptativos clássicos. Embora tenha o mesmo poder computacional, o autômato adaptativo de primeira ordem apresenta uma notação mais simples e rigorosa que o seu antecessor, permitindo derivar novas propriedades. Uma dessas propriedades é justamente sua capacidade de aprendizado. Como consequência, o modelo dos autômatos adaptativos de segunda ordem aumenta a expressividade computacional dos dispositivos adaptativos através da sua notação recursiva, e também através do seu potencial para o uso em aplicações de aprendizado de máquina, ilustrados nesta tese. Uma arquitetura de aprendizado de máquina usando os autômatos adaptativos de segunda ordem é proposto e um modelo de identificação no limite, aplicado em processos de inferência para linguagens livre de contexto, é apresentado. / The purpose of this work is to present the second-order adaptive automaton under an transformation automata approach and to show the strong connection of this model with learning in the limit. The connection is established using the adaptive mutations, in which any hypothesis can be used to start a learning process, and produces a correct final model following a step-by-step transformation of that hypothesis by a second-order adaptive automaton. Second-order adaptive automaton learner will be proved to acts as a learning in the limit. The presented formalism is developed over the first-order adaptive automaton, a natural and unified extension of the classical adaptive automaton. First-order adaptive automaton is a new and better representation for the adaptive finite automaton and to also show that both formulations the original and the newly created have the same computational power. Afterwards both formulations show to be equivalent in representation and in computational power, but the new one has a highly simplified notation. The use of the new formulation actually allows simpler theorem proofs and generalizations, as can be verified in this work. As results, the second-order adaptive automaton enhances the computational expressiveness of adaptive automaton through its recursive notation, and also its skills for the use in machine learning applications were illustrated here. An architecture of machine learning to use the adaptive technology is proposed and the model of identification in limit applied in inference processes for free-context languages.

Cette thèse s'articule autour de la gestion de ressources explicites dans les langages fonctionnels, en mettant l'accent sur des propriétés de calculs avec substitutions explicites raffinant le lambda-calcul. Dans une première partie, on s'intéresse à la propriété de préservation de la beta-normalisation forte (PSN) pour le calcul lambda s. Dans une seconde partie, on étudie la propriété de confluence pour un large ensemble de calculs avec substitutions explicites. Après avoir donné une preuve générique de confluence basée sur une série d'axiomes qu'un calcul doit satisfaire, on se focalise sur la métaconfluence de lambda j, un calcul où le mécanisme de propagation des substitutions utilise la notion de multiplicité, au lieu de celle de structure. Dans la troisième partie de la thèse on définit un prisme des ressources qui généralise de manière paramétrique le lambda-calcul dans le sens où non seulement la substitution peut être explicite, mais également la contraction et l'affaiblissement. Cela donne un ensemble de huit calculs répartis sur les sommets du prisme pour lesquels on prouve de manière uniforme plusieurs propriétés de bon comportement comme par exemple la simulation de la beta-réduction, la PSN, la confluence, et la normalisation forte pour les termes typés. Dans la dernière partie de la thèse on montre différentes ouvertures vers des domaines plus pratiques. On s'intéresse à la complexité d'un calcul avec substitutions en premier lieu. On présente des outils de recherche et on conjecture des bornes maximales. Enfin, on finit en donnant une spécification formelle du calcul lambda j dans l'assistant à la preuve Coq.

Les langages formels sont des séquences sur un ensemble discret de symboles appelé alphabet. On les spécifie souvent par des formules dans une certaine logique, par des expressions rationnelles ou bien par des automates discrets de types variés. La théorie actuelle est principalement qualitative, dans le sens où ses objets sont des séquence sur un temps discret, non-métrique, dans le sens où l'acceptation d'une séquence sur un automate dépend du fait que l'on visite ou non un état accepteur, et enfin dans le sens où la comparaison de langages est plus souvent considérée en termes d'inclusion, plutôt qu'en termes de mesures quantitatives. Cette thèse contribue à l'étude de ces aspects souvent négligés en présentant des résultats fondamentaux dans trois nouvelles classes de problèmes quantitatifs sur les langages formels. Dans la première partie, nous étudions une classe de problèmes d'ordonnancement qui combine les aspects structurels associés aux dépendances entre tâches avec les aspects dynamiques liés au fait qu'un flux de requêtes arrive en continu pendant l'exécution. Nous montrons que, dans cette classe de problèmes, certains flux, pourtant admissibles dans le sens que les requêtes ne représentent pas plus de travail que ce que les machines peuvent traiter, ne peuvent pas être ordonnancé avec une latence bornée. Cependant nous développons une politique d'ordonnancement que peut garantir une accumulation de retard bornée pour tout flux de requêtes admissible, même sans le connaître à l'avance. Nous montrons que si les flux sont sous-critiques, alors cette même politique peut garantir une latence bornée. En vérification quantitative, les états et transitions d'un système peuvent être associés à des coûts, et ceux-ci utilisés pour associer des coûts moyens aux comportements infinis. Dans cette seconde partie, nous proposons de définir des omega-langages par des requêtes booléennes sur les coûts moyens. Des spécifications concernant des moyennes, tels que " le taux de perte moyen de messages est inférieur à un certain seuil " ne sont pas omega-régulières, mais exprimables dans notre modèle. Ainsi, nous étudions l'expressivité et la complexité de Borel de telles spécifications. Nous montrons que pour la clôture par intersection, il est nécessaire de considérer des coûts multi-dimensionnels. Nous mettons en évidence que dans le cas général, les conditions d'acceptation portent sur l'ensemble des points d'accumulation de la séquence des coûts moyens des préfixes d'une exécution, et nous donnons une caractérisation précise de tels ensembles. Nous proposons une classe de langages de coût moyen à seuils multiples, comparant les coordonnées minimales et minimales des points de cet ensemble à des constantes. Nous montrons enfin que cette classe est close par opérations booléennes et analysable. Enfin, dans le dernier volet, nous définissons deux mesures pour un langage temporisé : le volume de ses sous-langages de mots à nombre d'événements fixe et l'entropie (vitesse de croissance), mesure asymptotique pour un nombre non borné d'événements. Ces mesures peuvent être utilisées pour la comparaison quantitative de langages, et l'entropie peut être vue comme la quantité d'information par événement dans un mot typique du langage temporisé. Pour les langages acceptés par des automates temporisés déterministes, nous donnons une formule exacte pour le volume. Ensuite, nous caractérisons l'entropie, en utilisant des méthodes d'analyse fonctionnelle, en tant que logarithme du rayon spectral d'un opérateur intégral positif. Nous établissons plusieurs méthodes pour calculer l'entropie : une symbolique pour les automates que nos appelons " à une horloge et demie ", et deux numériques : une utilisant les techniques d'analyse fonctionnelle, l'autre basée sur la discrétisation. Nous donnons une interprétation de l'entropie en théorie de l'information en termes de complexité de Kolmogorov.

High Performance Computing (HPC) aims at providing reasonably fast computing solutions to both scientific and real life technical problems. Many efforts have indeed been made on the way to powerful supercomputers, both generic and customized configurations. However, whatever their current and future breathtaking capabilities, supercomputers work by brute force and deterministic steps, while human mind works by few strokes of brilliance. Thus, in order to take a significant advantage of hardware advances, we need powerful methods to solve problems together with highly skillful programming efforts and relevant frameworks. The advent of multicore architectures is noteworthy in the HPC history, because it has brought the underlying concept of multiprocessing into common consideration and has changed the landscape of standard computing. At a larger scale, there is a keen desire to build or host frontline supercomputers. The yearly Top500 ranking nicely illustrates and orchestrates this supercomputers saga. For many years, computers have been falling in price while gaining processing power often strengthened by specialized accelerator units. We clearly see that what commonly springs up in mind when it comes to HPC is computer capability. However, this availability of increasingly fast computers has changed the rule of scientific discovery and has motivated the consideration of challenging applications. Thus, we are routinely at the door of large-scale problems, and most of time, the speed of calculation by itself is no longer sufficient. Indeed, the real concern of HPC users is the time-to-output. Thus, we need to study each important aspect in the critical path between inputs and outputs, and keep striving to reach the expected level of performance. This is the main concern of the viewpoints and the achievements reported in this book. The document is organized into five chapters articulated around our main contributions. The first chapter depicts the landscape of supercomputers, comments the need for tremendous processing speed, and analyze the main trends in supercomputing. The second chapter deals with solving large-scale combinatorial problems through a mixture of continuous and discrete optimization methods, we describe the main generic approaches and present an important framework on which we have been working so far. The third chapter is devoted to the topic accelerated computing, we discuss the motivations and the issues, and we describe three case studies from our contributions. In chapter four, we address the topic of energy minimization in a formal way and present our method based on a mathematical programming approach. Chapter five debates on hybrid supercomputing, we discuss technical issues with hierarchical shared memories and illustrate hybrid coding through a large-scale linear algebra implementation on a supercomputer.