×

On the coverability problem for pushdown vector addition systems in one dimension. (English) Zbl 1440.68177

Halldórsson, Magnús M. (ed.) et al., Automata, languages, and programming. 42nd international colloquium, ICALP 2015, Kyoto, Japan, July 6–10, 2015. Proceedings. Part II. Berlin: Springer. Lect. Notes Comput. Sci. 9135, 324-336 (2015).
Summary: 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.
For the entire collection see [Zbl 1316.68013].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Atig, M.F., Ganty, P.: Approximating Petri net reachability along context-free traces. In: FSTTCS, pp. 152-163 (2011) · Zbl 1246.68161
[2] 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) · Zbl 1401.68095
[3] Bouajjani, A.; Habermehl, P.; Mayr, R., Automatic verification of recursive procedures with one integer parameter, TCS, 295, 85-106 (2003) · Zbl 1053.68060 · doi:10.1016/S0304-3975(02)00397-3
[4] Courtois, J-B; Schmitz, S.; Csuhaj-Varjú, E.; Dietzfelbinger, M.; Ésik, Z., Alternating vector addition systems with states, Mathematical Foundations of Computer Science 2014, 220-231 (2014), Heidelberg: Springer, Heidelberg · Zbl 1425.68290
[5] Demri, S.; Jurdzinski, M.; Lachish, O.; Lazic, R., The covering and boundedness problems for branching vector addition systems, JCSS, 79, 1, 23-38 (2013) · Zbl 1260.68264
[6] Ganty, P.; Majumdar, R., Algorithmic verification of asynchronous programs, ACM Trans. Progr. Lang. Syst., 34, 1, 6:1-6:48 (2012) · doi:10.1145/2160910.2160915
[7] Ginsburg, S.; Spanier, EH, Semigroups, Presburger formulas and languages, Pacific J. Math., 16, 2, 285-296 (1966) · Zbl 0143.01602 · doi:10.2140/pjm.1966.16.285
[8] Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC, pp. 267-281 (1982)
[9] Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary (2013). CoRR abs/1310.1767
[10] Lazic, R., Schmitz, S.: Non-elementary complexities for branching VASS, MELL, and extensions. In: CSL/LICS (2014) · Zbl 1394.68189
[11] Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: POPL, pp. 307-316 (2011) · Zbl 1284.68429
[12] Leroux, J., Praveen, M., Sutre, G.: Hyper-ackermannian bounds for pushdown vector addition systems. In: CSL/LICS (2014) · Zbl 1392.68307
[13] Leroux, J.; Sutre, G.; Gardner, P.; Yoshida, N., On flatness for 2-dimensional vector addition systems with states, CONCUR 2004 - Concurrency Theory, 402-416 (2004), Heidelberg: Springer, Heidelberg · Zbl 1099.68071 · doi:10.1007/978-3-540-28644-8_26
[14] 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 · Zbl 1440.68177
[15] Lipton, R.J.: The reachability problem requires exponential space. Tech. Rep. 63, Yale University, January 1976
[16] Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: STOC, pp. 238-246 (1981)
[17] Rackoff, C., The covering and boundedness problems for vector addition systems, TCS, 6, 2, 223-231 (1978) · Zbl 0368.68054 · doi:10.1016/0304-3975(78)90036-1
[18] Reinhardt, K., Reachability in Petri nets with inhibitor arcs, ENTCS, 223, 239-264 (2008) · Zbl 1337.68191
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.