Variable binding operators in transition system specifications

Abstract

In this paper the approach to structural operational semantics (SOS) using transition system specifications (TSSs) is extended to deal with variable binding operators and many-sortedness. Verhoef's transition rule format, known as the panth format, generalizes naturally to the new TSSs. It is shown that, in case of a meaningful TSS defining ordinary transition relations, bisimulation is a congruence if transition rules in this format are used. Formats guaranteeing that bisimulation is a congruence are important for the application of TSSs to provide process calculi, and programming and specification languages, with an operational semantics. The new congruence result is relevant because in many of these applications, variable binding operators and many-sortedness are involved. It is also sketched how the presented approach can be further extended to deal with given sorts and parametrized transition relations. Given sorts are useful if the semantics of the terms of certain sorts has been given beforehand. This happens frequently in practice, as does the often related need of parametrized transition relations.