{"id":1211,"date":"2016-12-29T16:12:38","date_gmt":"2016-12-29T15:12:38","guid":{"rendered":"https:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=1211"},"modified":"2016-12-29T16:12:38","modified_gmt":"2016-12-29T15:12:38","slug":"interpreting-a-graph-in-its-tree-decomposition","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\/interpreting-a-graph-in-its-tree-decomposition","title":{"rendered":"Interpreting a graph in its tree decomposition"},"content":{"rendered":"

The goal of this page is to prove the following theorem.<\/p>\n

Theorem. <\/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

Recall sourced graphs, the algebraic definition of tree decompositions that was described here<\/a>. Define \"\Sigma_k\" to be the following ranked alphabet. For every sourced graph with at most \"k+1\" vertices and at most \"k\" sources contained in \"\set{1,\ldots,2k}\" we have a rank zero letter. For every set \"X \subseteq \set{1,\ldots,2k}\" of size at most \"k\" we have a rank two letter \"\oplus_X\". A tree \"t\" over this alphabet can be viewed as a term in the algebra of sourced graphs, which generates some sourced graph. The following<\/p>\n

Lemma 1.\u00a0<\/strong>For every tree decomposition of width at most \"k\" one can compute in linear time a tree over alphabet \"\Sigma_k\" which generates the same graph (a graph is interpreted as a sourced graph with no sources).<\/em><\/p>\n

Proof. <\/strong>A simple bottom-up pass through the tree decomposition, the same as is used in\u00a0the theorem here<\/a>. The only additional observation is that, by reusing source names, we can be sure that \"2k\" source names are enough. \"\Box\"<\/p>\n

Recall that for a given tree automaton, checking if an input tree is accepted can be done in linear time. Therefore, the theorem from the beginning of this page follows from Lemma 1 and Lemma 2 below.<\/p>\n

Lemma 2.\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)\". There is a tree automaton \"\Aa\" such that for every tree \"t\" over the ranked alphabet \"\Sigma_k\" the following conditions are equivalent:
\n<\/em><\/p>\n

    \n
  1. the tree \"t\" is accepted by \"\Aa\";<\/em><\/li>\n
  2. the graph generated by \"t\" satisfies \"\varphi\".<\/em><\/li>\n<\/ol>\n

    Proof.\u00a0<\/strong>Recall that over trees, mso and tree automata have the same expressive power. Therefore it suffices to find a formula of mso \"\psi\" over trees such that \"\psi\" is true in a tree \"t\" if and only if the graph generated by the tree \"t\" satisfies \"\varphi\".<\/p>\n

    We assume that for every rank zero letter \"a \in \Sigma_k\" there is an enumeration of the at most \"k+1\" vertices that appear in the sourced graph \"a\" which uses numbers \"\set{0,1,\ldots,k}\". Consider a \"t\" is a tree over \"\Sigma_k\". For a\u00a0leaf \"v\" of the tree \"t\" and \"i \in \set{0,1,\ldots,k}\", define \"t(v,i)\" to be the vertex in the graph generated by \"t\" which corresponds to the \"i\"-th vertex in the label of \"v\". The vertex \"t(v,i)\" might be undefined if \"i\" is not part of the enumeration in the label of \"v\". Furthermore it might be the case that \"t(v,i)=t(w,j)\" for some \"(v,i) \neq (w,j)\", this is because of the fuse operations. This definition is illustrated below (the green numbers are the enumerations of the vertices in the leaves).<\/p>\n

    \"\"<\/a><\/p>\n

    Furthermore, the equality \"t(v,i)=t(w,j)\" can be tested in mso on the tree \"t\" in the following sense.<\/p>\n

    Claim.\u00a0<\/strong>For every \"i,j \in \set{0,1,\ldots,k}\" there is an mso formula which selects a pair of nodes \"(v,w)\" in the tree \"t\" if and only if \"t(v,i)=t(w,j)\"<\/em><\/p>\n

    Proof of the claim.\u00a0<\/strong>The formula\u00a0says that there is some source\u00a0name \"n\" and a node \"u\" such that:<\/p>\n