Document Open Access Logo

The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets

Authors Petr Jančar , Jérôme Leroux

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.36.pdf
  • Filesize: 0.77 MB
  • 17 pages

Document Identifiers

Author Details

Petr Jančar
  • Dept of Comp. Sci., Faculty of Science, Palacký University Olomouc, Czech Republic
Jérôme Leroux
  • LaBRI, CNRS, Univ. Bordeaux, France

Funding

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

Cite AsGet BibTex

Petr Jančar and Jérôme Leroux. The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.36

Abstract

A set of configurations H is a home-space for a set of configurations X of a Petri net if every configuration reachable from (any configuration in) X can reach (some configuration in) H. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations X, H, if H is a home-space for X. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when X is a singleton and H is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any linear set of configurations L we can effectively compute a semilinear set C of configurations, called a non-reachability core for L, such that for every set X the set L is not a home-space for X if, and only if, C is reachable from X. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Petri nets
  • home-space property
  • semilinear sets
  • Ackermannian complexity

Metrics

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

References

  1. Henry G. Baker, Jr. Rabin’s proof of the undecidability of the reachability set inclusion problem of vector addition systems. Technical Report Computation Structures Group Memo 79, Massachusetts Institute of Technology, Project MAC, July 1973. Google Scholar
  2. Eike Best and Javier Esparza. Existence of home states in Petri nets is decidable. Inf. Process. Lett., 116(6):423-427, 2016. URL: https://doi.org/10.1016/j.ipl.2016.01.011.
  3. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  4. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  5. David de Frutos Escrig and Colette Johnen. Decidability of home space property. Technical Report LRI-503, Univ. de Paris-Sud, Centre d'Orsay, Laboratoire de Recherche en Informatique, July 1989. Google Scholar
  6. Javier Esparza and Mogens Nielsen. Decidability issues for Petri nets - A survey. Bulletin of the European Association for Theoretical Computer Science, 52:245-262, 1994. Google Scholar
  7. Seymour Ginsburg and Edwin H. Spanier. Bounded Algol-like languages. Transactions of the American Mathematical Society, 113(2):333-368, 1964. URL: https://doi.org/10.2307/1994067.
  8. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL: https://doi.org/10.2140/pjm.1966.16.285.
  9. Michel Hack. Decidability questions for Petri nets. PhD thesis, MIT, 1975. URL: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-161.pdf.
  10. Michel Hack. The equality problem for vector addition systems is undecidable. Theor. Comput. Sci., 2(1):77-95, 1976. URL: https://doi.org/10.1016/0304-3975(76)90008-6.
  11. Petr Jančar. Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci., 148(2):281-301, 1995. URL: https://doi.org/10.1016/0304-3975(95)00037-W.
  12. Slawomir Lasota. Improved Ackermannian lower bound for the Petri nets reachability problem. In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference), volume 219 of LIPIcs, pages 46:1-46:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.STACS.2022.46.
  13. Jérôme Leroux. Vector addition systems reachability problem (A simpler solution). In Andrei Voronkov, editor, Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. URL: https://doi.org/10.29007/bnx2.
  14. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  15. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  16. 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.
  17. 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.
  18. Sylvain Schmitz. Complexity hierarchies beyond elementary. TOCT, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  19. Sylvain Schmitz. The complexity of reachability in vector addition systems. SIGLOG News, 3(1):4-21, 2016. URL: https://dl.acm.org/citation.cfm?id=2893585.
  20. Rüdiger Valk and Matthias Jantzen. The residue of vector sets with applications to decidability problems in Petri nets. In Grzegorz Rozenberg, Hartmann J. Genrich, and Gérard Roucairol, editors, Advances in Petri Nets 1984, volume 188 of Lecture Notes in Computer Science, pages 234-258. Springer, 1984. URL: https://doi.org/10.1007/3-540-15204-0_14.
  21. Hsu-Chun Yen and Chien-Liang Chen. On minimal elements of upward-closed sets. Theor. Comput. Sci., 410(24-25):2442-2452, 2009. URL: https://doi.org/10.1016/j.tcs.2009.02.036.
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