Proof systems for message-passing process algebras

Abstract. We give sound and complete proof systems for a variety of bisimu-lation based equivalences over a message-passing process algebra. The process algebra is a generalisation of CCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operator a.p is replaced by the two operators c?x.p and c!e.p and in addition messages can be tested by a conditional construct. The various proof sys-tems are parameterised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.