diff options
| -rw-r--r-- | mgr.tex | 25 |
1 files changed, 13 insertions, 12 deletions
@@ -83,18 +83,19 @@ trees. While MSO model checking is NP-hard in general, \textcite{courcelle1990} 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. This, using the naive method described above, gives us an algorithm for MSO query answering -over trees that answers each question in time $O(n)$. - -In our setting we suppose that we want to answer multiple such questions and -thus allow a preprocessing step over the formula and tree. In this case, the -above naive algorithm could be improved with Amarilli et al.'s -\cite{amarilli2019} data structure that allows updates of the underlying tree. -Let $m$ be the size of a given question, i.e. $|W_1 \cup ... \cup W_k|$. -Amarilli's result allows us to preprocess the tree in linear time, label it with -a choice of $W_1, \ldots, W_k$ in time $O(m \log n)$, then answer model checking -in constant time, thus greatly improving over the naive algorithm for questions -that talk about a small number of vertices compared to the size of the whole -tree. +over trees that answers each question in time $O(n)$ ($n$ being the size of the +tree). + +In our setting we suppose that we want to answer multiple such questions about a +single tree and formula, varying the valuations we ask about, and thus allow a +preprocessing step over the formula and tree. In this case, the above naive +algorithm could be improved with Amarilli et al.'s \cite{amarilli2019} data +structure that allows updates of the underlying tree. Let $m$ be the size of a +given question, i.e. $|W_1 \cup ... \cup W_k|$. Amarilli's result allows us to +preprocess the tree in linear time, label it with a choice of $W_1, \ldots, W_k$ +in time $O(m \log n)$, then answer model checking in constant time, thus greatly +improving over the naive algorithm for questions that talk about a small number +of vertices compared to the size of the whole tree. \section{Main result} |