From 6092b2b0b455ed46e58dad46d70ed7b1873c35ea Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Wed, 24 Nov 2021 15:47:56 +0100 Subject: Revise Related Work --- mgr.tex | 41 ++++++++++++++++++----------------------- 1 file 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 -- cgit v1.2.3