Next: Mots infinis
Up: Home Page
Previous: Equations et
variétés
J'ai étudié, en collaboration avec D. Perrin, les liens entre la théorie des automates et la logique . Nous avons donné une nouvelle démonstration et enrichi le théorème de W. Thomas qui établit une correspondance bijective entre les hiérarchies de concaténation et les hiérarchies de quantification en logique de premier ordre [45]. Nous avons de plus étendu ce résultat aux mots infinis. J'ai également étudié, en collaboration avec D. Beauquier, la théorie (du premier ordre) du successeur interprété sur les mots [55,63]. Nos travaux résolvent d'une part un problème proposé par Parikh et caractérisent les langages de mots finis expressibles dans cette logique. En 1995, j'ai complété l'étude entreprise avec D. Beauquier et j'ai pu en particulier caractériser le pouvoir d'expression des formules existentielles de la logique du successeur. Il s'agit d'un résultat assez difficile, car cette caractérisation n'entre pas dans le cadre habituel des variétés de langages.
J'ai également travaillé, en collaboration avec J. Cohen et D. Perrin, sur la logique temporelle. Nous avons trouvé une preuve simple, basée sur le théorème de décomposition des semigroupes finis, de l'équivalence de la logique temporelle et de la logique du premier ordre. Une technique analogue nous a permis de donner une caractérisation effective (et un algorithme) de l'expressivité de la logique temporelle pure (i.e. sans l'opérateur until) [77].
L'article [83], déjà cité, étend les résultats de Thomas qui avait établi le parallèle entre la hiérarchie de logique du premier ordre et les hiérarchies de concaténation. Nous caractérisons en particulier la hiérarchie à l'aide du produit non ambigu.