Bisimulation and divergence (Q750163)

The purpose of this paper is to investigate how bisimulation equivalence may be refined to give preorders which provide divergence-respecting approximation orderings between processes whose associated theories are as close as possible to that of bisimulation equivalence. The work is based on ideas first introduced in \textit{M. Hennessy} and \textit{G. Plotkin} [A term model for CCS, Lecture Notes in Comput. Sci. 88, Springer-Verlag (1980; Zbl 0479.68011)] and \textit{R. Milner} [A modal characterization of observable machine-behaviour, Lecture Notes in Comput. Sci. 112 (1981; Zbl 0474.68074)]. The paper is divided into five sections, the first being an introduction. Section 2 contains characterizations of the largest precongruence relations included in the latter three preorders, and Sections 3 and 4 present axiomatizations of these relations of the classes of finite closed terms and sequential terms of CCS, respectively. The final section contains an example illustrating how the theory of one of the preorders may be used as the basis of a verification technique.