Nicolas Bedon (LITIS, Rouen)

Les liens entre automates et logiques sont aussi presque aussi anciens (1960) que les automates eux-mêmes (1956). Du point de vue des logiciens, les automates fournissent des algorithmes de décision pour de nombreuses questions. Du point de vue des informaticiens, les liens entre automates et logiques sont la base de la modélisation/vérification de programmes ou protocoles.

Les automates traditionnels (automates de Kleene) sont un modèle naturel et simple pour représenter des programmes séquentiels: les mots reconnus peuvent être vus comme des traces d’exécution de programmes séquentiels. Dans cet exposé nous nous intéressons aux automates branchants, définis et étudiés par Lodaya & Weil à la toute fin du siècle dernier, et à leurs liens avec la logique. Les automates branchants sont une extension des automates de Kleene avec deux nouvelles catégories de transitions permettant de mettre en parallèle des chemins de l’automate. Les étiquettes des chemins ne sont plus alors des mots (ordres totaux), mais des pomsets (ordres partiels), qui peuvent aussi être vus comme des traces d’exécution de programmes concurrents.

Il est bien connu que les langages reconnus par des automates de Kleene sont exactement ceux définissables en logique monadique du second-ordre MSO[<]. Nous verrons que ceux reconnus par automates branchants sont exactement ceux définissables dans MSO[<] étendue par l’arithmétique de Presburger.