On Kleisli liftings and decorated trace semantics

TL;DR

This paper develops a framework for decorated trace semantics in conditional transition systems using Kleisli categories, extending coalgebraic modeling to include language and ready equivalences.

Contribution

It introduces a method to define Kleisli liftings for relative monads and provides a recipe for constructing Kleisli liftings for general endofunctors.

Findings

Reduced Kleisli lifting problem to classical notions

Provided a recipe for Kleisli lifting in indexed categories

Extended coalgebraic semantics to conditional transition systems

Abstract

It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when nondeterministic automata are modelled as coalgebras living in the Kleisli category of the powerset monad. In this paper, our aim is to establish decorated trace semantics based on language and ready equivalences for conditional transition systems (CTSs) with/without upgrades. To this end, we model CTSs as coalgebras living in the Kleisli category of a relative monad. Our results are twofold. First, we reduce the problem of defining a Kleisli lifting for the machine endofunctor in the context of a relative monad to the classical notion of Kleisli lifting. Second, we provide a recipe based on indexed categories to construct a Kleisli lifting for general endofunctors.