LIPIcs.CONCUR.2017.40.pdf
- Filesize: 0.59 MB
- 17 pages
Document
On Petri Nets with Hierarchical Special Arcs
Authors
-
Part of:
Volume:
28th International Conference on Concurrency Theory (CONCUR 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-09-01
Cite As Get BibTex
S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath, and Sai Sandeep. On Petri Nets with Hierarchical Special Arcs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.40
Abstract
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.
Subject Classification
Keywords
- Petri Nets
- Hierarchy
- Reachability
- Coverability
- Termination
- Positivity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- S. Akshay, S. Chakraborty, A. Das, V. Jagannath, and S. Sandeep. On Petri Nets with Hierarchical Special Arcs. ArXiv e-prints, July 2017. URL: http://arxiv.org/abs/1707.01157.
-
Mohamed Faouzi Atig and Pierre Ganty. Approximating Petri net reachability along context-free traces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, pages 152-163, 2011.
-
Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4):16:1-16:24, December 2012.
-
Rémi Bonnet. The reachability problem for vector addition system with one zero-test. In Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings, pages 145-157, 2011.
-
Rémi Bonnet. Theory of well-structured transition systems and extended vector-addition systems. These de doctorat, ENS Cachan, France, 2013.
-
Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Place-boundedness for vector addition systems with one zero-test. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, pages 192-203, 2010.
-
Rémi Bonnet, Alain Finkel, Jérôme Leroux, and Marc Zeitoun. Model checking vector addition systems with one zero-test. Logical Methods in Computer Science, 8(2), 2012.
- Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theor. Comput. Sci., 147(1&2):117-136, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00231-7.
- Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13-17, 1998, Proceedings, pages 103-115, 1998. URL: http://dx.doi.org/10.1007/BFb0055044.
-
Alain Finkel and Arnaud Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In SOFSEM 2010: Theory and Practice of Computer Science, 36th Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlýn, Czech Republic, January 23-29, 2010. Proceedings, pages 394-406, 2010.
-
Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001.
- Michel Hack. The recursive equivalence of the reachability problem and the liveness problem for Petri nets and vector addition systems. In 15th Annual Symposium on Switching and Automata Theory, New Orleans, Louisiana, USA, October 14-16, 1974, pages 156-164, 1974. URL: http://dx.doi.org/10.1109/SWAT.1974.28.
- S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC '82, pages 267-281, New York, NY, USA, 1982. ACM. URL: http://dx.doi.org/10.1145/800070.802201.
- Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012, pages 214-228, 2012. URL: http://www.easychair.org/publications/?page=1673703727.
- Ernst W. Mayr. An algorithm for the general Petri net reachability problem. SIAM J. Comput., 13(3):441-460, 1984. URL: http://dx.doi.org/10.1137/0213029.
-
Marvin L Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967.
-
Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989.
- Joël Ouaknine and James Worrell. Positivity problems for low-order linear recurrence sequences. In Proceedings of the Twenty-fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '14, pages 366-379, Philadelphia, PA, USA, 2014. Society for Industrial and Applied Mathematics. URL: http://dl.acm.org/citation.cfm?id=2634074.2634101.
- Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. SIGLOG News, 2(2):4-13, 2015. URL: http://dx.doi.org/10.1145/2766189.2766191.
- Klaus Reinhardt. Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci., 223:239-264, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.042.