On the Decidability of Non-Interleaving Process Equivalences
Astrid Kiehn, Matthew Hennessy · 1994
We develop decision procedures based on proof tableaux for a number of noninterleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPP ø , 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. 1 Introduction This paper is concerned with the development of automatic verification techniques for process description languages. Typically if P and Q are process descriptions we wish to develop decision procedures for checking if P and Q are semantically equivalent. If P and Q are expressions from process algebras or given in terms of labelled transition systems then there are already a number of software systems which can automatically check for such semantic identities, [CPS89, SV89]. The main semantic equivalences handled by these tools are variations on bisimulatio...