On Weak Bisimilarities in CCSK

# On Weak Bisimilarities in CCSK
Source: [https://arxiv.org/html/2608.11531](https://arxiv.org/html/2608.11531)
###### Abstract

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τ\\tauactions 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τ\\tauactions\.

###### Keywords:

CCS, CCSK, Reversible Computation, Weak Bisimilarity, Behavioral Theory

This is a pre\-copy\-editing, author\-produced PDF of an article accepted for publication in RC 2026 following peer review\. The definitive publisher\-authenticated version is available online at https://link\.springer\.com/chapter/10\.1007/978\-3\-032\-30839\-9

## 1Introduction

Building concurrent systems is challenging due to the complexity of reasoning about numerous possible interleavings, yet concurrency is essential in modern systems like the Internet, cloud computing, and parallel processing\. Reversible computing, which allows systems to execute both forwards and backwards, recovering past states, has significant applications in low\-energy computing\[[9](https://arxiv.org/html/2608.11531#bib.bib8)\], simulation\[[5](https://arxiv.org/html/2608.11531#bib.bib5)\], biological modeling\[[4](https://arxiv.org/html/2608.11531#bib.bib7),[18](https://arxiv.org/html/2608.11531#bib.bib11)\], and program debugging\[[8](https://arxiv.org/html/2608.11531#bib.bib6),[13](https://arxiv.org/html/2608.11531#bib.bib9),[11](https://arxiv.org/html/2608.11531#bib.bib10)\]\. Many of these applications involve concurrent systems, leading to the development of reversible extensions of concurrent process calculi such as CCS\[[7](https://arxiv.org/html/2608.11531#bib.bib4),[19](https://arxiv.org/html/2608.11531#bib.bib2)\]and theπ\\pi\-calculus\[[6](https://arxiv.org/html/2608.11531#bib.bib12)\], and even of concurrent programming languages such as Erlang\[[10](https://arxiv.org/html/2608.11531#bib.bib15)\]and Go\[[17](https://arxiv.org/html/2608.11531#bib.bib16)\]\.

A main notion in the theory of process calculi is the notion of bisimilarity\[[20](https://arxiv.org/html/2608.11531#bib.bib13)\], allowing one to prove two processes equivalent, e\.g\., to prove an implementation equivalent to a more abstract specification\. In particular, bisimilarity requires equivalent processes to be able to match each other actions, and in doing so going to processes which are still equivalent\. While strong and weak bisimilarity \(weak bisimilarity differs from the strong one as the former abstracts away from internal actions, focusing only on interactions with the context\) have been extensively studied in concurrent systems, the literature lacks an analysis of weak bisimilarities in a reversible setting\. Our study addresses this gap by investigating the relationships between different notions of bisimilarity \(strong/weak, forward\-only/reversible\) in the context of CCSK\[[19](https://arxiv.org/html/2608.11531#bib.bib2)\], a causal\-consistent reversible extension of Milner CCS\[[15](https://arxiv.org/html/2608.11531#bib.bib3)\]\. In particular, in the definition of weak reversible bisimilarity, a main decision is whether auxiliaryτ\\tauactions \(representing internal steps\) allowed in the simulation of some actionα\\alphaneed to be in the same direction asα\\alphaor not\. The two alternatives lead to different equivalences\.

We consider this work as a first step in the exploration of weak bisimilarity in a reversible setting, paving the way for a deeper exploration in the future\. We claim as our main contributions the proposal of two notions of weak reversible bisimilarity \(mixed bisimilarity in Definition[10](https://arxiv.org/html/2608.11531#Thmdefinition10)and directional bisimilarity in Definition[11](https://arxiv.org/html/2608.11531#Thmdefinition11), both in Section[3](https://arxiv.org/html/2608.11531#S3)\), the study of the relations between different notions of bisimilarity in CCSK \(Section[4](https://arxiv.org/html/2608.11531#S4)\), and the study of which of these notions are congruences \(Section[5](https://arxiv.org/html/2608.11531#S5)\)\. In particular, we show that mixed bisimilarity is a congruence \(Theorem[5\.1](https://arxiv.org/html/2608.11531#S5.Thmtheorem1)\) and completely abstracts away fromτ\\tauactions \(Proposition[9](https://arxiv.org/html/2608.11531#Thmproposition9)and Theorem[5\.2](https://arxiv.org/html/2608.11531#S5.Thmtheorem2)\)\. Another surprising result is that extending CCS bisimilarities to CCSK gives equivalences which are not congruences \(Proposition[6](https://arxiv.org/html/2608.11531#Thmproposition6)\), even when they are congruences in CCS, as in the case of strong bisimilarity\.

## 2CCSK

In this section we recall the main elements of CCSK, while referring to\[[19](https://arxiv.org/html/2608.11531#bib.bib2)\]for further details\. We assume an infinite set ofNames𝒜\\mathcal\{A\}, ranged over bya,b,c,…a,b,c,\\ldots, and a disjoint infinite set ofCo\-names𝒜¯\\overline\{\\mathcal\{A\}\}, ranged over bya¯,b¯,c¯,…\\overline\{a\},\\overline\{b\},\\overline\{c\},\\ldots, where∗¯\\overline\{\*\}is an operator such thata¯¯=a\\overline\{\\overline\{a\}\}=a\. We callactionsthe elements of𝒜∪𝒜¯∪\{τ\}\\mathcal\{A\}\\cup\\overline\{\\mathcal\{A\}\}\\cup\\\{\\tau\\\}whereτ∉𝒜\\tau\\notin\\mathcal\{A\}andτ¯\\overline\{\\tau\}is undefined, ranged over byα,β,…\\alpha,\\beta,\\ldotsIntuitively, names represent input actions, co\-names represent output actions, andτ\\tauis an internal synchronisation\. CCS processes, which we shall also call*standard*processes, are given by:

P,Q:=0∣∣α\.P∣∣P\+Q∣∣P\|Q∣∣\(νa\)PP,Q:=0\\mid\\mid\\alpha\.P\\mid\\mid P\+Q\\mid\\mid P\\,\|\\,Q\\mid\\mid\(\\nu a\)PIntuitively,00is the inactive process,α\.P\\alpha\.Pis a process that performs actionα\\alphaand continues asPP,P\+QP\+Qis nondeterministic choice,P\|QP\\,\|\\,Qis parallel composition and restriction\(ν​a\)​P\(\\nu a\)Pbinds nameaaand the corresponding co\-namea¯\\overline\{a\}insidePP\. A name is*bound*if it is inside the scope of a restriction operator,*free*otherwise\. Function𝚏𝚗⁡\(P\)\\mathtt\{fn\}\(P\)computes the set of free names in processPP\. We set this convention: unary operators bind stronger than binary operators\.

CCSK extends CCS with the possibility of executing backwards\. In order to remember which input interacted with which output while going forwards, fresh*keys*are created at each forward step, and the same key is used to label an input and the corresponding output during a synchronisation\.

We denote the set of keys by𝙺𝚎𝚢𝚜\\mathtt\{Keys\}, ranged over bym,n,k,…m,n,k,\\ldots\. Prefixes, ranged over byπ\\pi, are of the formα⁡\[m\]\\alpha\[m\]orα\\alpha\. The former denotes thatα\\alphahas already been executed, the latter that it has not\.

CCSK processes are given by:

P,Q:=0∣∣π\.P∣∣P\+Q∣∣P\|Q∣∣\(νa\)PP,Q:=0\\mid\\mid\\pi\.P\\mid\\mid P\+Q\\mid\\mid P\\,\|\\,Q\\mid\\mid\(\\nu a\)Phence they are like CCS processes but for the fact that prefixes may be labelled with a key\. In the following, we may drop trailing00s\.

###### Definition 1\(Context\)\.

A CCSK*context*is a process with a hole, as generated by the grammar below:

C:=∙∣∣π\.C∣∣C\+Q∣∣P\+C∣∣C\|Q∣∣P\|C∣∣\(νa\)CC:=\\bullet\\mid\\mid\\pi\.C\\mid\\mid C\+Q\\mid\\mid P\+C\\mid\\mid C\\,\|\\,Q\\mid\\mid P\\,\|\\,C\\mid\\mid\(\\nu a\)CWe denote withC⁡\[P\]C\[P\]the process obtained by replacing∙\\bulletwithPPinsideCC\.

We use predicate𝚜𝚝𝚍⁡\(P\)\\mathtt\{std\}\(P\)to mean thatPPis standard, that is none of its actions has been executed, hence it has no keys\. We assume function𝚝𝚘𝚂𝚝𝚍⁡\(P\)\\mathtt\{toStd\}\(P\)that takes a CCSK processPPand gives back the standard process obtained by removing all keys fromPP\.

We take from\[[12](https://arxiv.org/html/2608.11531#bib.bib1), Def\. 2\.1\]the notions of free and bound keys\.

###### Definition 2\(Free and bound keys\)\.

A keykkis*bound*in a processXXiff it occurs either twice, attached to complementary prefixes, or once, attached to aτ\\tauprefix\. A keykkis*free*if it occurs once, attached to a non\-τ\\tauprefix\.

Figure[1](https://arxiv.org/html/2608.11531#S2.F1)shows the forward rules of CCSK\. Backward rules in Figure[2](https://arxiv.org/html/2608.11531#S2.F2)are obtained from forward rules by reversing the direction of transitions\. Both relations rely on a definition of structural congruence allowing one toα\\alpha\-convert bound keys, applicable only at top level \(this condition is needed to ensure that there are no other occurences ofnnin the context\):

P≡P⁡\[n/m\]m​bound in​P,n∉𝚔𝚎𝚢𝚜⁡\(P\)P\\equiv P\[n/m\]\\qquad m\\text\{ bound in \}P,n\\notin\\mathtt\{keys\}\(P\)
\(TOP\)𝚜𝚝𝚍⁡\(P\)α\.P→α⁡\[m\]fα\[m\]\.P\(PREFIX\)P→β⁡\[n\]fP′α\[m\]\.P→β⁡\[n\]fα\[m\]\.P′​m≠n\(CHOICE\)P→α⁡\[m\]fP′𝚜𝚝𝚍\(Q\)P\+Q→α⁡\[m\]fP′\+QQ→α⁡\[m\]fQ′𝚜𝚝𝚍\(P\)P\+Q→α⁡\[m\]fP\+Q′\(PAR\)P→α⁡\[m\]fP′m∉𝚔𝚎𝚢𝚜\(Q\)P\|Q→α⁡\[m\]fP′\|QQ→α⁡\[m\]fQ′m∉𝚔𝚎𝚢𝚜\(P\)P\|Q→α⁡\[m\]fP\|Q′\(SYNCH\)P→α⁡\[m\]fP′Q→α¯​\[m\]fQ′P\|Q→τ⁡\[m\]fP′\|Q′\(α≠τ\)\(RES\)P→α⁡\[m\]fP′\(νa\)P→α⁡\[m\]f\(νa\)P′​α∉\{a,a¯\}\(EQUIV\)P≡QQ→α⁡\[m\]fQ′Q′≡P′P→α⁡\[m\]fP′​applicable onlyat top level\\begin\{array\}\[\]\{c\}\\text\{\(TOP\)\}\\quad\\displaystyle\{\\frac\{\\mathtt\{std\}\(P\)\}\{\\alpha\.P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}\\alpha\[m\]\.P\}\}\\qquad\\text\{\(PREFIX\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\beta\[n\]\}\_\{f\}P^\{\\prime\}\}\{\\alpha\[m\]\.P\\xrightarrow\{\\beta\[n\]\}\_\{f\}\\alpha\[m\]\.P^\{\\prime\}\}\}\\;m\\neq n\\\\\[15\.0pt\] \\text\{\(CHOICE\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\\quad\\mathtt\{std\}\(Q\)\}\{P\+Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\+Q\}\}\\qquad\\displaystyle\{\\frac\{Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}Q^\{\\prime\}\\quad\\mathtt\{std\}\(P\)\}\{P\+Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P\+Q^\{\\prime\}\}\}\\\\\[15\.0pt\] \\text\{\(PAR\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\\quad m\\notin\\mathtt\{keys\}\(Q\)\}\{P\\,\|\\,Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\\,\|\\,Q\}\}\\qquad\\displaystyle\{\\frac\{Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}Q^\{\\prime\}\\quad m\\notin\\mathtt\{keys\}\(P\)\}\{P\\,\|\\,Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P\\,\|\\,Q^\{\\prime\}\}\}\\\\\[15\.0pt\] \\text\{\(SYNCH\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\\quad Q\\xrightarrow\{\\overline\{\\alpha\}\[m\]\}\_\{f\}Q^\{\\prime\}\}\{P\\,\|\\,Q\\xrightarrow\{\\tau\[m\]\}\_\{f\}P^\{\\prime\}\\,\|\\,Q^\{\\prime\}\}\}\\quad\(\\alpha\\neq\\tau\)\\\\\[15\.0pt\] \\text\{\(RES\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\}\{\(\\nu a\)P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}\(\\nu a\)P^\{\\prime\}\}\}\\ \\alpha\\notin\\\{a,\\overline\{a\}\\\}\\\\\[15\.0pt\] \\text\{\(EQUIV\)\}\\quad\\displaystyle\{\\frac\{P\\equiv Q\\quad Q\\xrightarrow\{\\alpha\[m\]\}\_\{f\}Q^\{\\prime\}\\quad Q^\{\\prime\}\\equiv P^\{\\prime\}\}\{P\\xrightarrow\{\\alpha\[m\]\}\_\{f\}P^\{\\prime\}\}\}\\;\\begin\{array\}\[\]\{c\}\\text\{applicable only\}\\\\ \\text\{at top level\}\\end\{array\}\\end\{array\}Figure 1:Forward SOS rules for CCSK\(BK\-TOP\)𝚜𝚝𝚍⁡\(P\)α\[m\]\.P→α⁡\[m\]rα\.P\(BK\-PREFIX\)P→β⁡\[n\]rP′α\[m\]\.P→β⁡\[n\]rα\[m\]\.P′​m≠n\(BK\-CHOICE\)P→α⁡\[m\]rP′𝚜𝚝𝚍\(Q\)P\+Q→α⁡\[m\]rP′\+QQ→α⁡\[m\]rQ′𝚜𝚝𝚍\(P\)P\+Q→α⁡\[m\]rP\+Q′\(BK\-PAR\)P→α⁡\[m\]rP′m∉𝚔𝚎𝚢𝚜\(Q\)P\|Q→α⁡\[m\]rP′\|QQ→α⁡\[m\]rQ′m∉𝚔𝚎𝚢𝚜\(P\)P\|Q→α⁡\[m\]rP\|Q′\(BK\-SYNCH\)P→α⁡\[m\]rP′Q→α¯​\[m\]rQ′P\|Q→τ⁡\[m\]rP′\|Q′\(α≠τ\)\(BK\-RES\)P→α⁡\[m\]rP′\(νa\)P→α⁡\[m\]r\(νa\)P′​α∉\{a,a¯\}\(BK\-EQUIV\)P≡QQ→α⁡\[m\]rQ′Q′≡P′P→α⁡\[m\]rP′​applicable onlyat top level\\begin\{array\}\[\]\{c\}\\text\{\(BK\-TOP\)\}\\quad\\displaystyle\{\\frac\{\\mathtt\{std\}\(P\)\}\{\\alpha\[m\]\.P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}\\alpha\.P\}\}\\qquad\\text\{\(BK\-PREFIX\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\beta\[n\]\}\_\{r\}P^\{\\prime\}\}\{\\alpha\[m\]\.P\\xrightarrow\{\\beta\[n\]\}\_\{r\}\\alpha\[m\]\.P^\{\\prime\}\}\}\\;m\\neq n\\\\\[15\.0pt\] \\text\{\(BK\-CHOICE\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\\quad\\mathtt\{std\}\(Q\)\}\{P\+Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\+Q\}\}\\qquad\\displaystyle\{\\frac\{Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}Q^\{\\prime\}\\quad\\mathtt\{std\}\(P\)\}\{P\+Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P\+Q^\{\\prime\}\}\}\\\\\[15\.0pt\] \\text\{\(BK\-PAR\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\\quad m\\notin\\mathtt\{keys\}\(Q\)\}\{P\\,\|\\,Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\\,\|\\,Q\}\}\\qquad\\displaystyle\{\\frac\{Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}Q^\{\\prime\}\\quad m\\notin\\mathtt\{keys\}\(P\)\}\{P\\,\|\\,Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P\\,\|\\,Q^\{\\prime\}\}\}\\\\\[15\.0pt\] \\text\{\(BK\-SYNCH\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\\quad Q\\xrightarrow\{\\overline\{\\alpha\}\[m\]\}\_\{r\}Q^\{\\prime\}\}\{P\\,\|\\,Q\\xrightarrow\{\\tau\[m\]\}\_\{r\}P^\{\\prime\}\\,\|\\,Q^\{\\prime\}\}\}\\quad\(\\alpha\\neq\\tau\)\\\\\[15\.0pt\] \\text\{\(BK\-RES\)\}\\quad\\displaystyle\{\\frac\{P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\}\{\(\\nu a\)P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}\(\\nu a\)P^\{\\prime\}\}\}\\ \\alpha\\notin\\\{a,\\overline\{a\}\\\}\\\\\[15\.0pt\] \\text\{\(BK\-EQUIV\)\}\\quad\\displaystyle\{\\frac\{P\\equiv Q\\quad Q\\xrightarrow\{\\alpha\[m\]\}\_\{r\}Q^\{\\prime\}\\quad Q^\{\\prime\}\\equiv P^\{\\prime\}\}\{P\\xrightarrow\{\\alpha\[m\]\}\_\{r\}P^\{\\prime\}\}\}\\;\\begin\{array\}\[\]\{c\}\\text\{applicable only\}\\\\ \\text\{at top level\}\\end\{array\}\\end\{array\}Figure 2:Reverse SOS rules for CCSKRule \(TOP\) allows a prefix to execute\. The rule generates a keymm\. Freshness ofmmis guaranteed by the side conditions of the other rules \(cf\. rule \(PAR\)\)\. Rule \(PREFIX\) states that an executed prefix does not block execution\. The two rules for \(CHOICE\) and the two for \(PAR\) allow processes to execute inside a choice or a parallel composition\. The side condition of rule \(CHOICE\) ensures that at most one branch can execute\. Rule \(SYNCH\) allows two complementary actions to synchronise producing aτ\\tau\. The key of the two actions needs to be the same\. Rule \(RES\) allows an action which does not involve the restricted name to propagate through restriction\.

The forward semantics of a CCSK process is the smallest relation→f\\xrightarrow\{\}\_\{f\}closed under the rules in Figure[1](https://arxiv.org/html/2608.11531#S2.F1)\. Analogously, its backward semantics is the smallest relation→r\\xrightarrow\{\}\_\{r\}closed under the rules in Figure[2](https://arxiv.org/html/2608.11531#S2.F2)\. The semantics is the union of the two relations\. From now on, we letϑ\\varthetarange overα⁡\[m\]\\alpha\[m\]andμ\\murange overα⁡\[m\]\\alpha\[m\]withα≠τ\\alpha\\neq\\tau\. Letx,y,…x,y,\\ldotsrange over the set of directions\{f,r\}\\\{f,r\\\}, for forward and reverse\.

As standard in reversible computing \(see, e\.g\.,\[[19](https://arxiv.org/html/2608.11531#bib.bib2)\]or the notion of coherent process in\[[7](https://arxiv.org/html/2608.11531#bib.bib4)\]\), all the developments consider only processes reachable from a standard process\.

###### Definition 3\(Reachable process\)\.

A processQQis*reachable*iff there exists a standard processPPand a finite sequence of transitions fromPPtoQQ\.

## 3Bisimilarities

In this section we introduce the various notions of bisimilarity we study\. We start from CCS bisimilarities, and then move to bisimilarities specific for CCSK\. Note that CCS can be seen as a subset of CCSK, considering only standard processes and only forward semantics\. Hence, we will extend CCS bisimulations to CCSK by just considering forward transitions of CCSK terms\. As a consequence, history becomes inaccessible, hence ideally irrelevant\. However, requiring that a transition is matched by a transition with identical label would leak information on which keys are used in the history, as shown by the following example\.

###### Example 1

We haveb→b⁡\[n\]fb\[n\]b\\xrightarrow\{b\[n\]\}\_\{f\}b\[n\]while no transition with the same label is enabled froma⁡\[n\]\.ba\[n\]\.b\. The second process hence cannot match the transition of the first one in the bisimulation game if equality of labels is required\. Hence, keys of forward transitions leak information about which keys are used in the history\.

In order to avoid this issue, we will remove keys from the labels\. Hence, we define CCS semantics for CCSK processes as follows:

###### Definition 4\(CCS semantics for CCSK processes\)\.

Given a CCSK processPP,P→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}iff there iskksuch thatP→α⁡\[k\]fP′P\\xrightarrow\{\\alpha\[k\]\}\_\{f\}P^\{\\prime\}\.

We show now that the semantics above, defined on all CCSK processes, is indeed strictly related to the classical semantics of CCS defined in\[[14](https://arxiv.org/html/2608.11531#bib.bib14), Chapter 5\]111Actually, the semantics in\[[14](https://arxiv.org/html/2608.11531#bib.bib14), Chapter 5\]includes additional operators, as well as value passing\. We consider its restriction to the operators we use in CCSK\., which we denote as→c​c​s\\xrightarrow\{\}\_\{ccs\}\. Let𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(\)\\mathtt\{delHist\}\(\)be the function that extracts the standard part of a process\.

###### Definition 5\(𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(\)\\mathtt\{delHist\}\(\)\)\.

The𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(\)\\mathtt\{delHist\}\(\)function is inductively defined as follows:

𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\)=P​if​𝚜𝚝𝚍​\(P\)𝚍𝚎𝚕𝙷𝚒𝚜𝚝\(a\[n\]\.P\)=𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\)𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\+Q\)=𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\)​if​¬𝚜𝚝𝚍⁡\(P\)𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\+Q\)=𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(Q\)​if​¬𝚜𝚝𝚍⁡\(Q\)𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\|Q\)=𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P\)\|𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(Q\)𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(\(ν​a\)​P\)=\(ν​a\)​𝚍𝚎𝚕𝙷𝚒𝚜𝚝​\(P\)\\begin\{array\}\[\]\{rcl\}\\mathtt\{delHist\}\(P\)&=&P\\textrm\{ if \}\\mathtt\{std\}\(P\)\\\\ \\mathtt\{delHist\}\(a\[n\]\.P\)&=&\\mathtt\{delHist\}\(P\)\\\\ \\mathtt\{delHist\}\(P\+Q\)&=&\\mathtt\{delHist\}\(P\)\\textrm\{ if \}\\neg\\mathtt\{std\}\(P\)\\\\ \\mathtt\{delHist\}\(P\+Q\)&=&\\mathtt\{delHist\}\(Q\)\\textrm\{ if \}\\neg\\mathtt\{std\}\(Q\)\\\\ \\mathtt\{delHist\}\(P\\,\|\\,Q\)&=&\\mathtt\{delHist\}\(P\)\\,\|\\,\\mathtt\{delHist\}\(Q\)\\\\ \\mathtt\{delHist\}\(\(\\nu a\)P\)&=&\(\\nu a\)\\mathtt\{delHist\}\(P\)\\end\{array\}

