Abstract
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.
This work was partially supported by ANR project ReacHard (ANR-11-BS02-001).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Atig, M.F., Ganty, P.: Approximating Petri net reachability along context-free traces. In: FSTTCS, pp. 152–163 (2011)
Blondin, M., Finkel, A., Göller, S., Haase, C., McKenzie, P.: Reachability in two-dimensional vector addition systems with states is PSPACE-complete. In: LICS (2015, to appear)
Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. TCS 295, 85–106 (2003)
Courtois, J.-B., Schmitz, S.: Alternating vector addition systems with states. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 220–231. Springer, Heidelberg (2014)
Demri, S., Jurdzinski, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. JCSS 79(1), 23–38 (2013)
Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Progr. Lang. Syst. 34(1), 6:1–6:48 (2012)
Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas and languages. Pacific J. Math. 16(2), 285–296 (1966)
Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC, pp. 267–281 (1982)
Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary (2013). CoRR abs/1310.1767
Lazic, R., Schmitz, S.: Non-elementary complexities for branching VASS, MELL, and extensions. In: CSL/LICS (2014)
Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: POPL, pp. 307–316 (2011)
Leroux, J., Praveen, M., Sutre, G.: Hyper-ackermannian bounds for pushdown vector addition systems. In: CSL/LICS (2014)
Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 402–416. Springer, Heidelberg (2004)
Leroux, J., Sutre, G., Totzke, P.: On the coverability problem for pushdown vector addition systems in one dimension. CoRR abs/1503.04018, April 2015. http://arxiv.org/abs/http://arxiv.org/abs/1503.04018
Lipton, R.J.: The reachability problem requires exponential space. Tech. Rep. 63, Yale University, January 1976
Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: STOC, pp. 238–246 (1981)
Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS 6(2), 223–231 (1978)
Reinhardt, K.: Reachability in Petri nets with inhibitor arcs. ENTCS 223, 239–264 (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leroux, J., Sutre, G., Totzke, P. (2015). On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-662-47666-6_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47665-9
Online ISBN: 978-3-662-47666-6
eBook Packages: Computer ScienceComputer Science (R0)