A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics

Abstract

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