Logics and Automata for Totally Ordered Trees

Marco Kuhlmann and Joachim Niehren. Logics and Automata for Totally Ordered Trees. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15–17. Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 217–231. Springer, 2008.


A totally ordered tree is a tree equipped with an additional total order on its nodes. It provides a formal model for data that comes with both a hierarchical and a sequential structure; one example for such data are natural language sentences, where a sequential structure is given by word order, and a hierarchical structure is given by grammatical relations between words. In this paper, we study monadic second-order logic (MSO) for total ly ordered terms. We show that the MSO satisfiability problem of unrestricted structures is undecidable, but give a decision procedure for practically relevant sub-classes, based on tree automata.