摘要：A data tree is a finite tree whose every node carries a label from a finitealphabet and a datum from some infinite domain. We introduce a new model ofautomata over unranked data trees with a decidable emptiness problem. It isessentially a bottom-up alternating automaton with one register that can storeone data value and can be used to perform equality tests with the data valuesoccurring within the subtree of the current node. We show that it captures theexpressive power of the vertical fragment of XPath - containing the child,descendant, parent and ancestor axes - obtaining thus a decision procedure forits satisfiability problem.
