Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Causal Reversibility Implies Time Reversibility

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14287))

Included in the following conference series:

  • 366 Accesses

Abstract

Several notions of reversibility exist in the literature. On the one hand, causal reversibility establishes that an action can be undone provided that all of its consequences have been undone already, thereby making it possible to bring a system back to a past consistent state. On the other hand, time reversibility stipulates that the stochastic behavior of a system remains the same when the direction of time is reversed, which supports efficient performance evaluation. In this paper we show that causal reversibility is a sufficient condition for time reversibility. The study is conducted on extended labeled transition systems. Firstly, they include a forward and a backward transition relations obeying the loop property. Secondly, their transitions feature an independence relation as well as rates for their exponentially distributed random durations. Our result can thus be smoothly applied to concurrent and distributed models, calculi, and languages that account for performance aspects.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 74.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

Institutional subscriptions

Data Availability Statement

The machine-checkable proof of the result in Sect. 3 has been accepted by the QEST 2023 artifact evaluation committee and is available at https://github.com/sacerdot/Causal2TimedFormalization.

Notes

  1. 1.

    It is often called causal-consistent reversibility in the literature after [18].

  2. 2.

    It was called coinitial propagation of independence (CPI) in [22].

  3. 3.

    A property called unique transitions (UT) in [22].

References

  1. Asperti, A., Ricciotti, W., Sacerdoti Coen, C.: Matita tutorial. J. Formaliz. Reason. 7, 91–199 (2014)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Bernardo, M., Mezzina, C.A.: Bridging causal reversibility and time reversibility: a stochastic process algebraic approach. Log. Methods Comput. Sci. 19(2:6), 1–27 (2023)

    Google Scholar 

  4. Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31, 59–75 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. 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 

  6. 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). https://doi.org/10.1007/11539452_31

    Chapter  Google Scholar 

  7. Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115–138 (1971)

    Article  MathSciNet  Google Scholar 

  8. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370–384. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_26

    Chapter  Google Scholar 

  9. Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)

    MATH  Google Scholar 

  10. Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  11. Hoare, C.: Communicating Sequential Processes. Prentice Hall, Hoboken (1985)

    MATH  Google Scholar 

  12. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kelly, F.P.: Reversibility and Stochastic Networks. Wiley, Hoboken (1979)

    MATH  Google Scholar 

  14. Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Van Nostrand, New York (1960)

    MATH  Google Scholar 

  15. Lami, P., Lanese, I., Stefani, J.B., Sacerdoti Coen, C., Fabbretti, G.: Reversibility in Erlang: Imperative constructs. In: Mezzina, C.A., Podlaski, K. (eds.) RC 2022. LNCS, vol. 13354, pp. 187–203. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-09005-9_13

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  17. Lanese, I., Lienhardt, M., Mezzina, C.A., Schmitt, A., Stefani, J.-B.: Concurrent flexible reversibility. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 370–390. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_21

    Chapter  Google Scholar 

  18. 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). https://doi.org/10.1007/978-3-642-15375-4_33

    Chapter  Google Scholar 

  19. Lanese, I., Mezzina, C.A., Stefani, J.B.: Reversibility in the higher-order \(\pi \)-calculus. Theoret. Comput. Sci. 625, 25–84 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  20. Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for Erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_16

    Chapter  Google Scholar 

  21. 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  MATH  Google Scholar 

  22. Lanese, I., Phillips, I., Ulidowski, I.: An axiomatic approach to reversible computation. In: FoSSaCS 2020. LNCS, vol. 12077, pp. 442–461. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45231-5_23

    Chapter  MATH  Google Scholar 

  23. Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  24. Laursen, J.S., Ellekilde, L.P., Schultz, U.P.: Modelling reversible execution of robotic assembly. Robotica 36, 625–654 (2018)

    Article  Google Scholar 

  25. Marin, A., Rossi, S.: On the relations between Markov chain lumpability and reversibility. Acta Informatica 54, 447–485 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  26. Mazurkiewicz, A.: Basic notions of trace theory. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 285–363. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0013025

    Chapter  Google Scholar 

  27. 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

  28. Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing place-transition nets. Log. Methods Comput. Sci. 16(4:5), 1–28 (2020)

    Google Scholar 

  29. Milner, R.: Communication and Concurrency. Prentice Hall, Hoboken (1989)

    MATH  Google Scholar 

  30. Perumalla, K.S., Park, A.J.: Reverse computation for rollback-based fault tolerance in large parallel systems - evaluating the potential gains and systems effects. Clust. Comput. 17, 303–313 (2014)

    Article  Google Scholar 

  31. Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis (1962)

    Google Scholar 

  32. Phillips, I.C.C., Ulidowski, I.: Reversing algebraic process calculi. J. Logic Algebraic Program. 73, 70–96 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  33. 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). https://doi.org/10.1007/978-3-642-36315-3_18

    Chapter  MATH  Google Scholar 

  34. Pinna, G.M.: Reversing steps in membrane systems computations. In: Gheorghe, M., Rozenberg, G., Salomaa, A., Zandron, C. (eds.) CMC 2017. LNCS, vol. 10725, pp. 245–261. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73359-3_16

    Chapter  MATH  Google Scholar 

  35. Sassone, V., Nielsen, M., Winskel, G.: Models of concurrency: towards a classification. Theoret. Comput. Sci. 170, 297–348 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  36. Schordan, M., Oppelstrup, T., Jefferson, D.R., Barnes, P.D., Jr.: Generation of reversible C++ code for optimistic parallel discrete event simulation. N. Gener. Comput. 36, 257–280 (2018)

    Article  MATH  Google Scholar 

  37. Schweitzer, P.: Aggregation methods for large Markov chains. In: Proceedings of the International Workshop on Computer Performance and Reliability, pp. 275–286. North Holland (1984)

    Google Scholar 

  38. Siljak, H., Psara, K., Philippou, A.: Distributed antenna selection for massive MIMO using reversing Petri nets. IEEE Wirel. Commun. Lett. 8, 1427–1430 (2019)

    Article  Google Scholar 

  39. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  40. Vassor, M., Stefani, J.-B.: Checkpoint/rollback vs causally-consistent reversibility. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 286–303. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99498-7_20

    Chapter  Google Scholar 

  41. de Vries, E., Koutavas, V., Hennessy, M.: Communicating transactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 569–583. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_39

    Chapter  Google Scholar 

  42. Winskel, G.: Events in computation. Ph.D. thesis (1980)

    Google Scholar 

  43. Winskel, G.: Synchronisation trees. Theoret. Comput. Sci. 34, 33–82 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  44. Ycart, B.: The philosophers’ process: an ergodic reversible nearest particle system. Ann. Appl. Probab. 3, 356–363 (1993)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

