Paper appeared in Mathematical Structures in Computer Science; previously available as Tech. Rep. 02/2006, Dip Informatica, Univ. di Roma "La Sapienza" with title "Characterising Bisimulations Functorially".
We study the functorial characterisation of bisimulation-based equivalences over a tree-based categorical model that can be used to represent different (interleaving and partial ordering) semantics of concurrent systems. In a setting where all actions are observable, we prove that strong bisimilarity can be characterised in terms of enriched functors by relying on the notion of fullness. This notion requires that the morphism object going from F(A) to F(B) be "covered by" the morphism object going from A to B. Moreover, it entails a very rigid form of lifting factorisation property that Lawvere (and, later, Bunge and Fiore) used to establish determinacy of the constructions they considered. Within the setting where silent actions are ignored, we characterise both weak and branching bisimilarity. The former is characterised again in terms of enriched functors fullness, but in this case no lifting factorisation property holds. The latter is obtained by requiring fullness and a weaker lifting factorisation property, called Conduché property. Thus, we can conclude that branching bisimilarity does preserves some determinacy of processes, while the same cannot be said for weak bisimilarity.
@Article{DGL:MSCS10,
author = {R. {De Nicola} and D. Gorla and A. Labella},
title = {Tree-Functors, Determinacy and Bisimulations},
journal = {Mathematical Structures in Compuetr Science},
volume = {20},
number = {3},
pages = {319--358},
year = {2010},
publisher = {Cambridge University Press},
}