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