diff options
| -rw-r--r-- | mgr.tex | 93 |
1 files changed, 82 insertions, 11 deletions
@@ -61,7 +61,47 @@ \tableofcontents \chapter{Introduction} -% \addcontentsline{toc}{chapter}{Introduction} + +The model checking problem is a classic problem in theoretical computer science +in which we are tasked with answering whether a given structure $S$ satisfies a +sentence $\varphi$ of some logic. Several other interesting computational +problems arise when we generalize to formulae with free variables. + +A natural computational problem one could consider is \definedterm{query +evaluation} in which, when given a formula $\varphi(\vec{X})$ and a structure +$S$, the expected output is all the valuations of $\vec{X}$ satisfying +$\varphi$. While in many respects this seems like a good generalization of model +checking, the size of the entire output could be exponential in the size of the +structure and query, thus waiting for an algorithm to output all the answers +might not always be feasible or desirable. + +Already model checking is known to be computationally difficult for various +interesting logics, but the situation can improve when restricting the class of +structures considered. For example, MSO model checking is NP-hard in general, +but Courcelle showed that deciding if an MSO sentence holds in a structure of +bounded treewidth can be done in time linear in the size of the structure. % TODO: referencja do Courcella + +Similarly, query evaluation of MSO queries on bounded treewidth structures was +shown to be polynomial in the size of the structure and the output by Courcelle +and Mosbah. Their result was improved by Frick, Flum, and Grohe to linear time. + +In this work, instead of evaluation, we will instead consider \definedterm{query +answering}. In this setting, we are insterested in alrogithms that first +preprocess the structure $S$ and formula $\varphi(\vec{X})$, and later are able +to quickly answer individual queries of the form ``does the valuation $\vec{W}$ +of $\vec{X}$ satisfy $\varphi$?'' + +\section{Main result} + +Our main result is that, for trees, after a preprocessing step linear in the +size of the tree, we can answer queries in time linearithmic with respect to the +query size (in particular, the time to answer a query does not depend on the +size of the tree). + +More explicitly, we will show how to solve Problem +\ref{mso-query-answering-problem}, with a preprocessing algorithm working in +time $O(n)$ (where $n$ is the size of the input tree), and then answer queries +in time $O(m \log m)$ (where $m$ is the size of the query): \queryproblem[% an MSO formula $\varphi(\vec{X})$ over trees with $k$ free @@ -74,11 +114,17 @@ given a $k$-tuple of subsets of $T$'s vertices $\vec{W} \in \mathcal{P}(V(T))^{k}$, is $\vec{W}$ a satisfying assignment to $\vec{X}$? In other words, does $T \models \varphi(\vec{W})$? -} +}\label{mso-query-answering-problem} Though we speak about MSO formulae with second-order variables only, first-order variables are also supported simply by restricting to queries in which sets -assigned to single-order variables are singletons. +assigned to single-order variables are singletons. Note that in the case when +the input formula has only first-order free variables, queries are answered in +constant time. + +Through a series of reductions, we will show that MSO query answering reduces to +the following problem about tree automata, which we solve in Chapter +\ref{mso-query-answering}: \queryproblem[% a deterministic bottom-up tree automaton $A$ over ranked alphabet $\Sigma$. @@ -93,13 +139,38 @@ assigned to single-order variables are singletons. label modified to the corresponding $a_i$. } -\chapter{Preliminaries}\label{r:pojecia} - -% \begin{quote} - % Blaba, który jest blaba, nie jest prawdziwym blaba. - -% \raggedleft\slshape tłum. z~chińskiego Robert Blarbarucki -% \end{quote} +\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 Colcombet's deterministic factorization forests rather than +Bagan's intricate indexing structure. + +Colcombet's result could likely be used to solve the problem of branch infix +regular queries, which we introduce as a subproblem of MSO query answering in +Chapter \ref{branchinfix}. However, Colcombet's factorization depends on fairly +deep and complex applications of semigroup theory. We present a much more +straightforward algorithmic approach. + +\chapter{Preliminaries} \section{Definitions} \subsection{Trees} @@ -539,7 +610,7 @@ down. Handling each jump takes constant time, and the number of jumps is bounded by $|Q|$ since we can only jump to a lower color. Thus we can answer branch infix regular queries in constant time. -\chapter{MSO Query Answering on Trees} +\chapter{MSO Query Answering on Trees}\label{mso-query-answering} We now have all the pieces necessary to present our \qptime{$O(n)$}{$O(m \log m)$} algorithm for MSO query answering on trees. We fix an MSO formula |