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 bisimulation 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.
Preprint available here.