Research On λ-bisimulation

Process algebra, as one of the important tools for describing and analyzing concurrent and distributed systems, became an central branch of research in concurrency theory. Bisimulation equivalence is considered as one of the fundamental notions of behavioural equivalence, and one of the important properties of bisimulation is its modal logic characterization. Following the development of process algebra, many different bisimulations are introduced. For describing the similarity of two processes,λ-bisimulation is introduced, its properties are associated with a metricρand the modal logic characterization ofλ-bisimulation whenρis an ultra-metric is given. However, becauseλ-bisimulation is not always an equivalence relation, such characterization in the usual style of HML does not always exist forλ-bisimulation associated with an arbitrary metric. Since composition does not satisfy substitutivity with respect toλ-bisimulation, CCSθis established and some properties ofλ-bisimulation in CCS_θare introduced.This paper pays attention to CCS_θand an open problem appeared in literature concerning the modal logical characterization ofλ-bisimulation in nomal case. The contributions of this paper include the following:(1) We establish a new form of the modal logical characterization satisfyingλ-bisimulation in nomal case.(2) We introduce a new modal operator. Based on it a new and more nature result about the modal logical characterization ofλ-bisimulation is given.(3) We study the properties of the system distributed by CCS_θ, introduce a permissible error function, establish CCS~θand give some properties of CCS~θ.