Summary: We consider two bounded versions of the model checking problem of a fixed temporal logic \(\mathrm{TL}\) whose modalities are MSO-definable and which is specifying properties of multiply nested words, i.e., of runs of pushdown automata with multiple stacks. One of the problems asks, given a multi-stack system \(\mathcal{A}\), a temporal formula \(F\) from \(\mathrm{TL}\), and a bound \(k\), whether all nested words \(\nu \) which are accepted by \(\mathcal{A}\) and whose split-width is bounded by \(k\) satisfy \(F\). We describe the connection between the complexity of this problem and the maximal number \(n\) of monadic quantifier alternations in the definitions of the modalities of \(\mathrm{TL}\). In fact, we present almost tight upper and lower bounds for every natural number \(n\). Regarding the other model checking problem considered, we require \(\nu \) to be a \(k\)-scope nested word. In this case, we can infer the same lower and upper bounds.
For the entire collection see [Zbl 1294.68016].