This work has been supported by the Italian PRIN 2020 project NiRvAna – Noninterference and Reversibility Analysis in Private Blockchains, the French ANR-18-CE25-0007 project DCore – Causal Debugging for Concurrent Systems, and the INdAM-GNCS E53C22001930001 project RISICO – Reversibilità in Sistemi Concorrenti: Analisi Quantitative e Funzionali.

Author information

Authors and Affiliations

  1. Department of Pure and Applied Sciences, University of Urbino, Urbino, Italy

    Marco Bernardo & Claudio A. Mezzina

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

    Ivan Lanese

  3. Department of Environmental Sciences, Informatics and Statistics, University Ca’ Foscari, Venice, Italy

    Andrea Marin & Sabina Rossi

  4. Department of Informatics – Science and Engineering, University of Bologna, Bologna, Italy

    Claudio Sacerdoti Coen

Authors
  1. Marco Bernardo
    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

  3. Andrea Marin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Claudio A. Mezzina
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Sabina Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Claudio Sacerdoti Coen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marco Bernardo .

Editor information

Editors and Affiliations

  1. Radboud University Nijmegen, Nijmegen, The Netherlands

    Nils Jansen

  2. IMT Lucca, Lucca, Italy

    Mirco Tribastone

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bernardo, M., Lanese, I., Marin, A., Mezzina, C.A., Rossi, S., Sacerdoti Coen, C. (2023). Causal Reversibility Implies Time Reversibility. In: Jansen, N., Tribastone, M. (eds) Quantitative Evaluation of Systems. QEST 2023. Lecture Notes in Computer Science, vol 14287. Springer, Cham. https://doi.org/10.1007/978-3-031-43835-6_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-43835-6_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-43834-9

  • Online ISBN: 978-3-031-43835-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation