Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic

TL;DR

This paper develops a unified coalgebraic modal logic framework to characterize behavioural equivalence in systems with side effects, using relation liftings in various categorical contexts, and applies it to weighted language equivalence and bisimilarity.

Contribution

It introduces a general categorical framework for relation liftings in coalgebras with side effects, unifying different categorical settings and deriving logical characterizations.

Findings

Unified framework for coalgebraic modal logic with side effects

Construction methods for relation liftings in various categories

Logical characterizations of language equivalence and bisimilarity

Abstract

We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from a relation lifting (a special kind of indexed morphism) and we give a general recipe to construct such liftings in the above three cases. Lastly, we apply this framework to derive logical characterisations for (weighted) language equivalence and conditional bisimilarity.