Les langages localement testables sont des exemples de langages reconnus par des scanners : l'appartenance d'un mot à un tel langage est déterminé par l'ensemble des facteurs de longueur fixée k (et ceci indépendamment de leur ordre d'apparition ou de leur fréquence dans le mot) et par les préfixes et les suffixes de longueur < k du mot. Les langages localement testables sont caractérisés par une propriété algébrique profonde de leur semigroupe syntactique, découverte indépendamment par Brzozowski-Simon et McNaughton.

Plusieurs variations sont possibles à partir de cette définition. Tout d'abord, on peut éliminer les conditions portant sur les préfixes et les suffixes. L'appartenance d'un mot à ce type de langages, que nous avons baptisés langages fortement localement testables (SLT), est entièrement déterminée par ses facteurs de longueur fixe k. Par conséquent, un langage est SLT si et seulement si il est combinaison booléenne finie de langages de la forme A^*wA^*, où w est un mot. On montre que cette classe de langages est également décidable et caractérisée par une autre propriété algébrique simple. Une autre extension naturelle consiste à tenir compte de la multiplicité des occurrences de facteurs dans un mot, jusqu'à un certain seuil. On définit ainsi la classe des langages localement testables à seuil (TLT). La combinaison de deux résultats profonds de Straubing et Thérien-Weiss conduit à une caractérisation syntactique de ces langages.

Les classes de langages que nous venons d'introduire sont également intimement reliées à l'étude de la logique du premier ordre du successeur, enrichie d'un prédicat pour chaque lettre, interprétée sur les mots finis. En effet, Thomas a montré que les langages définissables dans cette logique sont exactement les langages TLT. Comme on dispose par ailleurs d'une caractérisation syntactique de ces langages, on en déduit le résultat suivant: étant donné une formule du second ordre monadique de la théorie du successeur, on peut décider si cette formule est équivalente à une formule du premier ordre.

Locally testable languages are examples of languages recognized by scanners : the membership of a given word in such a language is determined by the set of factors of a fixed length k (the order in which these factors occur and their frequency is not relevant) of the word, and by the prefixes and suffixes of length < k of the word. The locally testable languages are characterized by a deep algebraic property of their syntactic semigroup, discovered independently by Brzozowski-Simon and McNaughton.

There are several possible variations on this definition. First, one can drop the conditions about the prefixes and suffixes. Membership in this type of language, that we call strongly locally testable (SLT), is determined only by factors of a fixed length k. Thus, a language is SLT if and only if it is a finite boolean combination of languages of the form A^*wA^*, where w is a word. We show that this family is also decidable and characterized by another simple algebraic property. A second natural extension is to take in account the number of occurrences of the factors of the word, up to a certain threshold. This defines the threshold locally testable languages (TLT). A combination of two deep results of Straubing and Thérien-Weiss yields a syntactic characterization of these languages.

The families of languages we have introduced are also deeply connected with the study of first order theory of successor, with a predicate for each letter, interpreted on finite words. Indeed Thomas proved that the languages definable in this logic are exactly the TLT languages. Since we have an effective syntactic characterization of these languages, we derive the following decidability result : given a monadic second order formula of the theory of successor, it is decidable whether this formula is equivalent to a first order formula.