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

J-E PIN

IBP-Litp 1996/27: Rapport de Recherche Litp / Litp research reports
12 pages - Juillet/July 1996 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: The expressive power of existential first order sentences of Büchi's sequential calculus

Résumé : Résumé

Cet article a pour objet l'étude de la théorie du premier ordre du successeur, interprétée sur les mots finis. De façon plus précise, nous complétons l'étude de la hiérarchie basée sur les alternances de quantificateurs (ou hiérarchie Sigma n). On savait (Thomas, 1982) que cette hiérarchie s'effondre au niveau 2, mais il restait à déterminer de façon effective le pouvoir expressif des niveaux inférieurs. Nous donnons une caractérisation effective des classes Sigma un, les formules existentielles, et BSigma un, les combinaisons booléennes des formules existentielles. Notre caractérisation est algébrique et repose sur la notion de semigroupe syntactique, mais, contrairement à la plupart des résultats de ce domaine, ne relève pas de la théorie des variétés d'Eilenberg, car les langages définissables dans BSigma un ne sont pas fermés par résiduel.

Sur le plan algorithmique, on en déduit le résultat suivant, valable pour tous les niveaux de la hiérarchie Sigma n : 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 : 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 Sigma n-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 Sigma one, the existential formulas, and BSigma one, 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 BSigma one-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.

Publications internes Litp 1996 / Litp research reports 1996