{"id":1140,"date":"2016-11-16T19:10:46","date_gmt":"2016-11-16T18:10:46","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=1140"},"modified":"2016-12-29T16:15:45","modified_gmt":"2016-12-29T15:15:45","slug":"monadic-second-order-logic-and-courcelles-theorem","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/monadic-second-order-logic-and-courcelles-theorem","title":{"rendered":"0. Monadic second-order logic and Courcelle’s Theorem"},"content":{"rendered":"

In this part of the lecture, we discuss how logic can be used to describe graphs or trees or words. The logic of interest is\u00a0monadic second-order logic (mso).\u00a0<\/em>The main result is Courcelle’s Theorem, which says that every fixed formula of\u00a0mso can be evaluated in linear time on graphs that are similar to trees.<\/p>\n

\n

Monadic second-order\u00a0logic.\u00a0<\/strong><\/p>\n

Monadic second-order logic (mso) is a logic with two types of quantifiers: one can quantify over elements, and one can quantify over sets of elements. One cannot, however, quantify over sets of pairs, or over sets triples, etc.<\/p>\n

Our main interest here is to use mso to describe properties of undirected graphs. For example, suppose that we view a undirected graph as relational structure (i.e. a model as in logic), where the universe is the vertices and there is one binary relation \"E(x,y)\" for the edges; this relation is symmetric. The following formula <\/p>\n

  <\/span>   <\/span>\"\[\forall x \forall y \ E(x,y)\]\"<\/p>\n

says that the graph is a clique. The formula only quantifies over vertices, i.e. it uses only first-order quantification. Now we consider a formula which uses also set quantification. We adopt the convention that small variables \"x,y,z,\ldots\" range over elements and big variables \"X,Y,Z,\ldots\" range over sets of elements. \u00a0The following formula says that input graph is not connected:<\/p>\n

  <\/span>   <\/span>\"\[\underbrace{\exists X}_{\text{exists a set}} \ \underbrace{(\forall x \forall y\ x \in X \land E(x,y) \Rightarrow y \in X)}_{\text{$X$ is closed under neighbours}} \land \underbrace{(\exists x \ x \in X) \land (\exists x \ x \not \in X)}_{\text{$X$ is neither empty nor full}}\]\"<\/p>\n

The above formula illustrates all constructs in mso: one can quantify over elements, over sets of elements, one can test membership of elements in sets, and one can use the predicates available in the input model.<\/p>\n

Here is another example: an mso formula which says that the input graph is three colourable:<\/p>\n

  <\/span>   <\/span>\"\[\exists X_1 \exists X_2 \exists X_3 \underbrace{\forall x \bigvee_{i} X_i}_{\text{every vertex is coloured}} \land \quad \underbrace{\forall x \forall y \ E(x,y) \Rightarrow \bigvee_{i \neq j} X_i(x) \land X_j(x)}_{\text{every edge has endpoints with different colours}}\]\"<\/p>\n

We say that a property of graphs (or more generally, structures over some vocabulary) is\u00a0mso definable\u00a0<\/em>if there is a formula of mso which is true exactly in those graphs which have the property.<\/p>\n

\n

Model checking of mso<\/strong><\/p>\n

Model checking of mso formulas is the problem of checking if a given formula is true in a given structure (here, a graph). This problem is computationally hard: if we assume that the input is both the graph and the formula, then the problem is PSPACE complete (actually, it is PSPACE complete even when the graph is fixed, e.g. the one vertex graph, by encoding QBF in a straightforward way). If the formula is fixed and the graph is the only input, then the problem can be NP complete, as the example of 3-colorability shows. Since mso has built in negation, then we can also get coNP problems, e.g. non-3-colorability, and by using alternation of set quantifiers we can\u00a0get problems that are complete for any level of the polynomial hierarchy. Summing up \u2013 in general, the\u00a0model checking problem\u00a0<\/em>is hard.<\/p>\n

The goal of this lecture is to show that the model checking becomes tractable \u2013 even linear time \u2013 when the formula is fixed and the graphs are similar to trees. In particular, 3-colorability is tractable on graphs similar to trees, but the same holds for any graph problem which can be formalised in mso.<\/p>\n

\n

Treewidth and Courcelle’s Theorem.<\/strong><\/p>\n

We now come to the main result of this part of the lecture, namely Courcelle’s theorem. The theorem is about evaluating model checking mso on graphs of bounded tree width. Treewidth is a graph parameter, i.e. every graph has a some treewidth, which is a natural\u00a0number. The treewidth\u00a0of a graph describes the smallest width\u00a0of a tree decomposition that can produce the graph. Treewidth, tree decompositions and their width are defined here<\/a>. The general idea is that small width tree decompositions can be obtained for graphs that are similar to trees, although there exists other inequivalent ways of quantifying similarity to a tree, e.g.\u00a0clique width<\/em>.<\/p>\n

Bodlaender and Kloks have shown that tree decompositions can be computed in linear time, when the width is fixed, i.e. every \"k \in \Nat\" there is a linear time algorithm which inputs a graph and outputs, if it exists, a tree decomposition of width \"k\". The constant in the linear time is exponential in \"k\". We will show an easier result, which is weaker in two ways: the algorithm is not linear, and the computed tree decomposition is not optimal.<\/p>\n

Theorem 1.\u00a0<\/strong>For every \"k \in \Nat\" there is a\u00a0cubic time algorithm which inputs a graph and fails or outputs a tree decomposition of width \"<3k\". The algorithm succeeds if the graph\u00a0has treewidth \"< k\".<\/em><\/p>\n

Theorem 1 is proved here<\/a>. The constant in the running time is exponential in \"k\".<\/p>\n

The second ingredient in Courcelle’s theorem is that, once the tree decomposition is given, \u00a0mso formulas can be evaluated in linear time.<\/p>\n

Theorem 2. <\/strong>Let \"k \in \Nat\" \u00a0and let \"\varphi\" be an mso formula over the vocabulary of graphs, i.e. using a binary relation \"E(x,y)\". \u00a0There is a linear time algorithm which inputs a tree decomposition of width \"k\" and decides if the underlying graph satisfies \"\varphi\".<\/em><\/p>\n

Theorem 2 is proved in two steps:\u00a0we introduce automata over trees and show that they are equivalent to mso<\/a>\u00a0and then we show that evaluating mso on a graph of bounded treewidth can be simulated by running a tree automaton over a tree decomposition<\/a>. The constant in the running time is nonelementary in \"\varphi\", i.e. it is more than exponential, more than doubly exponential, etc. Combining the two results above we get the following.<\/p>\n

Corollary (Courcelle’s Theorem).\u00a0<\/strong>Let \"k \in \Nat\" and let \"\varphi\" be an mso formula over the vocabulary of graphs, i.e. using a binary relation \"E(x,y)\". \u00a0There is a cubic algorithm which inputs an unidrected graph and fails or answers\u00a0if the graph satisfies \"\varphi\". The algorithm succeeds if the graph has tree width \"\le k\".<\/em><\/p>\n

Note that in the algorithm above, there are three possible outcomes: fail (don’t know), satisfies \"\varphi\", and does not satisfy \"\varphi\". Using the stronger, linear time, version of Theorem 1, we could get a linear running time for the algorithm in Courcelle’s Theorem.<\/p>\n","protected":false},"excerpt":{"rendered":"

In this part of the lecture, we discuss how logic can be used to describe graphs or trees or words. The logic of interest is\u00a0monadic second-order logic (mso).\u00a0The main result is Courcelle’s Theorem, which says that every fixed formula of\u00a0mso can be evaluated in linear time on graphs that are similar to trees. Monadic second-order\u00a0logic.\u00a0 […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":535,"menu_order":0,"comment_status":"open","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-1140","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1140"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=1140"}],"version-history":[{"count":42,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1140\/revisions"}],"predecessor-version":[{"id":1243,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1140\/revisions\/1243"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/535"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=1140"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}