详细信息
On bisimulation in absence of restriction ( SCI-EXPANDED收录 EI收录)
文献类型:期刊文献
英文题名:On bisimulation in absence of restriction
作者:Xu, Xian[1]
机构:[1]East China Univ Sci & Technol, Shanghai 200237, Peoples R China
年份:2026
卷号:60
外文期刊名:RAIRO-THEORETICAL INFORMATICS AND APPLICATIONS
收录:;EI(收录号:20260419971732);WOS:【SCI-EXPANDED(收录号:WOS:001662074200001)】;
基金:This research was funded by National Natural Science Foundation of China (62572319, 62072299, 61872142) and Shanghai "Science and Technology Innovation Action Plan" Special project for key technologies of blockchain (24BC3200500,24BC3200300).
语种:英文
外文关键词:Strong bisimulation; weak bisimulation; restriction; first-order; higher-order; processes
摘要: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 tau-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.
参考文献:
正在载入数据...
