Safe implementation equivalence for asynchronous nondeterministic processes

Abstract

intuitively, processes can be seen as objects which cannot do anything, but communicate (either internally or externally). Hence, they can be entirely specified, using only communication relations. Similarly, process equivalence relations, usually rely on communication relations exclusively. That is, the unique way for defining their equivalence, turns out to be the only means processes have in order to influence their environment. Therefore, it seems quite natural to insist that process equivalence relations be congruence relations. Moreover, such relations must characterize machine behaviours in such a way that they correspond to the intuitive meaning they usually have. Unfortunately this is not so general. In this paper we introduce an equivalence relation for processes. This equivalence is based exclusively on communication relations and on the notion of process interface. It is called safe implementation equivalence. It relates two processes if they both accept the same language and are equally deterministic. Actually this relation is generated by various preorders relying on relations which allow to evaluate formally the nondeterminism of processes. We apply it to various process languages. And, in each case, we show it to be a congruence, which we algebraically axiomatize.