Document Open Access Logo

How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation

Authors Clément Aubert , Ioana Cristescu

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.7.pdf
  • Filesize: 0.61 MB
  • 23 pages

Document Identifiers

Author Details

Clément Aubert
  • School of Computer and Cyber Sciences, Augusta University, GA, USA
Ioana Cristescu
  • Tarides, Paris, France

Acknowledgements

The authors would like to thank John Natale for correcting the definition of postfixing and the reviewers of an earlier version of this work and of this version for their precious comments that greatly improved the paper. We were unfortunately not able to accomodate all of their suggestions, but have tried to reflect their comments in the body of the paper.

Cite AsGet BibTex

Clément Aubert and Ioana Cristescu. How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.7

Abstract

Reversible computation opens up the possibility of overcoming some of the hardware’s current physical limitations. It also offers theoretical insights, as it enriches multiple paradigms and models of computation, and sometimes retrospectively enlightens them. Concurrent reversible computation, for instance, offered interesting extensions to the Calculus of Communicating Systems, but was still lacking a natural and pertinent bisimulation to study processes equivalences. Our paper formulates an equivalence exploiting the two aspects of reversibility: backward moves and memory mechanisms. This bisimulation captures classical equivalences relations for denotational models of concurrency (history- and hereditary history-preserving bisimulation, (H)HPB), that were up to now only partially characterized by process algebras. This result gives an insight on the expressiveness of reversibility, as both backward moves and a memory mechanism - providing "backward determinism" - are needed to capture HHPB.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
  • Computing methodologies → Concurrent programming languages
