Document Open Access Logo

Goal-Driven Unfolding of Petri Nets

Authors Thomas Chatain, Loïc Paulevé

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.18.pdf
  • Filesize: 0.55 MB
  • 16 pages

Document Identifiers

Author Details

Thomas Chatain
Loïc Paulevé

Cite AsGet BibTex

Thomas Chatain and Loïc Paulevé. Goal-Driven Unfolding of Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 18:1-18:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.18

Abstract

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.
Keywords
  • model reduction; reachability; concurrency; unfoldings; Petri nets; automata networks

Metrics

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

References

  1. Paolo Baldan, Alessandro Bruni, Andrea Corradini, Barbara König, César Rodríguez, and Stefan Schwoon. Efficient unfolding of contextual Petri nets. TCS, 449:2-22, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.04.046.
  2. Paolo Baldan, Andrea Corradini, and Barbara König. A static analysis technique for graph transformation systems. In CONCUR 2001, volume 2154 of LNCS, pages 381-395. Springer, 2001. URL: http://dx.doi.org/10.1007/3-540-44685-0_26.
  3. Blai Bonet, Patrik Haslum, Sarah L. Hickmott, and Sylvie Thiébaux. Directed unfolding of Petri nets. Trans. Petri Nets and Other Models of Concurrency, 1:172-198, 2008. URL: http://dx.doi.org/10.1007/978-3-540-89287-8_11.
  4. Laurence Calzone, Amélie Gelay, Andrei Zinovyev, Fran1.0 cois Radvanyi, and Emmanuel Barillot. A comprehensive modular map of molecular interactions in RB/E2F pathway. Molecular Systems Biology, 4(1), 2008. URL: http://dx.doi.org/10.1038/msb.2008.7.
  5. Thomas Chatain, Stefan Haar, Loïg Jezequel, Loïc Paulevé, and Stefan Schwoon. Characterization of reachable attractors using Petri net unfoldings. In Computational Methods in Systems Biology, volume 8859 of LNCS, pages 129-142. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-12982-2_10.
  6. Thomas Chatain and Victor Khomenko. On the well-foundedness of adequate orders used for construction of complete unfolding prefixes. Inf. Process. Lett., 104(4):129-136, 2007. URL: http://dx.doi.org/10.1016/j.ipl.2007.06.002.
  7. Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theor. Comput. Sci., 147(1&2):117-136, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00231-7.
  8. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Springer, 2008. Google Scholar
  9. Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first net unfoldings. STTT, 10(2):161-166, 2008. URL: http://dx.doi.org/10.1007/s10009-007-0030-5.
  10. Javier Esparza and Stefan Römer. An unfolding algorithm for synchronous products of transition systems. In CONCUR, volume 1664 of LNCS, pages 2-20. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48320-9_2.
  11. Javier Esparza, Stefan Römer, and Walter Vogler. An improvement of McMillan’s unfolding algorithm. FMSD, 20:285-310, 2002. URL: http://dx.doi.org/10.1007/3-540-61042-1_40.
  12. Javier Esparza and Claus Schröter. Unfolding based algorithms for the reachability problem. Fundam. Inform., 47(3-4):231-245, 2001. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi47-3-4-05.
  13. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pages 110-121. ACM, 2005. URL: http://dx.doi.org/10.1145/1040305.1040315.
  14. Victor Khomenko. Punf. URL: http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/.
  15. Victor Khomenko, Maciej Koutny, and Walter Vogler. Canonical prefixes of Petri net unfoldings. Acta Inf., 40(2):95-118, 2003. URL: http://dx.doi.org/10.1007/s00236-003-0122-y.
  16. Kenneth L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In CAV, pages 164-177, 1992. URL: http://dx.doi.org/10.1007/3-540-56496-9_14.
  17. Loïc Paulevé. Goal-Oriented Reduction of Automata Networks. In CMSB 2016 - 14th conference on Computational Methods for Systems Biology, volume 9859 of Lecture Notes in Bioinformatics. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-45177-0_16.
  18. Loïc Paulevé, Geoffroy Andrieux, and Heinz Koeppl. Under-approximating cut sets for reachability in large scale automata networks. In CAV, volume 8044 of LNCS, pages 69-84. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_4.
  19. Regina Samaga, Axel Von Kamp, and Steffen Klamt. Computing combinatorial intervention strategies and failure modes in signaling networks. J. of Computational Biology, 17(1):39-53, 2010. URL: http://dx.doi.org/10.1089/cmb.2009.0121.
  20. S. Schwoon. Mole. URL: http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/.
  21. Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. Peephole partial order reduction. In TACAS 2008, volume 4963 of LNCS, pages 382-396. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_29.
  22. Nathan Weinstein and Luis Mendoza. A network model for the specification of vulval precursor cells and cell fusion control in caenorhabditis elegans. Frontiers in Genetics, 4(112), 2013. URL: http://dx.doi.org/10.3389/fgene.2013.00112.
  23. Ranran Zhang, Mithun Vinod Shah, Jun Yang, Susan B Nyland, Xin Liu, Jong K Yun, Réka Albert, and Thomas P Loughran. Network model of survival signaling in large granular lymphocyte leukemia. PNAS, 105:16308-13, 2008. URL: http://dx.doi.org/10.1073/pnas.0806447105.
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact