Advertisement
Published in:
2011 | OriginalPaper | Chapter
Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
Authors : Salvatore La Torre, Margherita Napoli
Published in: CONCUR 2011 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
A multi-stack pushdown system is a natural model of concurrent programs. The basic verification problems are in general undecidable (two stacks suffice to encode a Turing machine), and in the last years, there have been some successful approaches based on under-approximating the system behaviors. In this paper, we propose a restriction of the semantics of the general model such that a symbol that is pushed onto a stack can be popped only within a bounded number of context-switches. Note that, we allow runs to be formed of unboundedly many execution contexts, we just bound the scope (in terms of number of contexts) of matching push and pop transitions. We call the resulting model a
multi-stack pushdown system with scope-bounded matching relations
(
SMpds
). We show that the configuration reachability and the location reachability problems for
SMpds
are both
Pspace
-complete, and that the set of the reachable configurations is regular, in the sense that there exists a multi-tape finite automaton that accepts it.