Paper detail

Simulations and Bisimulations For Coalgebraic Modal Logics

We define a notion of Lambda-simulation for coalgebraic modal logics, parametric on the choice Lambda of predicate liftings for a functor T. We show this notion is adequate in several ways: i) it preserves truth of positive formulas, ii) for Lambda a separating set of monotone predicate liftings, the associated notion of Lambda-bisimulation corresponds to T-behavioural equivalence (moreover Lambda-n-bisimulations correspond to T-n-behavioural equivalence), and iii) in fact, for Lambda-separating and T preserving weak pullbacks, difunctional Lambda-bisimulations are T-bisimulations. In essence, we arrive at a modular notion of equivalence that, when used with a separating set of monotone predicate liftings, coincides with T-behavioural equivalence regardless of whether T preserves weak pullbacks (unlike the notion of T-bisimilarity).