2015/07/27 by Jérôme Leroux, Leroux, Jérôme, Grégoire Sutre +3
Biochemistry, Genetics and Molecular Biology · Computer Science · #DNA and Biological Computing #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #cs.FL #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1507.07362
arxiv created 2015/07/27 · openalex publication_date 2015/07/27 · arxiv updated 2015/07/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability set for this model can be refined into two decision problems that ask if infinitely many counter values or stack configurations are reachable, respectively. Counter boundedness seems to be the more intricate problem. We show decidability in exponential time for one-dimensional systems. The proof is via a small witness property derived from an analysis of derivation trees of grammar-controlled vector addition systems.