Advertisement

Reversing Unbounded Petri Nets

  • Łukasz Mikulski
  • Ivan LaneseEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Petri nets Reverse transition Reversibility 

References

  1. 1.
    Badouel, E., Bernardinello, L., Darondeau, P.: Petri Net Synthesis. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-47967-4CrossRefzbMATHGoogle Scholar
  2. 2.
    Barylska, K., Erofeev, E., Koutny, M., Mikulski, Ł., Piątkowski, M.: Reversing transitions in bounded Petri nets. Fundamenta Informaticae 157(4), 341–357 (2018)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Barylska, K., Koutny, M., Mikulski, Ł., Piątkowski, M.: Reversible computation vs. reversibility in Petri nets. Sci. Comput. Program. 151, 48–60 (2018)CrossRefGoogle Scholar
  4. 4.
    Barylska, K., Mikulski, Ł.: On decidability of persistence notions. In: 24th Workshop on Concurrency, Specification and Programming, pp. 44–56 (2015)Google Scholar
  5. 5.
    Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. 17(6), 525–532 (1973)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Best, E., Esparza, J.: Existence of home states in Petri nets is decidable. Inf. Process. Lett. 116(6), 423–427 (2016)MathSciNetCrossRefGoogle Scholar
  7. 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. 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. 9.
    Carothers, C.D., Perumalla, K.S., Fujimoto, R.: Efficient optimistic parallel simulations using reverse computation. ACM TOMACS 9(3), 224–253 (1999)CrossRefGoogle Scholar
  10. 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_20CrossRefzbMATHGoogle Scholar
  11. 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. 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_19CrossRefGoogle Scholar
  13. 13.
    de Frutos Escrig, D., Johnen, C.: Decidability of home space property. Université de Paris-Sud. Centre d’Orsay. LRI (1989)Google Scholar
  14. 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)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Esparza, J., Nielsen, M.: Decidability issues for Petri nets. BRICS Report Series 1(8) (1994)Google Scholar
  16. 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_45CrossRefGoogle Scholar
  17. 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_6CrossRefGoogle Scholar
  18. 18.
    Ginsburg, S., Spanier, E.: Bounded ALGOL-like languages. Trans. Am. Math. Soc. 113(2), 333–368 (1964)MathSciNetzbMATHGoogle Scholar
  19. 19.
    Hack, M.: Petri nets and commutative semigroups. Technical Report CSN 18, MIT Laboratory for Computer Science, Project MAC (1974)Google Scholar
  20. 20.
    Hack, M.: Decidability questions for Petri nets. Ph.D. thesis, MIT (1976)Google Scholar
  21. 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. 22.
    Jancar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281–301 (1995)MathSciNetCrossRefGoogle Scholar
  23. 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. 24.
    Landauer, R.: Irreversibility and heat generated in the computing process. IBM J. Res. Dev. 5, 183–191 (1961)CrossRefGoogle Scholar
  25. 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_20CrossRefGoogle Scholar
  26. 26.
    Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. J. Log. Algebr. Methods Program. 100, 71–97 (2018)MathSciNetCrossRefGoogle Scholar
  27. 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. 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_22CrossRefGoogle Scholar
  29. 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. 30.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  31. 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. 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)CrossRefGoogle Scholar
  33. 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

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Folco TeamNicolaus Copernicus UniversityTorunPoland
  2. 2.Focus TeamUniversity of Bologna/INRIABolognaItaly

Personalised recommendations