The following proposition holds\.

###### Proposition 1

LetP,P′P,P^\{\\prime\}be CCSK processes, andQQa CCS process\. IfP→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}then𝚍𝚎𝚕𝙷𝚒𝚜𝚝\(P\)→𝛼c​c​s𝚍𝚎𝚕𝙷𝚒𝚜𝚝\(P′\)\\mathtt\{delHist\}\(P\)\\xrightarrow\{\\alpha\}\_\{ccs\}\\mathtt\{delHist\}\(P^\{\\prime\}\)\. If𝚍𝚎𝚕𝙷𝚒𝚜𝚝\(P\)→𝛼c​c​sQ\\mathtt\{delHist\}\(P\)\\xrightarrow\{\\alpha\}\_\{ccs\}Qthen there existsP′P^\{\\prime\}in CCSK such thatP→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}andQ=𝚍𝚎𝚕𝙷𝚒𝚜𝚝⁡\(P′\)Q=\\mathtt\{delHist\}\(P^\{\\prime\}\)\.

###### Proof

By rule inspection\.∎

### Bisimilarities for CCS

We start with the classical notion of CCS bisimilarity, extended as mentioned above\.

###### Definition 6\(Strong Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}on CCSK processes is a*strong bisimulation*if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

- •ifP→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ→𝛼Q′Q\\xrightarrow\{\\alpha\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\}\.

