Algebraic results for structured operational semantics
V.C. Galpin
South African Computer Journal, 26:13-21, November 2000.
(A research paper presented at SAICSIT 2000, 1-3 November 2000,
Cape Town, South Africa).
Abstract
This paper presents algebraic results that are important for the extended
tyft\tyxt format [Galpin 1998, Galpin 1999] which can be used
to describe many different process algebras. This format is based on
a many-sorted signature which permits both processes and labels to
be treated syntactically. Existing results for this format permit the
comparison of process algebra semantic equivalences by forming the sum
of two transition system specifications and imposing certain conditions.
The results presented in this paper involve the summing of congruences
that model the actual process algebra labels, and determine under
what conditions these congruences have important properties such as
compatibility and conservativity. The aim of this paper is to show that
the notion of sort-similarity on the sum of signatures is sufficient for
the sum of the congruences induced by each label algebra to be the same
as the congruence induced by the summed label algebras. Additionally,
sort-similarity is sufficient for compatibility and conservativity
when summing. Finally, conditions on the label algebra are given that
ensure compatibility.
Keywords
extended tyft\tyxt format, many-sorted, comparison of semantic
equivalences, sort-similar, process algebra, bisimulation, operational
semantics
Computing Review Categories
D.3.1, F.1.2, F.3.2, F.4.3
Full text - gzipped PostScript
Full text - PDF
Slides - gzipped PostScript
Slides - PDF
Back to Publications page