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).


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 - PDF 

Slides - PDF

Back to Publications page