# Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?

I am currently reading "Parameterized Complexity Theory" by J. Flum and M. Grohe. In Chapter 10.3 they state in the first paragraph:

Let us remind the reader that the model-checking problem for monadic second-order logic can be decided in polynomial space by a straightforward algorithm; actually, the problem is $$\textsf{PSPACE}$$-complete.

Unfortunately they do not seem to formally establish this result anywhere in the book.

The straight forward algorithm that I think of would simply brute force check whether for a given structure $$G$$ an MSO formula $$\phi$$ is satisfied. Since we can quantify over sets and we need to keep track of the elements in the set that we quantify over, our algorithm has to store potentially $$|G|$$ elements for each nesting level of quantifiers in $$\phi$$. That means that we might need to store $${|G|}^k$$ elements, where $$k$$ depends on (the quantifier nesting depth) of $$\phi$$. But then the space required is exponential and not polynomial. Where am I going wrong here?

Regarding $$\textsf{PSPACE}$$-hardness, I would expect to be able to reduce QBF to the problem of checking whether a structure $$G$$ (thought of as a graph) satisfies some MSO formula. It is stated earlier in the book that MSO formulas correspond to NFAs and one can convert NFAs to trees. I don't see, though, why this process would necessarily be bounded by polynomial time - which we need for the $$\textsf{PSPACE}$$ reduction I believe.

(I also search online for this apparently well known result and found that this paper is often referenced as the primary source for this result. However, I cannot find this result in the paper.)

If anybody could point me in the right direction, it would be much appreciated.

• I don't know about the hardness, it's probably a QBF reduction as you mention. But for membership in PSPACE I don't think you need to store $|G|$ elements per level of quantifier. If you have, say, $\phi = \forall x~\phi'$, you can imagine an algorithm that does "for each possible value of $x$, recurse on $\phi'$ with $x$ fixed". Although the for each might iterate over many values, it only stores one $x$ at a time. So the space taken should be proportional to the depth of the recursion tree. Mar 22 at 3:40
• You are miscounting. Each nested MSO quantifier requires you to store $|G|$ bits, hence if $k$ denotes the quantifier rank of $\phi$, the total is $k\lvert G\rvert$, not $|G|^k$. Mar 22 at 6:40
• Also, PSPACE-hardness indeed follows by a trivial reduction from QBF. Just represent each Boolean quantifier by an FO quantifier, fixing two distict elements to represent the Boolean 0 and 1. Or use MSO quantifiers, representing 0 and 1 by e.g. empty and nonempty sets, respectively. Mar 22 at 7:54
• Actually, it's not clear from the question which model-checking problem you are talking about (are both the structure and the formula part of the input, or is one of them fixed?). If the structure is part of the input, the reduction is even more trivial: just make the structure $\{0,1\}$; then a quantified Boolean formula is almost literally an FO formula over the structure, without any representation of the values. Mar 22 at 8:10
• Thank you, Emil Jeřábek and Manuel Lafond, for your helpful comments. I agree, that it is not clear, which model-checking problem exactly is meant, but I understand it as both the formula and the structure are the input. I see now how I was miscounting, which solves my problem for why this problem is in PSPACE. In the book is a straight forward reduction from QBF to model-checking for FOL, which can trivially be extended to MSO. That solves the second part. Mar 23 at 11:20