iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-031-77019-7_15
Reversibility in Process Calculi with Nondeterminism and Probabilities | SpringerLink
Skip to main content
Springer Nature Link
Log in

Reversibility in Process Calculi with Nondeterminism and Probabilities

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2024 (ICTAC 2024)

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

Included in the following conference series:

  • 59 Accesses

Abstract

A reversible system features not only forward computations, but also backward computations along which the effects of forward ones can be undone by starting from the last performed action. According to causal reversibility, an executed action can be undone provided that all the actions it caused have been undone already. We investigate causal reversibility in a nondeterministic and probabilistic setting by adapting the framework of Phillips and Ulidowski to define a reversible calculus in which action transitions and probabilistic transitions alternate in the style of Hansson and Jonsson. We show that the calculus meets causal reversibility through a suitable variant of the technique of Lanese, Phillips, and Ulidowski that ensures the proper forward and backward interplay of nondeterminism and probabilities. The use of the calculus is illustrated on a quantum computing example.

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

Similar content being viewed by others

References

  1. Andova, S., Georgievska, S., Trcka, N.: Branching bisimulation congruence for probabilistic systems. Theor. Comput. Sci. 413, 58–72 (2012)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  3. Bernardo, M., Esposito, A.: Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities. In: Proceedings of the 14th International Symposium on Games, Automata, Logics, and Formal Verification (GANDALF 2023). EPTCS, vol. 390, pp. 67–81 (2023)

    Google Scholar 

  4. Bernardo, M., Lanese, I., Marin, A., Mezzina, C.A., Rossi, S., Sacerdoti Coen, C.: Causal reversibility implies time reversibility. In: Jansen, N., Tribastone, M. (eds.) QEST 2023. LNCS, vol. 14287, pp. 270–287. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-43835-6_19

    Chapter  Google Scholar 

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

    Google Scholar 

  6. Bernardo, M., Mezzina, C.A.: Causal reversibility for timed process calculi with lazy/eager durationless actions and time additivity. In: Petrucci, L., Sproston, J. (eds.) FORMATS 2023. LNCS, vol. 14138, pp. 15–32. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-42626-1_2

    Chapter  Google Scholar 

  7. Bérut, A., Arakelyan, A., Petrosyan, A., Ciliberto, S., Dillenschneider, R., Lutz, E.: Experimental verification of Landauer’s principle linking information and thermodynamics. Nature 483, 187–189 (2012)

    Article  Google Scholar 

  8. Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–386. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45694-5_25

    Chapter  Google Scholar 

  9. Chatterjee, K., Goharshady, A.K., Pourdamghani, A.: Probabilistic smart contracts: secure randomness on the blockchain. In: Proceedings of the 1st IEEE International Conference on Blockchain and Cryptocurrency (ICBC 2019), pp. 403–412. IEEE-CS Press (2019)

    Google Scholar 

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

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

  12. De Nicola, R., Montanari, U., Vaandrager, F.: Back and forth bisimulations. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 152–165. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039058

    Chapter  Google Scholar 

  13. Derman, C.: Finite State Markovian Decision Processes. Academic Press (1970)

    Google Scholar 

  14. Esposito, A., Aldini, A., Bernardo, M.: Branching bisimulation semantics enables noninterference analysis of reversible systems. In: Huisman, M., Ravara, A. (eds.) FORTE 2023. LNCS, vol. 13910, pp. 57–74. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-35355-0_5

    Chapter  Google Scholar 

  15. Esposito, A., Aldini, A., Bernardo, M.: Noninterference analysis of reversible probabilistic systems. In: Castiglioni, V., Francalanza, A. (eds.) FORTE 2024. LNCS, vol. 14678, pp. 39–59. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-62645-6_3

    Chapter  Google Scholar 

  16. Frank, M.P.: Physical foundations of Landauer’s principle. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 3–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99498-7_1

    Chapter  Google Scholar 

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

  18. van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 59–80 (1995)

    Article  MathSciNet  Google Scholar 

  19. Hansson, H.: Time and probability in formal design of distributed systems. Ph.D. thesis (1992)

    Google Scholar 

  20. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings of the 11th IEEE Real-Time Systems Symposium (RTSS 1990), pp. 278–287. IEEE-CS Press (1990)

    Google Scholar 

  21. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  24. Krivine, J.: A verification technique for reversible process algebra. In: Glück, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 204–217. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36315-3_17

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

  27. Lanese, I., Medić, D., Mezzina, C.A.: Static versus dynamic reversibility in CCS. Acta Informatica 58, 1–34 (2021)

    Article  MathSciNet  Google Scholar 

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

  29. Lanese, I., Phillips, I., Ulidowski, I.: An axiomatic theory for reversible computation. ACM Trans. Comput. Logic 25(2), 11:1–11:40 (2024)

    Google Scholar 

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

    Article  Google Scholar 

  31. Lehmann, D., Rabin, M.O.: On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In: Proceedings of the 8th ACM Symposium on Principles of Programming Languages (POPL 1981), pp. 133–138. ACM Press (1981)

    Google Scholar 

  32. Lévy, J.J.: An algebraic interpretation of the \(\lambda \beta \)K-calculus; and an application of a labelled \(\lambda \)-calculus. Theor. Comput. Sci. 2, 97–114 (1976)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

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

  35. Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44618-4_25

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  37. 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  Google Scholar 

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

  39. Prabhu, P., Ramalingam, G., Vaswani, K.: Safe programmable speculative parallelism. In: Proceedings of the 31st ACM Conference on Programming Language Design and Implementation (PLDI 2010), pp. 50–61. ACM Press (2010)

    Google Scholar 

  40. Rabin, M.O.: Probabilistic automata. Inf. Control 6, 230–245 (1963)

    Article  Google Scholar 

  41. 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  Google Scholar 

  42. Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis (1995)

    Google Scholar 

  43. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994). https://doi.org/10.1007/978-3-540-48654-1_35

    Chapter  Google Scholar 

  44. Segala, R., Turrini, A.: Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: Proceedings of the 2nd International Conference on the Quantitative Evaluation of Systems (QEST 2005), pp. 44–53. IEEE-CS Press (2005)

    Google Scholar 

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

  46. Turrini, A., Hermanns, H.: Polynomial time decision algorithms for probabilistic automata. Inf. Comput. 244, 134–171 (2015)

    Article  MathSciNet  Google Scholar 

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

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

  49. Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: Proceedings of the 13th ACM Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM 2007), pp. 144–153. ACM Press (2007)

    Google Scholar 

Download references

Acknowledgments

This work has been supported by the Italian MUR PRIN 2020 project NiRvAna, the Italian MUR PRIN 2022 project DeKLA, the French ANR project DCore, and the Italian INdAM-GNCS project RISICO.

Author information

Authors and Affiliations

  1. Dipartimento di Scienze Pure e Applicate, Università di Urbino, Urbino, Italy

    Marco Bernardo & Claudio A. Mezzina

Authors
  1. Marco Bernardo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claudio A. Mezzina
    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. Asian Institute of Technology, Pathum Thani, Thailand

    Chutiporn Anutariya

  2. LIACS – Leiden University, Leiden, Zuid-Holland, The Netherlands

    Marcello M. Bonsangue

Rights and permissions

Reprints and permissions

Copyright information

© 2025 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., Mezzina, C.A. (2025). Reversibility in Process Calculi with Nondeterminism and Probabilities. In: Anutariya, C., Bonsangue, M.M. (eds) Theoretical Aspects of Computing – ICTAC 2024. ICTAC 2024. Lecture Notes in Computer Science, vol 15373. Springer, Cham. https://doi.org/10.1007/978-3-031-77019-7_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-77019-7_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-77018-0

  • Online ISBN: 978-3-031-77019-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation