2018/04/27 by Clément Aubert, Aubert, Clément, Ioana Cristescu +1
Computer Science · #Distributed #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Parallel #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1804.10355
openalex publication_date 2018/04/27 · openalex created_date 2018/05/07 · openalex updated_date 2026/07/28
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.