Automate d'arbres infinis

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[1]. 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é[2]. 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[3].

Notes et références
  1. (en) Frank Nießner, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », , 392 p. (ISBN 978-3-540-36387-3, DOI 10.1007/3-540-36387-4_8, lire en ligne), p. 135–152
  2. (en) Daniel Kirsten, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », , 392 p. (ISBN 978-3-540-36387-3, DOI 10.1007/3-540-36387-4_9, lire en ligne), p. 153–167
  3. (en) Júlia Zappe, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », , 392 p. (ISBN 978-3-540-36387-3, DOI 10.1007/3-540-36387-4_10, lire en ligne), p. 171–184
  • Portail de l'informatique théorique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.