Module « Automates et logique »

Volume horaire

  • 14 heures de cours magistral.
  • 10 heures de travaux dirigés.

Description du module

Les liens entre logique formelle et automates ont été établis par Büchi, Elgot et Traktenbrot. Depuis, ils sont l'objet de recherches actives, en particulier parce qu'ils permettent de donner une présentation algorithmique des problèmes de décision qui se posent en logique. L'apport est double: d'un coté, ils fournissent des outils à base d'automate aux logiciens. De l'autre, ils permettent aux informaticiens d'utiliser la logique formelle pour résoudre leurs problèmes, par exemple dans la vérification/certification de programmes. Dans ce cours, nous verrons :

  • Le théorème de Büchi-Elgot-Trakhtenbrot établissant l'équivalence d'expressivité entre logique monadique du second ordre et automates;
  • L'application de la théorie des automates pour caractériser les langages définissables en logique du premier ordre;
  • L'équivalence d'expressivité entre logique du premier ordre et la classe d'expressions rationnelles dite "sans-étoile", formée à partir des lettres, par clôture avec les opérations booléennes et le produit de concaténation;
  • L'application de la théorie des jeux d'Ehrenfeucht-Fraïssé à la logique.