On the Decidability of Non-Interleaving Process Equivalences

Abstract

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.