We introduce a mathematical structural operational semantics that yields a congruence result for bisimilarity and is suitable for investigating rule formats for name-passing systems. Indeed, we instantiate this general abstract model theory in a framework of nominal sets and extract from it a GSOS-like rule format for name-passing process calculi for which the associated notion of behavioural equivalence - given by a form of open bisimilarity - is a congruence.
Citation:
Marcelo Fiore, Sam Staton, "A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics," lics, pp.49-58, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006