### Pawel Sobocinski

*BRICS,
Department of Computer Science, Aarhus University.*

**Time: ** Tuesday, September 17, 13.00.

**Place:** Room E3-209, Fredrik Bajersvej 7.

### Deriving Bisimulation Congruences: A 2-categorical Approach

We introduce G-relative-pushouts (GRPO) which are a 2-categorical
generalisation of Leifer and Milner's relative-pushouts (RPO). The
2-cells can be seen as generalised proofs of structural congruence. By
keeping track of "how the squares commute" we are able to place
reaction in terms and therefore derive more informative labelled
transition systems (lts). Moreover, Leifer and Milner's result
guaranteeing that the largest bisimulation on the lts is a congruence
extends to the 2-categorical case. To illustrate the derivation
process we shall consider a simple process calculus as well as some
contexts-as-arrows categories considered previously in literature.