On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension

Jérôme Leroux, Grégoire Sutre, Patrick Totzke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new model called grammar-controlled vector addition systems.
Original languageEnglish
Title of host publicationAutomata, Languages, and Programming
Subtitle of host publication42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II
PublisherSpringer Berlin Heidelberg
Pages324-336
Number of pages13
ISBN (Electronic)978-3-662-47666-6
ISBN (Print)978-3-662-47665-9
DOIs
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume9135
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension'. Together they form a unique fingerprint.

Cite this