Document Open Access Logo

Distance Between Mutually Reachable Petri Net Configurations

Author Jérôme Leroux

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.47.pdf
  • Filesize: 477 kB
  • 14 pages

Document Identifiers

Author Details

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

Funding

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

Cite As Get BibTex

Jérôme Leroux. Distance Between Mutually Reachable Petri Net Configurations. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 47:1-47:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.47

Abstract

Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. In 2011, we proved that a variant of the reachability problem, called the reversible reachability problem is exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. In this paper we revisit the reversible reachability problem in order to prove that the minimal distance in the reachability graph of two mutually reachable configurations is linear with respect to the Euclidean distance between those two configurations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Petri nets
  • Vector addition systems
  • Formal verification
  • Reachability problem

Metrics

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

Related Versions

References

  1. Gérard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. Symbolic Counter Abstraction for Concurrent Software. In CAV, volume 5643 of Lecture Notes in Computer Science, pages 64-78. Springer, 2009. 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. Google Scholar
  3. Michael Blondin, Javier Esparza, and Stefan Jaax. Large Flocks of Small Birds: on the Minimal Size of Population Protocols. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.16.
  4. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the Coverability Problem Continuously. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. Google Scholar
  5. E. Cardoza, Richard J. Lipton, and Albert R. Meyer. Exponential Space Complete Problems for Petri Nets and Commutative Semigroups: Preliminary Report. In STOC'76, pages 50-54. ACM, 1976. URL: https://doi.org/10.1145/800113.803630.
  6. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets is Not Elementary (Extended Abstract). In STOC. ACM Computer Society, 2019. to appear. Google Scholar
  7. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. Acta Inf., 54(2):191-215, 2017. Google Scholar
  8. Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre. Occam’s Razor applied to the Petri net coverability problem. Theor. Comput. Sci., 750:38-52, 2018. Google Scholar
  9. V. S. Grinberg and S. V. Sevast'yanov. Value of the Steinitz constant. Functional Analysis and Its Applications, 14(2):125-126, April 1980. URL: https://doi.org/10.1007/BF01086559.
  10. Petr Jancar, Jérôme Leroux, and Grégoire Sutre. Co-finiteness and Co-emptiness of Reachability Sets in Vector Addition Systems with States. In Petri Nets, volume 10877 of Lecture Notes in Computer Science, pages 184-203. Springer, 2018. Google Scholar
  11. Jérôme Leroux. Vector Addition System Reversible Reachability Problem. Logical Methods in Computer Science, 9(1), 2013. Google Scholar
  12. Jérôme Leroux, M. Praveen, and Grégoire Sutre. A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness. In CONCUR, volume 8052 of Lecture Notes in Computer Science, pages 137-151. Springer, 2013. Google Scholar
  13. Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS. IEEE Computer Society, 2019. to appear. Google Scholar
  14. Jérôme Leroux and Grégoire Sutre. On Flatness for 2-Dimensional Vector Addition Systems with States. In CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. Google Scholar
  15. Loic Pottier. Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 162-173. Springer, 1991. Google Scholar
  16. C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. Google Scholar
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 About DROPS Imprint Privacy Contact