<p>I am currently reading &quot;Parameterized Complexity Theory&quot; by J. Flum and M. Grohe. In Chapter 10.3 they state in the first paragraph:</p>
<blockquote>
<p>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 <span class="math-container">$\textsf{PSPACE}$</span>-complete.</p>
</blockquote>
<p>Unfortunately they do not seem to formally establish this result anywhere in the book.</p>
<p>The straight forward algorithm that I think of would simply brute force check whether for a given structure <span class="math-container">$G$</span> an MSO formula <span class="math-container">$\phi$</span> 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 <span class="math-container">$|G|$</span> elements for each nesting level of quantifiers in <span class="math-container">$\phi$</span>. That means that we might need to store <span class="math-container">${|G|}^k$</span> elements, where <span class="math-container">$k$</span> depends on (the quantifier nesting depth) of <span class="math-container">$\phi$</span>. But then the space required is exponential and not polynomial. Where am I going wrong here?</p>
<p>Regarding <span class="math-container">$\textsf{PSPACE}$</span>-hardness, I would expect to be able to reduce QBF to the problem of checking whether a structure <span class="math-container">$G$</span> (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 <span class="math-container">$\textsf{PSPACE}$</span> reduction I believe.</p>
<p>(I also search online for this apparently well known result and found that <a href="https://dl.acm.org/doi/10.1145/800070.802186" rel="nofollow noreferrer">this paper</a> is often referenced as the primary source for this result. However, I cannot find this result in the paper.)</p>
<p>If anybody could point me in the right direction, it would be much appreciated.</p>

CC BY-SA 4.0
2024-03-22T03:40:00.913Z
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.
Manuel Lafond
CC BY-SA 4.0
2024-03-22T06:40:12.093Z
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$.
Emil Jeřábek
CC BY-SA 4.0
2024-03-22T07:54:16.730Z
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.
Emil Jeřábek
CC BY-SA 4.0
2024-03-22T08:10:58.083Z
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.
Emil Jeřábek
CC BY-SA 4.0
2024-03-23T11:20:24.110Z
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.
user11718766
<cc.complexity-theory><lo.logic><reductions><model-checking><pspace>
Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?
user11718766
# Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?

(Asked by: username_0 on 2024-03-22)

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](https://dl.acm.org/doi/10.1145/800070.802186) 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.

**Tags:** cc.complexity-theory, lo.logic, reductions, model-checking, pspace

> **Comments:**
> **username_1**: 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.  
> **username_2**: 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$.  
> **username_2**: 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.  
> **username_2**: 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.  
> **username_0**: Thank you, username_2 and username_1, 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.  

---

## 0 answers

