Abstract
Petri nets are a general formal model of concurrent systems which supports both action-based and state-based modelling and reasoning. One of important behavioural properties investigated in the context of Petri nets has been reversibility, understood as the possibility of returning to the initial marking from any reachable net marking. Thus reversibility in Petri nets is a global property. Reversible computation, on the other hand, is typically a local mechanism using which a system can undo some of the executed actions. This paper is concerned with the modelling of reversible computation within Petri nets. A key idea behind the proposed construction is to add ‘reverse’ versions of selected transitions. Since such a modification can severely impact on the behavior of the system, it is crucial, in particular, to be able to determine whether the modified system has a similar set of states as the original one. We first prove that the problem of establishing whether the two nets have the same reachable markings is undecidable even in the restricted case discussed in this paper. We then show that the problem of checking whether the reachability sets of the two nets cover the same markings is decidable.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The mirror of \(t_1t_2\ldots t_k\in T_A^*\) is \(t_1't_2'\ldots t_k' \in T_B^*\), and vice versa.
References
Araki, T., Kasami, T.: Decidable problems on the strong connectivity of Petri net reachability sets. Theoret. Comput. Sci. 4(1), 99–119 (1977)
Berry, G., Boudol, G.: The chemical abstract machine. Theoret. Comput. Sci. 96(1), 217–248 (1992)
Best, E., Desel, J., Esparza, J.: Traps characterize home states in free choice systems. Theoret. Comput. Sci. 101, 161–176 (1992)
Best, E., Esparza, J.: Existence of home states in Petri nets is decidable. Inf. Process. Lett. 116(6), 423–427 (2016)
Best, E., Schlachter, U.: Analysis of Petri nets and transition systems. In: Proceedings of 8th Interaction and Concurrency Experience (ICE 2015), EPTCS, vol. 189, pp. 53–67 (2015)
Best, E., Klaus, V.: Free choice systems have home states. Acta Informatica 21, 89–100 (1984)
Cardelli, L., Laneve, C.: Reversible structures. In: Fages, F. (ed.) Proceedings of 9th International Computational Methods in Systems Biology (CMSB 2011), pp. 131–140. ACM (2011)
Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 292–307. Springer, Heidelberg (2004)
Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 398–412. Springer, Heidelberg (2005)
Danos, V., Krivine, J., Sobocinski, P.: General reversibility. Electron. Notes Theoret. Comput. Sci. 175(3), 75–86 (2007)
de Frutos Escrig, D., Johnen, C.: Decidability of home space property. Technical report 503, Laboratoire de Recherche en Informatique, Université de Paris-Sud (1989)
Desel, J., Esparza, J.: Reachability in cyclic extended free-choice systems. Theoret. Comput. Sci. 114, 93–118 (1993)
Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) Petri Nets 1993. LNCS, vol. 674, pp. 210–243. Springer, Heidelberg (1993)
Michael, H.: Decidability questions for Petri nets. Technical report TR-161, MIT Laboratory for Computer Science (1976)
Michael, H.: Petri net languages. Technical report TR 159, MIT Laboratory for Computer Science (1976)
Hujsa, T., Delosme, J.-M., Munier-Kordon, A.: On the reversibility of live equal-conflict Petri nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 234–253. Springer, Heidelberg (2015)
Karp, R., Miller, R.: Parallel program schemata. J. Comput. Syst. Sci. 3, 147–195 (1969)
Kezić, D., Perić, N., Petrović, I.: An algorithm for deadlock prevention based on iterative siphon control of Petri net. Automatika 47, 19–30 (2006)
Lanese, I., Mezzina, C.A., Stefani, J.-B.: Reversing higher-order Pi. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 478–493. Springer, Heidelberg (2010)
Özkan, H.A., Aybar, A.: A reversibility enforcement approach for Petri nets using invariants. WSEAS Trans. Syst. 7, 672–681 (2008)
Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1–2), 70–96 (2007)
Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event structures. J. Log. Algebr. Methods Program. 84(6), 781–805 (2015)
Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 218–232. Springer, Heidelberg (2013)
Recalde, L., Teruel, E., Silva, M.: Modeling and analysis of sequential processes that cooperate through buffers. IEEE Trans. Robot. Autom. 14(2), 267–277 (1998)
Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science, vol. 4. Springer, Berlin (1985)
Teruel, E., Silva, M., Colom, J.M.: Choice-free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals. IEEE Trans. Syst. Man Cybern. Part A 27, 73–83 (1997)
Teruel, E., Silva, M.: Liveness and home states in equal conflict systems. PETRI NETS 1993. LNCS, vol. 691, pp. 415–432. Springer, Heidelberg (1993)
Vogler, W.: Live and bounded free choice nets have home states. Petri Net Newslett. 32, 18–21 (1989)
Wang, P., Ding, Z., Chai, H.: An algorithm for generating home states of Petri nets. J. Comput. Inf. Syst. 12(7), 4225–4232 (2011)
Acknowledgements
We would like to thank the anonymous reviewers for their remarks which allowed us to improve the presentation of the paper. This work was supported by the EU COST Action IC1405, and by the Polish National Science Center (grant No. 2013/09/D/ST6/03928).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Barylska, K., Koutny, M., Mikulski, Ł., Piątkowski, M. (2016). Reversible Computation vs. Reversibility in Petri Nets. In: Devitt, S., Lanese, I. (eds) Reversible Computation. RC 2016. Lecture Notes in Computer Science(), vol 9720. Springer, Cham. https://doi.org/10.1007/978-3-319-40578-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-40578-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40577-3
Online ISBN: 978-3-319-40578-0
eBook Packages: Computer ScienceComputer Science (R0)