Mikołaj Bojańczyk

The goal of this page is to prove the following theorem.

Theorem. 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 linear time algorithm which inputs a tree decomposition of width k and decides if the underlying graph satisfies \varphi.

Recall sourced graphs, the algebraic definition of tree decompositions that was described here. 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

Lemma 1. 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).

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

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.

Lemma 2. 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:

  1. the tree t is accepted by \Aa;
  2. the graph generated by t satisfies \varphi.

Proof. 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.

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 leaf 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).

Furthermore, the equality t(v,i)=t(w,j) can be tested in mso on the tree t in the following sense.

Claim. 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)

Proof of the claim. The formula says that there is some source name n and a node u such that:

  • u is an ancestor of both v and w
  • on the path from v to u, the vertex corresponding to t(v,i) is present all the time as an source with name n;
  • on the path from w to u, the vertex corresponding to t(w,j) is present all the time as an source with name n.

This completes the proof of the claim. \Box

In a similar way, we can write an mso formula which selects a pair of nodes (v,w) in the tree t if and only if the underlying graph has an edge from t(v,i) to t(w,j). Once we have these formulas, we can simulate mso on the graph generated by t using mso on the tree t itself. The idea is that instead of quantifying over a set W of vertices in the generated graph, we can quantify over sets W_0,\ldots,W_k of nodes in t, with

    \[W_i = \set{w : t(w,i) \in W}\]

Using the formulas from the claim and analogue for edges, we can interpret the tuple W_0,\ldots,W_k as a set of vertices in the graph, and test the edge relationship between these vertices. \Box