On the Decidability of Non-Interleaving Process Equivalences

Article type: Research Article

Authors: Kiehn, Astrid | Hennessy, Matthew

Affiliations: Institut für Informatik, Technische Universität, München, Germany. kiehn@informatik.tu-muenchen.de | Cognitive and Computing Sciences, University of Sussex, Brighton, England. matthewh@cogs.sussex.ac.uk

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 BPPr, 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.

Keywords: process algebra, observation equivalence, non-interleaving semantics, decidability

DOI: 10.3233/FI-1997-30102

Journal: Fundamenta Informaticae, vol. 30, no. 1, pp. 11-30, 1997