Deriving Bisimulation Congruences: 2-Categories vs. Precategories

Vladimiro Sassone, Pawel Sobocinski

Abstract


G-relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. This paper develops the theory of GRPOs further, arguing that they provide a simple and powerful basis towards a comprehensive solution. As an example, we construct GRPOs in a category of `bunches and wirings.' We then examine the approach based on Milner's precategories and Leifer's functorial reactive systems, and show that it can be recast in a much simpler way into the 2-categorical theory of GRPOs.

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v10i1.21772
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library