Advertisement

Parameterized Analysis of Immediate Observation Petri Nets

  • Javier Esparza
  • Mikhail Raskin
  • Chana Weil-KennedyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11522)

Abstract

We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in \(\mathsf {PSPACE}\) for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already \(\mathsf {PSPACE}\)-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is \(\mathsf {PSPACE}\)-complete, answering a question left open in a previous paper.

Keywords

Petri nets Reachability analysis Parameterized verification Population protocols 

Notes

Acknowledgments

We thank three anonymous reviewers for numerous suggestions to improve readability, and Pierre Ganty for many helpful discussions.

References

  1. 1.
    Alistarh, D., Aspnes, J., Eisenstat, D., Gelashvili, R., Rivest, R.L.: Time-space trade-offs in population protocols. In: Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 2560–2579 (2017)Google Scholar
  2. 2.
    Alistarh, D., Aspnes, J., Gelashvili, R.: Space-optimal majority in population protocols. In: Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 2221–2239 (2018)CrossRefGoogle Scholar
  3. 3.
    Alistarh, D., Gelashvili, R.: Recent algorithmic advances in population protocols. SIGACT News 49(3), 63–73 (2018)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Angeli, D., De Leenheer, P., Sontag, E.D.: A Petri net approach to the study of persistence in chemical reaction networks. Math. Biosci. 210(2), 598–618 (2007)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. In: Proceedings of the 23rd Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 290–299 (2004)Google Scholar
  6. 6.
    Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distrib. Comput. 20(4), 279–304 (2007)CrossRefGoogle Scholar
  7. 7.
    Baldan, P., Cocco, N., Marin, A., Simeoni, M.: Petri nets for modelling metabolic pathways: a survey. Nat. Comput. 9(4), 955–989 (2010)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theor. Comput. Sci. 147(1&2), 117–136 (1995)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary (extended abstract). CoRR, abs/1809.07115 (2018)Google Scholar
  10. 10.
    Elsässer, R., Radzik, T.: Recent results in population protocols for exact majority and leader election. Bull. EATCS 126 (2018)Google Scholar
  11. 11.
    Esparza, J.: Decidability and complexity of Petri net problems — an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-65306-6_20CrossRefzbMATHGoogle Scholar
  12. 12.
    Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. In: CONCUR. LIPIcs, vol. 42, pp. 470–482. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  13. 13.
    Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Informatica 54(2), 191–215 (2017)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of immediate observation population protocols. In: CONCUR. LIPIcs, vol. 118, pp. 31:1–31:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)Google Scholar
  15. 15.
    Esparza, J., Raskin, M., Weil-Kennedy, C.: Parameterized analysis of immediate observation petri nets. CoRR, abs/1902.03025 (2019)Google Scholar
  16. 16.
    Marwan, W., Wagler, A., Weismantel, R.: Petri nets as a framework for the reconstruction and analysis of signal transduction pathways and regulatory networks. Nat. Comput. 10(2), 639–654 (2011)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Mayr, E.W., Weihmann, J.: A framework for classical Petri net problems: conservative petri nets as an application. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 314–333. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-07734-5_17CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Technical University of MunichMunichGermany

Personalised recommendations