m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-12-16 17:35:39 +0100
committerMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-12-16 17:35:53 +0100
commit29f5d0b9c55179a60590d34953127cf8e0f19059 (patch)
treef4bbec71eaa5922dc655780f40c3ec6373a7fae1
parent846ec3bd7829fee41fdc815705bbf623f001a0ed (diff)
Style
-rw-r--r--mgr.tex10
1 files changed, 5 insertions, 5 deletions
diff --git a/mgr.tex b/mgr.tex
index 86b8a54..15fe64b 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -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.