Automate d'arbres infinis

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].

• Portail de l'informatique théorique