Logic, semigroups and automata on words

J-E. PIN

IBP-Litp 1994/16: Rapport de Recherche Litp / Litp research reports
34 pages - Décembre/December 1994 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: Logic, semigroups and automata on words

Résumé : Il s'agit d'un article de synthèse sur les liens entre la logique et les automates finis. La logique dont il est question est le "calcul séquentiel" de Büchi, qui permet de formaliser différentes propriétés des mots : il comporte un prédicat pour chaque lettre de l'alphabet et le symbole de relation < , qui est interprété comme étant l'ordre usuel sur les entiers, comme seul autre symbole non logique. Plusieurs classes célèbres ont été caractérisées dans cette logique. On présente rapidement les résultats principaux concernant le second ordre, où apparaissent les classes PH, NP, P et quelques autres et on se concentre principalement sur le second ordre monadique et sur le premier ordre. En particulier, on fait une synthèse des résultats et des problèmes fascinants qui concernent la hiérarchie de quantification du premier ordre. On s'intéresse également à la logique du premier ordre à un successeur et à la logique temporelle linéaire. On présente en fait trois niveaux de résultats, suivant que l'on interprète les formules sur les mots finis, infinis ou biinfinis. L'article ne suppose pas de prérequis particulier. En particulier, les résultats de théorie des automates et de semigroupes qui sont utilisés sont exposés dans une longue section introductive, qui comporte par ailleurs des résultats très récents sur la théorie algébrique des mots infinis.

Abstract : This is a survey article on the connections between the "sequential calculus" of Büchi, a system which allows to formalize properties of words, and the theory of automata. In the sequential calculus, there is a predicate for each letter and the unique extra non logical predicate is the relation symbol <, which is interpreted as the usual order on the integers. Several famous classes have been classified within this logic. We briefly review the main results concerning second order, which covers classes like PH, NP, P, etc. and then study in more detail the results concerning the monadic second order and the first order logic. In particular, we survey the results and fascinating open problems dealing with the first order quantifier hierarchy. We also discuss the first order logic of one successor and the linear temporal logic. There are in fact three levels of results, since these logics can be interpreted on finite words, infinite words or biinfinite words. The paper is self-contained. In particular, the necessary background on automata and finite semigroups is presented in a long introducing section, which includes some very recent results on the algebraic theory of infinite words.

Publications internes Litp 1994 / Litp research reports 1994