The Monadic Second-order Logic Evaluation Problem on Finite Colored Trees: a Database-theoretic Approach

We model the monadic second-order logic (MSO) evaluation problem on finite colored trees in a purely database theoretic framework, based on the well-known MSO-automata connection: we reduce the problem to an acyclic conjunctive query evaluation problem on the one hand and to a monadic datalog evaluation problem on the other hand. This approach offers the possibility to solve the MSO problem using optimized evaluation methods for relational algebra expressions and for datalog programs (such as Yannakakis algorithm [27] and the rewriting method using resolutionbased filtering referred to as "magic sets" method in [3]): we use these methods for evaluating our queries and giving estimates of their complexity. This is the first time, to our knowledge, that a solution to the MSO evaluation problem related to relational algebra is given; furthermore, thanks to this reduction, we prove that the automata-based algorithm given in [8] constitutes a particular "instance" of Yannakakis algorithm. Besides the optimized database methods that we propose for solving the MSO evaluation problem, our results prove that MSO-definable queries over colored trees are datalog-definable; this result subsumes the corresponding result in [12] which states that unary MSO queries are monadic datalog-definable and it also subsumes the well-known result that any MSO-definable class of trees is monadic datalog-definable.