Global reachability in bounded phase multi-stack pushdown systems

Abstract

Bounded phase multi-stack pushdown systems (mpds) have been studied recently. Given a set C of configurations of a mpds M, let pre* M(C, k) be the set of configurations of M from which M can reach an element of C in at most k phases. In this paper, we show that for any mpds M, any regular set C of configurations of M and any number k, the set pre*M(C, k), is regular. We use saturation like method to construct a non-deterministic finite multi-automaton recognizing pre*M(C, k). Size of the automaton constructed is double exponential in k which is optimal as the worst case complexity measure. © 2010 Springer-Verlag.