|
Open Maps (at) Work
Allan Cheng April 1995 |
Abstract:The notion of bisimilarity, as defined by Park and Milner, has turned out to be one of the most fundamental notions of operational equivalences in the field of process algebras. Not only does it induce a congruence (largest bisimulation) in CCS which have nice equational properties, it has also proven itself applicable for numerous models of parallel computation and settings such as Petri Nets and semantics of functional languages. In an attempt to understand the relationships and differences between the extensive amount of research within the field, Joyal, Nielsen, and Winskel recently presented an abstract category-theoretic definition of bisimulation. They identify spans of morphisms satisfying certain ``path lifting'' properties, so-called open maps, as a possible abstract definition of bisimilarity. In their LICS '93 paper they show, that they can capture Park and Milner's bisimulation. The aim of this paper is to show that the abstract definition of bisimilarity is applicable ``in practice'' by showing how a representative selection of well-known bisimulations and equivalences, such as e.g. Hennessy's testing equivalence, Milner and Sangiorgi's barbed bisimulation, and Larsen and Skou's probabilistic bisimulation, are captured in the setting of open maps and hence, that the proposed notion of open maps seems successful. Hence, we confirm that the treatment of strong bisimulation in the LICS '93 paper is not a one-off application of open maps.
Available as PostScript, PDF, DVI. |