En informatique théorique, plus précisément en théories des langages, un automate d'arbres infinis est une machine à états qui prend en entrée un arbre infini. Un automate d'arbres infinis étend les automates d'arbres et les automates de mots infinis : il étend les premiers aux arbres infinis et ajoute du branchement aux deuxièmes.
Automates d'arbres alternants Il existe une version d'automates d'arbres infinis avec de l'alternation, à l'instar des machines de Turing alternantes. On suppose ici que la condition d'acceptation est une condition de parité. Le problème de savoir si une structure finie est acceptée par un automate d'arbres infinis alternant avec condition de parité est dans UP ∩ co-UP. Décider si le langage d'un automate d'arbres alternant avec condition de parité est vide est dans EXPTIME.
Ces automates correspondent au μ-calcul. Ainsi, les résultats sur ces derniers se transfèrent au μ-calcul : le model checking du μ-calcul est dans UP ∩ co-UP et que le problème de satisfiabilité du μ-calcul est dans EXPTIME.
Notes et références
Catégorie:Théorie des automates Catégorie:Arbre (graphe)