##  [Automates sur les Arbres](/fr/node/60992) 

 Définition

Automates qui traitent des entrées structurées en arbres plutôt que des mots, reconnaissant des ensembles d′arbres finis ou infinis (rangés ou non) selon des conditions d′acceptation ; ils caractérisent les langages d′arbres réguliers et servent à décider des propriétés de modèles de termes, de logiques sur arbres et de problèmes de vérification à structure branchée.

 

 

 

 

 

 





## Principe

Principe

Définir un parcours qui associe des états aux nœuds selon des règles de transition locales (bottom-up, top-down ou alternant) et accepter un arbre si le parcours satisfait les critères d′acceptation désignés (par ex. états finaux à la racine, conditions de parité sur les branches infinies).

 

 

 

 

 





## Démonstration

Démonstration

Un automate d′arbres fini bottom-up reconnaît l′ensemble des arbres syntaxiques typés d′expressions bien formées ; en analyse de programmes, un automate d′arbres peut décrire l′ensemble des formes d′tas accessibles et ainsi réduire l′analyse de forme à la vérification de non-emptiness.

 

 

 

 

## Mauvaise application

Mauvaise application

Traiter les automates d′arbres comme des automates sur mots : utiliser des dispositifs déterministes top-down alors qu′ils sont strictement moins expressifs que les automates nondéterministes bottom-up, ou ignorer les distinctions rangé/non rangé et les coûts de traduction associés.

 

 

 

 

 





## Conséquence

Conséquence

Fournit des propriétés de fermeture par union, intersection et souvent complémentation (selon le modèle), des problèmes d′emptiness et d′appartenance décidables, et une correspondance avec MSO sur arbres qui donne des caractérisations logiques et des procédures décisionnelles.

 

 

 

 

## Inversion

Inversion

Au lieu d′utiliser des automates pour reconnaître des langages d′arbres, on peut exprimer des propriétés d′arbres en logiques (MSO, μ-calcul modal) et employer des outils logiques pour raisonner sur les arbres ; cette inversion privilégie l′expressivité logique et la manipulation syntaxique aux constructions par automates.

 

 

 

 

 





## Limite

Limite

S′applique aux arbres munis d′un étiquetage de nœuds et d′une structure de branchement claire ; les variantes (bottom-up, top-down, déterministe, nondéterministe, alternant, parité, Rabin) diffèrent en puissance expressive et en propriétés de fermeture ; toutes ne traitent pas les arbres non ordonnés ou portant des données sans extensions.

 

 

 

 

 





## Tension sémantique

Tension sémantique

Tension entre déterminisme et expressivité (les modèles déterministes peuvent être plus faibles ou coûteux à construire) et entre techniques pour arbres finis et infinis, où l′acceptation sur des branches infinies exige des conditions d′acceptation plus riches et des méthodes décisionnelles différentes.

 

 

 

 

 





## Synthèse

Synthèse

Les Automates Sur Les Arbres généralisent les automates sur mots aux structures branchées : en structurant les parcours le long des nœuds et en exploitant des conditions d′acceptation, ils offrent un cadre automates-théorique des propriétés d′arbres qui fonde des résultats de décidabilité et de caractérisation logique pour des modèles en forme d′arbre.