History-Preserving Bisimulations on Reversible Calculus of Communicating Systems
Logic in Computer Science
2018-04-30 v1 Distributed, Parallel, and Cluster Computing
Formal Languages and Automata Theory
Abstract
History-and hereditary history-preserving bisimulation (HPB and HHPB) are equivalences relations for denotational models of concurrency. Finding their counterpart in process algebras is an open problem, with some partial successes: there exists in calculus of communicating systems (CCS) an equivalence based on causal trees that corresponds to HPB. In Reversible CSS (RCCS), there is a bisimulation that corresponds to HHPB, but it considers only processes without auto-concurrency. We propose equivalences on CCS with auto-concurrency that correspond to HPB and HHPB, and their so-called "weak" variants. The equivalences exploit not only reversibility but also the memory mechanism of RCCS.
Keywords
Cite
@article{arxiv.1804.10355,
title = {History-Preserving Bisimulations on Reversible Calculus of Communicating Systems},
author = {Clément Aubert and Ioana Cristescu},
journal= {arXiv preprint arXiv:1804.10355},
year = {2018}
}