Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper explores various notions of bisimilarity within CCSK, a reversible extension of CCS, focusing on weak reversible bisimilarity, which has not been previously addressed in literature. The authors introduce two new variants, directional and mixed bisimilarity, which differ based on the alignment of $\tau$ actions with the actions being matched. A key finding is that mixed bisimilarity is a congruence that effectively abstracts away from $\tau$ actions, providing a clearer framework for analyzing reversible computation.
Mixed bisimilarity offers a novel congruence that simplifies the analysis of reversible computation by abstracting away from $\tau$ actions.
In the context of CCSK, a reversible extension of CCS, we study different notions of bisimilarity (strong/weak, forward-only/reversible) and highlight their differences and commonalities. In particular, for the weak reversible case, not previously studied in the literature, we propose two variants, dubbed directional and mixed bisimilarity, depending on whether $\tau$ actions should be in the same direction (forward/backward) as the action being matched or not. We show, in particular, that mixed bisimilarity is a congruence and completely abstracts away from $\tau$ actions.