Simulations and Bisimulations For Coalgebraic Modal Logics

TL;DR

This paper introduces a modular notion of simulation and bisimulation for coalgebraic modal logics, establishing their adequacy and equivalence with T-behavioral equivalence under various conditions.

Contribution

It defines Lambda-simulation and Lambda-bisimulation for coalgebraic modal logics, connecting them to T-behavioral equivalence and extending the understanding of behavioral equivalences.

Findings

Lambda-bisimulations correspond to T-behavioral equivalence

Lambda-simulation preserves truth of positive formulas

Difunctional Lambda-bisimulations are T-bisimulations under certain conditions

Abstract

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).