[webpage]
[abstract]
[bibtex]
[arXiv]
Multi-pushdown
systems
are a standard model for concurrent recursive programs, but they have an undecidable reachability
problem. Therefore, there have been several proposals to underapproximate their sets of runs so
that
reachability in this underapproximation becomes decidable. One such underapproximation that covers
a
relatively high portion of runs is scope boundedness. In such a run, after each push to stack i,
the
corresponding pop operation must come within a bounded number of visits to stack i.
In this work, we generalize this approach to a large class of infinite-state systems. For this, we
consider the model of valence systems, which consist of a finite-state control and an
infinite-state
storage mechanism that is specified by a finite undirected graph. This framework captures
pushdowns,
vector addition systems, integer vector addition systems, and combinations thereof. For this
framework, we propose a notion of scope boundedness that coincides with the classical notion when
the
storage mechanism happens to be a multi-pushdown.
We show that with this notion, reachability can be decided in PSPACE for every storage mechanism
in
the framework. Moreover, we describe the full complexity landscape of this problem across all
storage
mechanisms, both in the case of (i) the scope bound being given as input and (ii) for fixed scope
bounds. Finally, we provide an almost complete description of the complexity landscape if even a
description of the storage mechanism is part of the input.
@misc{shetty2021scopebounded,
title={Scope-Bounded Reachability in Valence Systems},
author={Aneesh K. Shetty and S. Krishna and Georg Zetzsche},
year={2021},
eprint={2108.00963},
archivePrefix={arXiv},
primaryClass={cs.FL}
}