Model Checking Concurrent Recursive Programs Using Temporal Logics

We consider two bounded versions of the model checking problem of a fixed temporal logic 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 A, a temporal formula F from TL, and a bound k, whether all nested words nu which are accepted by 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 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.