Revise Related Work

1 files changed, 18 insertions, 23 deletions

diff --git a/mgr.tex b/mgr.tex
index d639355..1054211 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -138,35 +138,30 @@ the following problem about tree automata, which we solve in Chapter
     a tree $T$ labeled with $\Sigma$.
 }{%
     given $m$ relabelings $v_1 \mapsto a_1, \ldots, v_m \mapsto a_m$, where
-    $v_i$ are vertices of $T$ and $a_i$ are elements of $\Sigma$, what state
+    $v_i$ are vertices of $T$ and $a_i$ are labels from $\Sigma$, what state
     does $A$ arrive  at in the root of $T'$, where $T'$ is $T$ with each $v_i$'s
     label modified to the corresponding $a_i$.
 }
 
 \section{Related Work}
 
-A different generalization of model checking to the case of formulae with free
-variables is \definedterm{query enumeration}. In query enumeration, as in query
-evaluation, we are interested in outputing all the valuations satisfying a
-formula. However, instead of considering the global time of the algorithm to
-output every single result, we are interested in enumerating the valuations one
-by one with as small a delay between individual answers as possible. In other
-words, we split the entire algorithm into a preprocessing algorithm which builds
-an indexing structure, and an enumeration algorithm that, given the indexing
-structure, outputs the next answer and prepares the indexing structure for the
-next step.
-
-The complexity class \constantdelaylin\ refers to those enumeration
-problems in which the preprocessing step takes linear time and the delay between
-each successive answer (i.e. the time complexity of the second algorithm) is
-constant. \lineardelaylin\ is a generalization of \constantdelaylin\ where the
-time complexity of the second algorithm is linear in the size of the answer
-being output. \textcite{bagan2006} introduced this second notion and showed that
-enumerating MSO queries is \lineardelaylin\ on trees. This in particular means
-that enumerating MSO queries for formulae whose free variables are all first
-order is in \constantdelaylin, and \textcite{kazana2013} revisit this result,
-proving it using deterministic factorization forests due to \textcite{colcombet}
-rather than Bagan's intricate indexing structure.
+Query answering is one generatlization of model checking to the case of formulae
+with free variables. Another related one is \definedterm{query enumeration}.
+Similar to query answering, we again allow the structure and query to be
+preprocessed. Then, instead of answering individual questions about valuations,
+we are interested in outputting all the satisfying valuations one-by-one.
+
+The complexity class \constantdelaylin\ refers to those enumeration problems in
+which the preprocessing step takes linear time and the delay between each
+successive answer is constant. \lineardelaylin\ is a generalization of
+\constantdelaylin\ where the time complexity of the second algorithm is linear
+in the size of the answer being output. \textcite{bagan2006} introduced this
+second notion and showed that enumerating MSO queries is \lineardelaylin\ on
+trees. This in particular means that enumerating MSO queries for formulae whose
+free variables are all first order is in \constantdelaylin, and
+\textcite{kazana2013} revisit this result, proving it using deterministic
+factorization forests due to \textcite{colcombet} rather than Bagan's intricate
+indexing structure.
 
 Colcombet's factorization could likely be used to solve the problem of branch
 infix regular queries, which we introduce as a subproblem of MSO query answering