3. Tεχνικές Αναφορές | Technical Reports

Permanent URI for this community

https://hdl.handle.net/10889/1350

Browse

Browsing 3. Tεχνικές Αναφορές | Technical Reports by Author "Foustoucos, Eugenie"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Open Access
    Automata-theoretic and datalog-based solutions of monadic second-order logic evaluation problems over structures of bounded-treewidth
    (2011-05-10T08:46:33Z) Καλαντζή, Λαμπρινή; Φουστούκου, Ευγενία; Kalantzi, Labrini; Foustoucos, Eugenie
    Τμήμα Μηχανικών Η/Υ και Πληροφορικής (Τεχνικές Αναφορές)
    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.
  • Thumbnail Image
    Item
    Open Access
    On model-theoretic approaches to monadic second-order logic evaluation
    (2014-01-13) Κοσμαδάκης, Σταύρος; Φουστούκου, Ευγενία; Cosmadakis, Stavros; Foustoucos, Eugenie
    Τμήμα Μηχανικών Η/Υ και Πληροφορικής (Τεχνικές Αναφορές)
    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.