Skip to main content
SpringerLink
Log in
Book cover

International Conference on Applications and Theory of Petri Nets and Concurrency

PETRI NETS 2019: Application and Theory of Petri Nets and Concurrency pp 213–233Cite as

Reversing Unbounded Petri Nets

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11522))

Abstract

In Petri nets, computation is performed by executing transitions. An effect-reverse of a given transition b is a transition that, when executed, undoes the effect of b. A transition b is reversible if it is possible to add enough effect-reverses of b so to always being able to undo its effect, without changing the set of reachable markings.

This paper studies the transition reversibility problem: in a given Petri net, is a given transition b reversible? We show that, contrarily to what happens for the subclass of bounded Petri nets, the transition reversibility problem is in general undecidable. We show, however, that the same problem is decidable in relevant subclasses beyond bounded Petri nets, notably including all Petri nets which are cyclic, that is where the initial marking is reachable from any reachable marking. We finally show that some non-reversible Petri nets can be restructured, in particular by adding new places, so to make them reversible, while preserving their behaviour.

This work has been partially supported by COST Action IC1405 on Reversible Computation - extending horizons of computing. The second author has been also partially supported by French ANR project DCore ANR-18-CE25-0007.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Note that there can be two reasons for \(\lnot M_0[ \rho b \rangle M_2\). Either \(\rho b\) is not enabled at \(M_0\) or \(M_0[ \rho b \rangle M\) but \(M\ne M_2\).

References

  1. Badouel, E., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47967-4

    Book  MATH  Google Scholar 

  2. Barylska, K., Erofeev, E., Koutny, M., Mikulski, Ł., Piątkowski, M.: Reversing transitions in bounded Petri nets. Fundamenta Informaticae 157(4), 341–357 (2018)

    Article  MathSciNet  Google Scholar 

  3. Barylska, K., Koutny, M., Mikulski, Ł., Piątkowski, M.: Reversible computation vs. reversibility in Petri nets. Sci. Comput. Program. 151, 48–60 (2018)

    Article  Google Scholar 

  4. Barylska, K., Mikulski, Ł.: On decidability of persistence notions. In: 24th Workshop on Concurrency, Specification and Programming, pp. 44–56 (2015)

    Google Scholar 

  5. Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. 17(6), 525–532 (1973)

    Article  MathSciNet  Google Scholar 

  6. Best, E., Esparza, J.: Existence of home states in Petri nets is decidable. Inf. Process. Lett. 116(6), 423–427 (2016)

    Article  MathSciNet  Google Scholar 

  7. Bouziane, Z., Finkel, A.: Cyclic Petri net reachability sets are semi-linear effectively constructible. In: Infinity, ENTCS, pp. 15–24. Elsevier (1997)

    Google Scholar 

  8. Cardoza, E., Lipton, R., Meyer, A.: Exponential space complete problems for Petri nets and commutative semigroups (preliminary report). In: Proceedings of STOC 1976, pp. 50–54. ACM (1976)

    Google Scholar 

  9. Carothers, C.D., Perumalla, K.S., Fujimoto, R.: Efficient optimistic parallel simulations using reverse computation. ACM TOMACS 9(3), 224–253 (1999)

    Article  Google Scholar 

  10. Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Crocodile: a symbolic/symbolic tool for the analysis of symmetric nets with bag. In: Kristensen, L.M., Petrucci, L. (eds.) PETRI NETS 2011. LNCS, vol. 6709, pp. 338–347. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21834-7_20

    Chapter  MATH  Google Scholar 

  11. Czerwiński, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. arXiv preprint arXiv:1809.07115 (2018)

  12. Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19

    Chapter  Google Scholar 

  13. de Frutos Escrig, D., Johnen, C.: Decidability of home space property. Université de Paris-Sud. Centre d’Orsay. LRI (1989)

    Google Scholar 

  14. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math. 35(4), 413–422 (1913)

    Article  MathSciNet  Google Scholar 

  15. Esparza, J., Nielsen, M.: Decidability issues for Petri nets. BRICS Report Series 1(8) (1994)

    Google Scholar 

  16. Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56689-9_45

    Chapter  Google Scholar 

  17. Francalanza, A., Mezzina, C.A., Tuosto, E.: Reversible choreographies via monitoring in Erlang. In: Bonomi, S., Rivière, E. (eds.) DAIS 2018. LNCS, vol. 10853, pp. 75–92. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-93767-0_6

    Chapter  Google Scholar 

  18. Ginsburg, S., Spanier, E.: Bounded ALGOL-like languages. Trans. Am. Math. Soc. 113(2), 333–368 (1964)

    MathSciNet  MATH  Google Scholar 

  19. Hack, M.: Petri nets and commutative semigroups. Technical Report CSN 18, MIT Laboratory for Computer Science, Project MAC (1974)

    Google Scholar 

  20. Hack, M.: Decidability questions for Petri nets. Ph.D. thesis, MIT (1976)

    Google Scholar 

  21. Haddad, S., Kordon, F., Petrucci, L., Pradat-Peyre, J.-F., Treves, L.: Efficient state-based analysis by introducing bags in Petri nets color domains. In: ACC, pp. 5018–5025. IEEE (2009)

    Google Scholar 

  22. Jancar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281–301 (1995)

    Article  MathSciNet  Google Scholar 

  23. Kezić, D., Perić, N., Petrović, I.: An algorithm for deadlock prevention based on iterative siphon control of Petri net. Automatika: časopis za automatiku, mjerenje, elektroniku, računarstvo i komunikacije 47(1–2), 19–30 (2006)

    Google Scholar 

  24. Landauer, R.: Irreversibility and heat generated in the computing process. IBM J. Res. Dev. 5, 183–191 (1961)

    Article  Google Scholar 

  25. Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Controlling reversibility in higher-order Pi. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 297–311. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_20

    Chapter  Google Scholar 

  26. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. J. Log. Algebr. Methods Program. 100, 71–97 (2018)

    Article  MathSciNet  Google Scholar 

  27. Laursen, J.S., Schultz, U.P., Ellekilde, L.: Automatic error recovery in robot assembly operations using reverse execution. In: IROS, pp. 1785–1792. IEEE (2015)

    Google Scholar 

  28. Leroux, J.: Vector addition system reversible reachability problem. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 327–341. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_22

    Chapter  Google Scholar 

  29. McNellis, J., Mola, J., Sykes, K.: Time travel debugging: root causing bugs in commercial scale software. CppCon talk (2017). https://www.youtube.com/watch?v=l1YJTg_A914

  30. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  31. Reveliotis, S.A., Choi, J.Y.: Designing reversibility-enforcing supervisors of polynomial complexity for bounded Petri nets through the theory of regions. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 322–341. Springer, Heidelberg (2006)

    Google Scholar 

  32. Shende, V.V., Prasad, A.K., Markov, I.L., Hayes, J.P.: Synthesis of reversible logic circuits. IEEE Trans. CAD Integr. Circ. Syst. 22(6), 710–722 (2003)

    Article  Google Scholar 

  33. Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: PEPM, pp. 144–153. ACM Press (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Folco Team, Nicolaus Copernicus University, Torun, Poland

    Łukasz Mikulski

  2. Focus Team, University of Bologna/INRIA, Bologna, Italy

    Ivan Lanese

Authors
  1. Łukasz Mikulski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ivan Lanese
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ivan Lanese .

Editor information

Editors and Affiliations

  1. Università di Torino, Turin, Italy

    Susanna Donatelli

  2. Inria and LSV, CNRS & ENS Paris-Saclay, Cachan Cedex, France

    Stefan Haar

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Mikulski, Ł., Lanese, I. (2019). Reversing Unbounded Petri Nets. In: Donatelli, S., Haar, S. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2019. Lecture Notes in Computer Science(), vol 11522. Springer, Cham. https://doi.org/10.1007/978-3-030-21571-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21571-2_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21570-5

  • Online ISBN: 978-3-030-21571-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation