From 0fa4f4f48ca9c0c882eca893b81ce8c02f1c527e Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Thu, 9 Dec 2021 15:22:16 +0100 Subject: Specify what n is, formatting --- mgr.tex | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) (limited to 'mgr.tex') diff --git a/mgr.tex b/mgr.tex index 0859df8..71e1d8c 100644 --- a/mgr.tex +++ b/mgr.tex @@ -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} -- cgit v1.2.3