Conservative Extension in Structural Operational Semantics

Luca Aceto
Willem Jan Fokkink
Chris Verhoef

September 1999


Over and over again, process calculi such as CCS, CSP, and ACP have been extended with new features, and the Transition System Specifications (TSSs) that provide the operational semantics for these process algebras were extended with transition rules to describe these features. A question that arises naturally is whether or not the original and the extended TSS induce the same transitions in the original domain. Usually it is desirable that an extension is operationally conservative, meaning that the provable transitions for an original term are the same both in the original and in the extended TSS. This paper contains an exposition of existing conservative extension formats for Structural Operational Semantics, and their applications with respect to term rewriting systems and completeness of axiomatizations

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.