Towards a Theory of Strong Bisimulation for the Service Rendezvous

In the present paper we start from an operational frame-work of concurrent processes in which the discipline of process inter-action is the service rendezvous. Our objective consists in examin-ing two notions of rendezvous based strong bisimulation equivalence. The first one is quite immediate and we can prove that it is a con-gruence. The second one is slightly less immediate but for it we can give a neat alternative characterization in terms of a minor variant of Aczel’s ε—bisimulation. Our motivation for using ε—bisimulation stems from the presence of conceptual non—well—foundedness in our framework. What is cru-cial, we bring this form of bisimulation to bear not in a set theoretical but in a logical context. Despite conceptual non—well—foundedness we, thus, do not have to leave standard set theory. The conceptual non—well—foundedness is induced by a (very lim-ited) higher order capability. To overcome certain technical difficul-ties arising in connection with it we transfer methods developed by Thomsen in the context of his Plain CHOCS higher order process cal-culus. In neither direction, however, a meaningful embedding seems to be possible.