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
- (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
- (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
- (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