DSpace Collection:http://hdl.handle.net/10889/13652020-07-02T18:37:20Z2020-07-02T18:37:20ZOn model-theoretic approaches to monadic second-order logic evaluationΚοσμαδάκης, ΣταύροςΦουστούκου, Ευγενίαhttp://hdl.handle.net/10889/65832014-01-13T11:42:48Z2014-01-13T00:00:00ZTitle: On model-theoretic approaches to monadic second-order logic evaluation
Authors: Κοσμαδάκης, Σταύρος; Φουστούκου, Ευγενία
Abstract: We review the model-theoretic approaches to Monadic Second-Order Logic
(MSO) evaluation, especially to model-checking on MSOL-inductive classes
of structures.
Starting our study with finite strings and finite trees, we then focus
on classes of structures of bounded treewidth.
For these classes we define the ``model-theoretical automaton'' which
generalizes the corresponding automaton defined by Ladner for strings.
First we prove that the model-theoretical automaton cannot be used as an
MSO model-checking algorithm on any of these classes of structures.
Then we study its relationship with other classical model-theoretic
methods as well as its relationship with recent datalog-based
approaches to the MSO model-checking problem.2014-01-13T00:00:00ZAutomata-theoretic and datalog-based solutions of monadic second-order logic evaluation problems over structures of bounded-treewidthΚαλαντζή, ΛαμπρινήΦουστούκου, Ευγενίαhttp://hdl.handle.net/10889/43272011-06-03T07:56:12Z2011-05-10T08:46:33ZTitle: Automata-theoretic and datalog-based solutions of monadic second-order logic evaluation problems over structures of bounded-treewidth
Authors: Καλαντζή, Λαμπρινή; Φουστούκου, Ευγενία
Abstract: 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.2011-05-10T08:46:33Z