Automata-theoretic and datalog-based solutions of monadic second-order logic evaluation problems over structures of bounded-treewidth

• Κύριοι συγγραφείς: Καλαντζή, Λαμπρινή, Φουστούκου, Ευγενία
• Άλλοι συγγραφείς: Kalantzi, Labrini
• Μορφή: Technical Report
• Γλώσσα: English
• Έκδοση: 2011
• Θέματα: Monadic second-order logic; Tree automata; Datalog; Treewidth

We propose automata-theoretic and datalog-based solutions for the Monadic Second Order (MSO) evaluation problem over finite structures of bounded treewidth, and then extend this approach to MSO-definable optimization problems. More precisely, we introduce decomposition-automata which can be thought as a generalization of assignment automata defined in [14]; these automata, running over tree-decompositions of an input structure, directly compute solutions to the considered MSO evaluation problems. The constructive proof of this result provides a direct reduction of the initial MSO evaluation problem to a decomposition-automata evaluation problem. We then use datalog and its optimization techniques to implement the computation mechanism of decomposition automata in order to provide optimized datalog solutions for the initial MSO evaluation problems. Since the automata construction can be completely expressed in datalog, we show that given an MSO formula we can directly define datalog queries that compute the solutions to the considered problems. The resulting datalog programs prove that k-ary MSO definable queries over structures of bounded-treewidth are definable in datalog of arity k +1, generalizing the result of [17] that unary MSO-definable queries are monadic datalog definable, and extending the corresponding result of [14] proven for the case of trees. Finally, we illustrate our approach by applying it in order to solve vertex cover and related optimization problems.