Open Maps, Behavioural Equivalences, and Congruences

Allan Cheng
Mogens Nielsen

January 1996


Spans of open maps have been proposed by Joyal, Nielsen, and Winskel as a way of adjoining an abstract equivalence, tex2html_wrap_inline33 -bisimilarity, to a category of models of computation tex2html_wrap_inline35 , where tex2html_wrap_inline33 is an arbitrary subcategory of observations. Part of the motivation was to recast and generalise Milner's well-known strong bisimulation in this categorical setting. An issue left open was the congruence properties of tex2html_wrap_inline33 -bisimilarity. We address the following fundamental question: given a category of models of computation tex2html_wrap_inline35 and a category of observations tex2html_wrap_inline33 , are there any conditions under which algebraic constructs viewed as functors preserve tex2html_wrap_inline33 -bisimilarity? We define the notion of functors being tex2html_wrap_inline33 -factorisable, show how this ensures that tex2html_wrap_inline33 -bisimilarity is a congruence with respect to such functors. Guided by the definition of tex2html_wrap_inline33 -factorisability we show how it is possible to parametrise proofs of functors being tex2html_wrap_inline33 -factorisable with respect to the category of observations tex2html_wrap_inline33 , i.e., with respect to a behavioural equivalence.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.