An enlarged definition and complete axiomatization of observational congruence of finite processes

Abstract

The paper is addressed to determine an adequate notion of observational equivalence of finite processes, and to give a complete axiomatization of the associated congruence. We begin with establishing the fact that recursive equivalence of processes as it has been defined in the work of Milner and his colleagues is not a fully observational equivalence, in that it is much more restrictive than it should be to agree in all cases with the judgement of an effective observer. Inspiring from CCS, an alternative syntax is proposed for processes, bringing forward n-ary guarding operators. Given p and q in that syntax, which allows invisible actions to be expressed, p and q are said equivalent iff after any common experiment, they both react by identical answers or absence of answer to any ambiguous communication offer that the observer may present. It is shown that this equivalence is also a congruence ; a finite set of equational axioms is given for the congruence, which we prove to be a complete proof system by argumenting over canonical forms of programs. In a second time, our language is enriched by adding it the necessary operators for expressing the parallel composition of processes and the renaming of their actions. The definition of the observational equivalence is extended accordingly, and it is shown that we still obtain a congruence, for which a complete proof system is finally given.