Transitive Closure Logic, Nested Tree Walking Automata, and XPath

We study FO(MTC), first-order logic with monadic transitive closure, a logical formalism in between FO and MSO on trees. We characterize the expressive power of FO(MTC) in terms of nested tree-walking automata. Using the latter, we show that FO(MTC) is strictly less expressive than MSO, solving an open problem. We also present a temporal logic on trees that is expressively complete for FO(MTC), in the form of an extension of the XML document navigation language XPath with two operators: the Kleene star for taking the transitive closure of path expressions, and a subtree relativisation operator, allowing one to restrict attention to a specific subtree while evaluating a subexpression. We show that the expressive power of this XPath dialect equals that of FO(MTC) for Boolean, unary and binary queries. We also investigate the complexity of the automata model as well as the XPath dialect. We show that query evaluation be done in polynomial time (combined complexity), but that emptiness (or, satisfiability) is 2ExpTime-complete.