Decidability of Behavioral Equivalences in Process Calculi with Name Scoping

摘要

Local channels and their name scoping rules play a significant role in the study of the expressiveness of process calculi. The paper contributes to the understanding of the expressiveness in the context of CCS by studying the decidability issues of the bisimilarity/similarity checking problems. The strong bisimilarity for a pair of processes in the calculi with only static local channels is shown ∏_1~0-complete. The strong bisimilarity between those processes and the finite state processes is proved decidable. The strong similarity between the finite state processes and the processes without name-passing capability is also shown decidable.