On bisimulation in absence of restriction

We revisit the standard bisimulation equalities in process models free of the restriction operator. As is well-known, in general the weak bisimilarity is coarser than the strong bisimilarity because it abstracts from internal actions. In absence of restriction, those internal actions become somewhat visible, so one might wonder if the weak bisimilarity is still ‘weak’. We show that in CCScore (i.e., Milner’s standard CCS without τ-prefix, summation and relabelling) the weak bisimilarity indeed remains weak, i.e., still strictly coarser than the strong bisimilarity, even without the restriction operator. Essentially, this is due to the existence of the replication operation, which can keep a process retaining its state (i.e., the capacity of interaction). By virtue of these observations, we examine a variant of the weak bisimilarity, called quasi-strong bisimilarity. This quasi-strong bisimilarity requires the matching of internal actions to be conducted in the strong manner, as for the strong bisimilarity, and the matching of visible actions to have no trailing internal actions. We exhibit that in CCScore without the restriction operator, the weak bisimilarity exactly collapses onto this quasi-strong bisimilarity, which is moreover shown to coincide with the branching bisimilarity. These results reveal that in absence of the restriction operation, some ingredient of the weak bisimilarity indeed turns into strong, particularly the matching of internal actions.