A coalgebraic perspective on monotone modal logic

There is an obvious connection between coalgebra and modal logic: Coalgebras for an endofunctor T can be seen as abstract dynamic systems or transition systems, and modal logic seems to be the natural specification language to talk about these systems. Monotone modal logics generalise normal modal logics by weakening the requirement of additivity for the modal operator Box to monotonicity: From p ---> q infer Box p ---> Box q. This entails that Kripke frames no longer constitute an adequate semantics, instead (non-normal) monotone modal logics are interpreted over monotone neighbourhood frames of the form (W, N: W --> PPW) where N(w) is upwards closed. We will make the connection between monotone modal logic and coalgebras precise by defining functors UpP: Set ---> Set and UpV: Stone ---> Stone such that UpP- and UpV-coalgebras correspond to monotone neighbourhood frames and descriptive general monotone frames, respectively. Furthermore, we will investigate the relationships between the coalgebraic notions of bisimulation and behavioural equivalence on the one hand, and bisimulation of monotone frames on the other. In particular, we will show that the UpP-functor does not preserve weak pullbacks, and we prove interpolation for a number of monotone modal logics using results on UpP-bisimulation.  

hosted by