Weak Bisimulation Properties Of A Higher-Order Process Algebra

Process algebra, as one of the important tools for describing and analyzing concurrent and distributed systems, became a central branch of research in concurrency systems. Bisimulations are considered as one of the core notions in process algebra, used to describe behavioral equivalences, among them, the weak bisimulation known as observational equivalence is one of the most important ones, but sometimes it is not easy to prove its properties.Higher-order process algebra has been paid more and more attentions, because of its advantage in describing some systems, but it is also not easy to prove its properties. As we known, higher-order pi calculus does not have a natural and simple equivalence based on labeled transition system, some are strict, and the others are hard to be proved. A contextual point of view of labelled semantics was introduced and the bisimulation based on it is better.This paper pays attention to contextually labeled semantics for restricted higher-order Pi calculus, and shows some properties of weak bisimulation including the algebraic properties and congruent property.Nowadays, reduction semantic is popular. It is indeed the simplicity of their semantics which make them attractive, and in turn facilitates a satisfactory mathematical analysis. We introduce a reduction system and show a correspondence between reduction semantics and behavioral semantics given above, that is to say two processes are weak bisimilar if and only if they are reduction barbed congruent.