×

zbMATH — the first resource for mathematics

On selective unboundedness of VASS. (English) Zbl 1285.68094
Summary: Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, counter values, run lengths). Some of these features can be checked in exponential space by using Rackoff’s proof or its variants, combined with Savitch’s Theorem. However, the question is still open for many others, e.g., regularity detection problem and reversal-boundedness detection problem. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff’s technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place boundedness problem, reversal-boundedness detection (several variants are present in the paper), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as to obtain a polynomial-space bound when the dimension is fixed.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
FLATA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.; Jonsson, B., Verifying programs with unreliable channels, Inform. and Comput., 127, 2, 91-101, (1996) · Zbl 0856.68096
[2] Atig, M. F.; Habermehl, P., On yenʼs path logic for Petri nets, Internat. J. Found. Comput. Sci., 22, 4, 783-799, (2011) · Zbl 1230.68153
[3] Atig, M. F.; Habermehl, P., On yenʼs path logic for Petri nets, (RPʼ09, Lecture Notes in Comput. Sci., vol. 5797, (2009), Springer), 51-63 · Zbl 1260.68255
[4] Baker, B.; Book, R., Reversal-bounded multipushdown machines, J. Comput. System Sci., 8, 315-332, (1974) · Zbl 0309.68043
[5] Blockelet, M.; Schmitz, S., Model-checking coverability graphs of vector addition systems, (MFCSʼ11, Lecture Notes in Comput. Sci., vol. 6907, (2011), Springer), 108-119 · Zbl 1343.68152
[6] Bonnet, R., Decidability of LTL model checking for vector addition systems with one zero-test, (RPʼ11, Lecture Notes in Comput. Sci., vol. 6945, (2011), Springer), 85-95 · Zbl 1348.68157
[7] Bonnet, R., The reachability problem for vector addition systems with one zero-test, (MFCSʼ11, Lecture Notes in Comput. Sci., vol. 6907, (2011), Springer), 145-157 · Zbl 1343.68160
[8] Borosh, I.; Treybig, L., Bounds on positive integral solutions of linear Diophantine equations, Proc. Amer. Math. Soc., 55, 299-304, (1976) · Zbl 0291.10014
[9] Bozga, M.; Iosif, R.; Konecný, F., Fast acceleration of ultimately periodic relations, (CAVʼ10, Lecture Notes in Comput. Sci., vol. 6174, (2009), Springer), 227-242
[10] E. Cardoza, R.J. Lipton, A.R. Meyer, Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report, in: STOCʼ76, 1976, pp. 50-54. · Zbl 0374.20067
[11] Comon, H.; Jurski, Y., Multiple counters automata, safety analysis and Presburger analysis, (CAVʼ98, Lecture Notes in Comput. Sci., vol. 1427, (1998), Springer), 268-279
[12] Dang, Z.; Ibarra, O.; San Pietro, P., Liveness verification of reversal-bounded multicounter machines with a free counter, (FST&TCSʼ01, Lecture Notes in Comput. Sci., vol. 2245, (2001), Springer), 132-143 · Zbl 1053.03021
[13] Demri, S., On selective unboundedness of VASS, (Proceedings of the 12th International Workshop on Verification of Infinite State Systems (INFINITYʼ10), Electron. Proc. Theor. Comput. Sci., vol. 39, (2010)), 1-15
[14] Demri, S., Slides on EXPSPACE-hard problems on VASS, (September 2010), available on
[15] Demri, S.; Dhar, A. K.; Sangnier, A., Taming past LTL and flat counter systems, (IJCARʼ12, Lecture Notes in Artificial Intelligence, vol. 7364, (2012), Springer), 179-193 · Zbl 1358.68186
[16] Dufourd, C.; Finkel, A.; Schnoebelen, Ph., Reset nets between decidability and undecidability, (ICALPʼ98, Lecture Notes in Comput. Sci., vol. 1443, (1998), Springer), 103-115 · Zbl 0909.68124
[17] Dufourd, C.; Jančar, P.; Schnoebelen, Ph., Boundedness of reset P/T nets, (ICALPʼ99, Lecture Notes in Comput. Sci., vol. 1644, (1999), Springer), 301-310 · Zbl 0943.68122
[18] Esparza, J., Decidability and complexity of Petri net problems — an introduction, (Advances in Petri Nets 1998, Lecture Notes in Comput. Sci., vol. 1491, (1998), Springer Berlin), 374-428 · Zbl 0926.68087
[19] Finkel, A., Reduction and covering of infinite reachability trees, Inform. and Comput., 89, 2, 144-179, (1990) · Zbl 0753.68073
[20] Finkel, A.; Sangnier, A., Reversal-bounded counter machines revisited, (MFCSʼ08, Lecture Notes in Comput. Sci., vol. 5162, (2008), Springer), 323-334 · Zbl 1173.68562
[21] Finkel, A.; Sangnier, A., Mixing coverability and reachability to analyze VASS with one zero-test, (SOFSEMʼ10, Lecture Notes in Comput. Sci., vol. 5901, (2010), Springer), 394-406 · Zbl 1274.68230
[22] Finkel, A.; Schnoebelen, Ph., Well-structured transitions systems everywhere!, Theoret. Comput. Sci., 256, 1-2, 63-92, (2001) · Zbl 0973.68170
[23] E. Gurari, O. Ibarra, An NP-complete number-theoretic problem, in: STOCʼ78, 1978, pp. 205-215. · Zbl 1282.68138
[24] Habermehl, P., On the complexity of the linear-time mu-calculus for Petri nets, (ICATPNʼ97, Lecture Notes in Comput. Sci., vol. 1248, (1997), Springer), 102-116
[25] D. Hauschildt, Semilinearity of the reachability set is decidable for Petri nets, PhD thesis, University of Hamburg, 1990.
[26] Hopcroft, J.; Pansiot, J. J., On the reachability problem for 5-dimensional vector addition systems, Theoret. Comput. Sci., 8, 135-159, (1979) · Zbl 0466.68048
[27] Howell, R.; Rosier, L., An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines, J. Comput. System Sci., 34, 1, 55-74, (1987) · Zbl 0629.68054
[28] Ibarra, O., Reversal-bounded multicounter machines and their decision problems, J. ACM, 25, 1, 116-133, (1978) · Zbl 0365.68059
[29] Ibarra, O.; Su, J.; Dang, Z.; Bultan, T.; Kemmerer, R., Counter machines and verification problems, Theoret. Comput. Sci., 289, 1, 165-189, (2002) · Zbl 1061.68095
[30] Jantzen, M., Complexity of place/transition nets, (Advances in Petri Nets 1986, Lecture Notes in Comput. Sci., vol. 254, (1987), Springer), 413-434
[31] Karp, R. M.; Miller, R. E., Parallel program schemata, J. Comput. System Sci., 3, 2, 147-195, (1969) · Zbl 0198.32603
[32] Kopczynski, E.; To, A., Parikh images of grammars: complexity and applications, (LICSʼ10, (2010), IEEE), 80-89
[33] R. Kosaraju, Decidability of reachability in vector addition systems, in: STOCʼ82, 1982, pp. 267-281.
[34] Lambert, J. L., A structure to decide reachability in Petri nets, Theoret. Comput. Sci., 99, 79-104, (1992) · Zbl 0769.68104
[35] J.L. Lambert, Vector addition systems and semi-linearity, manuscript, 1994.
[36] J. Leroux, Vector addition system reachability problem (a short self-contained proof), in: POPLʼ11, 2011, pp. 307-316. · Zbl 1284.68429
[37] R.J. Lipton, The reachability problem requires exponential space, Technical Report 62, Department of Computer Science, Yale University, 1976.
[38] Mayr, E. W., An algorithm for the general Petri net reachability problem, SIAM J. Comput., 13, 3, 441-460, (1984) · Zbl 0563.68057
[39] Minsky, M., Computation, finite and infinite machines, (1967), Prentice Hall · Zbl 0195.02402
[40] Parikh, R., On context-free languages, J. ACM, 13, 4, 570-581, (1966) · Zbl 0154.25801
[41] Perrin, D.; Pin, J.-E., Infinite words: automata, semigroups, logic and games, (2004), Elsevier · Zbl 1094.68052
[42] Praveen, M., Small vertex cover makes Petri net coverability and boundedness easier, (IPECʼ10, Lecture Notes in Comput. Sci., vol. 6478, (2010), Springer), 216-227 · Zbl 1253.68250
[43] Praveen, M.; Lodaya, K., Modelchecking counting properties of 1-safe nets with buffers in parapspace, (FST&TCSʼ09, (2009), LZI), 347-358 · Zbl 1248.68356
[44] M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, in: Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, 1929, pp. 92-101.
[45] Rackoff, C., The covering and boundedness problems for vector addition systems, Theoret. Comput. Sci., 6, 2, 223-231, (1978) · Zbl 0368.68054
[46] (Reisig, W.; Rozenberg, G., Lectures on Petri Nets I: Basic Models, Lecture Notes in Comput. Sci., vol. 1491, (1998), Springer) · Zbl 0903.00072
[47] Reutenauer, C., The mathematics of Petri nets, (1990), Masson and Prentice · Zbl 0694.68007
[48] Rosier, L.; Yen, H.-C., A multiparameter analysis of the boundedness problem for vector addition systems, J. Comput. System Sci., 32, 105-135, (1986) · Zbl 0614.68048
[49] A. Sangnier, Vérification de systèmes avec compteurs et pointeurs, Thèse de doctorat, LSV, ENS Cachan, France, 2008.
[50] Savitch, W. J., Relationships between nondeterministic and deterministic tape complexities, J. Comput. System Sci., 4, 2, 177-192, (1970) · Zbl 0188.33502
[51] Valk, R.; Jantzen, M., The residue of vector sets with applications to decidability problems in Petri nets, Acta Inform., 21, 643-674, (1985) · Zbl 0545.68051
[52] Valk, R.; Vidal-Naquet, G., Petri nets and regular languages, J. Comput. System Sci., 23, 299-325, (1981) · Zbl 0473.68057
[53] van Emde Boas, P., Machine models and simulations, (Handbook of Theoretical Computer Science, vol. A, Algorithms and Complexity, (1990), Elsevier), 2-66 · Zbl 0900.68265
[54] Yen, H.-C., A unified approach for deciding the existence of certain net paths, Inform. and Comput., 96, 119-137, (1992) · Zbl 0753.68078
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.