Tree Automata

Automata that operate on tree-structured inputs rather than words, recognizing sets of finite or infinite trees (ranked or unranked) according to acceptance conditions; used to characterize regular tree languages and to decide properties of term models, logics over trees, and verification problems with branching structure.