An automaton for XPath

I will talk about an automaton model for Xpath. The new model can capture many boolean queries of XPath (in particular, all queries of FOXPath). Consequently, emptiness is undecidable. Nevertheless, the automaton seems interesting for the following reasons. a) Model checking (query evaluation) is decidable, and automata methods could be used to derive efficient algorithms for XPath using this model. b) By restricting the class of models to some class X (such as bounded tree-width), emptiness for XPath becomes decidable again. To understand which classes X are a good idea, it helps to work with automata instead of formulas. c) Some nice techniques are used to show how XPath can be captured by the automaton.