The expressive power of first order sentences of Büchi's sequential calculus.

Jean-Éric Pin



Résumé : Le but de cet article est d'étudier la théorie du premier ordre du successeur, interprétée sur les mots finis. De façon plus spécifique, on complète l'étude de la hiérarchie &Sigman basée sur l'alternance des quantificateurs. On savait depuis (Thomas, 1982) que cette hiérarchie s'effondre au niveau 2, mais le pouvoir expressif des niveaux inférieurs n'était pas encore connu. Nous donnons, en termes de semigroupes finis, une description du pouvoir d'expression de &Sigma1, la classe des formules purement existentielles, et de sa fermeture booléenne, B&Sigma1. Notre caractérisation algébrique repose sur l'utilisation du semigroupe syntactique, mais, contrairement à de nombreux résultats du domaine, elle n'entre pas dans le cadre de la théorie des variétés d'Eillenberg, puisque les langages définissables dans B&Sigma1 ne sont pas fermés par résiduels. Sur le plan algorithmique, on en déduit le résultat suivant, valable pour tous les niveaux de la hiérarchie : on peut décider en temps polynomial si le langage accepté par un automate déterministe à n états peut être exprimé par une formule d’un niveau donné.

Abstract : The aim of this paper is to study the first order theory of the successor, interpreted on finite words. More specifically, we complete the study of the hierarchy based on quantifier alternations (or &Sigman-hierarchy). It was known (Thomas, 1982) that this hierarchy collapses at level 2, but the expressive power of the lower levels was not characterized effectively. We give a semigroup theoretic description of the expressive power of &Sigma1, the existential formulas, and B&Sigma1, the boolean combinations of existential formulas. Our characterization is algebraic and makes use of the syntactic semigroup, but contrary to a number of results in this field, is not in the scope of Eilenberg's variety theorem, since B&Sigma1-definable languages are not closed under residuals. An important consequence is the following: given one of the levels of the hierarchy, there is polynomial time algorithm to decide whether the language accepted by a deterministic n-state automaton is expressible by a sentence of this level.

PostScript file compressed with gzip, PDF file


Valid HTML 4.01!