Published in

Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020

DOI: 10.4230/lipics.concur.2020.7



Export citation

Search in Google Scholar

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

Journal article published in 2020 by Clément Aubert ORCID, Ioana Cristescu
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Green circle
Published version: archiving allowed
Data provided by SHERPA/RoMEO


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.