Méthode Théorique des Automates

Technique qui réduit des problèmes décisionnels logiques à des questions portant sur des automates finis ou infinis et sur les propriétés langagières des langages acceptés par ces automates, en effectuant des traductions effectives entre formules/modèles et automates de sorte que satisfaisabilité, validité ou model-checking se ramènent à des problèmes d′emptyness, d′inclusion ou d′acceptation pour