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.
Reachability of scope-bounded multistack pushdown systems
La Torre S.;Napoli M.;Parlato G.
2020-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.