Satisfiability of downward XPath

XPath is a logic for finite data trees, and the downward fragment restricts the syntax by allowing only descending paths. I will show that downward XPath has a decidable satisfiability problem. For this, I will work with an automaton model that captures the logic and has a decidable (Exptime) emptiness problem.