From 20549d52dc3066328a64000db4a9b4b6b1a42193 Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Sat, 5 Feb 2022 20:53:29 +0100 Subject: Give a better lower bound on MSO model checking --- mgr.tex | 10 +++++----- 1 file 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 -- cgit v1.2.3