Logique, automates finis, mots infinis...

[Sky-Doll]

Bonjour,

J'étudie en ce moment la preuve du théorème de McNaughton, et me heurte à la construction un peu sèche due à S. Safra permettant de créer un automate de Rabin équivalent à un automate de Büchi donné... Les explications données dans le livre de Pin (infinite words) et dans celui de W. Thomas restent désespérément obscures... Je suis donc à la recherche de constructions plus détaillées et plus didactiques... Si l'un d'entre vous a une idée de référence à me proposer!

Au plaisir de vous lire...