We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPP r , Basic Parallel Processes with communication, obtained by omitting the restriction operator from CCS. Decision procedures are given for both strong and weak versions of location equivalence and ST-bisimulation.

Abstract We study a notion of observation for concurrent processes which allows the observer to see the distributed nature of processes, giving explicit names for the location of actions. A general notion of bisimulation related to this observation of distributed systems is introduced. Our main result is that these bisimulation relations, particularized to a process algebra extending CCS, are completely axiomatizable. We discuss in detail two instances of location bisimulations, namely the location equivalence and the location preorder.