Equivalence semantics for concurrency: comparison and application
V.C. Galpin
Technical Report ECS-LFCS-98-397, PhD Thesis, Department of Computer
Science, University of Edinburgh, 1998.
Abstract
Since the development of CCS and other process algebras, many
extensions to these process algebras have been proposed to model
different aspects of concurrent computation. It is important both
theoretically and practically to understand the relationships between
these process algebras and between the semantic equivalences that
are defined for them.
In this thesis, I investigate the comparison of semantic equivalences
based on bisimulation which are defined for process algebras whose
behaviours are described by structured operational semantics, and
expressed as labelled transition systems. I first consider a hierarchy
of bisimulations for extensions to CCS, using both existing and new
results to describe the relationships between their equivalences with
respect to pure CCS terms. I then consider a more general approach to
comparison by investigating labelled transition systems with structured
labels. I define bisimulation homomorphisms between labelled
transition systems with different labels, and show how these can be
used to compare equivalences.
Next, I work in the meta-theory of process algebras and consider a new
format that is an extension of the \emph{tyft/tyxt} format for
transition system specifications. This format
treats labels syntactically instead of schematically, and hence I use
a definition of bisimulation which requires equivalence between
labels instead of exact matching. I show that standard results such as
congruence and conservative extension hold for the new format.
I then investigate how comparison of equivalences can be approached
through the notion of extension to transition system specifications.
This leads to the main results of this study which show how in a very
general fashion the bisimulations defined for two different process
algebras can be compared over a subset of terms of the process
algebras.
I also consider what implications the conditions which are required to
obtain these results have for modelling process algebras, and show that
these conditions do not impose significant limitations. Finally, I
show how these results can be applied to existing process algebras. I
model a number of process algebras with the extended format
and derive new results from the meta-theory developed.
Full text - various formats
Back to Publications page