On Bisimulation in Absence of Restriction
share
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 both CCScore (i.e., Milner's standard CCS without τ-prefix, summation and relabelling) and its higher-order variant (named HOCCScore), the weak bisimilarity indeed remains weak, i.e., still strictly coarser than the strong bisimilarity, even without the restriction operator. These results can be extended to other first-order or higher-order process models. Essentially, this is due to the direct or indirect existence of the replication operation, which can keep a process retaining its state (i.e., 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.
READ FULL TEXT