Causal Reversibility in Individual Token Interpretation of Petri Nets
DOI:
https://doi.org/10.7494/csci.2020.21.4.3728Keywords:
Reversibility, Concurrent Systems, Petri Nets, Causality.Abstract
Causal reversibility in concurrent systems means that events that the origin of other events can only be undone after undoing of its consequences. In opposite to backtracking, the events which are independent of each other can be reversed in an arbitrary order, in the other words, we have flexible reversibility w.r.t the causality relation. An implementation of Individual token interpretation of
Petri Nets (IPNs) was been proposed by Rob Van Glabbeek et al, the present paper investigates into a study of causal reversibility within IPNs. Given N be an IPN, by adding an intuitive firing rule to undo transitions according to the causality relation, the coherence of N is assured, i.e., the set of all reachable states of N in the reversible version and that of the original one are identical. Furthermore, reversibility in N is flexible and their initial state can be accessible in reverse from any state. In this paper an approach for controlling
causal-reversibility within IPNs is proposed.
Downloads
References
Altenkirch T., Grattage J.: A Functional Quantum Programming Language. In:20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pp. 249–258. 2005. URL http://dx.doi.org/10.1109/LICS.2005.1.
Barylska K., Erofeev E., Koutny M., Mikulski L., Piatkowski M.: Reversing Transitions in Bounded Petri Nets. In: Fundam. Inform., vol. 157(4), pp. 341–357, 2018. URL http://dx.doi.org/10.3233/FI-2018-1631.
Barylska K., Koutny M., Mikulski L., Piatkowski M.: Reversible Computation vs. Reversibility in Petri Nets. In: Reversible Computation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings, pp. 105–118. 2016. URL http://dx.doi.org/10.1007/978-3-319-40578-0_7.
Barylska K., Koutny M., Mikulski L., Piatkowski M.: Reversible computation vs.
reversibility in Petri nets. In: Sci. Comput. Program., vol. 151, pp. 48–60, 2018.
URL https://doi.org/10.1016/j.scico.2017.10.008.
Barylska K., Mikulski L., Piatkowski M., Koutny M., Erofeev E.: Reversing
Transitions in Bounded Petri Nets. In: Proceedings of the 25th International
Workshop on Concurrency, Specification and Programming, Rostock, Germany,
September 28-30, 2016, pp. 74–85. 2016. URL http://ceur-ws.org/Vol-1698/
CS&P2016_08_Barylska&Mikulski&Piatkowski&Koutny&Erofeev_Reversing-Transitions-in-Bounded-Petri-Nets.pdf.
Bednarczyk M.A.: Hereditary history preserving bisimulations or what is the
power of the future perfect in program logics. In: Technical report, Institute of
Computer Science, Polish Academy of Sciences, Gdask. 1991.
Best E., Devillers R.R.: Sequential and Concurrent Behaviour in Petri Net
Theory. In: Theor. Comput. Sci., vol. 55(1), pp. 87–136, 1987. URL http://dx.doi.org/10.1016/0304-3975(87)90090-9.
Best E., Devillers R.R., Kiehn A., Pomello L.: Concurrent Bisimulations in Petri
Nets. In: Acta Inf., vol. 28(3), pp. 231–264, 1991. URL http://dx.doi.org/
1007/BF01178506.
Cardelli L., Laneve C.: Reversible structures. In: Computational Methods in Sys-
tems Biology, 9th International Conference, CMSB 2011, Paris, France, September 21-23, 2011. Proceedings, pp. 131–140. 2011. URL http://dx.doi.org/10.
/2037509.2037529.
Clairambault P., de Visme M., Winskel G.: Concurrent Quantum Strategies. In:
Reversible Computation - 11th International Conference, RC 2019, Lausanne,
Switzerland, June 24-25, 2019, Proceedings, pp. 3–19. 2019. URL http://dx.
doi.org/10.1007/978-3-030-21500-2_1.
Clavel M., Durán F., Eker S., Lincoln P., Martı́-Oliet N., Meseguer J., Quesada
J.F.: Maude: specification and programming in rewriting logic. In: Theor. Com-
put. Sci., vol. 285(2), pp. 187–243, 2002. URL http://dx.doi.org/10.1016/
S0304-3975(01)00359-0.
Cook J.J.: Reverse Execution of Java Bytecode. In: Comput. J., vol. 45(6), pp.
–619, 2002. URL http://dx.doi.org/10.1093/comjnl/45.6.608.
Danos V., Krivine J.: Reversible Communicating Systems. In: CONCUR 2004
- Concurrency Theory, 15th International Conference, London, UK, August 31 -
September 3, 2004, Proceedings, pp. 292–307. 2004. URL http://dx.doi.org/
1007/978-3-540-28644-8_19.
Danos V., Krivine J.: Transactions in RCCS. In: CONCUR 2005 - Con-
currency Theory, 16th International Conference, CONCUR 2005, San Fran-
cisco, CA, USA, August 23-26, 2005, Proceedings, pp. 398–412. 2005. URL
http://dx.doi.org/10.1007/11539452_31.
Danos V., Krivine J.: Formal Molecular Biology Done in CCS-R. In: Electron.
Notes Theor. Comput. Sci., vol. 180(3), pp. 31–49, 2007. URL http://dx.doi.
org/10.1016/j.entcs.2004.01.040.
Danos V., Krivine J., Sobocinski P.: General Reversibility. In: Electr. Notes
Theor. Comput. Sci., vol. 175(3), pp. 75–86, 2007. URL https://doi.org/10.
/j.entcs.2006.07.036.
Danos V., Krivine J., Tarissan F.: Self-assembling Trees. In: Electron. Notes
Theor. Comput. Sci., vol. 175(1), pp. 19–32, 2007. URL http://dx.doi.org/
1016/j.entcs.2006.11.017.
Engelfriet J.: Branching Processes of Petri Nets. In: Acta Inf., vol. 28(6), pp.
–591, 1991. URL http://dx.doi.org/10.1007/BF01463946.
Fecher H.: A completed hierarchy of true concurrent equivalences. In: Inf. Pro-
cess. Lett., vol. 89(5), pp. 261–265, 2004. URL http://dx.doi.org/10.1016/j.
ipl.2003.11.008.
Feldman S.I., Brown C.B.: Igor: A System for Program Debugging via Reversible
Execution. In: Proceedings of the ACM SIGPLAN and SIGOPS Workshop on
Parallel and Distributed Debugging, University of Wisconsin, Madison, Wiscon-
sin, USA, May 5-6, 1988, pp. 112–123. 1988. URL http://dx.doi.org/10.
/68210.69226.
Frank M.P.: Physical Foundations of Landauer’s Principle. In: Reversible Com-
putation - 10th International Conference, RC 2018, Leicester, UK, September
-14, 2018, Proceedings, pp. 3–33. 2018. URL http://dx.doi.org/10.1007/978-3-319-99498-7_1.
van Glabbeek R.J.: The Linear Time - Branching Time Spectrum I. In: Hand-
book of Process Algebra, pp. 3–99. 2001. URL http://dx.doi.org/10.1016/
b978-044482830-9/50019-9.
van Glabbeek R.J.: The Individual and Collective Token Interpretations of Petri
Nets. In: CONCUR 2005 - Concurrency Theory, 16th International Conference,
CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, pp.
–337. 2005. URL https://doi.org/10.1007/11539452_26.
van Glabbeek R.J., Goltz U., Schicke-Uffmann J.: On Distributability of Petri
Nets - (Extended Abstract). In: Foundations of Software Science and Computa-
tional Structures - 15th International Conference, FOSSACS 2012, Held as Part
of the European Joint Conferences on Theory and Practice of Software, ETAPS
, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, pp. 331–345. 2012.
URL http://dx.doi.org/10.1007/978-3-642-28729-9_22.
Goltz U., Reisig W.: The Non-sequential Behavior of Petri Nets. In: Information
and Control, vol. 57(2/3), pp. 125–147, 1983. URL http://dx.doi.org/10.
/S0019-9958(83)80040-0.
Hoey J., Ulidowski I.: Reversible Imperative Parallel Programs and Debugging.
In: Reversible Computation - 11th International Conference, RC 2019, Lausanne,
Switzerland, June 24-25, 2019, Proceedings, pp. 108–127. 2019. URL http://
dx.doi.org/10.1007/978-3-030-21500-2_7.
Jr. G.B.L.: A Formal Approach to Undo Operations in Programming Languages.
In: ACM Trans. Program. Lang. Syst., vol. 8(1), pp. 50–87, 1986. URL http:
//dx.doi.org/10.1145/5001.5005.
Krivine J.: A Verification Technique for Reversible Process Algebra. In: Re-
versible Computation, 4th International Workshop, RC 2012, Copenhagen, Den-
mark, July 2-3, 2012. Revised Papers, pp. 204–217. 2012. URL http://dx.doi.
org/10.1007/978-3-642-36315-3_17.
Landauer R.: Irreversibility and Heat Generation in the Computing Process. In:
IBM Journal of Research and Development, vol. 5(3), pp. 183–191, 1961. URL
http://dx.doi.org/10.1147/rd.53.0183.
Lanese I., Lienhardt M., Mezzina C.A., Schmitt A., Stefani J.: Concurrent
Flexible Reversibility. In: Programming Languages and Systems - 22nd Eu-
ropean Symposium on Programming, ESOP 2013, Held as Part of the Eu-
ropean Joint Conferences on Theory and Practice of Software, ETAPS 2013,
Rome, Italy, March 16-24, 2013. Proceedings, pp. 370–390. 2013. URL http:
//dx.doi.org/10.1007/978-3-642-37036-6_21.
Lanese I., Mezzina C.A., Schmitt A., Stefani J.: Controlling Reversibility
in Higher-Order Pi. In: CONCUR 2011 - Concurrency Theory - 22nd In-
ternational Conference, CONCUR 2011, Aachen, Germany, September 6-9,
Proceedings, pp. 297–311. 2011. URL http://dx.doi.org/10.1007/
-3-642-23217-6_20.
Lanese I., Mezzina C.A., Stefani J.: Controlled Reversibility and Compensations.
In: Reversible Computation, 4th International Workshop, RC 2012, Copenhagen,
Denmark, July 2-3, 2012. Revised Papers, pp. 233–240. 2012. URL http://dx.
doi.org/10.1007/978-3-642-36315-3_19.
Lanese I., Nishida N., Palacios A., Vidal G.: CauDEr: A Causal-Consistent Re-
versible Debugger for Erlang. In: Functional and Logic Programming - 14th Inter-
national Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings,
pp. 247–263. 2018. URL http://dx.doi.org/10.1007/978-3-319-90686-7
_16.
Lanese I., Palacios A., Vidal G.: Causal-Consistent Replay Debugging for Mes-
sage Passing Programs. In: Formal Techniques for Distributed Objects, Com-
ponents, and Systems - 39th IFIP WG 6.1 International Conference, FORTE
, Held as Part of the 14th International Federated Conference on Distributed
Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-
, 2019, Proceedings, pp. 167–184. 2019. URL http://dx.doi.org/10.1007/
-3-030-21759-4_10.
Mazurkiewicz A.W.: Trace Theory. In: Petri Nets: Central Models and Their
Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced
Course, Bad Honnef, Germany, 8-19 September 1986, pp. 279–324. 1986. URL
http://dx.doi.org/10.1007/3-540-17906-2_30.
Mazurkiewicz A.W.: Basic notions of trace theory.
In: Linear Time,
Branching Time and Partial Order in Logics and Models for Concurrency,
School/Workshop, Noordwijkerhout, The Netherlands, May 30 - June 3,
, Proceedings, pp. 285–363. 1988. URL http://dx.doi.org/10.1007/
BFb0013025.
Philippou A., Psara K., Siljak H.: Controlling Reversibility in Reversing
Petri Nets with Application to Wireless Communications. In: CoRR, vol.
abs/1905.11958, 2019. URL http://arxiv.org/abs/1905.11958.
Phillips I., Ulidowski I.: A Logic with Reverse Modalities for History-preserving
Bisimulations. In: Proceedings 18th International Workshop on Expressiveness
in Concurrency, EXPRESS 2011, Aachen, Germany, 5th September 2011., pp.
–118. 2011. URL https://doi.org/10.4204/EPTCS.64.8.
Phillips I., Ulidowski I.: Reversibility and asymmetric conflict in event structures.
In: J. Log. Algebr. Meth. Program., vol. 84(6), pp. 781–805, 2015. URL https:
//doi.org/10.1016/j.jlamp.2015.07.004.
Phillips I., Ulidowski I., Yuen S.: A Reversible Process Calculus and the
Modelling of the ERK Signalling Pathway. In: Reversible Computation, 4th
International Workshop, RC 2012, Copenhagen, Denmark, July 2-3, 2012.
Revised Papers, pp. 218–232. 2012.
URL http://dx.doi.org/10.1007/
-3-642-36315-3_18.
Phillips I.C.C., Ulidowski I.: Reversing algebraic process calculi. In: J. Log.
Algebr. Program., vol. 73(1-2), pp. 70–96, 2007. URL http://dx.doi.org/10.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2020 Computer Science
This work is licensed under a Creative Commons Attribution 4.0 International License.
