The field of process algebra provides a way to model (concurrent) processes algebraically. The syntax of a process calculus is described by an algebraic signature and the semantics is described by a set of operational rules. Strong bisimilarity and branching bisimilarity are two well known behavioral equivalences on processes. Informally two processes are strongly bisimilar if they cannot be distinguished by an external observer. Branching bisimilarity is a weaker equivalence that abstracts from internal transitions.

In many process calculi, strong bisimilarity is a congruence. Informally this enables one to reason algebraically about strong bisimilarity of two processes. The GSOS format is a family of process calculi for which strong bisimilarity is guaranteed to be a congruence. Unfortunately branching bisimilarity is not a congruence for a GSOS language in general. To mitigate this issue, Bard Bloom introduced language formats by putting extra restrictions on the GSOS rules. In particular the BB-cool format guarantees that branching bisimilarity is a congruence.

In this talk I will demonstrate why congruence is a complicated issue in weak behavioral equivalences. We will discuss the GSOS format, the BB-cool format, and a sketch of a proof by Rob van Glabbeek that shows why the restrictions on GSOS are enough to make branching bisimilarity a congruence again. Currently I am studying this topic at a more abstract level with Bas Luttik and Jurriaan Rot, which I will briefly comment on.