Let∼\\simbe the largest strong bisimulation\. Two CCSK processesP,QP,Qare*strongly bisimilar*if\(P,Q\)∈∼\(P,Q\)\\in\\sim\.

We give below some examples of strongly bisimilar processes\.

###### Example 2\(Strongly Bisimilar CCSK Processes\)

1. 1\.a\+a∼aa\+a\\sim a
2. 2\.a\|a∼a\.aa\\,\|\\,a\\sim a\.a
3. 3\.a⁡\[m\]∼b⁡\[n\]a\[m\]\\sim b\[n\]
4. 4\.a\|b∼a\.b\+b\.aa\\,\|\\,b\\sim a\.b\+b\.a

Note that Item[3](https://arxiv.org/html/2608.11531#S3.I4.i3)shows that strong bisimilarity \(like all other CCS bisimilarities\) abstracts away from the history\. Item[4](https://arxiv.org/html/2608.11531#S3.I4.i4)is actually an instance of the Expansion Law\[[15](https://arxiv.org/html/2608.11531#bib.bib3)\], a cornerstone of the theory of classical CCS bisimilarity, whose general form is as follows:

P1\|P2\\displaystyle P\_\{1\}\\,\|\\,P\_\{2\}=\\displaystyle=∑\{α\.\(P1′\|P2\):P1→𝛼P1′\}\+∑\{α\.\(P1\|P2′\):P2→𝛼P2′\}\+\\displaystyle\\sum\\\{\\alpha\.\(P^\{\\prime\}\_\{1\}\\,\|\\,P\_\{2\}\):P\_\{1\}\\xrightarrow\{\\alpha\}P^\{\\prime\}\_\{1\}\\\}\+\\sum\\\{\\alpha\.\(P\_\{1\}\\,\|\\,P^\{\\prime\}\_\{2\}\):P\_\{2\}\\xrightarrow\{\\alpha\}P^\{\\prime\}\_\{2\}\\\}\+∑\{τ\.\(P1′\|P2′\):P1→𝛼P1′,P2→α¯P2′,α≠τ\}\\displaystyle\\sum\\\{\\tau\.\(P^\{\\prime\}\_\{1\}\\,\|\\,P^\{\\prime\}\_\{2\}\):P\_\{1\}\\xrightarrow\{\\alpha\}P^\{\\prime\}\_\{1\},P\_\{2\}\\xrightarrow\{\\overline\{\\alpha\}\}P^\{\\prime\}\_\{2\},\\alpha\\neq\\tau\\\}where∑\\sumisnn\-ary choice\.

It is well\-known\[[19](https://arxiv.org/html/2608.11531#bib.bib2)\]that the Expansion Law does not hold for reversible calculi, and indeed we can provide a counterexample using strong forward\-reverse bisimilarity \(cf\. Def\.[9](https://arxiv.org/html/2608.11531#Thmdefinition9)and Ex\.[5](https://arxiv.org/html/2608.11531#Thmexample5)\)\.

In order to introduce weaker notions of bisimilarity we need the notation below\. Let⇒=\(→𝜏\)∗\\Rightarrow=\(\\xrightarrow\{\\tau\}\)^\{\*\}be the reflexive and transitive closure ofτ\\tausteps\.

###### Definition 7\(Weak Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}on CCSK processes is a*weak bisimulation*if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

- •ifP→𝜏P′P\\xrightarrow\{\\tau\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ⇒Q′Q\\Rightarrow Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\};
- •ifP→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}withα≠τ\\alpha\\neq\\tauthen there existsQ′Q^\{\\prime\}such thatQ⇒→𝛼⇒Q′Q\\Rightarrow\\xrightarrow\{\\alpha\}\\Rightarrow Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\}\.

Let≈\\approxbe the largest weak bisimulation\. Two CCSK processesP,QP,Qare*weakly bisimilar*if\(P,Q\)∈≈\(P,Q\)\\in\\approx\.

###### Example 3\(Weakly Bisimilar CCSK Processes\)

1. 1\.τ\.a≈a\\tau\.a\\approx a
2. 2\.a\+τ\.a≈aa\+\\tau\.a\\approx a
3. 3\.a⁡\[m\]≈b⁡\[n\]a\[m\]\\approx b\[n\]
4. 4\.a\|b≈a\.b\+b\.aa\\,\|\\,b\\approx a\.b\+b\.a

We introduce also an intermediate notion, taken from\[[16](https://arxiv.org/html/2608.11531#bib.bib17)\], whereτ\\tausteps need to be matched by at least oneτ\\taustep\.

###### Definition 8\(Semi\-Weak Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}on CCSK processes is a*semi\-weak bisimulation*if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

- •ifP→𝛼P′P\\xrightarrow\{\\alpha\}P^\{\\prime\}then there isQ′Q^\{\\prime\}such thatQ⇒→𝛼⇒Q′Q\\Rightarrow\\xrightarrow\{\\alpha\}\\Rightarrow Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\}\.

Let≅\\congbe the largest semi\-weak bisimulation\. Two CCSK processesP,QP,Qare semi\-weak bisimilar if\(P,Q\)∈≅\(P,Q\)\\in\\cong\.

###### Example 4\(Semi\-Weakly Bisimilar Processes\)

- •a\+a≅aa\+a\\cong a
- •a\|a≅a\.aa\\,\|\\,a\\cong a\.a
- •a⁡\[n\]≅b⁡\[m\]a\[n\]\\cong b\[m\]
- •a\+τ\.a≅τ\.aa\+\\tau\.a\\cong\\tau\.a

### Bisimilarities for CCSK

The bisimulations below make sense only in reversible calculi, since they consider both forward and backward transitions\. We start with the notion of \(revised\) forward\-reverse bisimulation from\[[12](https://arxiv.org/html/2608.11531#bib.bib1)\]\.

###### Definition 9\(Strong Forward\-Reverse Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}is a*strong forward\-reverse bisimulation*\(also called FR\-bisimulation\) if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

- •ifP→ϑxP′P\\xrightarrow\{\\vartheta\}\_\{x\}P^\{\\prime\}then there isQ′Q^\{\\prime\}such thatQ→ϑxQ′Q\\xrightarrow\{\\vartheta\}\_\{x\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\}\.

Let∼F​R\\sim\_\{FR\}be the largest FR\-bisimulation\. Two CCSK processesPP,QQare FR\-bisimilar if\(P,Q\)∈∼F​R\(P,Q\)\\in\\sim\_\{FR\}\.

###### Example 5\(FR Bisimilar Processes\)

- •a\+a∼F​Raa\+a\\sim\_\{FR\}a
- •a\|a≁F​Ra\.aa\\,\|\\,a\\not\\sim\_\{FR\}a\.a
- •a\|b≁F​Ra\.b\+b\.aa\\,\|\\,b\\not\\sim\_\{FR\}a\.b\+b\.a

As expected, instances of the Expansion Law do not hold any more\.

We now introduce notations to study the weak bisimulations in CCSK, and to manipulateτ\\tausteps easily\. Let⇒x=\(→𝜏x\)∗\\Rightarrow\_\{x\}=\(\\xrightarrow\{\\tau\}\_\{x\}\)^\{\*\}the reflexive and transitive closure ofτ\\tausteps in the directionxx\. Let mixedτ\\taureachability be⇒m=\(→𝜏f∪→𝜏r\)∗\\Rightarrow\_\{m\}=\(\\xrightarrow\{\\tau\}\_\{f\}\\cup\\xrightarrow\{\\tau\}\_\{r\}\)^\{\*\}\. This is an equivalence relation\. LetP​⇒𝜇m,x​P′P\\overset\{\\mu\}\{\\Rightarrow\}\_\{m,x\}P^\{\\prime\}iff∃Q,Q′s\.t\.\(P⇒mQ→𝜇xQ′⇒mP′\)\\exists Q,Q^\{\\prime\}\\text\{ s\.t\. \}\(P\\Rightarrow\_\{m\}Q\\xrightarrow\{\\mu\}\_\{x\}Q^\{\\prime\}\\Rightarrow\_\{m\}P^\{\\prime\}\)\.

We now define two variants of weak reversible bisimulation, which differ in whether theτ\\tausteps used to match some actionμ\\muneed to be in the same direction asμ\\muor not\.

###### Definition 10\(Weak Mixed Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}is a*weak mixed bisimulation*\(called mixed bisimulation\) if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

1. 1\.ifP→𝜏xP′P\\xrightarrow\{\\tau\}\_\{x\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ⇒mQ′Q\\Rightarrow\_\{m\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\};
2. 2\.ifP→𝜇xP′P\\xrightarrow\{\\mu\}\_\{x\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ​⇒𝜇m,x​Q′Q\\overset\{\\mu\}\{\\Rightarrow\}\_\{m,x\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\}\.

Let≈m\\approx\_\{m\}be the largest mixed weak bisimulation\. Two CCSK processesP,QP,Qare*weakly mixed bisimilar*if\(P,Q\)∈≈m\(P,Q\)\\in\\approx\_\{m\}\.

Intuitively, weak mixed bisimilarity abstracts away all theτ\\tausteps\.

###### Example 6\(Mixed Bisimilar Processes\)

- •τ\.a≈ma\\tau\.a\\approx\_\{m\}a
- •τ\|a≈ma\\tau\\,\|\\,a\\approx\_\{m\}a
- •τ\+a≈ma\\tau\+a\\approx\_\{m\}a
- •τ\[m\]\+a≈ma\\tau\[m\]\+a\\approx\_\{m\}a

We also introduce a ”directional” weak bisimulation, in which theτ\\tausteps have to be in the same direction as the actionμ\\mu\. LetP​⇒𝜇d,x​P′P\\overset\{\\mu\}\{\\Rightarrow\}\_\{d,x\}P^\{\\prime\}iff∃Q,Q′s\.t\.\(P⇒xQ→𝜇xQ′⇒xP′\)\\exists Q,Q^\{\\prime\}\\text\{ s\.t\. \}\(P\\Rightarrow\_\{x\}Q\\xrightarrow\{\\mu\}\_\{x\}Q^\{\\prime\}\\Rightarrow\_\{x\}P^\{\\prime\}\)\.

###### Definition 11\(Weak Directional Bisimulation\)\.

A symmetric relationℛ\\mathrel\{\\mathcal\{R\}\}is a*weak directional bisimulation*\(called directional bisimulation\) if wheneverPℛQP\\mathrel\{\\mathcal\{R\}\}Q:

1. 1\.ifP→𝜏xP′P\\xrightarrow\{\\tau\}\_\{x\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ⇒xQ′Q\\Rightarrow\_\{x\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\};
2. 2\.ifP→𝜇xP′P\\xrightarrow\{\\mu\}\_\{x\}P^\{\\prime\}then there existsQ′Q^\{\\prime\}such thatQ​⇒𝜇d,x​Q′Q\\overset\{\\mu\}\{\\Rightarrow\}\_\{d,x\}Q^\{\\prime\}andP′ℛQ′P^\{\\prime\}\\mathrel\{\\mathcal\{R\}\}Q^\{\\prime\};

Let≈d\\approx\_\{d\}be the largest directional bisimulation\. Two CCSK processesP,QP,Qare directionally bisimilar if\(P,Q\)∈≈d\(P,Q\)\\in\\approx\_\{d\}\.

###### Example 7\(Directionally Bisimilar Processes\)

- •τ\.a≈da\\tau\.a\\approx\_\{d\}a
- •τ\|a≈da\\tau\\,\|\\,a\\approx\_\{d\}a
- •τ\+a≉da\\tau\+a\\not\\approx\_\{d\}a

## 4Relations between Bisimilarities

We now compare the notions of bisimilarity introduced in the previous section\. Interestingly, the considered notions give rise to two hierarchies\.

###### Proposition 2\(Hierarchies of Bisimilarities\)

1. 1\.∼F​R⊂∼⊂≅⊂≈\\sim\_\{FR\}\\subset\\sim\\subset\\cong\\subset\\approx;
2. 2\.∼F​R⊂≈d⊂\{≈m≈\\sim\_\{FR\}\\subset\\approx\_\{d\}\\subset\\begin\{cases\}\\approx\_\{m\}\\\\ \\approx\\end\{cases\}\.

###### Proof

Inclusions follow directly from the definitions\. The proof of their strictness will actually be deferred to Proposition[3](https://arxiv.org/html/2608.11531#Thmproposition3), providing witnesses for each of them\.∎

∼F​R\\sim\_\{FR\}∼\\sim≅\\cong≈\\approx≈d\\approx\_\{d\}≈m\\approx\_\{m\}123456789101111Figure 3:Hierarchies of bisimilaritiesThe first hierarchy relates strong forward\-reverse bisimilarity to CCS bisimilarities\. The second hierarchy instead focuses on reversible bisimilarities\. Note that≈d\\approx\_\{d\}is included in both≈m\\approx\_\{m\}and≈\\approx\(hence in their intersection\)\. The two hierarchies are graphically represented in Fig\.[3](https://arxiv.org/html/2608.11531#S4.F3)\. The relations are written just inside the elliptical set they represent\. The lines on the set for≈d\\approx\_\{d\}are just a visual help to distinguish the corresponding ellipse\.

We now show that there are no other inclusions beyond the ones in Proposition[2](https://arxiv.org/html/2608.11531#Thmproposition2), and that all the inclusions there are actually strict\. Graphically, it means that all the areas in Figure[3](https://arxiv.org/html/2608.11531#S4.F3)are not empty\. We show this by providing examples of pairs of processes in each of them\. Notably, all the examples are made of standard processes, hence none of these notions collapse when restricting the attention to standard processes\. In other words, all these notions induce different equivalence relations on CCS processes\.

###### Proposition 3\(Hierarchies are Strict on Standard Processes\)

All the areas in Fig\.[3](https://arxiv.org/html/2608.11531#S4.F3)are not empty, and each of them contains at least a pair of standard processes\.

###### Proof

The ones below are witnesses for every area\.

1. 1\.∼F​R:\(a\+a,a\)\\sim\_\{FR\}\\ :\\ \(a\+a,a\)\. The twoaas are indistinguishable\.
2. 2\.\(∼∩≈d\)\\∼F​R:\(τ\.τ\.\(a\.b\+b\.a\)\+τ\.\(a\|b\),τ\.τ\.\(a\|b\)\+τ\.\(a\.b\+b\.a\)\)\(\\sim\\cap\\approx\_\{d\}\)\\backslash\\sim\_\{FR\}\\ :\\ \(\\tau\.\\tau\.\(a\.b\+b\.a\)\+\\tau\.\(a\\,\|\\,b\),\\ \\tau\.\\tau\.\(a\\,\|\\,b\)\+\\tau\.\(a\.b\+b\.a\)\)\. We have thata\.b\+b\.a∼a\|ba\.b\+b\.a\\sim a\\,\|\\,bis an instance of the expansion law, but the same equivalence is not valid for∼F​R\\sim\_\{FR\}\. Under≈d\\approx\_\{d\}one can use equal subterms to match the challenge since they can be reached by taking a different number ofτ\\tausteps\.
3. 3\.\(∼∩≈m\)\\≈d:\(τ\.\(\(a\.b\+b\.a\)\+\(c\|d\)\)\+τ\.\(\(a\|b\)\+τ\.\(c\.d\+d\.c\)\),τ\.\(\(a\|b\)\+τ\.\(c\|d\)\)\+τ\.\(\(a\.b\+b\.a\)\+\(c\.d\+d\.c\)\)\(\\sim\\cap\\approx\_\{m\}\)\\backslash\\approx\_\{d\}\\ :\\ \(\\tau\.\(\(a\.b\+b\.a\)\+\(c\\,\|\\,d\)\)\+\\tau\.\(\(a\\,\|\\,b\)\+\\tau\.\(c\.d\+d\.c\)\),\\ \\tau\.\(\(a\\,\|\\,b\)\+\\tau\.\(c\\,\|\\,d\)\)\+\\tau\.\(\(a\.b\+b\.a\)\+\(c\.d\+d\.c\)\)\. The equivalence holds under∼\\simthanks to the expansion law\. It holds also under≈m\\approx\_\{m\}since the choice of whichτ\\tauto execute can always be undone to select the desired branch\. This is not the case under≈d\\approx\_\{d\}where on the left one can reach a state where the only forward actions enabled are fromc\.d\+d\.cc\.d\+d\.c, while on the right no such state exists \(ifc\.d\+d\.cc\.d\+d\.cis forward enabled, then alsoa\.b\+b\.aa\.b\+b\.ais enabled\)\.
4. 4\.∼\\≈m:\(a\|b,a\.b\+b\.a\)\\sim\\backslash\\approx\_\{m\}\\ :\\ \(a\\,\|\\,b,\\ a\.b\+b\.a\)\. We use again an instance of the expansion law\.
5. 5\.≅\\\(∼∪≈m\):\(b\|\(a\+a\.τ\),a\.\(τ\|b\)\+a\.b\+b\.a\.τ\)\\cong\\backslash\(\\sim\\cup\\approx\_\{m\}\)\\ :\\ \(b\\,\|\\,\(a\+a\.\\tau\),\\ a\.\(\\tau\\,\|\\,b\)\+a\.b\+b\.a\.\\tau\)\. This fails under≈m\\approx\_\{m\}, since the right hand side has noa\|ba\\,\|\\,bto match the left hand side one\. This fails under∼\\simsince on the right if one starts frombb, there is no way to avoid aτ\\tau, while this can be avoided on the left\. This is not an issue under≅\\congsince theaawithoutτ\\taucan be matched by executing bothaaandτ\\tau\.
6. 6\.≈\\\(≅∪≈m\):\(a\.τ\|b,a\.b\+b\.a\)\\approx\\backslash\(\\cong\\cup\\approx\_\{m\}\)\\ :\\ \(a\.\\tau\\,\|\\,b,\\ a\.b\+b\.a\)\. This holds under≈\\approxthanks to the expansion law and since theτ\\taucan be abstracted away\. Instead, the expansion law fails under≈m\\approx\_\{m\}and theτ\\tauneeds to be matched by anotherτ\\tauunder≅\\cong\.
7. 7\.\(≅∩≈d\)\\∼:\(a\+a\.τ,a\.τ\)\(\\cong\\cap\\approx\_\{d\}\)\\backslash\\sim\\ :\\ \(a\+a\.\\tau,\\ a\.\\tau\)\. This fails under∼\\simsince on the left executing anaaleads to a state where noτ\\taucan be performed\. This is not an issue for≈d\\approx\_\{d\}where theτ\\taucan be matched by staying idle\. For≅\\cong, leftaacan be matched by executing bothaaandτ\\tau\.
8. 8\.≈d\\≅:\(τ,0\)\\approx\_\{d\}\\backslash\\cong\\ :\\ \(\\tau,\\ 0\)\. This fails under≅\\congsince theτ\\taucannot be matched, instead under≈d\\approx\_\{d\}theτ\\taucan be matched by staying idle\.
9. 9\.\(≈∩≈m\)\\\(≅∪≈d\):\(τ\.\(\(a\.b\+b\.a\)\+\(c\|d\)\)\+τ\.\(\(a\|b\)\+τ\.\(c\.d\+d\.c\)\)\+τ,τ\.\(\(a\|b\)\+τ\.\(c\|d\)\)\+τ\.\(\(a\.b\+b\.a\)\+\(c\.d\+d\.c\)\)\+τ\.τ\(\\approx\\cap\\approx\_\{m\}\)\\backslash\(\\cong\\cup\\approx\_\{d\}\)\\ :\\newline \(\\tau\.\(\(a\.b\+b\.a\)\+\(c\\,\|\\,d\)\)\+\\tau\.\(\(a\\,\|\\,b\)\+\\tau\.\(c\.d\+d\.c\)\)\+\\tau,\\ \\tau\.\(\(a\\,\|\\,b\)\+\\tau\.\(c\\,\|\\,d\)\)\+\\tau\.\(\(a\.b\+b\.a\)\+\(c\.d\+d\.c\)\)\+\\tau\.\\tau\. This holds under≈\\approxthanks to the expansion law, and sinceτ\\tauandτ\.τ\\tau\.\\tauare weakly bisimilar\. However, the latter are not semi\-weakly bisimilar, hence≅\\congfails\. Also, this holds under≈m\\approx\_\{m\}, since it abstracts away fromτ\\tauactions\.≈d\\approx\_\{d\}fails as well, for the same reason as in item[3](https://arxiv.org/html/2608.11531#S4.I2.i3)\.
10. 10\.≈m\\≈:\(a,a\+τ\)\\approx\_\{m\}\\backslash\\approx\\ :\\ \(a,\\ a\+\\tau\)\. This is well\-known not to hold under≈\\approx\. Instead under≈m\\approx\_\{m\}theτ\\taustep can be mimicked by staying idle since theaaaction remains enabled also after theτ\\tau, since theτ\\taucan be undone to doaa\.
11. 11\.\(≅∩≈m\)\\\(∼∪≈d\):\(τ\.\(a\.b\+b\.a\+τ\+τ\.τ\)\+\(a\|b\),τ\.\(a\.b\+b\.a\+\(a\|b\)\+τ\.τ\)\)\(\\cong\\cap\\approx\_\{m\}\)\\backslash\(\\sim\\cup\\approx\_\{d\}\)\\ :\\ \(\\tau\.\(a\.b\+b\.a\+\\tau\+\\tau\.\\tau\)\+\(a\\,\|\\,b\),\\tau\.\(a\.b\+b\.a\+\(a\\,\|\\,b\)\+\\tau\.\\tau\)\)\. This fails under∼\\simsinceτ\.τ\\tau\.\\tauis not matched on the right, since afterwards a thirdτ\\tauwould be enabled\. This fails under≈d\\approx\_\{d\}since after the firstτ\\tauwe can still go to\(a\|b\)\(a\\,\|\\,b\)on the right, but not on the left\. This succeeds under≈m\\approx\_\{m\}sinceτ\\taus are abstracted away, and terms withoutτ\\taus are identical\. This succeeds under≅\\congsinceτ\\taus can always be matched, and thanks to the expansion law\. ∎

If instead of considering only pairs of standard processes we consider only pairs of non\-standard processes, then all the areas remain non\-empty\.

###### Proposition 4

Each of the areas in Fig\.[3](https://arxiv.org/html/2608.11531#S4.F3)contains at least a pair of non\-standard processes\.

###### Proof

One can take the witnesses from the proof of Proposition[3](https://arxiv.org/html/2608.11531#Thmproposition3)add aτ⁡\[n\]\\tau\[n\]prefix in front of both processes to obtain witnesses made of non\-standard processes\. ∎

Finally, if we consider pairs made of a non\-standard process and a standard one, then∼F​R\\sim\_\{FR\}becomes empty\. The other areas remain non\-empty\.

###### Proposition 5

Each of the areas in Fig\.[3](https://arxiv.org/html/2608.11531#S4.F3)contains at least a pair made of a non\-standard process and a standard one, but for the area 1, corresponding to∼F​R\\sim\_\{FR\}\.

###### Proof

The area for∼F​R\\sim\_\{FR\}is empty since∼F​R\\sim\_\{FR\}can always distinguish a non\-standard process, that can make a backward move, from a standard one, that cannot\. For the others, one can take the witnesses from the proof of Proposition[3](https://arxiv.org/html/2608.11531#Thmproposition3)add aτ⁡\[n\]\\tau\[n\]prefix in front of only one of the two components\. This preserves all the CCS bisimilarities, which cannot observe the history, as well as the weak CCSK bisimilarities, where the backwardτ⁡\[n\]\\tau\[n\]can be matched by the other process by staying idle\. ∎

## 5Congruence Properties of Bisimilarities

We first discuss whether the considered equivalences are congruences or not, namely in the case of strong CCS bisimilarity whetherP∼Q⟹C⁡\[P\]∼C⁡\[Q\]P\\sim Q\\implies C\[P\]\\sim C\[Q\]\. Note that this implication makes sense only if all the involved processes are well\-formed, hence we only consider this case\.

Strong bisimilarity is a congruence in CCS\[[15](https://arxiv.org/html/2608.11531#bib.bib3)\]\. Somehow surprisingly, its extension to CCSK is not a congruence, as shown in the counterexample below\.

###### Example 8\(∼\\simis not a congruence\)

τ⁡\[n\]∼0／⟹a\+τ⁡\[n\]∼a\+0\\tau\[n\]\\sim 0\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\implies\}\}\}a\+\\tau\[n\]\\sim a\+0Processes on the left are strongly bisimilar since∼\\simabstracts away from the history\. Processes on the right are not strongly bisimilar sincea\+τ⁡\[n\]a\+\\tau\[n\]cannot execute any forward move, whilea\+0a\+0can executeaa\.

The key point here is that forward equivalences abstract away from the history, but adding a choice where the added branch is a non\-standard process disables the other branch \(which needs to be standard to ensure well\-formedness\)\. Thus, the same issue also occurs for the other forward equivalences we consider, namely weak \(≈\\approx\) and semi\-weak \(≅\\cong\) bisimilarities, as stated below\.

###### Proposition 6\(Forward equivalences are not congruences in CCSK\)

None of∼\\sim,≈\\approxand≅\\congare congruences on CCSK terms\.

###### Proof

Counterexample[8](https://arxiv.org/html/2608.11531#Thmexample8)proves the thesis for all the equivalences\.∎

Note that for≈\\approxthe usual problem of CCS thatτ\.a≈a／⟹τ\.a\+b≈a\+b\\tau\.a\\approx a\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\implies\}\}\}\\tau\.a\+b\\approx a\+bremains\. However,≅\\congis a congruence in CCS\[[16](https://arxiv.org/html/2608.11531#bib.bib17)\], but not in CCSK for the reason above\.

Concerning reversible equivalences,∼F​R\\sim\_\{FR\}has been proved to be a congruence in\[[12](https://arxiv.org/html/2608.11531#bib.bib1), Proposition 4\.9\]\. Instead, for weak directional bisimilarity a problem similar to the one above occurs\.

###### Proposition 7\(Weak directional bisimilarity is not a congruence\)

≈d\\approx\_\{d\}is not a congruence on CCSK terms\.

###### Proof

The following counterexample proves the thesis: τ\[n\]≈d0／⟹a\+τ\[n\]≈da\+0\\tau\[n\]\\approx\_\{d\}0\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.75pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 2\.625pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\implies\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 1\.875pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\implies\}\}\}a\+\\tau\[n\]\\approx\_\{d\}a\+0∎

This is not the case for weak mixed bisimilarity, which, somehow surprisingly is a congruence\. In order to clarify why this is the case, we first show a property of≈m\\approx\_\{m\}which rules out counterexamples as the ones above\.

###### Proposition 8

AssumeP≈mQP\\approx\_\{m\}QwherePPis standard\. ThenQ⇒mQ′Q\\Rightarrow\_\{m\}Q^\{\\prime\}withQ′Q^\{\\prime\}standard\.

###### Proof

Assume towards a contradiction that there is no suchQ′Q^\{\\prime\}\. By definition, we haveQ\(→𝜃r\)∗𝚝𝚘𝚂𝚝𝚍\(Q\)Q\(\\xrightarrow\{\\theta\}\_\{r\}\)^\{\*\}\\mathtt\{toStd\}\(Q\)\. At least one of the steps is not aτ\\tau, otherwise we would have proven the thesis\. Let us take the first such action\. ThenQQcan perform a backward non\-τ\\tauaction\. However, such an action cannot be matched byPP, sincePPis standard \(and executingτ\\tausteps only enables backwardτ\\tausteps, while we need to match a non\-τ\\taubackward action\)\. ∎

We also show that indeed weak mixed bisimilarity completely abstracts away fromτ\\tausteps\.

###### Proposition 9\(Weak mixed bisimilarity abstracts away fromτ\\tausteps\)

P⇒mQP\\Rightarrow\_\{m\}QimpliesP≈mQP\\approx\_\{m\}Q\.

###### Proof

Thanks to the Loop Lemma \(cf\.\[[19](https://arxiv.org/html/2608.11531#bib.bib2), Prop\. 5\.1\]\), we also haveQ⇒mPQ\\Rightarrow\_\{m\}P\. Hence, any challenge fromPPcan be matched byQQby first reducing toPP, and vice versa\.∎

Note that even ifP⇒mQP\\Rightarrow\_\{m\}QandP≈mQP\\approx\_\{m\}Qare both equivalence relations, they do not coincide\. E\.g\.,a\+a≈maa\+a\\approx\_\{m\}a, buta\+a／⇒maa\+a\{\\mathchoice\{\\mathrel\{\\hbox to0\.0pt\{\\kern 5\.0pt\\kern\-5\.27776pt$\\displaystyle\\not$\\hss\}\{\\Rightarrow\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 5\.0pt\\kern\-5\.27776pt$\\textstyle\\not$\\hss\}\{\\Rightarrow\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.98611pt\\kern\-4\.45831pt$\\scriptstyle\\not$\\hss\}\{\\Rightarrow\}\}\}\{\\mathrel\{\\hbox to0\.0pt\{\\kern 3\.40282pt\\kern\-3\.95834pt$\\scriptscriptstyle\\not$\\hss\}\{\\Rightarrow\}\}\}\}\_\{m\}a\.

###### Theorem 5\.1\(Weak mixed bisimilarity is a congruence\)

≈m\\approx\_\{m\}is a congruence on CCSK terms\.

###### Proof

We prove the thesis by induction on the structure of the context, with a case for each operator\. Cases for prefix and restriction are trivial\. Let us consider choice and parallel composition\.

Choice:we have to show that ifP≈mQP\\approx\_\{m\}QthenP\+R≈mQ\+RP\+R\\approx\_\{m\}Q\+R\. Note that at most one amongPPandRRcan be non\-standard due to well\-formedness\. Assume first bothPPandRRare standard\. If the challenge is fromPP, thenQQinsideQ\+RQ\+Rcan match the challenge with the same sequence of moves used inQQalone, all lifted thanks to rule \(CHOICE\)\. IfRRmoves, andQQis standard, then the very same moves can be performed in both the cases, again using rule \(CHOICE\) to lift them\. IfQQis not standard, thanks to Proposition[8](https://arxiv.org/html/2608.11531#Thmproposition8)above, we can first reduceQQto𝚝𝚘𝚂𝚝𝚍⁡\(Q\)\\mathtt\{toStd\}\(Q\), and then match the moves fromRRas above\. Note thatQQand𝚝𝚘𝚂𝚝𝚍⁡\(Q\)\\mathtt\{toStd\}\(Q\)are mixed bisimilar thanks to Proposition[9](https://arxiv.org/html/2608.11531#Thmproposition9), hence the reduction preserves mixed bisimilarity\. Assume nowPPis non\-standard\. Then onlyPPcan move, and transitions can be lifted using rule \(CHOICE\) since by well\-formednessRRis standard\. Assume nowRRis non\-standard\. Analogously to the above, onlyRRcan move, in both the cases sincePPandQQneed to be standard due to well\-formedness\.

Parallel composition:we have to show that ifP≈mQP\\approx\_\{m\}QthenP\|R≈mQ\|RP\\,\|\\,R\\approx\_\{m\}Q\\,\|\\,R\. AssumeP\|R→𝛼fP\\,\|\\,R\\xrightarrow\{\\alpha\}\_\{f\}\. There are three subcases depending on which component contributes to the transition\.

Transition fromPP:QQcan match the transition, and the matching computation can be lifted toQ\|RQ\\,\|\\,Rthanks to rule \(PAR\)\.

Transition fromRR:the same transitions can be done on both the sides, remaining in the relation\.

Synchronization:QQcan match transitions fromPPby hypothesis, and transitions fromRRcan be performed on both the sides\. This includes the components of the transitions that give rise to the synchronization\. Hence we stay in the relation\.

The case of backward transitions is analogous\.

∎

We believe that the notion of mixed bisimilarity is very relevant\. Indeed it provides a notion of bisimilarity which completely abstracts away fromτ\\tauactions, which is coinductive \(since it can be formulated as a bisimulation\), and which is a congruence\. We are not aware of any other notion of bisimilarity which has all these properties\.

While leaving a more detailed analysis of this equivalence for future work, we discuss here some relevant axioms enabling to axiomatically reason on this equivalence\. Notice that it makes sense to discuss about axioms since mixed bisimilarity is a congruence\.

Various correct axioms for∼F​R\\sim\_\{FR\}have been proposed in\[[12](https://arxiv.org/html/2608.11531#bib.bib1), Theorem 4\.10\]\. While trivially all these axioms are correct also for≈m\\approx\_\{m\}, we focus here on axioms which are specific of weak mixed bisimilarity\.

The axioms in Fig\.[4](https://arxiv.org/html/2608.11531#S5.F4)hold for weak mixed bisimilarity\.

###### Theorem 5\.2

The axioms in Figure[4](https://arxiv.org/html/2608.11531#S5.F4)are correct w\.r\.t\. weak mixed bisimilarity\.

###### Proof

τ\\taumoves can always be matched by the other process by staying idle, while moves fromPPcan be matched by first doing or undoingτ\\tausteps as needed\. Note that executingτ\\tau\-steps moves from the top\-3 rows to the bottom ones\. ∎

τ\.P\\displaystyle\\tau\.P=P\\displaystyle=P\(TAU\-PREF\-M\)τ\+P\\displaystyle\\tau\+P=P\\displaystyle=P\(TAU\-CH\-M\)τ\|P\\displaystyle\\tau\\,\|\\,P=P\\displaystyle=P\(TAU\-PAR\-M\)τ⁡\[n\]\.P\\displaystyle\\tau\[n\]\.P=P\\displaystyle=P\(TAU\-PREF\-K\)τ⁡\[n\]\+P\\displaystyle\\tau\[n\]\+P=P\\displaystyle=P\(TAU\-CH\-K\)τ⁡\[n\]\|P\\displaystyle\\tau\[n\]\\,\|\\,P=P\\displaystyle=P\(TAU\-PAR\-K\)Figure 4:CCSK axioms for weak mixed bisimilarity≈m\\approx\_\{m\}The axioms in Fig\.[4](https://arxiv.org/html/2608.11531#S5.F4)are aligned with Proposition[9](https://arxiv.org/html/2608.11531#Thmproposition9)in showing that mixed bisimilarity completely abstracts away fromτ\\tausteps\.

We remark that as shown in Figure[3](https://arxiv.org/html/2608.11531#S4.F3), axioms which hold for weak bisimilarity≈\\approxdo not necessarily hold for≈m\\approx\_\{m\}\. Let us now discuss the well\-known Milnerτ\\tau\-laws of weak bisimilarity \(collected in Fig\.[5](https://arxiv.org/html/2608.11531#S5.F5)\)\. The laws \(TAU\-CH\) and \(TAU\-SEQ\) follow directly from \(TAU\-PREF\-M\), and idempotence of \+ for the former\.

Instead \(TAU\-DUPL\-CH\) fails, as shown below\.

###### Example 9\(\(TAU\-DUPL\-CH\) does not hold\)

Consider the right\-hand side challenge:

α\.\(P\+τ\.Q\)\+α\.Q→α⁡\[n\]fα\.\(P\+τ\.Q\)\+α\[n\]\.Q\\alpha\.\(P\+\\tau\.Q\)\+\\alpha\.Q\\xrightarrow\{\\alpha\[n\]\}\_\{f\}\\alpha\.\(P\+\\tau\.Q\)\+\\alpha\[n\]\.QThere are two possible answers from the left\-hand side, namely:

α\.\(P\+τ\.Q\)\\displaystyle\\alpha\.\(P\+\\tau\.Q\)→α⁡\[n\]fα\[n\]\.\(P\+τ\.Q\)\\displaystyle\\xrightarrow\{\\alpha\[n\]\}\_\{f\}\\alpha\[n\]\.\(P\+\\tau\.Q\)→α⁡\[n\]f→τ⁡\[m\]fα\[n\]\.\(P\+τ\[m\]\.Q\)\\displaystyle\\xrightarrow\{\\alpha\[n\]\}\_\{f\}\\xrightarrow\{\\tau\[m\]\}\_\{f\}\\alpha\[n\]\.\(P\+\\tau\[m\]\.Q\)\(We can also reach the same states after having undone and redone multiple times theτ\\taustep\.\) In both the cases, actions fromPPare enabled, directly in the first case, and by first undoingτ⁡\[m\]\\tau\[m\]in the second case\. However, no action fromPPcan be executed in the right\-hand side above, since we need to undo oneα⁡\[n\]\\alpha\[n\]and doα\\alphaon the other side\.

P\+τ\.P\\displaystyle P\+\\tau\.P=τ\.P\\displaystyle=\\tau\.P\(TAU\-CH\)α\.τ\.P\\displaystyle\\alpha\.\\tau\.P=α\.P\\displaystyle=\\alpha\.P\(TAU\-SEQ\)α\.\(P\+τ\.Q\)\\displaystyle\\alpha\.\(P\+\\tau\.Q\)=α\.\(P\+τ\.Q\)\+α\.Q\\displaystyle=\\alpha\.\(P\+\\tau\.Q\)\+\\alpha\.Q\(TAU\-DUPL\-CH\)Figure 5:τ\\taulaws for weak bisimilarity≈\\approx
## 6Conclusion and Future Work

In this paper, we contrasted different notions of bisimilarity for CCSK processes, including two definitions of weak bisimilarities not previously discussed in the literature\. We also proved that none of these notions are equivalent, not even if we restrict to standard processes only\. Notably, weak mixed bisimilarity turns out to be coinductive, to be a congruence, and to completely abstract away fromτ\\tau\-steps, making it a very interesting equivalence\.

We hope that these results can be the basis of a more detailed study of bisimilarities in CCSK\. We remark that such a deeper understanding may also impact classical concurrency theory, since there are strong relations\[[1](https://arxiv.org/html/2608.11531#bib.bib18),[2](https://arxiv.org/html/2608.11531#bib.bib20)\]between reversible strong bisimilarities and history\-preserving\[[21](https://arxiv.org/html/2608.11531#bib.bib19)\]and hereditary history\-preserving\[[3](https://arxiv.org/html/2608.11531#bib.bib21)\]bisimilarities\. Also, weak mixed bisimilarity induces an equivalence on CCS, which is a congruence and abstracts away fromτ\\tausteps\. Notice however that its current definition is not coinductive in CCS, since it relies on CCSK terms\.

We present now a few other items for future research\. First, we remark that while giving correct axioms for weak mixed bisimilarity, we have not provided a complete axiomatization\. This is definitely a relevant item for future work \(given the interesting properties of weak mixed bisimilarity\) but not easy\. Indeed, there are no complete axiomatizations for forward\-reverse bisimilarity either, which we expect to be needed as first step before tackling the mixed case\.

Another interesting item would be to understand how other bisimilarities, and more in general behavioral equivalences, can be extended from CCS to CCSK\. Given that reversibility provides quite a strong observational power \(as shown by the relations with history\-preserving and hereditary history\-preserving bisimilarities\), it may be the case that some of them collapse\.

## References

- \[1\]C\. Aubert and I\. Cristescu\(2020\)How reversibility can solve traditional questions: the example of hereditary history\-preserving bisimulation\.In31st International Conference on Concurrency Theory, CONCUR 2020, Vienna, Austria \(Virtual Conference\), September 1\-4, 2020,I\. Konnov and L\. Kovács \(Eds\.\),LIPIcs, Vol\.171,pp\. 7:1–7:23\.External Links:[Link](https://doi.org/10.4230/LIPIcs.CONCUR.2020.7),[Document](https://dx.doi.org/10.4230/LIPICS.CONCUR.2020.7)Cited by:[§6](https://arxiv.org/html/2608.11531#S6.p2.1)\.
- \[2\]C\. Aubert, I\. Phillips, and I\. Ulidowski\(2026\)Bisimulations and reversibility\.InComponents Operationally: Reversibility and System Engineering: Essays Dedicated to Jean\-Bernard Stefani on the Occasion of His 65th Birthday,C\. A\. Mezzina and A\. Schmitt \(Eds\.\),Lecture Notes in Computer Science, Vol\.16065,pp\. 46–67\.External Links:[Link](https://doi.org/10.1007/978-3-031-99717-4/_3),[Document](https://dx.doi.org/10.1007/978-3-031-99717-4%5F3)Cited by:[§6](https://arxiv.org/html/2608.11531#S6.p2.1)\.
- \[3\]M\.A\. Bednarczyk\(1991\)Hereditary history preserving bisimulations or what is the power of the future perfect in program logics\.Technical reportPolish Academy of Sciences\.Cited by:[§6](https://arxiv.org/html/2608.11531#S6.p2.1)\.
- \[4\]L\. Cardelli and C\. Laneve\(2011\)Reversibility in massive concurrent systems\.Scientific Annals of Computer Science21\(2\),pp\. 175\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[5\]C\. D\. Carothers, K\. S\. Perumalla, and R\. M\. Fujimoto\(1999\)Efficient optimistic parallel simulations using reverse computation\.ACM Transactions on Modeling and Computer Simulation \(TOMACS\)9\(3\),pp\. 224–253\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[6\]I\. Cristescu, J\. Krivine, and D\. Varacca\(2013\)A compositional semantics for the reversibleπ\\pi\-calculus\.In28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25\-28, 2013,pp\. 388–397\.External Links:[Link](https://doi.org/10.1109/LICS.2013.45),[Document](https://dx.doi.org/10.1109/LICS.2013.45)Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[7\]V\. Danos and J\. Krivine\(2004\)Reversible communicating systems\.InInternational Conference on Concurrency Theory,pp\. 292–307\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1),[§2](https://arxiv.org/html/2608.11531#S2.p11.1)\.
- \[8\]J\. Engblom\(2012\)A review of reverse debugging\.InProceedings of the 2012 System, Software, SoC and Silicon Debug Conference,pp\. 1–6\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[9\]R\. Landauer\(1961\)Irreversibility and heat generation in the computing process\.IBM journal of research and development5\(3\),pp\. 183–191\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[10\]I\. Lanese, N\. Nishida, A\. Palacios, and G\. Vidal\(2018\)A theory of reversibility for Erlang\.J\. Log\. Algebraic Methods Program\.100,pp\. 71–97\.External Links:[Link](https://doi.org/10.1016/j.jlamp.2018.06.004),[Document](https://dx.doi.org/10.1016/J.JLAMP.2018.06.004)Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[11\]I\. Lanese, N\. Nishida, A\. Palacios, and G\. Vidal\(2018\)CauDEr: a causal\-consistent reversible debugger for Erlang\.InInternational Symposium on Functional and Logic Programming,pp\. 247–263\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[12\]I\. Lanese and I\. Phillips\(2021\)Forward\-reverse observational equivalences in CCSK\.InRC,Lecture Notes in Computer Science,pp\. 126–143\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-79837-6%5F8)Cited by:[§2](https://arxiv.org/html/2608.11531#S2.p6.1),[§3](https://arxiv.org/html/2608.11531#S3.SS0.SSSx2.p1.1),[§5](https://arxiv.org/html/2608.11531#S5.p11.1),[§5](https://arxiv.org/html/2608.11531#S5.p5.1)\.
- \[13\]J\. McNellis, J\. Mola, and K\. Sykes\(2017\)Time travel debugging: root causing bugs in commercial scale software\. CppCon talk\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[14\]R\. Milner\(1980\)A calculus of communicating systems\.Lecture Notes in Computer Science, Vol\.92,Springer\.External Links:[Link](https://doi.org/10.1007/3-540-10235-3),[Document](https://dx.doi.org/10.1007/3-540-10235-3),ISBN 3\-540\-10235\-3Cited by:[§3](https://arxiv.org/html/2608.11531#S3.p3.1),[footnote 1](https://arxiv.org/html/2608.11531#footnote1)\.
- \[15\]R\. Milner\(1989\)Communication and concurrency\.Prentice\-Hall, Inc\.\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p2.1),[§3](https://arxiv.org/html/2608.11531#S3.SS0.SSSx1.p3.1),[§5](https://arxiv.org/html/2608.11531#S5.p2.1)\.
- \[16\]U\. Montanari and V\. Sassone\(1991\)CCS dynamic bisimulation is progressing\.InMathematical Foundations of Computer Science 1991, 16th International Symposium, MFCS’91, Kazimierz Dolny, Poland, September 9\-13, 1991, Proceedings,A\. Tarlecki \(Ed\.\),Lecture Notes in Computer Science, Vol\.520,pp\. 346–356\.External Links:[Link](https://doi.org/10.1007/3-540-54345-7/_78),[Document](https://dx.doi.org/10.1007/3-540-54345-7%5F78)Cited by:[§3](https://arxiv.org/html/2608.11531#S3.SS0.SSSx1.p6.1),[§5](https://arxiv.org/html/2608.11531#S5.p4.1)\.
- \[17\]S\. Oguchi, S\. Yuen, and N\. Yoshida\(2025\)RevMiGo: reversible channel\-based communication in Go language\.InReversible Computation \- 17th International Conference, RC 2025, Odense, Denmark, July 3\-4, 2025, Proceedings,R\. Glück and R\. Kaarsgaard \(Eds\.\),Lecture Notes in Computer Science, Vol\.15716,pp\. 119–127\.External Links:[Link](https://doi.org/10.1007/978-3-031-97063-4/_9),[Document](https://dx.doi.org/10.1007/978-3-031-97063-4%5F9)Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[18\]I\. Phillips, I\. Ulidowski, and S\. Yuen\(2012\)A reversible process calculus and the modelling of the ERK signalling pathway\.InInternational Workshop on Reversible Computation,pp\. 218–232\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1)\.
- \[19\]I\. Phillips and I\. Ulidowski\(2007\)Reversing algebraic process calculi\.The Journal of Logic and Algebraic Programming73\(1\-2\),pp\. 70–96\.Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p1.1),[§1](https://arxiv.org/html/2608.11531#S1.p2.1),[§2](https://arxiv.org/html/2608.11531#S2.p1.1),[§2](https://arxiv.org/html/2608.11531#S2.p11.1),[§3](https://arxiv.org/html/2608.11531#S3.SS0.SSSx1.p4.1),[Proof](https://arxiv.org/html/2608.11531#Thmproofx9.p1.1)\.
- \[20\]D\. Sangiorgi\(2012\)Introduction to bisimulation and coinduction\.Cambridge University Press\.External Links:ISBN 9780511777110,[Document](https://dx.doi.org/https%3A//doi.org/10.1017/CBO9780511777110)Cited by:[§1](https://arxiv.org/html/2608.11531#S1.p2.1)\.
- \[21\]R\. J\. van Glabbeek and U\. Goltz\(2001\)Refinement of actions and equivalence notions for concurrent systems\.Acta Informatica37\(4/5\),pp\. 229–327\.External Links:[Link](https://doi.org/10.1007/s002360000041),[Document](https://dx.doi.org/10.1007/S002360000041)Cited by:[§6](https://arxiv.org/html/2608.11531#S6.p2.1)\.