Relational Connectors and Heterogeneous Bisimulations
Pedro Nora, Jurriaan Rot, Lutz Schröder, Paul Wild
TL;DR
The paper develops a principled framework for heterogeneous (bi)simulation by introducing relational connectors between set functors in universal coalgebra, thereby relating systems of different types (e.g., nondeterministic, probabilistic). It extends lax extensions with a rich set of constructions (composition, converse, identity) and a Kantorovich construction that derives connectors from modality relations, enabling a dual-purpose modal logic that simultaneously interprets across both system types. A central HM-type expressiveness theorem shows that, for finitely branching coalgebras, heterogeneous similarities coincide with theory inclusion in the corresponding modal logic, unifying behavioural characterizations across diverse transition systems. The framework applies to a range of scenarios, including LTS with different alphabets, trace sharing, probabilistic abstractions, and ioco conformance, and opens questions about completeness and composition properties of Kantorovich connectors.
Abstract
While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different type is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances.