Abstract Congruence Criteria for Weak Bisimilarity

TL;DR

This paper presents three compositionality criteria for operational semantics that ensure weak bisimulation is a congruence, using a coalgebraic framework and connecting to existing rule formats.

Contribution

It introduces a novel set of three criteria that, when combined, guarantee weak bisimulation congruence within a coalgebraic operational semantics framework.

Findings

Criteria successfully identify when weak bisimulation is a congruence

Examples demonstrate success and failure of criteria

Formal links to existing rule formats and lax models

Abstract

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.