×

zbMATH — the first resource for mathematics

On Petri nets with hierarchical special arcs. (English) Zbl 1442.68122
Meyer, Roland (ed.) et al., 28th international conference on concurrency theory. CONCUR 2017, Berlin, Germany, September 5–8, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 85, Article 40, 17 p. (2017).
Summary: We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy of places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of the above four problems for all combinations of hierarchy, inhibitor, reset and transfer arcs, except the termination problem for two combinations. For both these combinations, we show that deciding termination is as hard as deciding the positivity problem on linear recurrence sequences – a long-standing open problem.
For the entire collection see [Zbl 1372.68016].
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[2] S. Akshay, S. Chakraborty, A. Das, V. Jagannath, and S. Sandeep. On Petri Nets with Hierarchical Special Arcs. \it ArXiv e-prints, July 2017. arXiv:1707.01157.
[3] Mohamed Faouzi Atig and Pierre Ganty.Approximating Petri net reachability along context-free traces. In \it IARCS Annual Conference on Foundations of Software Technol- \it ogy and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, \it India, pages 152-163, 2011. · Zbl 1246.68161
[4] Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. \it ACM Trans. Program. Lang. Syst., 34(4):16:1-16:24, December 2012. · Zbl 1325.68056
[5] Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In \it Mathematical Foundations of Computer Science 2011 - 36th International Symposium, \it MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings, pages 145-157, 2011. · Zbl 1343.68160
[6] Rémi Bonnet. Theory of well-structured transition systems and extended vector-addition systems. \it These de doctorat, ENS Cachan, France, 2013.
[7] Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-boundedness for vector addition systems with one zero-test. In \it IARCS Annual Conference on Foundations \it of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, \it 2010, Chennai, India, pages 192-203, 2010. · Zbl 1245.68131
[8] Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Model checking vector addition systems with one zero-test. \it Logical Methods in Computer Science, 8(2), 2012. · Zbl 1242.68196
[9] Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. \it Theor. \it Comput. Sci., 147(1&2):117-136, 1995. doi:10.1016/0304-3975(94)00231-7. · Zbl 0873.68146
[10] Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decid ability and undecidability. In \it Automata, Languages and Programming, 25th International \it Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, pages 103-115, 1998. doi:10.1007/BFb0055044. · Zbl 0909.68124
[11] Alain Finkel and Arnaud Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In \it SOFSEM 2010: Theory and Practice of Computer Science, 36th \it Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv \it Mlýn, Czech Republic, January 23-29, 2010. Proceedings, pages 394-406, 2010. · Zbl 1274.68230
[12] Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! \it Theor. Comput. Sci., 256(1-2):63-92, 2001. · Zbl 0973.68170
[13] Michel Hack. The recursive equivalence of the reachability problem and the liveness problem for Petri nets and vector addition systems. In \it 15th Annual Symposium on Switching and \it Automata Theory, New Orleans, Louisiana, USA, October 14-16, 1974, pages 156-164, 1974. doi:10.1109/SWAT.1974.28.
[14] S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary ver sion). In \it Proceedings of the Fourteenth Annual ACM Symposium on Theory of Comput- \it ing, STOC ’82, pages 267-281, New York, NY, USA, 1982. ACM. doi:10.1145/800070. 802201.
[15] Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In \it Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012, pages 214- 228, 2012. URL: http://www.easychair.org/publications/?page=1673703727.
[16] Ernst W. Mayr. An algorithm for the general Petri net reachability problem. \it SIAM J. \it Comput., 13(3):441-460, 1984. doi:10.1137/0213029. · Zbl 0563.68057
[17] Marvin L Minsky. \it Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. · Zbl 0195.02402
[18] Tadao Murata. Petri nets: Properties, analysis and applications. \it Proceedings of the IEEE, 77(4):541-580, 1989.
[19] Joël Ouaknine and James Worrell. Positivity problems for low-order linear recurrence se quences. In \it Proceedings of the Twenty-fifth Annual ACM-SIAM Symposium on Discrete
[20] Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. \it SIGLOG News, 2(2):4-13, 2015. doi:10.1145/2766189.2766191.
[21] Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. \it Electr. Notes Theor. \it Comput. Sci., 223:239-264, 2008. doi:10.1016/j.entcs.2008.12.042. · Zbl 1337.68191
[22] :17 \it Algorithms, SODA ’14, pages 366-379, Philadelphia, PA, USA, 2014. Society for Indus trial and Applied Mathematics. URL: http://dl.acm.org/citation.cfm?id=2634074. 2634101.
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.