Model-Checking Bounded Multi-Pushdown Systems

Overview & Synopsis

We provide complexity characterizations of model checking multi-pushdown systems. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formalism is a linear-time temporal logic extending well-known logic CaRet but dedicated to multi-pushdown systems in which abstract operators are parameterized by stacks. We show that the problem is ExpTime-complete for context-bounded runs and unary encoding of the number of context switches; we also prove that the problem is 2ExpTime-complete for phase-bounded runs and unary encoding of the number of phase switches. In both cases, the value kis given as an input, which makes a substantial difference in the complexity.