Finite automata on unranked trees : extensions by arithmetical and equality constraints
Wong Karianto, Wolfgang H Thomas, Christof Löding, Thomas Schwentick · RWTH Publications (RWTH Aachen) · 2010
The notion of unranked trees has attracted much interest in current research, especially due to their application as formal models of XML documents. In particular, several automata and logic formalisms on unranked trees have been considered (again) in the literature, and many results that had previously been shown for the ranked-tree setting have turned out to hold for the unranked-tree setting as well. In this thesis, we study two kinds of extensions of finite automata on unranked trees, namely, the extension by arithmetical constraints and the extension by subtree-equality constraints. In the first part of the thesis we introduce a framework of automata on unranked trees that unifies two different approaches to incorporating arithmetical constraints known from the literature, namely the global-constraint approach of Klaedtke and Rueß (2003) and the local-constraint approach of Seidl et al. (2003). We investigate the relationship between the two types of arithmetical constraints with respect to language recognition, and we show that the emptiness problem for this automaton model is decidable. In the second part of this thesis, we introduce automata on unranked trees that are equipped with equality and disequality constraints between direct subtrees, thereby extending the corresponding automaton model in the ranked-tree setting, which was introduced by Bogaert and Tison (1982). In the definition of the automaton model, we propose using formulas of monadic second-order logic to capture the possibility of comparing unboundedly many direct subtrees for equality, a feature that arises naturally in light of the unrankedness. Our main result is that the emptiness problem for this automaton model is decidable. Based upon this result, furthermore, we introduce a logic over data words (that is, words over an infinite alphabet) for which the satisfiability problem is decidable.