In this note, we provide complexity characterizations of model checking multi-pushdown systems. Multi-pushdown systems model re- cursive concurrent programs in which any sequential process has a fi- nite control. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formal- ism is a linear-time temporal logic extending well-known logic CaRet but dedicated to multi-pushdown systems in which abstract operators (re- lated to calls and returns) such as those for next-time and until are pa- rameterized 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 k is given as an input (whence it is not a constant of the model-checking problem), which makes a substantial difference in the complexity. In certain cases, our results improve previous complexity results.
['Kshitij Bansal', 'Stéphane Demri']
A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems