Give a better lower bound on MSO model checking

1 files changed, 5 insertions, 5 deletions

diff --git a/mgr.tex b/mgr.tex
index 0c52c76..9194f59 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -87,11 +87,11 @@ can answer an individual question in the same time as model checking.
 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. In this work we will focus on the case of MSO logic over
-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
+trees. While MSO model checking is PSpace-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_{\varphi}(n)$\footnote{Throughout the text we use $O_{x}(f(n))$ notation,
 where $x$ is some portion of an algorithm's input. It indicates $x$ as a
 parameter of the algorithm, i.e. that for every integer $k$, there is some