m-chrzan.xyz
aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-11-24 15:47:56 +0100
committerMarcin Chrzanowski <mc370754@students.mimuw.edu.pl>2021-11-24 15:47:56 +0100
commit6092b2b0b455ed46e58dad46d70ed7b1873c35ea (patch)
treed693c5eaf07f3e5cbdad787050192e767cc8fcea
parentaeaf8060972472eddc462cc5c88e03ea4a30d846 (diff)
Revise Related Work
-rw-r--r--mgr.tex41
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