Operational conservativity with binding terms

Abstract

In a previous paper the approach to structural operational semantics using transition system specifications (TSSs) was extended to deal with variable binding operators. It was shown that in this setting a generalization of the transition rule format known as the panth format guarantees that bisimilation is a congruence for meaningful TSSs. In this paper, it is shown that certain syntactic criteria, originating from Fokkink and Verhoef, to determine whether a TSS is an operational conservative extension of another TSS are applicable in this setting as well. This result can for example be used to simplify proofs of axiomatic conservativity and completeness in cases where an existing process calculus is extended with new features.