How reversibility can solve traditional questions: The example of hereditary history-preserving bisimulation

Clément Aubert, Ioana Cristescu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication31st International Conference on Concurrency Theory, CONCUR 2020
EditorsIgor Konnov, Laura Kovacs
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages71-723
Number of pages653
ISBN (Electronic)9783959771603
DOIs
StatePublished - Aug 1 2020
Event31st International Conference on Concurrency Theory, CONCUR 2020 - Virtual, Vienna, Austria
Duration: Sep 1 2020Sep 4 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume171
ISSN (Print)1868-8969

Conference

Conference31st International Conference on Concurrency Theory, CONCUR 2020
CountryAustria
CityVirtual, Vienna
Period9/1/209/4/20

Keywords

  • Bisimulation
  • Configuration structures
  • Distributed and reversible computation
  • Formal semantics
  • Process algebras and calculi
  • Reversible CCS

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'How reversibility can solve traditional questions: The example of hereditary history-preserving bisimulation'. Together they form a unique fingerprint.

Cite this