diff options
| -rw-r--r-- | mgr.tex | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -722,10 +722,10 @@ $y$ consider the vertex $y.q$, the unique vertex here of color $c$. If it is in the same connected component as $x'.q_0$ (which we check by comparing $\componenttable[x'.q_0]$ with $\componenttable[y.q]$), we can immediately answer whether or not $A$ will accept the word on this path based on whether -this state is accepting. Indeed, if that is the case then we have not changed -connected components, thus there is a single-color path from $x'.q_0$ down to -$y.q$ and $q$ is indeed the state $A$ would have ended in after running on the -word given by the labels from $x$ down to $y$. +this state is accepting. Indeed, if the two vertices are in the same component +then there is a single-color path from $x'.q_0$ down to $y.q$ and $q$ is indeed +the state $A$ would have ended in after running on the word given by the labels +from $x$ down to $y$. Otherwise, we need to jump down to a lower copy of $Q$. We can find the first such copy where the color on our path changes from $c$ to something lower by @@ -783,7 +783,7 @@ 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 -$a_1 \ldots a_k$ (where $k = |\vec{X}|$ and each $a_i \in \{ 0, 1 \}$) should be +$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. |