Roughly one year ago I gave a colloquium talk about up-to techniques for branching bisimilarity. In particular we discussed the soundness of branching bisimilarity up to context for CCS with guarded sums. In combination with other up-to techniques this result allows for more feasible proofs when attempting to prove two CCS terms bisimilar. We added two levels of abstraction to this result, yielding the same result for a larger class of process algebras and allowing for easier instantiation to other notions of bisimilarity that abstract from silent transitions. The first level involves Bloom’s cool congruence formats. The second level involves a bialgebraic approach, which will be the main focus of this talk.
Based on joint work with Jurriaan Rot and Bas Luttik.