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.