Logic-Induced Bisimulations

TL;DR

This paper introduces a new coalgebraic bisimulation concept called $ ho$-bisimulation, which is defined via a logic connection, and explores its properties, relation to existing notions, and a key Hennessy-Milner theorem.

Contribution

It defines $ ho$-bisimulation based solely on coalgebra structure and semantics, providing a structural and relation-lifting characterization, independent of duality assumptions.

Findings

$ ho$-bisimulation is structural and relation-liftable.

Collection of bisimulations forms a complete lattice.

Hennessy-Milner theorem links logical equivalence to $ ho$-bisimilarity.

Abstract

We define a new logic-induced notion of bisimulation (called $\rho$-bisimulation) for coalgebraic modal logics given by a logical connection, and investigate its properties. We show that it is structural in the sense that it is defined only in terms of the coalgebra structure and the one-step modal semantics and, moreover, can be characterised by a form of relation lifting. Furthermore we compare $\rho$-bisimulations to several well-known equivalence notions, and we prove that the collection of bisimulations between two models often forms a complete lattice. The main technical result is a Hennessy-Milner type theorem which states that, under certain conditions, logical equivalence implies $\rho$-bisimilarity. In particular, the latter does \emph{not} rely on a duality between functors $\mathsf{T}$ (the type of the coalgebras) and $\mathsf{L}$ (which gives the logic), nor on properties of the logical connection $\rho$.