Open Maps (at) Work

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 has 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 [JNW93] 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 [JNW93] is not
a one-off application of open maps.