diff options
| -rw-r--r-- | mgr.tex | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -512,7 +512,7 @@ before, by looking at $k' := \breaktable[(k+1).q']$, comparing it to $j$, and either halting if $k' \geq j$, or jumping again otherwise. Because with each jump we move to a color strictly smaller than before, the number of jumps is bounded by the number of colors, $|Q|$. Thus the question is answered in time -constant with respect to $|w|$. +$O(|Q|)$, which is constant with respect to $|w|$. \chapter{Branch Infix Regular Questions}\label{branchinfix} @@ -797,11 +797,11 @@ with unary relation $U_X$ is equivalent to a valuation of $\vec{X}$ in which the variable $X$ is set to $W$. Now by Theorem \ref{mso-to-automaton}, there is a tree automaton $A$ for binary -trees over the alphabet $\{ 0, 1 \}^{\vec{X}}$ which accepts a tree if and only -if its labeling corresponds to a model satisfying $\varphi''$. Here a label -$b_1 \ldots b_k$ (where $k = |\vec{X}|$ and each $b_i \in \{ 0, 1 \}$) should be -interpreted as a bit vector signifying which unary relations $U_X$ a vertex is -assigned to. +trees over the alphabet $\Sigma \times \{ 0, 1 \}^{\vec{X}}$ which accepts a +tree if and only if its labeling corresponds to a model satisfying $\varphi''$. +Here a label $b_1 \ldots b_k$ (where $k = |\vec{X}|$ and each $b_i \in \{ 0, 1 +\}$) should be interpreted as a bit vector signifying which unary relations +$U_X$ a vertex is assigned to. By combining the above reductions, we can solve MSO query answering on trees by solving the relabel regular qeustions problem on trees. Indeed, fix a formula |