Deriving Bisimulation Congruences: 2-Categories vs. Precategories
Vladimiro Sassone
January 2003 |
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
Available as PostScript, PDF, DVI. |