A multi-stack pushdown system is a natural model of concurrent programs. The basic verification problems are undecidable and a common trend is to consider under-approximations of the system behaviors to gain decidability. In this paper, we restrict the semantics such that a symbol that is pushed onto a stack s can be popped only within a given number of contexts involving s, i.e., we bound the scope (in terms of number of contexts) of matching push and pop transitions. This restriction permits runs with unboundedly many contexts even between matching push and pop transitions (for systems with at least three stacks). 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 can be captured by a finite automaton.
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1016/j.ic.2020.104588|
|Codice identificativo Scopus:||2-s2.0-85085091314|
|Titolo:||Reachability of scope-bounded multistack pushdown systems|
|Appare nelle tipologie:||1.1 Articolo in rivista|