Document Open Access Logo

Petri Net Reachability Problem (Invited Talk)

Author Jérôme Leroux

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.5.pdf
  • Filesize: 252 kB
  • 3 pages

Document Identifiers

Author Details

Jérôme Leroux
  • Univ.Bordeaux, CNRS, Bordeaux-INP, France

Funding

  • Leroux, Jérôme: The author was supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).

Cite AsGet BibTex

Jérôme Leroux. Petri Net Reachability Problem (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.MFCS.2019.5

Abstract

Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation
Keywords
  • Petri net
  • Reachability problem
  • Formal verification
  • Concurrency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  2. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In Moses Charikar and Edith Cohen, editors, Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019., pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  3. Stéphane Demri. On selective unboundedness of VASS. J. Comput. Syst. Sci., 79(5):689-713, 2013. URL: https://doi.org/10.1016/j.jcss.2013.01.014.
  4. Matthias Englert, Ranko Lazic, and Patrick Totzke. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 477-484. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933577.
  5. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  6. Richard M. Karp and Raymond E. Miller. Parallel Program Schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  7. S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems (Preliminary Version). In STOC, pages 267-281. ACM, 1982. URL: https://doi.org/10.1145/800070.802201.
  8. Jean-Luc Lambert. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  9. Jérôme Leroux. Vector Addition Systems Reachability Problem (A Simpler Solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. Google Scholar
  10. Jérôme Leroux and Sylvain Schmitz. Demystifying Reachability in Vector Addition Systems. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 56-67. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.16.
  11. Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. CoRR, abs/1903.08575, 2019. To appear at LICS'19. URL: http://arxiv.org/abs/1903.08575.
  12. Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_26.
  13. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University, 1976. URL: http://cpsc.yale.edu/sites/default/files/files/tr63.pdf.
  14. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC, pages 238-246. ACM, 1981. URL: https://doi.org/10.1145/800076.802477.
  15. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  16. Ernst W. Mayr and Albert R. Meyer. The Complexity of the Finite Containment Problem for Petri Nets. J. ACM, 28(3):561-576, 1981. URL: https://doi.org/10.1145/322261.322271.
  17. Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact