×

zbMATH — the first resource for mathematics

On functions weakly computable by pushdown Petri nets and related systems. (English) Zbl 1427.68203
Summary: We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions \(F_\alpha\) for \(\alpha<\omega^\omega \), hence they are computationally more powerful than standard vector addition systems. On the other hand they cannot weakly compute the inverses \(F_\alpha^{-1}\) or indeed any sublinear function. The proof relies on a pumping lemma for runs of GVASes that is of independent interest.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
PDF BibTeX XML Cite
Full Text: arXiv
References:
[1] P. A. Abdulla, K. Čer¯ans, B. Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information & Computation, 160(1-2):109-127, 2000. · Zbl 1046.68567
[2] M. F. Atig and P. Ganty. Approximating Petri net reachability along context-free traces. In FSTTCS 2011, volume 13 of LIPIcs, pages 152-163. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. · Zbl 1246.68161
[3] A. Bouajjani and M. Emmi. Analysis of recursively parallel programs. In POPL 2012, pages 203-214. ACM, 2012. · Zbl 1321.68184
[4] P. Chambart and Ph. Schnoebelen. The ordinal recursive complexity of lossy channel systems. In LICS 2008, pages 205-216. IEEE, 2008. · Zbl 1160.68460
[5] W. Czerwiński, S. Lasota, R. Lazic, J. Leroux, and F. Mazowiecki. The reachability problem for Petri nets is not elementary. In STOC 2019, pages 24-33. ACM, 2019.
[6] S. Demri, D. Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. In LICS 2013, pages 33-42. IEEE, 2013. · Zbl 1366.68202
[7] S. Demri, M. Jurdziński, O. Lachish, and R. Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 79(1):23-38, 2013.
[8] A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. · Zbl 0973.68170
[9] S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas, and languages. Pacific J. Math., 16(2):285-296, 1966. · Zbl 0143.01602
[10] S. A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science, 7:311-324, 1978. · Zbl 0389.68030
[11] Ch. Haase, S. Schmitz, and Ph. Schnoebelen. The power of priority channel systems. Logical Methods in Comp. Science, 10(4:4), 2014. · Zbl 1448.68341
[12] M. Hack. The equality problem for vector addition systems is undecidable. Theoretical Computer Science, 2(1):77-95, 1976. · Zbl 0357.68038
[13] S. Haddad and D. Poitrenaud. Recursive Petri nets: Theory and application to discrete event systems. Acta Informatica, 44(7-8):463-508, 2007. · Zbl 1133.68056
[14] S. Haddad, S. Schmitz, and Ph. Schnoebelen. The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In LICS 2012, pages 355-364. IEEE, 2012. · Zbl 1362.68214
[15] P. Jančar. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science, 74(1):71-93, 1990.
[16] P. Jančar. Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theoretical Computer Science, 256(1-2):23-30, 2001. · Zbl 0974.68130
[17] M. Jantzen and R. Valk. Formal properties of Place/Transition nets. In Net Theory and Applications, volume 84 of Lect. Notes Comp. Sci., pages 165-212. Springer, 1980.
[18] J. B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc., 95(2):210-225, 1960. · Zbl 0158.27002
[19] R. Lazić. The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767, 2013.
[20] R. Lazić and P. Totzke. What makes Petri nets harder to verify: Stack or data? In Concurrency, Security, and Puzzles, volume 10160 of Lect. Notes Comp. Sci., pages 144-161. Springer, 2017. · Zbl 06852768
[21] J. Leroux, M. Praveen, and G. Sutre. Hyper-Ackermannian bounds for pushdown vector addition systems. In CSL-LICS 2014, pages 63:1-63:10. ACM, 2014. · Zbl 1392.68307
[22] J. Leroux and S. Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In LICS 2019. IEEE, 2019.
[23] J. Leroux and Ph. Schnoebelen. On functions weakly computable by Petri Nets and Vector Addition Systems. In RP 2014, volume 8762 of Lect. Notes Comp. Sci., pages 190-202. Springer, 2014. · Zbl 1448.68346
[24] J. Leroux, G. Sutre, and P. Totzke. On boundedness problems for pushdown vector addition systems. In RP 2015, volume 9328 of Lecture Notes in Computer Science, pages 101-113. Springer, 2015. · Zbl 06798770
[25] J. Leroux, G. Sutre, and P. Totzke. On the coverability problem for pushdown vector addition systems in one dimension. In ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. · Zbl 1440.68177
[26] Jérôme Leroux. Vector addition system reachability problem: a short self-contained proof. In POPL, pages 307-316. ACM, 2011. · Zbl 1284.68429
[27] E. W. Mayr and A. R. Meyer. The complexity of the finite containment problem for Petri nets. Journal of the ACM, 28(3):561-576, 1981. · Zbl 0462.68020
[28] R. Mayr. Process rewrite systems. Information and Computation, 156(1/2):264-286, 2000. · Zbl 1046.68566
[29] K. Reinhardt. Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci., 223:239- 264, 2008. · Zbl 1337.68191
[30] S. Schmitz. Complexity hierarchies beyond Elementary. ACM Trans. Computation Theory, 8(1), 2016. · Zbl 1347.68162
[31] Ph. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters, 83(5):251-261, 2002. · Zbl 1043.68016
[32] Ph. Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In MFCS 2010, volume 6281 of Lect. Notes Comp. Sci., pages 616-628. Springer, 2010. · Zbl 1287.68059
[33] K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV 2006, volume 4144 of Lect. Notes Comp. Sci., pages 300-314. Springer, 2006. · Zbl 1188.68198
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.