Document Open Access Logo

Bi-Reachability in Petri Nets with Data

Authors Łukasz Kamiński , Sławomir Lasota

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.31.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Author Details

Łukasz Kamiński
  • University of Warsaw, Poland
Sławomir Lasota
  • University of Warsaw, Poland

Funding

  • Kamiński, Łukasz: Partially supported by NCN grant 2021/41/B/ST6/00535.
  • Lasota, Sławomir: Partially supported by the ERC grant INFSYS, agreement no. 950398.

Acknowledgements

We are grateful to Piotrek Hofman for inspiring discussions.

Cite AsGet BibTex

Łukasz Kamiński and Sławomir Lasota. Bi-Reachability in Petri Nets with Data. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.31

Abstract

We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
Keywords
  • Petri nets
  • Petri nets with data
  • reachability
  • bi-reachability
  • reversible reachability
  • mutual reachability
  • orbit-finite sets

Metrics

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

References

  1. Michael Blondin and Franccois Ladouceur. Population protocols with unordered data. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, Proc. ICALP 2023, volume 261 of LIPIcs, pages 115:1-115:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.115.
  2. Mikołaj Bojańczyk. Slightly infinite sets, 2019. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  3. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, 10(3:4):paper 4, 2014. Google Scholar
  4. Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota, and Szymon Toruńczyk. Turing machines with atoms. In LICS, pages 183-192, 2013. Google Scholar
  5. Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln, John C. Mitchell, and Andre Scedrov. A meta-notation for protocol analysis. In Proc. CSFW 1999, pages 55-69. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/CSFW.1999.779762.
  6. Iliano Cervesato, Nancy A. Durgin, Patrick Lincoln, John C. Mitchell, and Andre Scedrov. A meta-notation for protocol analysis. In Proc. CSFW 1999, pages 55-69, 1999. Google Scholar
  7. Giorgio Delzanno. An overview of MSR(C): A CLP-based framework for the symbolic verification of parameterized concurrent systems. Electr. Notes Theor. Comput. Sci., 76:65-82, 2002. Google Scholar
  8. Giorgio Delzanno. Constraint multiset rewriting. Technical Report DISI-TR-05-08, DISI, Universitá di Genova, 2005. Google Scholar
  9. Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Proc. ICALP 2017, volume 80 of LIPIcs, pages 119:1-119:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.119.
  10. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: completions. In Susanne Albers and Jean-Yves Marion, editors, Proc. STACS 2009, volume 3 of LIPIcs, pages 433-444. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009. Google Scholar
  11. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part II: complete WSTS. Log. Methods Comput. Sci., 8(3), 2012. Google Scholar
  12. Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in bidirected pushdown VASS. In Proc. ICALP 2022, volume 229 of LIPIcs, pages 124:1-124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  13. Hartmann J. Genrich and Kurt Lautenbach. System modelling with high-level Petri nets. Theor. Comput. Sci., 13:109-136, 1981. Google Scholar
  14. A. Ghosh, P. Hofman, and S. Lasota. Orbit-finite linear programming. In Proc. LICS 2023, pages 1-14, 2023. Google Scholar
  15. Arka Ghosh and Slawomir Lasota. Equivariant ideals of polynomials. In Proc. LICS 2024, pages 38:1-38:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662074.
  16. Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke. Coverability trees for petri nets with unordered data. In Bart Jacobs and Christof Löding, editors, Proc. FOSSACS 2016, volume 9634 of Lecture Notes in Computer Science, pages 445-461. Springer, 2016. Google Scholar
  17. Kurt Jensen. Coloured Petri nets and the invariant-method. Theor. Comput. Sci., 14:317-336, 1981. Google Scholar
  18. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary version). In Proc. STOC 1982, pages 267-281, 1982. Google Scholar
  19. Jean-Luc Lambert. A structure to decide reachability in Petri nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  20. Slawomir Lasota. Decidability border for Petri nets with data: WQO dichotomy conjecture. In Proc. Petri Nets 2016, volume 9698 of Lecture Notes in Computer Science, pages 20-36. Springer, 2016. Google Scholar
  21. Slawomir Lasota. VASS reachability in three steps. CoRR, abs/1812.11966, 2018. URL: https://arxiv.org/abs/1812.11966.
  22. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. In Proc. ICATPN 2007, volume 4546 of Lecture Notes in Computer Science, pages 301-320. Springer, 2007. Google Scholar
  23. Ranko Lazic and Patrick Totzke. What makes Petri nets harder to verify: stack or data? In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, volume 10160 of Lecture Notes in Computer Science, pages 144-161. Springer, 2017. Google Scholar
  24. Jérôme Leroux. Vector addition system reversible reachability problem. Log. Methods Comput. Sci., 9(1), 2013. Google Scholar
  25. Jérôme Leroux and Sylvain Schmitz. Demystifying reachability in vector addition systems. In Proc. LICS 2015, pages 56-67. IEEE Computer Society, 2015. Google Scholar
  26. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Proc. LICS 2019, pages 1-13. IEEE, 2019. Google Scholar
  27. Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proc. STOC 1981, pages 238-246, 1981. Google Scholar
  28. Fernando Rosa-Velardo and David de Frutos-Escrig. Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci., 412(34):4439-4451, 2011. Google Scholar
  29. Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS. Discret. Math. Theor. Comput. Sci., 7(1):217-230, 2005. URL: https://doi.org/10.46298/DMTCS.350.
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