Multi-pushdown systems with budgets
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman · 2012
Abstract. We address the verification problem for concurrent programs modeled as multi-pushdown automata (MPDA). In general, they are Turing powerful and hence come along with undecidability of basic de-cision problems [15]. Therefore, several subclasses of MPDA have been proposed and studied in the literature [3, 13, 9, 2, 11]. In this paper, we mainly propose the class of bounded-budget MPDA where we restrict multi-pushdown automata, in the sense that each stack can perform a fi-nite number of consecutive contexts without its size goes strictly below a given bound on that stack. We show that the reachability problem for this sub-class is Pspace-complete. Furthermore, we propose a code-to-code translation that takes as input a concurrent program P and produces a sequential program P ′ such that, running P under the bounded-budget restriction yields the same set of reachable states as running P ′. We implement our analysis by a systematic code-to-code translation from multithreaded programs to sequential programs. By leveraging standard sequential analysis tools, we applied a prototype implementation on a set of benchmarks in order to show that our translation scheme is feasible. 1