Document Open Access Logo

Flatness and Complexity of Immediate Observation Petri Nets

Authors Mikhail Raskin , Chana Weil-Kennedy , Javier Esparza

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.45.pdf
  • Filesize: 0.56 MB
  • 19 pages

Document Identifiers

Author Details

Mikhail Raskin
  • Technical University of Munich, Germany
Chana Weil-Kennedy
  • Technical University of Munich, Germany
Javier Esparza
  • Technical University of Munich, Germany

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).

Acknowledgements

We thank Jérôme Leroux and Rupak Majumdar for interesting conversations that put us on the path of flatness and BIO nets. We also thank the reviewers whose comments allowed us to improve this paper, and fix a small mistake in Lemma 18.

Cite AsGet BibTex

Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza. Flatness and Complexity of Immediate Observation Petri Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.45

Abstract

In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Concurrency
Keywords
  • Petri Nets
  • Reachability Analysis
  • Parameterized Verification
  • Flattability

Metrics

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

References

  1. David Angeli, Patrick De Leenheer, and Eduardo D Sontag. A petri net approach to the study of persistence in chemical reaction networks. Mathematical biosciences, 210(2):598-618, 2007. Google Scholar
  2. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279-304, 2007. Google Scholar
  3. Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu. TReX: A tool for reachability analysis of complex systems. In Lecture Notes in Computer Science, volume 2102, pages 368-372, 2001. Google Scholar
  4. Paolo Baldan, Nicoletta Cocco, Andrea Marin, and Marta Simeoni. Petri nets for modelling metabolic pathways: a survey. Natural Computing, 9(4):955-989, 2010. Google Scholar
  5. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: Fast acceleration of symbolic transition systems. In Lecture Notes in Computer Science, volume 2725, pages 118-121, 2003. Google Scholar
  6. Bernard Boigelot. The LASH toolset homepage, 2014. URL: http://www.montefiore.ulg.ac.be/~boigelot/research/lash/index.html.
  7. P. Chelikani, I. Fita, and P.C. Loewen. Diversity of structures and properties among catalases. Cell. Mol. Life Sci., 61, 2004. Google Scholar
  8. Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In LICS, pages 386-396, 1993. URL: https://www.wikidata.org/entity/Q59557027.
  9. Javier Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Inform., 31(1):13-25, 1997. Google Scholar
  10. Javier Esparza, Mikhail Raskin, and Chana Weil-Kennedy. Parameterized analysis of immediate observation petri nets. In Lecture Notes in Computer Science, volume 11522, pages 365-385, 2019. Google Scholar
  11. Laurent Fribourg. Petri nets, flat languages and linear arithmetic. In WFLP, pages 344-365, 2000. Google Scholar
  12. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. Google Scholar
  13. Slawomir Lasota. EXPSPACE lower bounds for the simulation preorder between a communication-free petri net and a finite-state system. Inf. Process. Lett., 109(15):850-855, 2009. Google Scholar
  14. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In ATVA, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. Google Scholar
  15. Wolfgang Marwan, Annegret Wagler, and Robert Weismantel. Petri nets as a framework for the reconstruction and analysis of signal transduction pathways and regulatory networks. Natural Computing, 10(2):639-654, 2011. Google Scholar
  16. Ernst W. Mayr and Jeremias Weihmann. Complexity results for problems of communication-free petri nets and related formalisms. Fundam. Inform., 137(1):61-86, 2015. Google Scholar
  17. Hsu-Chun Yen. On reachability equivalence for BPP-nets. Theor. Comput. Sci., 179(1-2):301-317, 1997. 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 Imprint Privacy Contact