Keywords
  • Formal semantics
  • Process algebras and calculi
  • Distributed and reversible computation
  • Configuration structures
  • Reversible CCS
  • Bisimulation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S. L. Brandao, David A. Buell, Brian Burkett, Yu Chen, Zijun Chen, Ben Chiaro, Roberto Collins, William Courtney, Andrew Dunsworth, Edward Farhi, Brooks Foxen, Austin Fowler, Craig Gidney, Marissa Giustina, Rob Graff, Keith Guerin, Steve Habegger, Matthew P. Harrigan, Michael J. Hartmann, Alan Ho, Markus Hoffmann, Trent Huang, Travis S. Humble, Sergei V. Isakov, Evan Jeffrey, Zhang Jiang, Dvir Kafri, Kostyantyn Kechedzhi, Julian Kelly, Paul V. Klimov, Sergey Knysh, Alexander Korotkov, Fedor Kostritsa, David Landhuis, Mike Lindmark, Erik Lucero, Dmitry Lyakh, Salvatore Mandrà, Jarrod R. McClean, Matthew McEwen, Anthony Megrant, Xiao Mi, Kristel Michielsen, Masoud Mohseni, Josh Mutus, Ofer Naaman, Matthew Neeley, Charles Neill, Murphy Yuezhen Niu, Eric Ostby, Andre Petukhov, John C. Platt, Chris Quintana, Eleanor G. Rieffel, Pedram Roushan, Nicholas C. Rubin, Daniel Sank, Kevin J. Satzinger, Vadim Smelyanskiy, Kevin J. Sung, Matthew D. Trevithick, Amit Vainsencher, Benjamin Villalonga, Theodore White, Z. Jamie Yao, Ping Yeh, Adam Zalcman, Hartmut Neven, and John M. Martinis. Quantum supremacy using a programmable superconducting processor. Nature, 574(7779):505-510, October 2019. URL: https://doi.org/10.1038/s41586-019-1666-5.
  2. Clément Aubert and Ioana Cristescu. Contextual equivalences in configuration structures and reversibility. Journal of Logical and Algebraic Methods in Programming, 86(1):77-106, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.08.004.
  3. Holger Bock Axelsen and Robert Glück. On reversible turing machines and their function universality. Acta Informatica, 53(5):509-543, 2016. URL: https://doi.org/10.1007/s00236-015-0253-y.
  4. Paolo Baldan and Silvia Crafa. Hereditary history-preserving bisimilarity: Logics and automata. In Jacques Garrigue, editor, APLAS, volume 8858 of Lecture Notes in Computer Science, pages 469-488. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-12736-1_25.
  5. Paolo Baldan and Silvia Crafa. A logic for true concurrency. Journal of the ACM, 61(4):24, 2014. URL: https://doi.org/10.1145/2629638.
  6. Marek A. Bednarczyk. Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Instytut Podstaw Informatyki PAN filia w Gdańsku, 1991. URL: http://www.ipipan.gda.pl/~marek/papers/historie.ps.gz.
  7. Gérard Boudol and Ilaria Castellani. On the semantics of concurrency: Partial orders and transition systems. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT'87, volume 249 of Lecture Notes in Computer Science, pages 123-137. Springer, 1987. URL: https://doi.org/10.1007/3-540-17660-8_52.
  8. Gérard Boudol and Ilaria Castellani. Permutation of transitions: An event structure semantics for CCS and SCCS. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30 - June 3, 1988, Proceedings, volume 354 of Lecture Notes in Computer Science, pages 411-427. Springer, 1988. URL: https://doi.org/10.1007/BFb0013028.
  9. Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the reversible p-calculus. In LICS, pages 388-397. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.45.
  10. Ioana Cristescu, Jean Krivine, and Daniele Varacca. Rigid families for CCS and the π-calculus. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, volume 9399 of Lecture Notes in Computer Science, pages 223-240. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_14.
  11. Vincent Danos and Jean Krivine. Reversible communicating systems. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 292-307. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_19.
  12. Vincent Danos and Jean Krivine. Transactions in RCCS. In Martín Abadi and Luca de Alfaro, editors, CONCUR, volume 3653 of Lecture Notes in Computer Science, pages 398-412. Springer, 2005. URL: https://doi.org/10.1007/11539452_31.
  13. Philippe Darondeau and Pierpaolo Degano. Causal trees: Interleaving + causality. In Irène Guessarian, editor, Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science, La Roche Posay, France, April 23-27, 1990, Proceedings, volume 469 of Lecture Notes in Computer Science, pages 239-255. Springer, 1990. URL: https://doi.org/10.1007/3-540-53479-2_10.
  14. David de Frutos-Escrig, Maciej Koutny, and Lukasz Mikulski. Reversing steps in petri nets. In Susanna Donatelli and Stefan Haar, editors, Application and Theory of Petri Nets and Concurrency - 40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23-28, 2019, Proceedings, volume 11522 of Lecture Notes in Computer Science, pages 171-191. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-21571-2_11.
  15. Rocco De Nicola, Ugo Montanari, and Frits W. Vaandrager. Back and forth bisimulations. In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 152-165. Springer, 1990. URL: https://doi.org/10.1007/BFb0039058.
  16. Michael P. Frank. Foundations of generalized reversible computing. In Iain Phillips and Hafizur Rahaman, editors, Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-7, 2017, Proceedings, volume 10301 of Lecture Notes in Computer Science, pages 19-34. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59936-6_2.
  17. Michael P. Frank. Throwing computing into reverse. IEEE Spectrum, 54(9):32-37, September 2017. URL: https://doi.org/10.1109/MSPEC.2017.8012237.
  18. Eva Graversen, Iain Phillips, and Nobuko Yoshida. Event structure semantics of (controlled) reversible CCS. In Jarkko Kari and Irek Ulidowski, editors, Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 102-122. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_7.
  19. Thomas Troels Hildebrandt. Categorical Models for Concurrency: Independence, Fairness and Dataflow. PhD thesis, BRICS, University of Aarhus, February 2000. URL: http://www.brics.dk/DS/00/1/.
  20. Markus Holzer and Martin Kutrib. Reversible nondeterministic finite automata. In Iain Phillips and Hafizur Rahaman, editors, Reversible Computation, pages 35-51. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-59936-6_3.
  21. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Information and Computation, 127(2):164-185, 1996. URL: https://doi.org/10.1006/inco.1996.0057.
  22. Yonggun Jun, Momčilo Gavrilov, and John Bechhoefer. High-precision test of landauer’s principle in a feedback trap. Phys. Rev. Lett., 113:190601, November 2014. URL: https://doi.org/10.1103/PhysRevLett.113.190601.
  23. Vasileios Koutavas and Matthew Spaccasassi, Carloand Hennessy. Bisimulations for communicating transactions - (extended abstract). In Anca Muscholl, editor, FoSSaCS, volume 8412 of Lecture Notes in Computer Science, pages 320-334. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_21.
  24. Ivan Lanese, Doriana Medić, and Claudio Antares Mezzina. Static versus dynamic reversibility in CCS. Acta Informatica, November 2019. URL: https://doi.org/10.1007/s00236-019-00346-6.
  25. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversing higher-order pi. In Paul Gastin and François Laroussinie, editors, CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 478-493. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_33.
  26. Michael Aaron Nielsen and Isaac L. Chuang. Quantum computation and quantum information. Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9780511976667.
  27. Anna Philippou and Kyriaki Psara. Reversible computation in petri nets. In Jarkko Kari and Irek Ulidowski, editors, Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 84-101. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_6.
  28. Iain Phillips and Irek Ulidowski. Reversing algebraic process calculi. In Luca Aceto and Anna Ingólfsdóttir, editors, FoSSaCS, volume 3921 of Lecture Notes in Computer Science, pages 246-260. Springer, 2006. URL: https://doi.org/10.1007/11690634_17.
  29. Iain Phillips and Irek Ulidowski. Reversibility and models for concurrency. Electronic Notes in Theoretical Computer Science, 192(1):93-108, 2007. URL: https://doi.org/10.1016/j.entcs.2007.08.018.
  30. Iain Phillips and Irek Ulidowski. Reversing algebraic process calculi. The Journal of Logic and Algebraic Programming, 73(1-2):70-96, 2007. URL: https://doi.org/10.1016/j.jlap.2006.11.002.
  31. Iain Phillips and Irek Ulidowski. Event identifier logic. Mathematical Structures in Computer Science, 24(2), 2014. URL: https://doi.org/10.1017/S0960129513000510.
  32. Alexander Rabinovich and Boris Avraamovich Trakhtenbrot. Behavior structures and nets. Fundamenta Informaticae, 11(4):357-404, 1988. Google Scholar
  33. Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. Models for concurrency: Towards a classification. Theoretical Computer Science, 170(1-2):297-348, 1996. URL: https://doi.org/10.1016/S0304-3975(96)80710-9.
  34. Rob J. van Glabbeek and Ursula Goltz. Refinement of actions in causality based models. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, Proceedings REX Workshop on Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 267-300. Springer, 1989. URL: https://doi.org/10.1007/3-540-52559-9_68.
  35. Robert J. van Glabbeek. History preserving process graphs. Technical report, Stanford University, 1996. URL: http://kilby.stanford.edu/~rvg/pub/history.draft.dvi.
  36. Robert J. van Glabbeek and Ursula Goltz. Equivalence notions for concurrent systems and refinement of actions (extended abstract). In Antoni Kreczmar and Grazyna Mirkowska, editors, MFCS, volume 379 of Lecture Notes in Computer Science, pages 237-248. Springer, 1989. URL: https://doi.org/10.1007/3-540-51486-4_71.
  37. Robert J. van Glabbeek and Ursula Goltz. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica, 37(4/5):229-327, 2001. URL: https://doi.org/10.1007/s002360000041.
  38. Robert J. van Glabbeek and Gordon D. Plotkin. Configuration structures, event structures and petri nets. Theoretical Computer Science, 410(41):4111-4159, 2009. URL: https://doi.org/10.1016/j.tcs.2009.06.014.
  39. Glynn Winskel. Event structure semantics for CCS and related languages. In Mogens Nielsen and Erik Meineche Schmidt, editors, ICALP, volume 140 of Lecture Notes in Computer Science, pages 561-576. Springer, 1982. URL: https://doi.org/10.1007/BFb0012800.
  40. Glynn Winskel. Event structures. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986, volume 255 of Lecture Notes in Computer Science, pages 325-392. Springer, 1986. URL: https://doi.org/10.1007/3-540-17906-2_31.
  41. Glynn Winskel. Event structures, stable families and concurrent games. Lecture notes, University of Cambridge, 2017. URL: https://www.cl.cam.ac.uk/~gw104/ecsym-notes.pdf.
  42. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Samson Abramsky, Dov M. Gabbay, and Thomas Stephen Edward Maibaum, editors, Semantic Modelling, volume 4 of Handbook of Logic in Computer Science, pages 1-148. Oxford University Press, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact