Conservative Extension in Structural Operational Semantics
Luca Aceto
September 1999 |
Abstract:
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. |